QuantumInfo.Finite.CPTPMap.Unbundled

Let $R$ be a semiring and $A, B$ be index types. A linear matrix map $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ is said to be trace preserving if for every matrix $x \in \text{Mat}_A(R)$, the trace of its image under $M$ is equal to the trace of the original matrix, i.e., $\text{Tr}(M(x)) = \text{Tr}(x)$.

Let $R$ be a semiring and $A, B$ be finite types. Let $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ be a linear map between square matrix spaces. $M$ is trace-preserving if and only if the partial trace over the first subsystem of its Choi matrix $\mathcal{J}(M)$ is equal to the identity matrix, i.e., $\text{Tr}_B(\mathcal{J}(M)) = I_A$.

Let $R$ be a semiring and $A, B$ be index types. Let $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ be a linear map between square matrix spaces. If $M$ is trace-preserving, then for any matrix $\rho \in \text{Mat}_A(R)$, the trace of the image $(M \rho)$ is equal to the trace of the original matrix $\rho$, i.e., $\text{Tr}(M \rho) = \text{Tr}(\rho)$.

Let $R$ be a semiring and let $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ be a linear map between square matrix spaces. If $M$ is trace-preserving, then the trace of its Choi matrix $\mathcal{J}(M)$ is equal to the cardinality of the input index set $A$, denoted by $|A|$.

Let $R$ be a semiring and $A, B, C$ be types representing the indices of square matrices. Let $M: \text{Mat}_A(R) \to_R \text{Mat}_B(R)$ and $M_2: \text{Mat}_B(R) \to_R \text{Mat}_C(R)$ be two matrix maps. If $M$ and $M_2$ are trace-preserving, then their composition $M_2 \circ M$ is also trace-preserving.

The identity matrix map $\text{id}$ on the space of square matrices $M_A(R)$ is trace-preserving.

Let $R$ be a semiring and $A, B$ be index types for square matrices. Let $M_1, M_2: \text{Mat}_A(R) \to_R \text{Mat}_B(R)$ be two matrix maps. If $M_1$ and $M_2$ are trace-preserving, then for any $x, y \in R$ such that $x + y = 1$, the linear combination $x M_1 + y M_2$ is also trace-preserving.

Let $R$ be a commutative semiring and let $A, B, C, D$ be types representing matrix indices. Suppose $M_1: \text{Mat}_A(R) \to \text{Mat}_B(R)$ and $M_2: \text{Mat}_C(R) \to \text{Mat}_D(R)$ are two trace-preserving linear maps between square matrix spaces. Then their Kronecker product $M_1 \otimes_{km} M_2: \text{Mat}_{A \times C}(R) \to \text{Mat}_{B \times D}(R)$ is also trace-preserving.

Let $S$ be a star-ring and $A, B$ be finite index types. Given two families of matrices $M_k, N_k \in \text{Mat}_{B \times A}(S)$ for $k \in \kappa$, let $\Phi: \text{Mat}_{A \times A}(S) \to \text{Mat}_{B \times B}(S)$ be the matrix map defined by $\Phi(X) = \sum_{k \in \kappa} M_k X N_k^*$, where $N_k^*$ denotes the conjugate transpose of $N_k$. If the condition $\sum_{k \in \kappa} N_k^* M_k = I$ holds, where $I$ is the identity matrix, then the map $\Phi$ is trace-preserving.

Let $R$ be a semiring and $e : B \simeq A$ be an equivalence (bijection) between index sets $A$ and $B$. Let $\Phi : \text{Mat}_A(R) \to \text{Mat}_{B}(R)$ be the linear map that sends a matrix $M$ to its submatrix defined by $e$ (such that $\Phi(M)_{i,j} = M_{e(i), e(j)}$ for $i, j \in B$). Then $\Phi$ is trace-preserving, meaning $\text{Tr}(\Phi(M)) = \text{Tr}(M)$ for all $M \in \text{Mat}_A(R)$.

