Duals of matrix map #

Definitions and theorems about the dual of a matrix map.

@[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

Instances For

source

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.

source

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.

source

theorem Matrix.PosSemidef.trace_mul_nonneg {𝕜 : Type u_4} [RCLike 𝕜] {n : Type u_5} [Fintype n] [DecidableEq n] {A B : Matrix n n 𝕜} (hA : A.PosSemidef) (hB : B.PosSemidef) :

0 ≤ (A * B).trace

source

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.

source

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.

source

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.

source

theorem MatrixMap.dual_unique {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' : MatrixMap dOut dIn 𝕜) (h : ∀ (A : Matrix dIn dIn 𝕜) (B : Matrix dOut dOut 𝕜), (M A * B).trace = (A * M' B).trace) :

M.dual = M'

If two matrix maps satisfy the trace duality property, they are equal.

source

theorem MatrixMap.dual_choi_matrix {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.choi_matrix = (Matrix.reindex (Equiv.prodComm dOut dIn) (Equiv.prodComm dOut dIn)) M.choi_matrix.transpose

The Choi matrix of the dual map is the transpose of the reindexed Choi matrix of the original map.

source

theorem MatrixMap.dual_choi_matrix_posSemidef_of_posSemidef {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.choi_matrix.PosSemidef) :

M.dual.choi_matrix.PosSemidef

If the Choi matrix of a map is positive semidefinite, then the Choi matrix of its dual is also positive semidefinite.

source

theorem MatrixMap.dual_id {dIn : Type u_1} [Fintype dIn] {𝕜 : Type u_4} [RCLike 𝕜] [DecidableEq dIn] :

(id dIn 𝕜).dual = id dIn 𝕜

The dual of the identity map is the identity map.

source

theorem MatrixMap.dual_kron {𝕜 : Type u_4} [RCLike 𝕜] {A : Type u_5} {B : Type u_6} {C : Type u_7} {D : Type u_8} [Fintype A] [Fintype B] [Fintype C] [Fintype D] [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D] (M : MatrixMap A B 𝕜) (N : MatrixMap C D 𝕜) :

(M.kron N).dual = M.dual.kron N.dual

The dual of a Kronecker product of maps is the Kronecker product of their duals.

source

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

source

theorem MatrixMap.Module.Basis.dualMap_toDualEquiv_symm_comp_toDualEquiv {ι : Type u_5} {R : Type u_6} {M : Type u_7} [Fintype ι] [DecidableEq ι] [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] (b : Module.Basis ι R M) :

(↑b.toDualEquiv.symm).dualMap ∘ₗ ↑b.toDualEquiv = ↑(Module.evalEquiv R M)

The composition of the dual of the inverse of the dual basis isomorphism with the dual basis isomorphism is the evaluation map.

source

theorem MatrixMap.Module.Basis.toDualEquiv_symm_comp_dualMap_toDualEquiv {ι : Type u_5} {R : Type u_6} {M : Type u_7} [Fintype ι] [DecidableEq ι] [CommRing R] [AddCommGroup M] [Module R M] [Module.IsReflexive R M] (b : Module.Basis ι R M) :

↑b.toDualEquiv.symm ∘ₗ (↑b.toDualEquiv).dualMap = ↑(Module.evalEquiv R M).symm

The composition of the inverse of the dual basis isomorphism with the dual of the dual basis isomorphism is the inverse of the evaluation map.

source

@[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

source

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 := ⋯ }

Instances For

source

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

source

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.

source

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.

source

def HPMap.ofHermitianMat {dIn : Type u_1} [Fintype dIn] {dOut : Type u_5} (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 := ⋯ }

Instances For

source

@[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

source

@[simp]

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

ofHermitianMat (LinearMapClass.linearMap f) = f

source

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))

Instances For

source

@[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

source

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.

source

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)

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

source

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.

source

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.

source

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.

source

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 := ⋯ }

Instances For

source

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

source

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.

source

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.

Physlib Documentation

QuantumInfo.Finite.CPTPMap.Dual

Duals of matrix map #