Completely positive maps

A linear map φ : A₁ →ₗ[ℂ] A₂ (where A₁ and A₂ are C⋆-algebras) is called completely positive (CP) if CStarMatrix.map (Fin k) (Fin k) φ (i.e. applying φ to all entries of a k × k matrix) is also positive for every k : ℕ.

This file defines completely positive maps and develops their basic API.

Main results

• NonUnitalStarAlgHomClass.instCompletelyPositiveMapClass: Non-unital star algebra homomorphisms are completely positive.

Notation

• A₁ →CP A₂ denotes the type of CP maps from A₁ to A₂. This notation is scoped to CStarAlgebra.

Implementation notes

The morphism class CompletelyPositiveMapClass is designed to be part of the order hierarchy, and only includes the order property; linearity is not mentioned at all. It is therefore meant to be used in conjunction with LinearMapClass. This is meant to avoid mixing order and algebra as much as possible.

structure CompletelyPositiveMap (A₁ : Type u_1) (A₂ : Type u_2) [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] extends A₁ →ₗ[ℂ] A₂ : Type (max u_1 u_2)

A linear map φ : A₁ →ₗ[ℂ] A₂ is called completely positive (CP) if CStarMatrix.mapₗ (Fin k) (Fin k) φ (i.e. applying φ to all entries of a k × k matrix) is also positive for every k ∈ ℕ.

Note that Fin k here is hardcoded to avoid having to quantify over types and introduce a new universe parameter. See CompletelyPositiveMap.map_cstarMatrix_nonneg for a version of the property that holds for matrices indexed by any finite type.

• toFun : A₁ → A₂
• map_add' (x y : A₁) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : ℂ) (x : A₁) : self.toFun (m • x) = (RingHom.id ℂ) m • self.toFun x
• map_cstarMatrix_nonneg' (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M) : 0 ≤ M.map ⇑self.toLinearMap

class CompletelyPositiveMapClass (F : Type u_1) (A₁ : Type u_2) (A₂ : Type u_3) [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] [FunLike F A₁ A₂] : Prop

A linear map φ : A₁ →ₗ[ℂ] A₂ is called completely positive (CP) if CStarMatrix.mapₗ (Fin k) (Fin k) φ (i.e. applying φ to all entries of a k × k matrix) is also positive for every k ∈ ℕ.

Note that Fin k here is hardcoded to avoid having to quantify over types and introduce a new universe parameter. See CompletelyPositiveMap.map_cstarMatrix_nonneg for a version of the property that holds for matrices indexed by any finite type.

• map_cstarMatrix_nonneg' (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M) : 0 ≤ M.map ⇑φ

def CStarAlgebra.«term_→CP_» : Lean.TrailingParserDescr

Notation for a CompletelyPositiveMap.

Equations

• CStarAlgebra.«term_→CP_» = Lean.ParserDescr.trailingNode `CStarAlgebra.«term_→CP_» 25 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →CP ") (Lean.ParserDescr.cat `term 0))

def CompletelyPositiveMapClass.toCompletelyPositiveLinearMap {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [CompletelyPositiveMapClass F A₁ A₂] (f : F) : CompletelyPositiveMap A₁ A₂

Reinterpret an element of a type of completely positive maps as a completely positive linear map.

Equations

• ↑f = { toLinearMap := ↑f, map_cstarMatrix_nonneg' := ⋯ }

instance CompletelyPositiveMapClass.instCoeToCompletelyPositiveMap {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [CompletelyPositiveMapClass F A₁ A₂] : CoeHead F (CompletelyPositiveMap A₁ A₂)

Reinterpret an element of a type of completely positive maps as a completely positive linear map.

Equations

• CompletelyPositiveMapClass.instCoeToCompletelyPositiveMap = { coe := fun (f : F) => ↑f }

theorem OrderHomClass.of_map_cstarMatrix_nonneg {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] (h : ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ) : OrderHomClass F A₁ A₂

Linear maps which are completely positive are order homomorphisms (i.e., positive maps).

instance CompletelyPositiveMapClass.instOrderHomClass {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [CompletelyPositiveMapClass F A₁ A₂] : OrderHomClass F A₁ A₂

instance CompletelyPositiveMap.instFunLike {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] : FunLike (CompletelyPositiveMap A₁ A₂) A₁ A₂

Equations

• CompletelyPositiveMap.instFunLike = { coe := fun (f : CompletelyPositiveMap A₁ A₂) => f.toFun, coe_injective' := ⋯ }

instance CompletelyPositiveMap.instLinearMapClassComplex {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] : LinearMapClass (CompletelyPositiveMap A₁ A₂) ℂ A₁ A₂

instance CompletelyPositiveMap.instCompletelyPositiveMapClass {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] : CompletelyPositiveMapClass (CompletelyPositiveMap A₁ A₂) A₁ A₂

theorem CompletelyPositiveMap.map_cstarMatrix_nonneg {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] {n : Type u_3} [Fintype n] (φ : CompletelyPositiveMap A₁ A₂) (M : CStarMatrix n n A₁) (hM : 0 ≤ M) : 0 ≤ M.map ⇑φ

instance NonUnitalStarAlgHomClass.instCompletelyPositiveMapClass {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [PartialOrder A₂] [StarOrderedRing A₁] [StarOrderedRing A₂] [FunLike F A₁ A₂] [NonUnitalAlgHomClass F ℂ A₁ A₂] [StarHomClass F A₁ A₂] : CompletelyPositiveMapClass F A₁ A₂

Non-unital star algebra homomorphisms are completely positive.