Let $R$ be a semiring and $A, B$ be index sets. For a linear matrix map $\Phi: \text{Mat}_A(R) \to \text{Mat}_B(R)$, $\Phi$ is said to be **unital** if it maps the identity matrix in $\text{Mat}_A(R)$ to the identity matrix in $\text{Mat}_B(R)$, i.e., $\Phi(I_A) = I_B$.

Let $R$ be a semiring and $A, B$ be types indexing square matrices. Let $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ be a linear map between matrix spaces. If $M$ is unital, then $M(1) = 1$, where $1$ denotes the identity matrix in the respective matrix spaces.

Let $R$ be a semiring and $A$ be a type representing matrix indices. The identity matrix map $\text{id}: \text{Mat}_A(R) \to \dots \text{Mat}_A(R)$ is unital. In other words, $\text{id}(1) = 1$, where $1$ denotes the identity matrix in $M_A(R)$.

Let $R$ be a star-semiring and $A, B$ be types indexing square matrices. An $R$-linear map $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ is said to be **Hermitian preserving** if for every Hermitian matrix $x \in \text{Mat}_A(R)$ (where $x = x^\dagger$), its image $M(x)$ is also a Hermitian matrix in $\text{Mat}_B(R)$.

Let $R$ be a star-ordered ring (typically $\mathbb{R}$ or $\mathbb{C}$), and let $A$ and $B$ be finite sets indexing the rows and columns of square matrices. A linear matrix map $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ is said to be **positive** if for every positive semi-definite matrix $x \in \text{Mat}_A(R)$, its image $M(x) \in \text{Mat}_B(R)$ is also positive semi-definite.

Let $R$ be a commutative semiring and $A, B$ be finite types. A linear matrix map $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ is said to be **completely positive** if for every natural number $n$, the Kronecker product of $M$ with the identity map on $n \times n$ matrices, denoted $M \otimes_{km} \text{id}_{\text{Mat}_n(R)}$, is a positive map.

The identity matrix map $\text{id}$ on the space of square matrices $M_A(R)$ is a positive map. Specifically, for any square matrix $X \in M_A(R)$, if $X$ is a positive semidefinite matrix, then its image under the identity map $\text{id}(X) = X$ is also a positive semidefinite matrix.

Let $R$ be a semiring and $A, B, C$ be types of indices. Let $M_1: \text{Mat}_A(R) \to_R \text{Mat}_B(R)$ and $M_2: \text{Mat}_B(R) \to_R \text{Mat}_C(R)$ be two matrix maps. If $M_1$ and $M_2$ are both Hermitian-preserving, then their composition $M_2 \circ M_1$ is also Hermitian-preserving.

Let $R$ be a semiring, and let $A$ and $B$ be finite types. Let $M: \text{Mat}_A(R) \to_R \text{Mat}_B(R)$ be a linear map between spaces of square matrices. If $M$ is a positive map (i.e., it maps positive semidefinite matrices to positive semidefinite matrices), then $M$ is hermitian-preserving (i.e., it maps Hermitian matrices to Hermitian matrices).

Let $R$ be a semiring and $A, B, C$ be finite types. For any two matrix maps $M_1 : \text{Mat}_A(R) \to_R \text{Mat}_B(R)$ and $M_2 : \text{Mat}_B(R) \to_R \text{Mat}_C(R)$, if $M_1$ and $M_2$ are both positive maps, then their composition $M_2 \circ M_1$ is also a positive map.

The identity matrix map $\text{id}$ on the space of square matrices $M_A(R)$ is a positive map. Specifically, for any positive semidefinite matrix $X \in M_A(R)$, its image $\text{id}(X) = X$ is also positive semidefinite.

Let $R$ be a semiring and $A, B$ be finite types. For any two matrix maps $M_1, M_2 : \text{Mat}_A(R) \to_R \text{Mat}_B(R)$, if $M_1$ and $M_2$ are both positive maps, then their sum $M_1 + M_2$ is also a positive map.

