Duals of matrix map

Definitions and theorems about the dual of a matrix map.

theorem HermitianMat.toMat_add {d : Type u_5} (x y : HermitianMat d ℂ) : ↑(x + y) = ↑x + ↑y

@[irreducible]

def MatrixMap.dual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {R : Type u_3} [CommRing R] [DecidableEq dIn] [DecidableEq dOut] (M : MatrixMap dIn dOut R) : MatrixMap dOut dIn R

The dual of a map between matrices, defined by Tr[A M(B)] = Tr[(dual M)(A) B]. Sometimes called the adjoint of the map instead.

Equations

• M.dual = ↑(Matrix.stdBasis R dIn dIn).toDualEquiv.symm ∘ₗ LinearMap.dualMap M ∘ₗ ↑(Matrix.stdBasis R dOut dOut).toDualEquiv

theorem MatrixMap.Dual.trace_eq {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {R : Type u_3} [CommRing R] [DecidableEq dIn] [DecidableEq dOut] (M : MatrixMap dIn dOut R) (A : Matrix dIn dIn R) (B : Matrix dOut dOut R) : (M A * B).trace = (A * M.dual B).trace

The defining property of a dual map: inner products are preserved on the opposite argument.

theorem MatrixMap.IsHermitianPreserving.dual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {M : MatrixMap dIn dOut 𝕜} (h : M.IsHermitianPreserving) : M.dual.IsHermitianPreserving

The dual of a IsHermitianPreserving map also IsHermitianPreserving.

theorem MatrixMap.IsPositive.dual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {M : MatrixMap dIn dOut 𝕜} (h : M.IsPositive) : M.dual.IsPositive

The dual of a IsPositive map also IsPositive.

theorem MatrixMap.dual_Unital {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {M : MatrixMap dIn dOut 𝕜} (h : M.IsTracePreserving) : M.dual.Unital

The dual of TracePreserving map is not trace-preserving, it's unital, that is, M*(I) = I.

theorem MatrixMap.IsTracePreserving.dual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {M : MatrixMap dIn dOut 𝕜} (h : M.IsTracePreserving) : M.dual.Unital

Alias of MatrixMap.dual_Unital.

---

The dual of TracePreserving map is not trace-preserving, it's unital, that is, M*(I) = I.

theorem MatrixMap.IsCompletelyPositive.dual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {M : MatrixMap dIn dOut 𝕜} (h : M.IsCompletelyPositive) : M.dual.IsCompletelyPositive

@[simp]

theorem MatrixMap.dual_dual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {M : MatrixMap dIn dOut 𝕜} : M.dual.dual = M

def CPTPMap.dual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (M : CPTPMap dIn dOut ℂ) : CPUMap dOut dIn ℂ

Equations

• M.dual = { toLinearMap := (((M.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map.dual, HP := ⋯, pos := ⋯, cp := ⋯, unital := ⋯ }

theorem CPTPMap.dual_pos {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (M : CPTPMap dIn dOut ℂ) {T : HermitianMat dOut ℂ} (hT : 0 ≤ T) : 0 ≤ M.dual T

theorem CPTPMap.dual.PTP_POVM {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (M : CPTPMap dIn dOut ℂ) {T : HermitianMat dOut ℂ} (hT : 0 ≤ T ∧ T ≤ 1) : 0 ≤ M.dual T ∧ M.dual T ≤ 1

The dual of a CPTP map preserves POVMs. Stated here just for two-element POVMs, that is, an operator T between 0 and 1.

theorem CPTPMap.exp_val_Dual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (ℰ : CPTPMap dIn dOut ℂ) (ρ : MState dIn) (T : HermitianMat dOut ℂ) : (ℰ ρ).exp_val T = ρ.exp_val (ℰ.dual T)

The defining property of a dual channel, as specialized to MState.exp_val.

def HPMap.ofHermitianMat {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HermitianMat dIn ℂ →ₗ[ℝ] HermitianMat dOut ℂ) : HPMap dIn dOut ℂ

Equations

• HPMap.ofHermitianMat f = { toFun := fun (x : Matrix dIn dIn ℂ) => ↑(f (realPart x)) + Complex.I • ↑(f (imaginaryPart x)), map_add' := ⋯, map_smul' := ⋯, HP := ⋯ }

@[simp]

theorem HPMap.linearMap_ofHermitianMat {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HermitianMat dIn ℂ →ₗ[ℝ] HermitianMat dOut ℂ) : LinearMapClass.linearMap (ofHermitianMat f) = f

@[simp]

theorem HPMap.ofHermitianMat_linearMap {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HPMap dIn dOut ℂ) : ofHermitianMat (LinearMapClass.linearMap f) = f

def HPMap.hermDual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HPMap dIn dOut ℂ) : HPMap dOut dIn ℂ

Equations

• f.hermDual = HPMap.ofHermitianMat (LinearMap.adjoint (LinearMapClass.linearMap f))

@[simp]

theorem HPMap.hermDual_hermDual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HPMap dIn dOut ℂ) : f.hermDual.hermDual = f

theorem HPMap.inner_hermDual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HPMap dIn dOut ℂ) (A : HermitianMat dIn ℂ) (B : HermitianMat dOut ℂ) : inner ℝ (f A) B = inner ℝ A (f.hermDual B)

The defining property of a dual map: inner products are preserved on the opposite argument.

theorem HPMap.inner_hermDual' {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HPMap dIn dOut ℂ) (A : HermitianMat dIn ℂ) (B : HermitianMat dOut ℂ) : (f A).inner B = A.inner (f.hermDual B)

Version of HPMap.inner_hermDual that uses HermitiaMat.inner directly. TODO cleanup

theorem HermitianMat.inner_negPart_nonpos {dIn : Type u_1} [Fintype dIn] (A : HermitianMat dIn ℂ) [DecidableEq dIn] : Inner.inner ℝ A A⁻ ≤ 0

theorem HermitianMat.cfc_eq_cfc_iff_eqOn {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] (A : HermitianMat dIn ℂ) (f g : ℝ → ℝ) : A.cfc f = A.cfc g ↔ Set.EqOn f g (spectrum ℝ ↑A)

theorem HermitianMat.inner_negPart_zero_iff {dIn : Type u_1} [Fintype dIn] (A : HermitianMat dIn ℂ) [DecidableEq dIn] : Inner.inner ℝ A A⁻ = 0 ↔ 0 ≤ A

theorem HermitianMat.inner_negPart_neg_iff {dIn : Type u_1} [Fintype dIn] (A : HermitianMat dIn ℂ) [DecidableEq dIn] : Inner.inner ℝ A A⁻ < 0 ↔ ¬0 ≤ A

theorem HermitianMat.zero_le_iff_inner_pos {dIn : Type u_1} [Fintype dIn] (A : HermitianMat dIn ℂ) : 0 ≤ A ↔ ∀ (B : HermitianMat dIn ℂ), 0 ≤ B → 0 ≤ Inner.inner ℝ A B

theorem MatrixMap.IsPositive.hermDual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HPMap dIn dOut ℂ) (h : f.map.IsPositive) : f.hermDual.map.IsPositive

The dual of a IsPositive map also IsPositive.

theorem HPMap.hermDual_Unital {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HPMap dIn dOut ℂ) [DecidableEq dIn] [DecidableEq dOut] (h : f.map.IsTracePreserving) : f.hermDual.map.Unital

The dual of TracePreserving map is not trace-preserving, it's unital, that is, M*(I) = I.

theorem MatrixMap.IsTracePreserving.hermDual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (f : HPMap dIn dOut ℂ) [DecidableEq dIn] [DecidableEq dOut] (h : f.map.IsTracePreserving) : f.hermDual.map.Unital

Alias of HPMap.hermDual_Unital.

---

The dual of TracePreserving map is not trace-preserving, it's unital, that is, M*(I) = I.

def PTPMap.hermDual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (M : PTPMap dIn dOut ℂ) : PUMap dOut dIn ℂ

Equations

• M.hermDual = { toHPMap := ((M.toPMap ℂ).toHPMap ℂ).hermDual, pos := ⋯, unital := ⋯ }

theorem PTPMap.hermDual_pos {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (M : PTPMap dIn dOut ℂ) {T : HermitianMat dOut ℂ} (hT : 0 ≤ T) : 0 ≤ M.hermDual T

theorem PTPMap.hermDual.PTP_POVM {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (M : PTPMap dIn dOut ℂ) {T : HermitianMat dOut ℂ} (hT : 0 ≤ T ∧ T ≤ 1) : 0 ≤ M.hermDual T ∧ M.hermDual T ≤ 1

The dual of a PTP map preserves POVMs. Stated here just for two-element POVMs, that is, an operator T between 0 and 1.

theorem PTPMap.exp_val_hermDual {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (ℰ : PTPMap dIn dOut ℂ) (ρ : MState dIn) (T : HermitianMat dOut ℂ) : (ℰ ρ).exp_val T = ρ.exp_val (ℰ.hermDual T)

The defining property of a dual channel, as specialized to MState.exp_val.