Classes of Matrix Maps

The bundled MatrixMaps: HPMap, UnitalMap, TPMap, PMap, and CPMap. These are defined over the bare minimum rings (Semiring or RCLike, respectively).

The combinations PTPMap (positive trace-preserving), CPTPMap, and CPUMap (CP unital maps) take ℂ as the default class.

The majority of quantum theory revolves around CPTPMaps, so those are explored more thoroughly in their file CPTP.lean.

theorem Matrix.PosSemidef.trace_pos {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.PosSemidef) (h : A ≠ 0) : 0 < A.trace

theorem HermitianMat.trace_pos {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] {A : HermitianMat n 𝕜} (hA : 0 < A) : 0 < A.trace

structure HPMap (dIn : Type u_1) (dOut : Type u_2) (𝕜 : Type := ℂ) [RCLike 𝕜] extends Matrix dIn dIn 𝕜 →ₗ[𝕜] Matrix dOut dOut 𝕜 : Type (max u_1 u_2)

Hermitian-preserving linear maps.

• toFun : Matrix dIn dIn 𝕜 → Matrix dOut dOut 𝕜
• map_add' (x y : Matrix dIn dIn 𝕜) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : 𝕜) (x : Matrix dIn dIn 𝕜) : self.toFun (m • x) = (RingHom.id 𝕜) m • self.toFun x
• HP : MatrixMap.IsHermitianPreserving self.toLinearMap

structure UnitalMap (dIn : Type u_1) (dOut : Type u_2) (R : Type u_3) [Semiring R] [DecidableEq dIn] [DecidableEq dOut] extends Matrix dIn dIn R →ₗ[R] Matrix dOut dOut R : Type (max (max u_1 u_2) u_3)

Unital linear maps.

• toFun : Matrix dIn dIn R → Matrix dOut dOut R
• map_add' (x y : Matrix dIn dIn R) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : R) (x : Matrix dIn dIn R) : self.toFun (m • x) = (RingHom.id R) m • self.toFun x
• unital : MatrixMap.Unital self.toLinearMap

structure TPMap (dIn : Type u_1) (dOut : Type u_2) (R : Type u_3) [Fintype dIn] [Fintype dOut] [Semiring R] extends Matrix dIn dIn R →ₗ[R] Matrix dOut dOut R : Type (max (max u_1 u_2) u_3)

Trace-preserving linear maps.

• toFun : Matrix dIn dIn R → Matrix dOut dOut R
• map_add' (x y : Matrix dIn dIn R) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : R) (x : Matrix dIn dIn R) : self.toFun (m • x) = (RingHom.id R) m • self.toFun x
• TP : MatrixMap.IsTracePreserving self.toLinearMap

structure PMap (dIn : Type u_1) (dOut : Type u_2) (𝕜 : Type := ℂ) [Fintype dIn] [Fintype dOut] [RCLike 𝕜] extends HPMap dIn dOut 𝕜 : Type (max u_1 u_2)

Positive linear maps.

• toFun : Matrix dIn dIn 𝕜 → Matrix dOut dOut 𝕜
• map_add' (x y : Matrix dIn dIn 𝕜) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : 𝕜) (x : Matrix dIn dIn 𝕜) : self.toFun (m • x) = (RingHom.id 𝕜) m • self.toFun x
• HP : MatrixMap.IsHermitianPreserving self.toLinearMap
• pos : MatrixMap.IsPositive self.toLinearMap

structure CPMap (dIn : Type u_1) (dOut : Type u_2) (𝕜 : Type := ℂ) [Fintype dIn] [Fintype dOut] [RCLike 𝕜] [DecidableEq dIn] extends PMap dIn dOut 𝕜 : Type (max u_1 u_2)

Completely positive linear maps.