Let $R$ be a semiring and $A, B$ be finite types. For any matrix map $M : \text{Mat}_A(R) \to_R \text{Mat}_B(R)$ and any scalar $x \in R$, if $M$ is a positive map and $x \ge 0$, then the scaled map $x \cdot M$ is also a positive map.

Let $R$ be a commutative semiring and $A, B$ be index sets for matrices. Let $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ be a linear map between matrix spaces. If $M$ is completely positive, then for any finite type $T$, the Kronecker product of $M$ with the identity map on $\text{Mat}_T(R)$ (denoted $M \otimes_{km} \text{id}_T$) is a positive map from $\text{Mat}_{A \times T}(R)$ to $\text{Mat}_{B \times T}(R)$.

Let $R$ be a star-ordered ring and $A, B$ be finite types. For any linear map between matrix spaces $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$, if $M$ is completely positive, then $M$ is positive.

[DecidableEq B] {M₁ : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M₁.IsCompletelyPositive) (h₂ : M₂.IsCompletelyPositive) : IsCompletelyPositive (M₂ ∘ₗ M₁)

Let $R$ be a commutative semiring and $A$ be a finite type. The identity matrix map $\text{id}: \text{Mat}_A(R) \to \text{Mat}_A(R)$ is completely positive.

Let $R$ be a commutative semiring and $A, B$ be finite types. If $M_1, M_2: \text{Mat}_A(R) \to \text{Mat}_B(R)$ are completely positive linear matrix maps, then their sum $M_1 + M_2$ is also completely positive.

Let $R$ be a commutative semiring, and let $A$ and $B$ be finite types. If a linear map between matrix spaces $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ is completely positive, then for any scalar $x \in R$ such that $0 \le x$, the scaled map $x \cdot M$ is also completely positive.

Let $R$ be a semiring and $A, B$ be types representing the indices of square matrices. The zero linear map $0: \text{Mat}_A(R) \to \text{Mat}_B(R)$ is completely positive.

Let $R$ be a commutative semiring and $A, B$ be finite types. Let $\iota$ be a finite index set. If $\{M_i\}_{i \in \iota}$ is a collection of linear matrix maps $M_i: \text{Mat}_A(R) \to \text{Mat}_B(R)$ such that each $M_i$ is completely positive, then their sum $\sum_{i \in \iota} M_i$ is also a completely positive map.

Let $R$ be a ring. Let $C \in \text{Mat}_d(R)$ be a positive semidefinite matrix. The matrix map $M \mapsto M \otimes_k C$, which maps a square matrix $M \in \text{Mat}_A(R)$ to the Kronecker product $M \otimes_k C \in \text{Mat}_{A \times d}(R)$, is a completely positive map.

Let $\mathbb{k}$ be a field with a star operation (typically $\mathbb{C}$) and let $K: \kappa \to \text{Mat}_{B \times A}(\mathbb{k})$ be a family of Kraus operators. Let $\Phi$ be the linear matrix map defined by $\Phi(X) = \sum_{k \in \kappa} K_k X K_k^*$. Then the Choi matrix $\mathcal{J}(\Phi)$ of this map is given by the sum of outer products: $$\mathcal{J}(\Phi) = \sum_{k \in \kappa} |v_k\rangle \langle v_k|$$ where each $v_k$ is a vector indexed by $B \times A$ such that $(v_k)_{(j, i)} = (K_k)_{j, i}$, and $\langle v_k|$ denotes the conjugate transpose of $v_k$ (represented by the `star` operation on its entries).

Given a matrix $y$ in $\text{Mat}_{B \times A}(R)$, the function `MatrixMap.conj` returns the linear map from $\text{Mat}_A(R)$ to $\text{Mat}_B(R)$ defined by $x \mapsto y x y^H$, where $y^H$ denotes the conjugate transpose of $y$.

