Linear maps of matrices

This file works with MatrixMaps, 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.

@[reducible, inline]

abbrev MatrixMap (A : Type u_1) (B : Type u_2) (R : Type u_3) [Semiring R] : Type (max (max u_3 u_1) u_3 u_2)

A MatrixMap is a linear map between squares matrices of size A to size B, over R.

Equations

• MatrixMap A B R = (Matrix A A R →ₗ[R] Matrix B B R)

@[reducible]

def MatrixMap.id (A : Type u_1) (R : Type u_7) [Semiring R] : MatrixMap A A R

Alias of LinearMap.id, but specifically as a MatrixMap.

Equations

• MatrixMap.id A R = LinearMap.id

def MatrixMap.choi_matrix {A : Type u_1} {B : Type u_2} {R : Type u_7} [Semiring R] [DecidableEq A] (M : MatrixMap A B R) : Matrix (A × B) (A × B) R

Choi matrix of a given linear matrix map. Note that this is defined even for things that aren't CPTP, it's just rarely talked about in those contexts. This is the inverse of MatrixMap.of_choi_matrix. Compare with MatrixMap.toMatrix, which gives the transfer matrix.

Equations

• M.choi_matrix (i₂, j₂) (i₂_1, j₂_1) = M (Matrix.stdBasisMatrix i₂ i₂_1 1) j₂ j₂_1

def MatrixMap.of_choi_matrix {A : Type u_1} {B : Type u_2} {R : Type u_7} [Fintype A] [Semiring R] (M : Matrix (A × B) (A × B) R) : MatrixMap A B R

Given the Choi matrix, generate the corresponding R-linear map between matrices as a MatrixMap. This is the inverse of MatrixMap.choi_matrix.

Equations

• MatrixMap.of_choi_matrix M = { toFun := fun (X : Matrix A A R) (b₁ b₂ : B) => ∑ a₁ : A, ∑ a₂ : A, X a₁ a₂ * M (a₁, b₁) (a₂, b₂), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MatrixMap.map_choi_inv {A : Type u_1} {B : Type u_2} {R : Type u_7} [Fintype A] [Semiring R] [DecidableEq A] (M : Matrix (A × B) (A × B) R) : (of_choi_matrix M).choi_matrix = M

Proves that MatrixMap.of_choi_matrix and MatrixMap.choi_matrix inverses.

@[simp]

theorem MatrixMap.choi_map_inv {A : Type u_1} {B : Type u_2} {R : Type u_7} [Fintype A] [Semiring R] [DecidableEq A] (M : MatrixMap A B R) : of_choi_matrix M.choi_matrix = M

Proves that MatrixMap.choi_matrix and MatrixMap.of_choi_matrix inverses.

theorem MatrixMap.choi_matrix_inj {A : Type u_1} {B : Type u_2} {R : Type u_7} [Fintype A] [Semiring R] [DecidableEq A] : Function.Injective choi_matrix

The correspondence induced by MatrixMap.of_choi_matrix is injective.

noncomputable def MatrixMap.toMatrix {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq A] {R : Type u_8} [CommSemiring R] [Fintype B] : MatrixMap A B R ≃ₗ[R] Matrix (B × B) (A × A) R

The linear equivalence between MatrixMap's and transfer matrices on a larger space. Compare with MatrixMap.choi_matrix, which gives the Choi matrix instead of the transfer matrix.

Equations

• MatrixMap.toMatrix = LinearMap.toMatrix (Matrix.stdBasis R A A) (Matrix.stdBasis R B B)

theorem MatrixMap.toMatrix_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [DecidableEq A] {R : Type u_8} [CommSemiring R] [Fintype B] [Fintype C] [DecidableEq B] (M₁ : MatrixMap A B R) (M₂ : MatrixMap B C R) : toMatrix (M₂ ∘ₗ M₁) = toMatrix M₂ * toMatrix M₁

Multiplication of transfer matrices, MatrixMap.toMatrix, is equivalent to composition of maps.

noncomputable def MatrixMap.kron {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} {R : Type u_12} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommSemiring R] (M₁ : MatrixMap A B R) (M₂ : MatrixMap C D R) : MatrixMap (A × C) (B × D) R

The Kronecker product of MatrixMaps. Defined here using TensorProduct.map M₁ M₂, with appropriate reindexing operations and LinearMap.toMatrix/Matrix.toLin. Notation ⊗ₖₘ.

Equations

• One or more equations did not get rendered due to their size.

def MatrixMap.«term_⊗ₖₘ_» : Lean.TrailingParserDescr

Equations

• MatrixMap.«term_⊗ₖₘ_» = Lean.ParserDescr.trailingNode `MatrixMap.«term_⊗ₖₘ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₖₘ ") (Lean.ParserDescr.cat `term 101))

