Positive linear maps in C⋆-algebras

This file develops the API for positive linear maps over C⋆-algebras.

Main results

• PositiveLinearMap.exists_norm_apply_le: positive maps are bounded (and therefore continuous) on non-unital C⋆-algebras.

References

• The proof that positive maps are bounded was taken from https://math.stackexchange.com/questions/426487/why-is-every-positive-linear-map-between-c-algebras-bounded

theorem map_isSelfAdjoint {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalRing A₁] [Module ℂ A₁] [SMulCommClass ℝ A₁ A₁] [IsScalarTower ℝ A₁ A₁] [StarRing A₁] [TopologicalSpace A₁] [NonUnitalContinuousFunctionalCalculus ℝ A₁ IsSelfAdjoint] [PartialOrder A₁] [StarOrderedRing A₁] [NonUnitalRing A₂] [Module ℂ A₂] [StarRing A₂] [PartialOrder A₂] [StarOrderedRing A₂] (f : A₁ →ₚ[ℂ] A₂) (a : A₁) (ha : IsSelfAdjoint a) : IsSelfAdjoint (f a)

theorem PositiveLinearMap.apply_le_of_isSelfAdjoint {B₁ : Type u_3} {B₂ : Type u_4} [CStarAlgebra B₁] [CStarAlgebra B₂] [PartialOrder B₁] [PartialOrder B₂] [StarOrderedRing B₁] [StarOrderedRing B₂] (f : B₁ →ₚ[ℂ] B₂) (x : B₁) (hx : IsSelfAdjoint x) : f x ≤ f ((algebraMap ℝ B₁) ‖x‖)

theorem PositiveLinearMap.norm_apply_le_of_nonneg {B₁ : Type u_3} {B₂ : Type u_4} [CStarAlgebra B₁] [CStarAlgebra B₂] [PartialOrder B₁] [PartialOrder B₂] [StarOrderedRing B₁] [StarOrderedRing B₂] (f : B₁ →ₚ[ℂ] B₂) (x : B₁) (hx : 0 ≤ x) : ‖f x‖ ≤ ‖f 1‖ * ‖x‖

theorem PositiveLinearMap.exists_norm_apply_le {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [StarOrderedRing A₁] [PartialOrder A₂] [StarOrderedRing A₂] (f : A₁ →ₚ[ℂ] A₂) : ∃ (C : NNReal), ∀ (a : A₁), ‖f a‖ ≤ ↑C * ‖a‖

If f is a positive map, then it is bounded (and therefore continuous).

instance PositiveLinearMap.instContinuousLinearMapClassComplexOfPositiveLinearMapClass {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [StarOrderedRing A₁] [PartialOrder A₂] [StarOrderedRing A₂] {F : Type u_5} [FunLike F A₁ A₂] [PositiveLinearMapClass F ℂ A₁ A₂] : ContinuousLinearMapClass F ℂ A₁ A₂

instance PositiveLinearMap.instStarHomClassOfPositiveLinearMapClassComplex {A₁ : Type u_1} {A₂ : Type u_2} [NonUnitalCStarAlgebra A₁] [NonUnitalCStarAlgebra A₂] [PartialOrder A₁] [StarOrderedRing A₁] [PartialOrder A₂] [StarOrderedRing A₂] {F : Type u_5} [FunLike F A₁ A₂] [PositiveLinearMapClass F ℂ A₁ A₂] : StarHomClass F A₁ A₂