QuantumInfo.Finite.CPTPMap.MatrixMap

Let $R$ be a semiring and $A, B$ be types representing the indices of square matrices. A `MatrixMap` is the type of $R$-linear maps from the space of $A \times A$ square matrices to the space of $B \times B$ square matrices, denoted by $\text{Mat}_A(R) \to_R \text{Mat}_B(R)$.

The identity map $\text{id}$ on the space of square matrices $M_A(R)$, which maps every matrix $X \in M_A(R)$ to itself. Formally, this is the linear map $\text{id}: M_A(R) \to M_A(R)$ defined by $\text{id}(X) = X$ for all $X \in \text{Matrix}(A, A, R)$.

The Choi matrix of a linear map $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ is a matrix in $\text{Mat}_{B \times A}(R)$ whose entries are defined by: $$(\mathcal{J}(M))_{(j_1, i_1), (j_2, i_2)} = (M(E_{i_1, i_2}))_{j_1, j_2}$$ where $E_{i_1, i_2}$ is the matrix with $1$ at index $(i_1, i_2)$ and $0$ elsewhere, and $(M(E_{i_1, i_2}))_{j_1, j_2}$ denotes the entry at row $j_1$ and column $j_2$ of the matrix resulting from applying $M$ to $E_{i_1, i_2}$.

Given a matrix $M \in \text{Mat}_{(B \times A) \times (B \times A)}(R)$, the function constructs the corresponding $R$-linear map $\Phi_M: \text{Mat}_A(R) \to \text{Mat}_B(R)$. For an input matrix $X \in \text{Mat}_A(R)$, the output matrix $\Phi_M(X)$ has entries defined by: $$(\Phi_M(X))_{b_1, b_2} = \sum_{a_1 \in A} \sum_{a_2 \in A} X_{a_1, a_2} M_{(b_1, a_1), (b_2, a_2)}$$ This construction serves as the inverse of the Choi matrix mapping $\mathcal{J}$.

Let $R$ be a semiring and let $M$ be a matrix in $M_{B \times A}(R)$. Then the Choi matrix of the matrix map associated with $M$ is equal to $M$ itself; that is, $\text{choi\_matrix}(\text{of\_choi\_matrix}(M)) = M$.

Let $R$ be a semiring and let $M$ be a linear map between square matrices, specifically $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$. Let $\mathcal{C}(M)$ denote the Choi matrix of $M$ and let $\Phi(X)$ denote the linear map reconstructed from a Choi-type matrix $X$. Then, applying the reconstruction to the Choi matrix of $M$ recovers the original map: $\Phi(\mathcal{C}(M)) = M$.

Let $R$ be a semiring and let $A$ and $B$ be types indexing square matrices. The operation $\mathcal{C}$ that assigns a linear map $M: \text{Mat}_A(R) \to \text{Mat}_B(R)$ to its Choi matrix $\mathcal{C}(M) \in \text{Mat}_{B \times A}(R)$ is injective. That is, if $\mathcal{C}(M_1) = \mathcal{C}(M_2)$, then $M_1 = M_2$.

Let $R$ be a semiring and $A, B$ be types. Let $\text{MatrixMap}(A, B, R)$ denote the space of $R$-linear maps from $A \times A$ matrices to $B \times B$ matrices over $R$. There exists a linear equivalence between $\text{MatrixMap}(A, B, R)$ and the space of matrices indexed by $(B \times A) \times (B \times A)$ over $R$, defined by mapping a linear map $M$ to its Choi matrix $C(M)$ and vice versa.

Let $R$ be a semiring and $A, B$ be types indexing square matrices. A `MatrixMap` is a linear map between matrix spaces, denoted as $\mathcal{L}(M_A(R), M_B(R))$. For finite $B$, there exists a linear equivalence between these linear maps and the "transfer matrices" of size $(|B| \times |B|) \times (|A| \times |A|)$. Specifically, the map `toMatrix` sends a linear map $\Phi: M_A(R) \to M_B(R)$ to its representation in the standard bases of $M_A(R)$ and $M_B(R)$. This transfer matrix is constructed such that the composition of matrix maps corresponds to the product of their respective transfer matrices.

Let $R$ be a semiring and $A, B, C$ be finite types. For any two linear maps between square matrices $M_1: \text{Mat}_A(R) \to \text{Mat}_B(R)$ and $M_2: \text{Mat}_B(R) \to \text{Mat}_C(R)$, let $\text{toMatrix}(M)$ denote the transfer matrix associated with a map $M$. Then the transfer matrix of the composition $M_2 \circ M_1$ is equal to the matrix product of their respective transfer matrices: $$\text{toMatrix}(M_2 \circ M_1) = \text{toMatrix}(M_2) \cdot \text{toMatrix}(M_1)$$