• toFun : Matrix dIn dIn 𝕜 → Matrix dOut dOut 𝕜
• map_add' (x y : Matrix dIn dIn 𝕜) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : 𝕜) (x : Matrix dIn dIn 𝕜) : self.toFun (m • x) = (RingHom.id 𝕜) m • self.toFun x
• HP : MatrixMap.IsHermitianPreserving self.toLinearMap
• pos : MatrixMap.IsPositive self.toLinearMap
• cp : MatrixMap.IsCompletelyPositive self.toLinearMap

structure PTPMap (dIn : Type u_1) (dOut : Type u_2) (𝕜 : Type := ℂ) [Fintype dIn] [Fintype dOut] [RCLike 𝕜] extends PMap dIn dOut 𝕜, TPMap dIn dOut 𝕜 : Type (max u_1 u_2)

Positive trace-preserving linear maps. These includes all channels, but aren't necessarily completely positive, see CPTPMap.

• toFun : Matrix dIn dIn 𝕜 → Matrix dOut dOut 𝕜
• map_add' (x y : Matrix dIn dIn 𝕜) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : 𝕜) (x : Matrix dIn dIn 𝕜) : self.toFun (m • x) = (RingHom.id 𝕜) m • self.toFun x
• HP : MatrixMap.IsHermitianPreserving self.toLinearMap
• pos : MatrixMap.IsPositive self.toLinearMap
• TP : MatrixMap.IsTracePreserving self.toLinearMap

structure PUMap (dIn : Type u_1) (dOut : Type u_2) (𝕜 : Type := ℂ) [Fintype dIn] [Fintype dOut] [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] extends PMap dIn dOut 𝕜, UnitalMap dIn dOut 𝕜 : Type (max u_1 u_2)

Positive unital maps. These are important because they are the dual to PTPMap: they are the most general way to map observables.

• toFun : Matrix dIn dIn 𝕜 → Matrix dOut dOut 𝕜
• map_add' (x y : Matrix dIn dIn 𝕜) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : 𝕜) (x : Matrix dIn dIn 𝕜) : self.toFun (m • x) = (RingHom.id 𝕜) m • self.toFun x
• HP : MatrixMap.IsHermitianPreserving self.toLinearMap
• pos : MatrixMap.IsPositive self.toLinearMap
• unital : MatrixMap.Unital self.toLinearMap

structure CPTPMap (dIn : Type u_1) (dOut : Type u_2) (𝕜 : Type := ℂ) [Fintype dIn] [Fintype dOut] [RCLike 𝕜] [DecidableEq dIn] extends PTPMap dIn dOut 𝕜, CPMap dIn dOut 𝕜 : Type (max u_1 u_2)

Completely positive trace-preserving linear maps. This is the most common meaning of "channel", often described as "the most general physically realizable quantum operation".

• toFun : Matrix dIn dIn 𝕜 → Matrix dOut dOut 𝕜
• map_add' (x y : Matrix dIn dIn 𝕜) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : 𝕜) (x : Matrix dIn dIn 𝕜) : self.toFun (m • x) = (RingHom.id 𝕜) m • self.toFun x
• HP : MatrixMap.IsHermitianPreserving self.toLinearMap
• pos : MatrixMap.IsPositive self.toLinearMap
• TP : MatrixMap.IsTracePreserving self.toLinearMap
• cp : MatrixMap.IsCompletelyPositive self.toLinearMap

structure CPUMap (dIn : Type u_1) (dOut : Type u_2) (𝕜 : Type := ℂ) [Fintype dIn] [Fintype dOut] [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] extends CPMap dIn dOut 𝕜, PUMap dIn dOut 𝕜 : Type (max u_1 u_2)

Completely positive unital maps. These are important because they are the dual to CPTPMap: they are the physically realizable ways to map observables.

• toFun : Matrix dIn dIn 𝕜 → Matrix dOut dOut 𝕜
• map_add' (x y : Matrix dIn dIn 𝕜) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : 𝕜) (x : Matrix dIn dIn 𝕜) : self.toFun (m • x) = (RingHom.id 𝕜) m • self.toFun x
• HP : MatrixMap.IsHermitianPreserving self.toLinearMap
• pos : MatrixMap.IsPositive self.toLinearMap
• cp : MatrixMap.IsCompletelyPositive self.toLinearMap
• unital : MatrixMap.Unital self.toLinearMap