Let $M$ be a matrix in $\text{Matrix}_{B \times A}(\mathbb{k})$. Let $\Phi_M$ be the matrix map defined by the conjugation $\Phi_M(X) = M X M^\dagger$. Then the map $\Phi_M$ is positive.

Let $\iota$ be a finite index set and let $\{f_i\}_{i \in \iota}$ be a family of linear matrix maps $f_i: \text{Mat}_A(\mathbb{C}) \to \text{Mat}_B(\mathbb{C})$. If each map $f_i$ is positive, then their sum $\sum_{i \in \iota} f_i$ is also a positive matrix map.

Let $K = \{K_k\}_{k \in \kappa}$ be a family of matrices in $\text{Mat}_{B \times A}(\mathbb{C})$ indexed by a finite set $\kappa$. Let $\Phi$ be the matrix map defined by $\Phi(X) = \sum_{k \in \kappa} K_k X K_k^\dagger$. Then the map $\Phi$ is positive.

Let $\mathbf{k}$ be a field. For any matrices $M \in \text{Mat}_{B \times A}(\mathbf{k})$ and $N \in \text{Mat}_{D \times C}(\mathbf{k})$, the Kronecker product of their associated congruence maps is equal to the congruence map associated with their Kronecker product. That is, $$\text{conj}(M) \otimes_{km} \text{conj}(N) = \text{conj}(M \otimes_k N),$$ where $\text{conj}(M)$ denotes the matrix map $X \mapsto MXM^\dagger$, $\otimes_{km}$ denotes the Kronecker product of matrix maps, and $\otimes_k$ denotes the Kronecker product of matrices.

Let $I_A$ be the identity matrix in the space of $A \times A$ complex matrices $\text{Mat}_A(\mathbb{C})$. The congruence matrix map associated with $I_A$, defined by the transformation $X \mapsto I_A X I_A^\dagger$, is equal to the identity matrix map $\text{id}$ on $\text{Mat}_A(\mathbb{C})$.

Let $\mathbf{k}$ be a field (typically $\mathbb{R}$ or $\mathbb{C}$). For any finite types $A$ and $B$, and any matrix $M \in \text{Mat}_{B \times A}(\mathbf{k})$, the matrix map defined by the congruence transformation $X \mapsto MXM^\dagger$ (denoted as `conj M`) is completely positive.

Let $A$ and $B$ be finite types and let $\text{Mat}_A(\mathbb{C}) \to_{\mathbb{C}} \text{Mat}_B(\mathbb{C})$ denote the space of linear maps between square matrices over the complex numbers. For any finite collection of such matrix maps $\{f_i\}_{i \in \iota}$, if each individual map $f_i$ is completely positive, then their sum $\sum_{i \in \iota} f_i$ is also completely positive.

Let $\mathbf{k}$ be a field and $K: \kappa \to \text{Mat}_{B \times A}(\mathbf{k})$ be a family of matrices indexed by a finite set $\kappa$. The matrix map $\Phi$ defined by the Kraus representation $\Phi(X) = \sum_{k \in \kappa} K_k X K_k^\dagger$ is equal to the sum of the congruence maps $X \mapsto K_k X K_k^\dagger$ for each $k \in \kappa$.

Let $\mathbf{k}$ be a field and $A, B$ be finite types. For any family of matrices $\{K_k\}_{k \in \kappa}$ where $K_k \in \text{Mat}_{B \times A}(\mathbf{k})$, the linear matrix map $\Phi: \text{Mat}_A(\mathbf{k}) \to \text{Mat}_B(\mathbf{k})$ defined in Kraus form by $$\Phi(X) = \sum_{k \in \kappa} K_k X K_k^*$$ is completely positive.