Given two families of matrices $M, N: \kappa \to \text{Mat}_{B \times A}(R)$, the function constructs a linear map $\Phi: \text{Mat}_{A \times A}(R) \to \text{Mat}_{B \times B}(R)$ defined by the action: $$\Phi(X) = \sum_{k \in \kappa} M_k X N_k^*$$ where $N_k^*$ denotes the conjugate transpose (Hermitian adjoint) of the matrix $N_k$.

For any linear map $\Phi: \text{Mat}_A(R) \to \text{Mat}_B(R)$ between square matrices over a semiring $R$, there exists a natural number $r$ and two families of $B \times A$ matrices $\{M_i\}_{i=1}^r$ and $\{N_i\}_{i=1}^r$ such that $\Phi$ can be represented in a generalized Kraus form: \[ \Phi(X) = \sum_{i=1}^r M_i X N_i^\top \] where $M_i, N_i \in \text{Mat}_{B \times A}(R)$.

Given a ring $R$ and a function $f: B \to A$ between index sets, the `MatrixMap.submatrix` defines a linear map from the space of $A \times A$ matrices to the space of $B \times B$ matrices over $R$. For any matrix $M \in \text{Mat}_{A \times A}(R)$, the map sends $M$ to the submatrix $M_{f,f}$ whose $(i, j)$-th entry is defined as $M_{f(i), f(j)}$ for all $i, j \in B$.

Let $A$ be a type and $R$ be a semiring. Let $\text{id}_A: A \to A$ be the identity function on indices. The matrix map $\text{submatrix}(R, \text{id}_A)$ (which maps a matrix $M$ to the matrix with entries $M_{\text{id}(i), \text{id}(j)}$) is equal to the identity matrix map $\text{id}_{A, R}$ (which maps a matrix $M$ to itself).

Let $R$ be a ring and $A, B, C$ be types. For any functions $f: C \to B$ and $g: B \to A$, the composition of the matrix map submatrix operations $(\text{submatrix}_R f) \circ (\text{submatrix}_R g)$ is equal to the submatrix operation defined by the composed function $\text{submatrix}_R (g \circ f)$.

Given two linear maps between square matrices $M_1: \text{Mat}_A(R) \to \text{Mat}_B(R)$ and $M_2: \text{Mat}_C(R) \to \text{Mat}_D(R)$ over a commutative semiring $R$, their Kronecker product $M_1 \otimes_{km} M_2$ is a linear map from $\text{Mat}_{A \times C}(R)$ to $\text{Mat}_{B \times D}(R)$. It is constructed by taking the tensor product of the linear maps $M_1 \otimes M_2$, reindexing the resulting basis from $(B \times B) \times (D \times D)$ to $(B \times D) \times (B \times D)$ (and similarly for the domain), and converting the result back into a linear map between matrices.

An infix notation `⊗ₖₘ` is defined to represent the Kronecker product of matrix maps, specifically mapping it to the `MatrixMap.kron` operation.

Let $R$ be a commutative semiring. For two linear maps of matrices $M_1: \text{Mat}_{A \times A}(R) \to \text{Mat}_{B \times B}(R)$ and $M_2: \text{Mat}_{C \times C}(R) \to \text{Mat}_{D \times D}(R)$, their Kronecker product $M_1 \otimes_{km} M_2$ is a linear map acting on matrices $M \in \text{Mat}_{(A \times C) \times (A \times C)}(R)$. The entries of the resulting matrix are given by the formula: $$((M_1 \otimes_{km} M_2) M)_{(b_1, d_1), (b_2, d_2)} = \sum_{a_1, a_2, c_1, c_2} (M_1(E_{a_1, a_2}))_{b_1, b_2} \cdot (M_2(E_{c_1, c_2}))_{d_1, d_2} \cdot M_{(a_1, c_1), (a_2, c_2)}$$ where $E_{i, j}$ denotes the standard basis matrix (a matrix with $1$ at position $(i, j)$ and $0$ elsewhere).

Let $R$ be a commutative semiring. For any linear maps between square matrices $M_{L1}, M_{L2} \in \text{MatrixMap}(A, B, R)$ and $M_R \in \text{MatrixMap}(C, D, R)$, the Kronecker product of matrix maps $\otimes_{km}$ distributes over addition on the left: $$(M_{L1} + M_{L2}) \otimes_{km} M_R = (M_{L1} \otimes_{km} M_R) + (M_{L2} \otimes_{km} M_R)$$

