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 (B × A) (B × A) 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 (j₂, i₂) (j₂_1, i₂_1) = M (Matrix.single 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 (B × A) (B × A) 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 (b₁, a₁) (b₂, a₂), 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 (B × A) (B × A) 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.

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

The linear equivalence between linear maps of matrices,and Choi matrices.

Equations

• MatrixMap.choi_equiv = { toFun := MatrixMap.choi_matrix, map_add' := ⋯, map_smul' := ⋯, invFun := MatrixMap.of_choi_matrix, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MatrixMap.choi_equiv_symm_apply {A : Type u_1} {B : Type u_2} {R₂ : Type u_8} [Fintype A] [DecidableEq A] [CommSemiring R₂] (M : Matrix (B × A) (B × A) R₂) : choi_equiv.symm M = of_choi_matrix M

@[simp]

theorem MatrixMap.choi_equiv_apply {A : Type u_1} {B : Type u_2} {R₂ : Type u_8} [Fintype A] [DecidableEq A] [CommSemiring R₂] (M : MatrixMap A B R₂) : choi_equiv M = M.choi_matrix

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_9} [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_9} [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.

def MatrixMap.of_kraus {A : Type u_1} {B : Type u_2} {R : Type u_7} [Fintype A] [Semiring R] [SMulCommClass R R R] [Star R] {κ : Type u_9} [Fintype κ] (M N : κ → Matrix B A R) : MatrixMap A B R

Construct a matrix map out of families of matrices M N : Σ → Matrix B A R indexed by κ via X ↦ ∑ k : κ, (M k) * X * (N k)ᴴ

Equations

• MatrixMap.of_kraus M N = ∑ k : κ, { toFun := fun (X : Matrix A A R) => M k * X * (N k).conjTranspose, map_add' := ⋯, map_smul' := ⋯ }

def MatrixMap.exists_kraus {A : Type u_1} {B : Type u_2} {R : Type u_7} [Fintype A] [Semiring R] [SMulCommClass R R R] [Star R] (Φ : MatrixMap A B R) : ∃ (r : ℕ) (M : Fin r → Matrix B A R) (N : Fin r → Matrix B A R), Φ = of_kraus M N

Equations

• ⋯ = ⋯

def MatrixMap.submatrix {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] (f : B → A) : MatrixMap A B R

The MatrixMap corresponding to applying a submatrix operation on each side.

Equations

• MatrixMap.submatrix R f = { toFun := fun (x : Matrix A A R) => x.submatrix f f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MatrixMap.submatrix_apply {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] (f : B → A) (x : Matrix A A R) : (submatrix R f) x = x.submatrix f f

@[simp]

theorem MatrixMap.submatrix_id {A : Type u_9} (R : Type u_11) [Semiring R] : submatrix R _root_.id = id A R

@[simp]

theorem MatrixMap.submatrix_comp {C : Type u_3} {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] (f : C → B) (g : B → A) : submatrix R f ∘ₗ submatrix R g = submatrix R (g ∘ f)

noncomputable def MatrixMap.kron {A : Type u_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [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_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] {b₁ : B} {d₁ : D} {b₂ : B} {d₂ : D} [CommSemiring 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.single a₁ a₂ 1) b₁ b₂ * M₂ (Matrix.single 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_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [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_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [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_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [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_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [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_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [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_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [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_9} {B : Type u_10} {R : Type u_13} [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_13} [CommSemiring R] {Dl₁ : Type u_14} {Dl₂ : Type u_15} {Dl₃ : Type u_16} {Dr₁ : Type u_17} {Dr₂ : Type u_18} {Dr₃ : Type u_19} [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_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [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.

theorem MatrixMap.choi_matrix_state_rep {A : Type u_9} [Fintype A] [DecidableEq A] {B : Type u_14} [Fintype B] [Nonempty A] (M : MatrixMap A B ℂ) : M.choi_matrix = ↑(Fintype.card A) • (M.kron LinearMap.id) (MState.pure (Ket.MES A)).m

theorem MatrixMap.submatrix_kron_submatrix {A : Type u_9} {B : Type u_10} {C : Type u_11} {D : Type u_12} {R : Type u_13} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommSemiring R] (f : B → A) (g : D → C) : (submatrix R f).kron (submatrix R g) = submatrix R (Prod.map f g)

theorem MatrixMap.submatrix_kron_id {A : Type u_9} {B : Type u_10} {C : Type u_11} {R : Type u_13} [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] [DecidableEq C] [CommSemiring R] (f : B → A) : (submatrix R f).kron (id C R) = submatrix R (Prod.map f _root_.id)

theorem MatrixMap.id_kron_submatrix {A : Type u_9} {B : Type u_10} {C : Type u_11} {R : Type u_13} [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] [DecidableEq C] [CommSemiring R] (f : B → A) : (id C R).kron (submatrix R f) = submatrix R (Prod.map _root_.id f)

noncomputable def Module.Basis.piTensorProduct {ι : Type u_9} {R : Type u_10} [CommSemiring R] {s : ι → Type u_11} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {L : ι → Type u_12} [(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

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

noncomputable def MatrixMap.piKron {R : Type u_9} [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.