theorem MatrixMap.kron_def {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} {R : Type u_12} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] {b₁ : B} {d₁ : D} {b₂ : B} {d₂ : D} [CommRing R] (M₁ : MatrixMap A B R) (M₂ : MatrixMap C D R) (M : Matrix (A × C) (A × C) R) : (M₁.kron M₂) M (b₁, d₁) (b₂, d₂) = ∑ a₁ : A, ∑ a₂ : A, ∑ c₁ : C, ∑ c₂ : C, M₁ (Matrix.stdBasisMatrix a₁ a₂ 1) b₁ b₂ * M₂ (Matrix.stdBasisMatrix c₁ c₂ 1) d₁ d₂ * M (a₁, c₁) (a₂, c₂)

The extensional definition of the Kronecker product MatrixMap.kron, in terms of the entries of its image.

theorem MatrixMap.add_kron {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} {R : Type u_12} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommSemiring R] (ML₁ ML₂ : MatrixMap A B R) (MR : MatrixMap C D R) : (ML₁ + ML₂).kron MR = ML₁.kron MR + ML₂.kron MR

theorem MatrixMap.kron_add {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} {R : Type u_12} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommSemiring R] (ML : MatrixMap A B R) (MR₁ MR₂ : MatrixMap C D R) : ML.kron (MR₁ + MR₂) = ML.kron MR₁ + ML.kron MR₂

theorem MatrixMap.smul_kron {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} {R : Type u_12} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommSemiring R] (r : R) (ML : MatrixMap A B R) (MR : MatrixMap C D R) : (r • ML).kron MR = r • ML.kron MR

theorem MatrixMap.kron_smul {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} {R : Type u_12} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommSemiring R] (r : R) (ML : MatrixMap A B R) (MR : MatrixMap C D R) : ML.kron (r • MR) = r • ML.kron MR

@[simp]

theorem MatrixMap.zero_kron {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} {R : Type u_12} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommSemiring R] (MR : MatrixMap C D R) : kron 0 MR = 0

@[simp]

theorem MatrixMap.kron_zero {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} {R : Type u_12} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommSemiring R] (ML : MatrixMap A B R) : ML.kron 0 = 0

theorem MatrixMap.kron_id_id {A : Type u_8} {B : Type u_9} {R : Type u_12} [Fintype A] [Fintype B] [DecidableEq A] [CommSemiring R] [DecidableEq B] : (id A R).kron (id B R) = id (A × B) R

theorem MatrixMap.kron_comp_distrib {R : Type u_12} [CommSemiring R] {Dl₁ : Type u_13} {Dl₂ : Type u_14} {Dl₃ : Type u_15} {Dr₁ : Type u_16} {Dr₂ : Type u_17} {Dr₃ : Type u_18} [Fintype Dl₁] [Fintype Dl₂] [Fintype Dl₃] [Fintype Dr₁] [Fintype Dr₂] [Fintype Dr₃] [DecidableEq Dl₁] [DecidableEq Dl₂] [DecidableEq Dr₁] [DecidableEq Dr₂] (L₁ : MatrixMap Dl₁ Dl₂ R) (L₂ : MatrixMap Dl₂ Dl₃ R) (R₁ : MatrixMap Dr₁ Dr₂ R) (R₂ : MatrixMap Dr₂ Dr₃ R) : kron (L₂ ∘ₗ L₁) (R₂ ∘ₗ R₁) = L₂.kron R₂ ∘ₗ L₁.kron R₁

For maps L₁, L₂, R₁, and R₂, the product (L₂ ∘ₗ L₁) ⊗ₖₘ (R₂ ∘ₗ R₁) = (L₂ ⊗ₖₘ R₂) ∘ₗ (L₁ ⊗ₖₘ R₁)

theorem MatrixMap.kron_map_of_kron_state {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} {R : Type u_12} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommRing R] (M₁ : MatrixMap A B R) (M₂ : MatrixMap C D R) (MA : Matrix A A R) (MC : Matrix C C R) : (M₁.kron M₂) (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) MA MC) = Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (M₁ MA) (M₂ MC)

The operational definition of the Kronecker product MatrixMap.kron, that it maps a Kronecker product of inputs to the Kronecker product of outputs. It is the unique bilinear map doing so.

def MatrixMap.Basis.piTensorProduct {ι : Type u_8} {R : Type u_9} [CommSemiring R] {s : ι → Type u_10} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {L : ι → Type u_11} [(i : ι) → Fintype (L i)] (b : (i : ι) → Basis (L i) R (s i)) : Basis ((i : ι) → L i) R (PiTensorProduct R s)

Like Basis.tensorProduct, but for PiTensorProduct

Equations

• MatrixMap.Basis.piTensorProduct b = Finsupp.basisSingleOne.map sorry