Let $R$ be a commutative semiring. For any linear map between matrices $M_L: \text{Mat}_{A \times A}(R) \to \text{Mat}_{B \times B}(R)$ and any linear maps $M_{R1}, M_{R2}: \text{Mat}_{C \times C}(R) \to \text{Mat}_{D \times D}(R)$, the Kronecker product of $M_L$ with the sum $M_{R1} + M_{R2}$ is equal to the sum of the Kronecker products, i.e., $M_L \otimes_{km} (M_{R1} + M_{R2}) = M_L \otimes_{km} M_{R1} + M_L \otimes_{km} M_{R2}$.

Let $R$ be a commutative semiring and let $M_L$ and $M_R$ be linear maps between spaces of square matrices (matrix maps). For any scalar $r \in R$, the Kronecker product of the scaled matrix map $r \cdot M_L$ with $M_R$ is equal to the scalar $r$ multiplied by the Kronecker product of $M_L$ and $M_R$. That is, $(r \cdot M_L) \otimes_{km} M_R = r \cdot (M_L \otimes_{km} M_R)$, where $\otimes_{km}$ denotes the Kronecker product of matrix maps.

Let $R$ be a commutative semiring and let $M_L$ and $M_R$ be linear maps between square matrices (specifically, $M_L$ is a `MatrixMap` from $A$-indexed matrices to $B$-indexed matrices, and $M_R$ is a `MatrixMap` from $C$-indexed matrices to $D$-indexed matrices). For any scalar $r \in R$, the Kronecker product of $M_L$ and the scalar multiple $r \cdot M_R$ is equal to the scalar multiple of the Kronecker product of $M_L$ and $M_R$. That is, $M_L \otimes_{km} (r \cdot M_R) = r \cdot (M_L \otimes_{km} M_R)$.

Let $R$ be a commutative semiring. For any linear map between square matrices $M_R: \text{Mat}_C(R) \to \text{Mat}_D(R)$, the Kronecker product of the zero matrix map $0: \text{Mat}_A(R) \to \text{Mat}_B(R)$ with $M_R$ is equal to the zero map from $\text{Mat}_{A \times C}(R)$ to $\text{Mat}_{B \times D}(R)$. That is, $0 \otimes_{km} M_R = 0$.

Let $R$ be a commutative semiring. For any linear map between matrices $M_L: \text{Matrix}(A, A, R) \to \text{Matrix}(B, B, R)$, the Kronecker product of $M_L$ with the zero map $0: \text{Matrix}(C, C, R) \to \text{Matrix}(D, D, R)$ is equal to the zero map from $\text{Matrix}(A \times C, A \times C, R)$ to $\text{Matrix}(B \times D, B \times D, R)$. That is, $M_L \otimes_{km} 0 = 0$.

For any types $A$ and $B$ and a commutative semiring $R$, the Kronecker product of the identity matrix maps on $A$ and $B$ is equal to the identity matrix map on the product type $A \times B$. That is, $\text{id}_A \otimes_{km} \text{id}_B = \text{id}_{A \times B}$.

Let $R$ be a commutative semiring. For any linear maps between square matrices $L_1: \text{Mat}_{Dl_1}(R) \to \text{Mat}_{Dl_2}(R)$, $L_2: \text{Mat}_{Dl_2}(R) \to \text{Mat}_{Dl_3}(R)$, $R_1: \text{Mat}_{Dr_1}(R) \to \text{Mat}_{Dr_2}(R)$, and $R_2: \text{Mat}_{Dr_2}(R) \to \text{Mat}_{Dr_3}(R)$, the Kronecker product of their compositions satisfies the distributive law: $$(L_2 \circ L_1) \otimes_{km} (R_2 \circ R_1) = (L_2 \otimes_{km} R_2) \circ (L_1 \otimes_{km} R_1)$$ where $\circ$ denotes linear map composition and $\otimes_{km}$ denotes the Kronecker product of matrix maps.

Let $R$ be a commutative ring. For any two matrix maps $M_1: \text{Mat}_{A \times A}(R) \to \text{Mat}_{B \times B}(R)$ and $M_2: \text{Mat}_{C \times C}(R) \to \text{Mat}_{D \times D}(R)$, and for any two matrices $M_A \in \text{Mat}_{A \times A}(R)$ and $M_C \in \text{Mat}_{C \times C}(R)$, the Kronecker product of the maps applied to the Kronecker product of the matrices satisfies $$(M_1 \otimes_{km} M_2) (M_A \otimes_k M_C) = (M_1 M_A) \otimes_k (M_2 M_C),$$ where $\otimes_{km}$ denotes the Kronecker product of matrix maps and $\otimes_k$ denotes the Kronecker product of matrices.