@[reducible, inline]

abbrev HPMap.map {dIn : Type u_1} {dOut : Type u_2} {𝕜 : Type} [RCLike 𝕜] (M : HPMap dIn dOut 𝕜) : MatrixMap dIn dOut 𝕜

Equations

• M.map = M.toLinearMap

theorem HPMap.ext {dIn : Type u_1} {dOut : Type u_2} {𝕜 : Type} [RCLike 𝕜] {Λ₁ Λ₂ : HPMap dIn dOut 𝕜} (h : Λ₁.map = Λ₂.map) : Λ₁ = Λ₂

theorem HPMap.ext_iff {dIn : Type u_1} {dOut : Type u_2} {𝕜 : Type} [RCLike 𝕜] {Λ₁ Λ₂ : HPMap dIn dOut 𝕜} : Λ₁ = Λ₂ ↔ Λ₁.map = Λ₂.map

theorem HPMap.funext_hermitian {dIn : Type u_1} {dOut : Type u_2} {CΛ₁ CΛ₂ : HPMap dIn dOut ℂ} (h : ∀ (M : HermitianMat dIn ℂ), CΛ₁.map ↑M = CΛ₂.map ↑M) : CΛ₁ = CΛ₂

Two maps are equal if they agree on all Hermitian inputs.

theorem HPMap.funext_pos {dIn : Type u_1} {dOut : Type u_2} {CΛ₁ CΛ₂ : HPMap dIn dOut ℂ} [Fintype dIn] (h : ∀ (M : HermitianMat dIn ℂ), 0 ≤ M → CΛ₁.map ↑M = CΛ₂.map ↑M) : CΛ₁ = CΛ₂

Two maps are equal if they agree on all positive inputs.

theorem HPMap.funext_pos_trace {dIn : Type u_1} {dOut : Type u_2} {CΛ₁ CΛ₂ : HPMap dIn dOut ℂ} [Fintype dIn] (h : ∀ (M : HermitianMat dIn ℂ), 0 ≤ M → M.trace = 1 → CΛ₁.map ↑M = CΛ₂.map ↑M) : CΛ₁ = CΛ₂

Two maps are equal if they agree on all positive inputs with trace one

