Properties of Matrix Maps

Building on MatrixMaps, this defines the properties: IsTracePreserving, Unital, IsHermitianPreserving, IsPositive and IsCompletelyPositive. They have basic facts such as closure under composition, addition, and scaling.

These are the unbundled versions, which just state the relevant properties of a given MatrixMap. The bundled versions are HPMap, UnitalMap, TPMap, PMap, and CPMap respectively, given in Bundled.lean.

def MatrixMap.IsTracePreserving {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {R : Type u_7} [Semiring R] (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} [Fintype A] [Fintype B] {R : Type u_7} [Semiring R] [DecidableEq A] (M : MatrixMap A B R) : M.IsTracePreserving ↔ M.choi_matrix.traceLeft = 1

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

@[simp]

theorem MatrixMap.IsTracePreserving.apply_trace {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {R : Type u_7} [Semiring R] {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} [Fintype A] [Fintype B] {R : Type u_7} [Semiring R] {M : MatrixMap A B R} [DecidableEq A] (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 {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] {R : Type u_7} [Semiring R] {M : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M.IsTracePreserving) (h₂ : M₂.IsTracePreserving) : IsTracePreserving (M₂ ∘ₗ M)

The composition of IsTracePreserving maps is also trace preserving.

@[simp]

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

The identity MatrixMap IsTracePreserving.

theorem MatrixMap.IsTracePreserving.unit_linear {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {R : Type u_8} [CommSemiring R] {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} {D : Type u_4} [Fintype A] [Fintype B] [Fintype C] [Fintype D] {R : Type u_8} [CommSemiring R] [DecidableEq C] [DecidableEq A] {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.

theorem MatrixMap.IsTracePreserving.of_kraus_isTracePreserving {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {κ : Type u_5} [Fintype κ] {S : Type u_8} [CommSemiring S] [Star S] [DecidableEq A] (M N : κ → Matrix B A S) (hTP : ∑ k : κ, (N k).conjTranspose * M k = 1) : (of_kraus M N).IsTracePreserving

The channel X ↦ ∑ k : κ, (M k) * X * (N k)ᴴ formed by Kraus operators M, N : κ → Matrix B A R is trace-preserving if ∑ k : κ, (N k)ᴴ * (M k) = 1

theorem MatrixMap.IsTracePreserving.submatrix {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {R : Type u_7} [Semiring R] (e : A ≃ B) : (MatrixMap.submatrix R ⇑e).IsTracePreserving

MatrixMap.submatrix is trace-preserving when the function is an equivalence.

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

A linear matrix map is unital if it preserves the identity.

Equations

• M.Unital = (M 1 = 1)

@[simp]

theorem MatrixMap.Unital.map_1 {R : Type u_7} {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] [Semiring R] {M : MatrixMap A B R} (h : M.Unital) : M 1 = 1

@[simp]

theorem MatrixMap.Unital.id {R : Type u_7} {A : Type u_1} [DecidableEq A] [Semiring R] : (MatrixMap.id A R).Unital

The identity MatrixMap is Unital.

def MatrixMap.IsHermitianPreserving {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] (M : MatrixMap A B R) : Prop

A linear matrix map is Hermitian preserving if it maps IsHermitian matrices to IsHermitian.

Equations

• M.IsHermitianPreserving = ∀ ⦃x : Matrix A A R⦄, x.IsHermitian → (M x).IsHermitian

def MatrixMap.IsPositive {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] (M : MatrixMap A B R) : Prop

A linear matrix map is positive if it maps PosSemidef matrices to PosSemidef.

Equations

• M.IsPositive = ∀ ⦃x : Matrix A A R⦄, x.PosSemidef → (M x).PosSemidef

def MatrixMap.IsCompletelyPositive {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] (M : MatrixMap A B R) : Prop

A linear matrix map is completely positive if, for any integer n, the tensor product with I(n) is positive.

Equations

• M.IsCompletelyPositive = ∀ (n : ℕ), (M.kron LinearMap.id).IsPositive

theorem MatrixMap.IsHermitianPreserving.id {R : Type u_10} [RCLike R] {A : Type u_11} [Fintype A] : (MatrixMap.id A R).IsPositive

The identity MatrixMap IsHermitianPreserving.

theorem MatrixMap.IsHermitianPreserving.comp {A : Type u_7} {B : Type u_8} {C : Type u_9} {R : Type u_10} [RCLike R] {M₁ : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M₁.IsHermitianPreserving) (h₂ : M₂.IsHermitianPreserving) : IsHermitianPreserving (M₂ ∘ₗ M₁)

The composition of IsHermitianPreserving maps is also Hermitian preserving.

theorem MatrixMap.IsPositive.IsHermitianPreserving {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] {M : MatrixMap A B R} (hM : M.IsPositive) : M.IsHermitianPreserving

theorem MatrixMap.IsPositive.comp {A : Type u_7} {B : Type u_8} {C : Type u_9} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [Fintype C] {M₁ : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M₁.IsPositive) (h₂ : M₂.IsPositive) : IsPositive (M₂ ∘ₗ M₁)

The composition of IsPositive maps is also positive.

@[simp]

theorem MatrixMap.IsPositive.id {R : Type u_10} [RCLike R] {A : Type u_11} [Fintype A] : (MatrixMap.id A R).IsPositive

The identity MatrixMap IsPositive.

theorem MatrixMap.IsPositive.add {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] {M₁ M₂ : MatrixMap A B R} (h₁ : M₁.IsPositive) (h₂ : M₂.IsPositive) : (M₁ + M₂).IsPositive

Sums of IsPositive maps are IsPositive.

theorem MatrixMap.IsPositive.smul {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] {M : MatrixMap A B R} (hM : M.IsPositive) {x : R} (hx : 0 ≤ x) : (x • M).IsPositive

Nonnegative scalings of IsPositive maps are IsPositive.

theorem MatrixMap.IsCompletelyPositive.of_Fintype {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {M : MatrixMap A B R} (h : M.IsCompletelyPositive) (T : Type u_11) [Fintype T] [DecidableEq T] : (M.kron LinearMap.id).IsPositive

Definition of a CP map, but with Fintype T in the definition instead of a Fin n.

theorem MatrixMap.IsCompletelyPositive.IsPositive {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {M : MatrixMap A B R} (hM : M.IsCompletelyPositive) : M.IsPositive

theorem MatrixMap.IsCompletelyPositive.comp {A : Type u_7} {B : Type u_8} {C : Type u_9} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] [DecidableEq B] {M₁ : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M₁.IsCompletelyPositive) (h₂ : M₂.IsCompletelyPositive) : IsCompletelyPositive (M₂ ∘ₗ M₁)

The composition of IsCompletelyPositive maps is also completely positive.

@[simp]

theorem MatrixMap.IsCompletelyPositive.id {A : Type u_7} {R : Type u_10} [RCLike R] [Fintype A] [DecidableEq A] : (MatrixMap.id A R).IsCompletelyPositive

The identity MatrixMap IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.add {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {M₁ M₂ : MatrixMap A B R} (h₁ : M₁.IsCompletelyPositive) (h₂ : M₂.IsCompletelyPositive) : (M₁ + M₂).IsCompletelyPositive

Sums of IsCompletelyPositive maps are IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.smul {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {M : MatrixMap A B R} (hM : M.IsCompletelyPositive) {x : R} (hx : 0 ≤ x) : (x • M).IsCompletelyPositive

Nonnegative scalings of IsCompletelyPositive maps are IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.zero (A : Type u_7) (B : Type u_8) {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] : IsCompletelyPositive 0

The zero map IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.finset_sum {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {ι : Type u_11} [Fintype ι] {m : ι → MatrixMap A B R} (hm : ∀ (i : ι), (m i).IsCompletelyPositive) : (∑ i : ι, m i).IsCompletelyPositive

A finite sum of completely positive maps is completely positive.

theorem MatrixMap.kron_kronecker_const {A : Type u_7} {R : Type u_10} [RCLike R] [Fintype A] [DecidableEq A] {d : Type u_11} [Fintype d] {C : Matrix d d R} (h : C.PosSemidef) {h₁ : ∀ (x y : Matrix A A R), (fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C) (x + y) = (fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C) x + (fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C) y} {h₂ : ∀ (m : R) (x : Matrix A A R), { toFun := fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C, map_add' := h₁ }.toFun x} : IsCompletelyPositive { toFun := fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C, map_add' := h₁, map_smul' := h₂ }

The map that takes M and returns M ⊗ₖ C, where C is positive semidefinite, is a completely positive map.

theorem MatrixMap.choi_of_kraus {κ : Type u_5} {𝕜 : Type u_6} [Fintype κ] [RCLike 𝕜] {A : Type u_7} {B : Type u_8} [Fintype A] [DecidableEq A] (K : κ → Matrix B A 𝕜) : (of_kraus K K).choi_matrix = ∑ k : κ, Matrix.vecMulVec (fun (x : B × A) => K k x.1 x.2) fun (x : B × A) => star (K k x.1 x.2)

def MatrixMap.conj {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] (y : Matrix B A R) : MatrixMap A B R

The linear map of conjugating a matrix by another, x → y * x * yᴴ.

Equations

• MatrixMap.conj y = { toFun := fun (x : Matrix A A R) => y * x * y.conjTranspose, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MatrixMap.conj_apply {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] (y : Matrix B A R) (x : Matrix A A R) : (conj y) x = y * x * y.conjTranspose

theorem MatrixMap.conj_isPositive {𝕜 : Type u_6} [RCLike 𝕜] {A : Type u_7} {B : Type u_8} [Fintype A] [Fintype B] (M : Matrix B A 𝕜) : (conj M).IsPositive

theorem MatrixMap.IsPositive_sum {A : Type u_7} {B : Type u_8} [Fintype A] [Fintype B] {ι : Type u_12} [Fintype ι] (f : ι → MatrixMap A B ℂ) (h : ∀ (i : ι), (f i).IsPositive) : (∑ i : ι, f i).IsPositive

theorem MatrixMap.of_kraus_isPositive {κ : Type u_5} [Fintype κ] {A : Type u_7} {B : Type u_8} [Fintype A] [Fintype B] (K : κ → Matrix B A ℂ) : (of_kraus K K).IsPositive

theorem MatrixMap.conj_kron {D : Type u_4} [Fintype D] {𝕜 : Type u_6} [RCLike 𝕜] {A : Type u_7} {B : Type u_8} {C : Type u_9} [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] (M : Matrix B A 𝕜) (N : Matrix D C 𝕜) [DecidableEq C] : (conj M).kron (conj N) = conj (Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) M N)

theorem MatrixMap.congruence_one_eq_id {A : Type u_7} [Fintype A] [DecidableEq A] : conj 1 = id A ℂ

theorem MatrixMap.congruence_CP {𝕜 : Type u_6} [RCLike 𝕜] {A : Type u_12} {B : Type u_13} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (M : Matrix B A 𝕜) : (conj M).IsCompletelyPositive

theorem MatrixMap.IsCompletelyPositive_sum {A : Type u_7} {B : Type u_8} [Fintype A] [Fintype B] [DecidableEq A] {ι : Type u_12} [Fintype ι] (f : ι → MatrixMap A B ℂ) (h : ∀ (i : ι), (f i).IsCompletelyPositive) : (∑ i : ι, f i).IsCompletelyPositive

theorem MatrixMap.of_kraus_eq_sum_conj {κ : Type u_5} {𝕜 : Type u_6} [Fintype κ] [RCLike 𝕜] {A : Type u_7} {B : Type u_8} [Fintype A] (K : κ → Matrix B A 𝕜) : of_kraus K K = ∑ k : κ, conj (K k)

theorem MatrixMap.of_kraus_CP {κ : Type u_5} {𝕜 : Type u_6} [Fintype κ] [RCLike 𝕜] {A : Type u_7} {B : Type u_8} [Fintype A] [Fintype B] [DecidableEq A] (K : κ → Matrix B A 𝕜) : (of_kraus K K).IsCompletelyPositive

theorem MatrixMap.exists_kraus_of_choi_PSD {𝕜 : Type u_6} [RCLike 𝕜] {A : Type u_7} {B : Type u_8} [Fintype A] [Fintype B] [DecidableEq A] (C : Matrix (B × A) (B × A) 𝕜) (hC : C.PosSemidef) : ∃ (K : B × A → Matrix B A 𝕜), C = (of_kraus K K).choi_matrix

theorem MatrixMap.choi_matrix_eq_map_proj {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] (M : MatrixMap A B R) : M.choi_matrix = (M.kron (id A R)) (Matrix.vecMulVec (fun (x : A × A) => if x.1 = x.2 then 1 else 0) fun (x : A × A) => star (if x.1 = x.2 then 1 else 0))

theorem MatrixMap.choi_PSD_iff_CP_map {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] (M : MatrixMap A B R) : M.IsCompletelyPositive ↔ M.choi_matrix.PosSemidef

Choi's theorem on completely positive maps: A map IsCompletelyPositive iff its Choi Matrix is PSD.

theorem MatrixMap.conj_eq_mulRightLinearMap_comp_mulRightLinearMap {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] (y : Matrix B A R) : conj y = mulRightLinearMap B R y.conjTranspose ∘ₗ mulLeftLinearMap A R y

theorem MatrixMap.conj_isCompletelyPositive {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] (M : Matrix B A R) : (conj M).IsCompletelyPositive

The act of conjugating (not necessarily by a unitary, just by any matrix at all) is completely positive.

theorem MatrixMap.IsCompletelyPositive.submatrix {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] (f : B → A) : (MatrixMap.submatrix R f).IsCompletelyPositive

MatrixMap.submatrix is completely positive

theorem MatrixMap.of_kraus_isCompletelyPositive {κ : Type u_5} [Fintype κ] {A : Type u_7} {B : Type u_8} {R : Type u_10} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] (M : κ → Matrix B A R) : (of_kraus M M).IsCompletelyPositive

The channel X ↦ ∑ k : κ, (M k) * X * (M k)ᴴ formed by Kraus operators M : κ → Matrix B A R is completely positive

theorem MatrixMap.choi_of_kraus_R {κ : Type u_5} {𝕜 : Type u_6} [Fintype κ] [RCLike 𝕜] {A : Type u_7} {B : Type u_8} [Fintype A] [DecidableEq A] (K : κ → Matrix B A 𝕜) : (of_kraus K K).choi_matrix = ∑ k : κ, Matrix.vecMulVec (fun (x : B × A) => K k x.1 x.2) fun (x : B × A) => star (K k x.1 x.2)

The Choi matrix of a map in symmetric Kraus form is a sum of rank-1 projectors.

theorem MatrixMap.choi_eq_kron_id_apply_choi_id {A : Type u_12} {B : Type u_13} {R : Type u_14} [Fintype A] [Fintype B] [DecidableEq A] [RCLike R] (M : MatrixMap A B R) : M.choi_matrix = (M.kron (id A R)) (id A R).choi_matrix

theorem MatrixMap.choi_id_is_PSD {A : Type u_15} {R : Type u_16} [Fintype A] [DecidableEq A] [RCLike R] : (id A R).choi_matrix.PosSemidef

theorem MatrixMap.is_CP_implies_choi_PSD {A : Type u_15} {B : Type u_16} {R : Type u_17} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [RCLike R] (M : MatrixMap A B R) (hCP : M.IsCompletelyPositive) : M.choi_matrix.PosSemidef

theorem MatrixMap.IsCompletelyPositive.exists_kraus {A : Type u_12} {B : Type u_13} {R : Type u_14} [Fintype A] [Fintype B] [DecidableEq A] [RCLike R] (Φ : MatrixMap A B R) (hCP : Φ.IsCompletelyPositive) : ∃ (M : B × A → Matrix B A R), Φ = of_kraus M M

theorem MatrixMap.kron_of_kraus {A : Type u_15} {B : Type u_16} {C : Type u_17} {D : Type u_18} {R : Type u_19} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq C] [CommSemiring R] [StarRing R] [SMulCommClass R R R] {κ : Type u_20} {ι : Type u_21} [Fintype κ] [Fintype ι] (M : κ → Matrix B A R) (N : ι → Matrix D C R) : (of_kraus M M).kron (of_kraus N N) = of_kraus (fun (k : κ × ι) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (M k.1) (N k.2)) fun (k : κ × ι) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (M k.1) (N k.2)

The Kronecker product of two Kraus maps is the Kraus map of the Kronecker products of the operators.

theorem MatrixMap.IsCompletelyPositive.kron {C : Type u_9} [Fintype C] {A : Type u_12} {B : Type u_13} {R : Type u_14} [Fintype A] [Fintype B] [DecidableEq A] [RCLike R] {D : Type u_15} [DecidableEq C] [Fintype D] {M₁ : MatrixMap A B R} {M₂ : MatrixMap C D R} (h₁ : M₁.IsCompletelyPositive) (h₂ : M₂.IsCompletelyPositive) : (M₁.kron M₂).IsCompletelyPositive

The Kronecker product of IsCompletelyPositive maps is also completely positive.

theorem MatrixMap.IsCompletelyPositive.piProd {R : Type u_14} [RCLike 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 : ι) → DecidableEq (dO i)] {Λi : (i : ι) → MatrixMap (dI i) (dO i) R} (h₁ : ∀ (i : ι), (Λi i).IsCompletelyPositive) : (MatrixMap.piProd Λi).IsCompletelyPositive

The MatrixMap.piProd product of IsCompletelyPositive maps is also completely positive.