Let $A$ and $B$ be finite non-empty types. Let $M$ be a linear map from $A \times A$ matrices to $B \times B$ matrices over the complex numbers $\mathbb{C}$. The Choi matrix of $M$, denoted $\text{choi\_matrix}(M)$, is given by: $$\text{choi\_matrix}(M) = |A| \cdot \left( (M \otimes \text{id}_A) (\rho_{\Psi}) \right)$$ where $|A|$ is the cardinality of $A$, $\otimes$ denotes the Kronecker product of matrix maps, $\text{id}_A$ is the identity map on $A \times A$ matrices, and $\rho_{\Psi} = |\Psi\rangle\langle\Psi|$ is the density matrix of the maximally entangled state $|\Psi\rangle$ on $A \times A$.

Let $R$ be a commutative semiring. For any functions $f: B \to A$ and $g: D \to C$, let $\text{submatrix}_f$ and $\text{submatrix}_g$ denote the linear maps that take a square matrix and return the submatrix indexed by $f$ and $g$ respectively. Then the Kronecker product of these matrix maps is equal to the submatrix map indexed by the product function $f \times g$: $$\text{submatrix}_f \otimes_{km} \text{submatrix}_g = \text{submatrix}_{f \times g}$$ where $f \times g: B \times D \to A \times C$ is defined by $(b, d) \mapsto (f(b), g(d))$.

Let $R$ be a commutative semiring and $f: B \to A$ be a function between index sets. Let $\text{submatrix}_f$ denote the linear map that sends a matrix $M \in \text{Mat}_A(R)$ to the submatrix $M_{f,f} \in \text{Mat}_B(R)$, and let $\text{id}_C$ denote the identity linear map on square matrices over the index set $C$. Then the Kronecker product of the submatrix map and the identity map is equal to the submatrix map defined by the product function $f \times \text{id}_C$: $$\text{submatrix}_f \otimes_{km} \text{id}_C = \text{submatrix}_{(f, \text{id}_C)}$$ where $f \times \text{id}_C$ is the map $(b, c) \mapsto (f(b), c)$.

Let $R$ be a commutative semiring and $f: B \to A$ be a function. Let $\text{id}_C$ denote the identity linear map on square matrices over $C$, and let $\text{submatrix}_f$ denote the linear map that takes a square matrix and returns the submatrix indexed by $f$. Then the Kronecker product of the identity map and the submatrix map is equal to the submatrix map indexed by the product function $\text{id}_C \times f$: $$\text{id}_C \otimes_{km} \text{submatrix}_f = \text{submatrix}_{(\text{id}_C, f)}$$ Where $\text{id}_C \times f$ is the map $(c, b) \mapsto (c, f(b))$.

Let $R$ be a ring and $\iota$ be an indexing type. For each $i \in \iota$, let $s_i$ be an $R$-module and $L_i$ be a finite type. If $b_i$ is a basis for $s_i$ indexed by $L_i$ for every $i$, then there exists a basis for the family tensor product $\bigotimes_{i \in \iota} s_i$ (denoted `PiTensorProduct R s`) indexed by the dependent function type $\prod_{i \in \iota} L_i$. This basis is constructed by taking the tensor products of the basis elements from each $b_i$.

Given a family of matrix maps $\Lambda_i \in \text{MatrixMap}(dI_i, dO_i, R)$ for $i \in \iota$, where each $\Lambda_i$ is a linear map between square matrices, the function returns the tensor product of these maps $\bigotimes_{i \in \iota} \Lambda_i$. This is a linear map from matrices indexed by $\prod_{i \in \iota} dI_i$ to matrices indexed by $\prod_{i \in \iota} dO_i$. It is defined by taking the $\pi$-tensor product of the underlying linear maps and reindexing the resulting basis to match the structure of a square matrix map over the product types.

Let $R$ be a semiring and $\iota$ be an indexing type. For each $i \in \iota$, let $d_1(i)$, $d_2(i)$, and $d_3(i)$ be finite types with decidable equality. Suppose we have two families of linear maps between square matrices, $\Lambda_1(i): \text{Matrix}(d_1(i), d_1(i), R) \to \text{Matrix}(d_2(i), d_2(i), R)$ and $\Lambda_2(i): \text{Matrix}(d_2(i), d_2(i), R) \to \text{Matrix}(d_3(i), d_3(i), R)$, for each $i \in \iota$. Then the product map of the compositions is equal to the composition of the product maps: $$\bigotimes_{i \in \iota} (\Lambda_2(i) \circ \Lambda_1(i)) = \left( \bigotimes_{i \in \iota} \Lambda_2(i) \right) \circ \left( \bigotimes_{i \in \iota} \Lambda_1(i) \right)$$ where $\bigotimes$ (represented by `piProd` in the formal statement) denotes the tensor product of matrix maps.