Let $\mathbf{k}$ be a field with a star operation, and let $A$ and $B$ be finite index sets. For any matrix $C \in \text{Mat}_{(B \times A) \times (B \times A)}(\mathbf{k})$, if $C$ is positive semidefinite ($C \succeq 0$), then there exists a family of matrices $\{K_k\}_{k \in B \times A}$ with $K_k \in \text{Mat}_{B \times A}(\mathbf{k})$ such that $C$ is the Choi matrix of the linear map $\Phi(X) = \sum_k K_k X K_k^*$.

Let $R$ be a semiring and $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ be a linear map between square matrix spaces. The Choi matrix $\mathcal{J}(M)$ of the map $M$ is equal to the result of applying the extended map $M \otimes_{km} \text{id}_A$ to the matrix $|\Omega\rangle\langle\Omega|$, where $|\Omega\rangle\langle\Omega|$ is the matrix in $\text{Mat}_{A \times A}(R)$ defined by the outer product of the vector $\sum_i e_i \otimes e_i$ with its adjoint. Specifically, $$\mathcal{J}(M) = (M \otimes_{km} \text{id}_A) \left( \sum_{i, j} E_{i, j} \otimes E_{i, j} \right)$$ where $\text{id}_A$ is the identity map on $\text{Mat}_A(R)$, $\otimes_{km}$ denotes the Kronecker product of matrix maps, and the input matrix has entries $\delta_{i_1, i_2} \overline{\delta_{j_1, j_2}}$ at index $((i_1, j_1), (i_2, j_2))$.

Let $R$ be a semiring and $A, B$ be finite types. For a linear map between square matrix spaces $M: \text{Mat}_A(R) \to \text{Mat}_{B}(R)$, $M$ is completely positive if and only if its Choi matrix $\mathcal{J}(M)$ is positive semidefinite.

Let $R$ be a star-semiring and $y$ be a $B \times A$ matrix over $R$. Let $\text{conj } y$ denote the matrix map defined by $X \mapsto y X y^\dagger$, where $y^\dagger$ is the conjugate transpose of $y$. This map is equal to the composition of the left-multiplication map by $y$ and the right-multiplication map by $y^\dagger$. That is, $$\text{conj } y = L_y \circ R_{y^\dagger}$$ where $L_y(X) = yX$ and $R_{y^\dagger}(X) = Xy^\dagger$.

Let $R$ be a star-ordered ring (such as $\mathbb{C}$) and let $B, A$ be finite types. For any matrix $M \in \text{Mat}_{B \times A}(R)$, the conjugation map defined by $X \mapsto M X M^*$ (denoted as `conj M`) is a completely positive map from $\text{Mat}_A(R)$ to $\text{Mat}_B(R)$.

Let $R$ be a semiring and $f: B \to A$ be a function between finite index sets. The linear map $\text{Mat}_A(R) \to \text{Mat}_B(R)$ defined by taking the submatrix $M \mapsto M_{f,f}$, where $(M_{f,f})_{i,j} = M_{f(i), f(j)}$ for all $i, j \in B$, is completely positive.

Let $R$ be a star-semiring and let $A$ and $B$ be finite index sets. Given a family of matrices $M_k \in \text{Mat}_{B \times A}(R)$ indexed by $k \in \kappa$, the linear map $\Phi: \text{Mat}_{A \times A}(R) \to \text{Mat}_{B \times B}(R)$ defined by $$\Phi(X) = \sum_{k \in \kappa} M_k X M_k^*$$ is completely positive, where $M_k^*$ denotes the conjugate transpose of $M_k$.

Let $\mathbf{k}$ be a star-ring and let $A, B$ be finite index sets. Given a family of matrices $K_k \in \text{Mat}_{B \times A}(\mathbf{k})$ indexed by $k \in \kappa$, let $\Phi$ be the linear map defined in symmetric Kraus form by $\Phi(X) = \sum_{k \in \kappa} K_k X K_k^*$. Then the Choi matrix $\mathcal{J}(\Phi)$ is given by the sum of outer products: $$\mathcal{J}(\Phi) = \sum_{k \in \kappa} |v_k\rangle \langle v_k|$$ where $v_k$ is the vectorization of the matrix $K_k$, such that for $(j, i) \in B \times A$, the component is $(v_k)_{(j, i)} = (K_k)_{j, i}$, and $(|v_k\rangle \langle v_k|)_{(j_1, i_1), (j_2, i_2)} = (K_k)_{j_1, i_1} \cdot \overline{(K_k)_{j_2, i_2}}$.