def MatrixMap.Equiv.piProdProdPi {ι : Type u} (κ : ι → Type v) : ((i : ι) → κ i × κ i) ≃ ((i : ι) → κ i) × ((i : ι) → κ i)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MatrixMap.Equiv.piProdProdPi_symm_apply {ι : Type u} (κ : ι → Type v) (f : ((i : ι) → κ i) × ((i : ι) → κ i)) (i : ι) : (piProdProdPi κ).symm f i = (f.1 i, f.2 i)

@[simp]

theorem MatrixMap.Equiv.piProdProdPi_apply {ι : Type u} (κ : ι → Type v) (f : (i : ι) → κ i × κ i) : (piProdProdPi κ) f = (fun (i : ι) => (f i).1, fun (i : ι) => (f i).2)

noncomputable def MatrixMap.piKron {R : Type u_8} [CommSemiring R] {ι : Type u} [DecidableEq ι] [fι : Fintype ι] {dI : ι → Type v} [(i : ι) → Fintype (dI i)] [(i : ι) → DecidableEq (dI i)] {dO : ι → Type w} [(i : ι) → Fintype (dO i)] (Λi : (i : ι) → MatrixMap (dI i) (dO i) R) : MatrixMap ((i : ι) → dI i) ((i : ι) → dO i) R

Finite Pi-type tensor product of MatrixMaps. Defined as PiTensorProduct.tprod of the underlying Linear maps. Notation ⨂ₜₘ[R] i, f i, eventually.

Equations

• One or more equations did not get rendered due to their size.

def MatrixMap.IsTracePreserving {A : Type u_1} {B : Type u_2} {R : Type u_7} [Fintype A] [Semiring R] [Fintype B] (M : MatrixMap A B R) : Prop

A linear matrix map is trace preserving if trace of the output equals trace of the input.

Equations

• M.IsTracePreserving = ∀ (x : Matrix A A R), (M x).trace = x.trace

theorem MatrixMap.IsTracePreserving_iff_trace_choi {A : Type u_1} {B : Type u_2} {R : Type u_7} [Fintype A] [Semiring R] [DecidableEq A] [Fintype B] (M : MatrixMap A B R) : M.IsTracePreserving ↔ M.choi_matrix.traceRight = 1

A map is trace preserving iff the partial trace of the Choi matrix is the identity.

@[simp]

theorem MatrixMap.IsTracePreserving.apply_trace {B : Type u_2} {R : Type u_7} [Semiring R] [Fintype B] {A : Type u_8} [Fintype A] {M : MatrixMap A B R} (h : M.IsTracePreserving) (ρ : Matrix A A R) : (M ρ).trace = ρ.trace

Simp lemma: the trace of the image of a IsTracePreserving map is the same as the original trace.

theorem MatrixMap.IsTracePreserving.trace_choi {A : Type u_1} {B : Type u_2} {R : Type u_7} [Fintype A] [Semiring R] [DecidableEq A] [Fintype B] {M : MatrixMap A B R} (h : M.IsTracePreserving) : M.choi_matrix.trace = ↑Finset.univ.card

The trace of a Choi matrix of a TP map is the cardinality of the input space.

theorem MatrixMap.IsTracePreserving.comp {B : Type u_2} {C : Type u_3} {R : Type u_7} [Semiring R] [Fintype B] [Fintype C] {A : Type u_8} [Fintype A] {M₁ : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M₁.IsTracePreserving) (h₂ : M₂.IsTracePreserving) : IsTracePreserving (M₂ ∘ₗ M₁)

The composotion of IsTracePreserving maps is also trace preserving.

theorem MatrixMap.IsTracePreserving.id {R : Type u_7} [Semiring R] {A : Type u_8} [Fintype A] : (MatrixMap.id A R).IsTracePreserving

The identity MatrixMap IsTracePreserving.

theorem MatrixMap.IsTracePreserving.unit_linear {B : Type u_2} [Fintype B] {A : Type u_8} {R : Type u_9} [CommSemiring R] [Fintype A] {M₁ M₂ : MatrixMap A B R} {x y : R} (h₁ : M₁.IsTracePreserving) (h₂ : M₂.IsTracePreserving) (hxy : x + y = 1) : (x • M₁ + y • M₂).IsTracePreserving

Unit linear combinations of IsTracePreserving maps are IsTracePreserving.

theorem MatrixMap.IsTracePreserving.kron {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [DecidableEq A] [Fintype B] [Fintype C] {D : Type u_8} {R : Type u_9} [CommSemiring R] [DecidableEq C] [Fintype D] {M₁ : MatrixMap A B R} {M₂ : MatrixMap C D R} (h₁ : M₁.IsTracePreserving) (h₂ : M₂.IsTracePreserving) : (M₁.kron M₂).IsTracePreserving

The kronecker product of IsTracePreserving maps is also trace preserving.