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} {R : Type u_3} [Fintype A] [Fintype B] [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} {R : Type u_3} [Fintype A] [DecidableEq A] [Fintype B] [Semiring R] (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 {B : Type u_2} {R : Type u_3} [Fintype B] [Semiring R] {A : Type u_1} [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_3} [Fintype A] [DecidableEq A] [Fintype B] [Semiring R] {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_4} {R : Type u_3} [Fintype B] [Fintype C] [Semiring R] {A : Type u_1} [Fintype A] {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 {R : Type u_2} [Semiring R] {A : Type u_1} [Fintype A] : (MatrixMap.id A R).IsTracePreserving

The identity MatrixMap IsTracePreserving.

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

theorem MatrixMap.IsTracePreserving.of_kraus_isTracePreserving {A : Type u_3} {B : Type u_2} {S : Type u_4} [Fintype A] [DecidableEq A] [Fintype B] [CommSemiring S] [Star S] [SMulCommClass S S S] {κ : Type u_1} [Fintype κ] (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} {R : Type u_3} [Fintype A] [Fintype B] [Semiring R] (e : A ≃ B) : (MatrixMap.submatrix R ⇑e).IsTracePreserving

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

def MatrixMap.Unital {A : Type u_1} {B : Type u_2} {R : Type u_3} [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 {A : Type u_1} {B : Type u_2} {R : Type u_3} [DecidableEq A] [DecidableEq B] [Semiring R] {M : MatrixMap A B R} (h : M.Unital) : M 1 = 1

@[simp]

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

The identity MatrixMap is Unital.

def MatrixMap.IsHermitianPreserving {A : Type u_1} {B : Type u_2} {R : Type u_4} [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_1} {B : Type u_2} {R : Type u_4} [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_1} {B : Type u_2} {R : Type u_4} [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_4} [RCLike R] {A : Type u_5} [Fintype A] : (MatrixMap.id A R).IsPositive

The identity MatrixMap IsHermitianPreserving.

theorem MatrixMap.IsHermitianPreserving.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {R : Type u_4} [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_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] {M : MatrixMap A B R} (hM : M.IsPositive) : M.IsHermitianPreserving

theorem MatrixMap.IsPositive.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {R : Type u_4} [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_4} [RCLike R] {A : Type u_5} [Fintype A] : (MatrixMap.id A R).IsPositive

The identity MatrixMap IsPositive.

theorem MatrixMap.IsPositive.add {A : Type u_1} {B : Type u_2} {R : Type u_4} [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_1} {B : Type u_2} {R : Type u_4} [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_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {M : MatrixMap A B R} (h : M.IsCompletelyPositive) (T : Type u_5) [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_1} {B : Type u_2} {R : Type u_4} [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_1} {B : Type u_2} {C : Type u_3} {R : Type u_4} [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_1} {R : Type u_4} [RCLike R] [Fintype A] [DecidableEq A] : (MatrixMap.id A R).IsCompletelyPositive

The identity MatrixMap IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.add {A : Type u_1} {B : Type u_2} {R : Type u_4} [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_1} {B : Type u_2} {R : Type u_4} [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_1) (B : Type u_2) {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] : IsCompletelyPositive 0

The zero map IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.finset_sum {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {ι : Type u_5} [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.IsCompletelyPositive.kron_kronecker_const {A : Type u_1} {R : Type u_4} [RCLike R] [Fintype A] [DecidableEq A] {d : Type u_5} [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_PSD_iff_CP_map {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq A] (M : MatrixMap A B ℂ) : M.IsCompletelyPositive ↔ M.choi_matrix.PosSemidef

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

def MatrixMap.IsCompletelyPositive.conj {A : Type u_1} {B : Type u_2} {R : Type u_4} [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.IsCompletelyPositive.conj y = { toFun := fun (x : Matrix A A R) => y * x * y.conjTranspose, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MatrixMap.IsCompletelyPositive.conj_apply {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] (y : Matrix B A R) (x : Matrix A A R) : (conj y) x = y * x * y.conjTranspose

theorem MatrixMap.IsCompletelyPositive.conj_eq_mulRightLinearMap_comp_mulRightLinearMap {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] (y : Matrix B A R) : conj y = mulRightLinearMap B R y.conjTranspose ∘ₗ mulLeftLinearMap A R y

theorem MatrixMap.IsCompletelyPositive.conj_isCompletelyPositive {A : Type u_1} {B : Type u_2} {R : Type u_4} [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 Matrix.submatrix_eq_mul_mul {R : Type u_4} [RCLike R] {d : Type u_5} [Fintype d] {d₂ : Type u_6} {d₃ : Type u_7} [DecidableEq d] (A : Matrix d d R) (e : d₂ → d) (f : d₃ → d) : A.submatrix e f = submatrix 1 e id * A * submatrix 1 id f

theorem MatrixMap.IsCompletelyPositive.submatrix {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] (f : B → A) : (MatrixMap.submatrix R f).IsCompletelyPositive

MatrixMap.submatrix is completely positive

theorem MatrixMap.IsCompletelyPositive.of_kraus_isCompletelyPositive {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {κ : Type u_6} [Fintype κ] (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.IsCompletelyPositive.exists_kraus {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] (Φ : MatrixMap A B R) (hCP : Φ.IsCompletelyPositive) : ∃ (r : ℕ) (M : Fin r → Matrix B A R), Φ = of_kraus M M

theorem MatrixMap.IsCompletelyPositive.kron {A : Type u_1} {B : Type u_2} {C : Type u_3} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] {D : Type u_6} [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.piKron {R : Type u_4} [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.piKron Λi).IsCompletelyPositive

The piKron product of IsCompletelyPositive maps is also completely positive.