Let $R$ be a commutative semiring and $M: \text{Mat}_{A}(R) \to \text{Mat}_{B}(R)$ be a linear map between square matrix spaces. The Choi matrix of $M$, denoted $\mathcal{J}(M)$, is equal to the result of applying the Kronecker product of $M$ and the identity map $\text{id}_A$ to the Choi matrix of the identity map on $\text{Mat}_A(R)$. That is, $$\mathcal{J}(M) = (M \otimes_{km} \text{id}_A)(\mathcal{J}(\text{id}_A))$$ where $\otimes_{km}$ denotes the Kronecker product of matrix maps.

Let $R$ be a field of either real or complex numbers ($\mathbb{R}$ or $\mathbb{C}$), and let $A$ be a finite index set. Let $\text{id}: \text{Mat}_A(R) \to \text{Mat}_A(R)$ be the identity matrix map. Then the Choi matrix of the identity map, $\mathcal{J}(\text{id})$, is a positive semidefinite matrix.

Let $R$ be a real or complex field (an `RCLike` ring), and let $A$ and $B$ be finite types. Let $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ be a linear map between square matrix spaces. If $M$ is completely positive, then its Choi matrix $\mathcal{J}(M) \in \text{Mat}_{B \times A}(R)$ is positive semidefinite.

Let $R$ be a conjugate-transposable ring (typically $\mathbb{C}$ or $\mathbb{R}$) and $A, B$ be finite types indexing square matrices. Let $\Phi: \text{Mat}_A(R) \to \text{Mat}_B(R)$ be a linear matrix map. If $\Phi$ is completely positive, then there exists a family of matrices $M_k \in \text{Mat}_{B \times A}(R)$ indexed by $k \in B \times A$ such that $\Phi$ can be represented in Kraus form: $$\Phi(X) = \sum_{k} M_k X M_k^*$$ where $M_k^*$ denotes the conjugate transpose of $M_k$.

Let $R$ be a commutative star-semiring. Given two families of Kraus operators $M: \kappa \to \text{Mat}_{B \times A}(R)$ and $N: \iota \to \text{Mat}_{D \times C}(R)$, the Kronecker product of their associated Kraus maps is equal to the Kraus map generated by the Kronecker products of the individual operators. That is, $$\Phi_M \otimes_{km} \Phi_N = \Phi_{M \otimes N}$$ where the resulting Kraus map $\Phi_{M \otimes N}$ is defined by the family of operators $(M_k \otimes_k N_i)$ indexed by $(k, i) \in \kappa \times \iota$.

Let $R$ be a commutative semiring and $A, B, C, D$ be finite types indexing square matrices. Let $M_1: \text{Mat}_A(R) \to \text{Mat}_B(R)$ and $M_2: \text{Mat}_C(R) \to \text{Mat}_D(R)$ be linear matrix maps. If $M_1$ and $M_2$ are both completely positive, then their Kronecker product $M_1 \otimes_{km} M_2: \text{Mat}_{A \times C}(R) \to \text{Mat}_{B \times D}(R)$ is also completely positive.

Let $R$ be a *-semiring. For a given family of matrix maps $\Lambda_i: \text{Mat}_{dI_i}(R) \to \text{Mat}_{dO_i}(R)$ indexed by $i \in \iota$, if every map $\Lambda_i$ is completely positive, then their tensor product $\bigotimes_{i \in \iota} \Lambda_i$ is also a completely positive map from $\text{Mat}_{\prod dI_i}(R)$ to $\text{Mat}_{\prod dO_i}(R)$.