Physlib

QuantumInfo.Channels.MatrixMap

Linear maps of matrices

This file works with `MatrixMap`s, that is, linear maps from square matrices to square matrices. Although this is just a shorthand for `Matrix A A R →ₗ[R] Matrix B B R`, there are several concepts that specifically make sense in this context.

* `toMatrix` is the rectangular "transfer matrix", where matrix multiplication commutes with map composition. * `choi_matrix` is the square "Choi matrix", see `MatrixMap.choi_PSD_iff_CP_map` for example usage * `kron` is the Kronecker product of matrix maps * `IsTracePreserving` states the trace of the output is always equal to the trace of the input.

We provide simp lemmas for relating these facts, prove basic facts e.g. composition and identity, and some facts about `IsTracePreserving` maps.

2 declarations

theorem

J(⨂iΛi)=⨂iJ(Λi)\mathcal{J}(\bigotimes_i \Lambda_i) = \bigotimes_i \mathcal{J}(\Lambda_i) (up to reindexing)

Let RR be a commutative semiring and ι\iota be an index set. For each i∈ιi \in \iota, let Λi\Lambda_i be a linear map between square matrices (a `MatrixMap`) from MatdIi(R)\text{Mat}_{dI_i}(R) to MatdOi(R)\text{Mat}_{dO_i}(R). The Choi matrix J\mathcal{J} of the tensor product of these maps ⨂i∈ιΛi\bigotimes_{i \in \iota} \Lambda_i is equal to the Kronecker product of the individual Choi matrices ⨂i∈ιJ(Λi)\bigotimes_{i \in \iota} \mathcal{J}(\Lambda_i), subject to a reindexing of the indices from ∏i∈ι(dOi×dIi)\prod_{i \in \iota} (dO_i \times dI_i) to (∏i∈ιdOi)×(∏i∈ιdIi)(\prod_{i \in \iota} dO_i) \times (\prod_{i \in \iota} dI_i).

theorem

The tensor product of identity matrix maps is the identity map (⨂iidi=id\bigotimes_i \text{id}_i = \text{id})

Let RR be a semiring and {dIi}i∈ι\{dI_i\}_{i \in \iota} be a family of types representing matrix indices. For each i∈ιi \in \iota, let idi:MatdIi(R)→MatdIi(R)\text{id}_i: \text{Mat}_{dI_i}(R) \to \text{Mat}_{dI_i}(R) be the identity linear map on the space of square matrices. Then the tensor product of this family of identity maps, denoted by ⨂i∈ιidi\bigotimes_{i \in \iota} \text{id}_i, is equal to the identity map on the space of square matrices indexed by the product type ∏i∈ιdIi\prod_{i \in \iota} dI_i.