theorem HPMap.funext_mstate {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [DecidableEq dIn] {Λ₁ Λ₂ : HPMap dIn dOut ℂ} (h : ∀ (ρ : MState dIn), Λ₁.map ρ.m = Λ₂.map ρ.m) : Λ₁ = Λ₂

Two maps are equal if they agree on all MStates.

instance HPMap.instFunLike {dIn : Type u_1} {dOut : Type u_2} : FunLike (HPMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

Hermitian-preserving maps are functions from HermitianMats to HermitianMats.

Equations

• HPMap.instFunLike = { coe := fun (Λ : HPMap dIn dOut ℂ) (ρ : HermitianMat dIn ℂ) => ⟨Λ.map ↑ρ, ⋯⟩, coe_injective' := ⋯ }

instance HPMap.instContinuousLinearMapClassComplexRealHermitianMat {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] : ContinuousLinearMapClass (HPMap dIn dOut ℂ) ℝ (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

theorem PMap.ext {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] {Λ₁ Λ₂ : PMap dIn dOut 𝕜} (h : Λ₁.map = Λ₂.map) : Λ₁ = Λ₂

theorem PMap.ext_iff {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] {Λ₁ Λ₂ : PMap dIn dOut 𝕜} : Λ₁ = Λ₂ ↔ Λ₁.map = Λ₂.map

theorem PMap.injective_toHPMap {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] : Function.Injective toHPMap

instance PMap.instFunLike {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] : FunLike (PMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

Positive maps are functions from HermitianMats to HermitianMats.

Equations

• PMap.instFunLike = { coe := DFunLike.coe ∘ PMap.toHPMap ℂ, coe_injective' := ⋯ }

instance PMap.instLinearMapClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] : LinearMapClass (PMap dIn dOut ℂ) ℝ (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

instance PMap.instContinuousOrderHomClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] : ContinuousOrderHomClass (PMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

@[simp]

theorem PMap.pos_Hermitian {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (M : PMap dIn dOut ℂ) {x : HermitianMat dIn ℂ} (h : 0 ≤ x) : 0 ≤ M x

Positive-presering maps also preserve positivity on, specifically, Hermitian matrices.

def CPMap.of_kraus_CPMap {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] {κ : Type u_4} [Fintype κ] [DecidableEq dIn] (M : κ → Matrix dOut dIn 𝕜) : CPMap dIn dOut 𝕜

Equations

• CPMap.of_kraus_CPMap M = { toLinearMap := MatrixMap.of_kraus M M, HP := ⋯, pos := ⋯, cp := ⋯ }

theorem PTPMap.ext {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] {Λ₁ Λ₂ : PTPMap dIn dOut 𝕜} (h : Λ₁.map = Λ₂.map) : Λ₁ = Λ₂

theorem PTPMap.ext_iff {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] {Λ₁ Λ₂ : PTPMap dIn dOut 𝕜} : Λ₁ = Λ₂ ↔ Λ₁.map = Λ₂.map

theorem PTPMap.injective_toPMap {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] : Function.Injective toPMap

instance PTPMap.instFunLike {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] : FunLike (PTPMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

Positive trace-preserving maps are functions from HermitianMats to HermitianMats.

Equations

• PTPMap.instFunLike = { coe := DFunLike.coe ∘ PTPMap.toPMap ℂ, coe_injective' := ⋯ }

instance PTPMap.instLinearMapClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] : LinearMapClass (PTPMap dIn dOut ℂ) ℝ (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

instance PTPMap.instHContinuousOrderHomClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] : ContinuousOrderHomClass (PTPMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

@[simp]

theorem PTPMap.pos_Hermitian {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (M : PTPMap dIn dOut ℂ) {x : HermitianMat dIn ℂ} (h : 0 ≤ x) : 0 ≤ M x

PTP maps also preserve positivity on Hermitian matrices.

instance PTPMap.instMFunLike {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : FunLike (PTPMap dIn dOut ℂ) (MState dIn) (MState dOut)

PTPMaps are functions from MStates to MStates.

Equations

• PTPMap.instMFunLike = { coe := fun (Λ : PTPMap dIn dOut ℂ) (ρ : MState dIn) => { M := ((Λ.toPMap ℂ).toHPMap ℂ) ↑ρ, zero_le := ⋯, tr := ⋯ }, coe_injective' := ⋯ }

instance PTPMap.instMContinuousMapClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : ContinuousMapClass (PTPMap dIn dOut ℂ) (MState dIn) (MState dOut)

theorem PTPMap.val_apply_MState {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (M : PTPMap dIn dOut ℂ) (ρ : MState dIn) : M ↑ρ = M ↑ρ

theorem PTPMap.nonemptyOut {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (Λ : PTPMap dIn dOut ℂ) [hIn : Nonempty dIn] [DecidableEq dIn] : Nonempty dOut

theorem CPTPMap.ext {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] {Λ₁ Λ₂ : CPTPMap dIn dOut 𝕜} (h : Λ₁.map = Λ₂.map) : Λ₁ = Λ₂

Two CPTPMaps are equal if their MatrixMaps are equal.

theorem CPTPMap.ext_iff {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] {Λ₁ Λ₂ : CPTPMap dIn dOut 𝕜} : Λ₁ = Λ₂ ↔ Λ₁.map = Λ₂.map

theorem CPTPMap.injective_toPTPMap {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] : Function.Injective toPTPMap

instance CPTPMap.instMFunLike {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : FunLike (CPTPMap dIn dOut ℂ) (MState dIn) (MState dOut)

CPTPMaps are functions from MStates to MStates.

Equations

• CPTPMap.instMFunLike = { coe := DFunLike.coe ∘ CPTPMap.toPTPMap ℂ, coe_injective' := ⋯ }

@[simp]

theorem CPTPMap.IsTracePreserving {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] (Λ : CPTPMap dIn dOut 𝕜) : Λ.map.IsTracePreserving

def CPTPMap.of_kraus_CPTPMap {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] {κ : Type u_4} [Fintype κ] [DecidableEq dIn] (M : κ → Matrix dOut dIn 𝕜) (hTP : ∑ k : κ, (M k).conjTranspose * M k = 1) : CPTPMap dIn dOut 𝕜

Equations

• CPTPMap.of_kraus_CPTPMap M hTP = { toLinearMap := MatrixMap.of_kraus M M, HP := ⋯, pos := ⋯, TP := ⋯, cp := ⋯ }

theorem PUMap.ext {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {Λ₁ Λ₂ : PUMap dIn dOut 𝕜} (h : Λ₁.map = Λ₂.map) : Λ₁ = Λ₂

theorem PUMap.ext_iff {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {Λ₁ Λ₂ : PUMap dIn dOut 𝕜} : Λ₁ = Λ₂ ↔ Λ₁.map = Λ₂.map

theorem PUMap.injective_toPMap {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] : Function.Injective toPMap

instance PUMap.instFunLike {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : FunLike (PUMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

PUMaps are functions from HermitianMats to HermitianMats.

Equations

• PUMap.instFunLike = { coe := fun (Λ : PUMap dIn dOut ℂ) => ⇑(Λ.toPMap ℂ), coe_injective' := ⋯ }

instance PUMap.instLinearMapClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : LinearMapClass (PUMap dIn dOut ℂ) ℝ (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

instance PUMap.instHContinuousOrderHomClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : ContinuousOrderHomClass (PUMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

instance PUMap.instOneHomClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : OneHomClass (PUMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

@[simp]

theorem PUMap.pos_Hermitian {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (M : PUMap dIn dOut ℂ) {x : HermitianMat dIn ℂ} (h : 0 ≤ x) : 0 ≤ M x

CPTP maps also preserve positivity on Hermitian matrices.

theorem CPUMap.ext {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {Λ₁ Λ₂ : CPUMap dIn dOut 𝕜} (h : Λ₁.map = Λ₂.map) : Λ₁ = Λ₂

theorem CPUMap.ext_iff {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] {Λ₁ Λ₂ : CPUMap dIn dOut 𝕜} : Λ₁ = Λ₂ ↔ Λ₁.map = Λ₂.map

theorem CPUMap.injective_toPMap {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {𝕜 : Type} [RCLike 𝕜] [DecidableEq dIn] [DecidableEq dOut] : Function.Injective (CPMap.toPMap ∘ toCPMap)

instance CPUMap.instFunLike {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : FunLike (CPUMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

CPUMaps are functions from HermitianMats to HermitianMats.

Equations

• CPUMap.instFunLike = { coe := fun (Λ : CPUMap dIn dOut ℂ) => ⇑((Λ.toCPMap ℂ).toPMap ℂ), coe_injective' := ⋯ }

instance CPUMap.instLinearMapClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : LinearMapClass (CPUMap dIn dOut ℂ) ℝ (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

instance CPUMap.instHContinuousOrderHomClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : ContinuousOrderHomClass (CPUMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

instance CPUMap.instOneHomClass {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] : OneHomClass (CPUMap dIn dOut ℂ) (HermitianMat dIn ℂ) (HermitianMat dOut ℂ)

@[simp]

theorem CPUMap.pos_Hermitian {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (M : CPUMap dIn dOut ℂ) {x : HermitianMat dIn ℂ} (h : 0 ≤ x) : 0 ≤ M x

CPTP maps also preserve positivity on Hermitian matrices.