Positive linear maps

This file defines positive linear maps as a linear map that is also an order homomorphism.

Implementation notes

We do not define PositiveLinearMapClass to avoid adding a class that mixes order and algebra. One can achieve the same effect by using a combination of LinearMapClass and OrderHomClass. We nevertheless use the namespace for lemmas using that combination of typeclasses.

Notes

More substantial results on positive maps such as their continuity can be found in the Analysis/CStarAlgebra folder.

structure PositiveLinearMap (R : Type u_1) (E₁ : Type u_2) (E₂ : Type u_3) [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] extends E₁ →ₗ[R] E₂, E₁ →o E₂ : Type (max u_2 u_3)

A positive linear map is a linear map that is also an order homomorphism.

• toFun : E₁ → E₂
• map_add' (x y : E₁) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : R) (x : E₁) : self.toFun (m • x) = (RingHom.id R) m • self.toFun x
• monotone' : Monotone self.toFun

def «term_→ₚ[_]_» : Lean.TrailingParserDescr

Notation for a PositiveLinearMap.

Equations

• One or more equations did not get rendered due to their size.

def PositiveLinearMap.ofClass {F : Type u_1} {R : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [FunLike F E₁ E₂] [LinearMapClass F R E₁ E₂] [OrderHomClass F E₁ E₂] (f : F) : E₁ →ₚ[R] E₂

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

Equations

• PositiveLinearMap.ofClass f = { toLinearMap := ↑f, monotone' := ⋯ }

@[deprecated PositiveLinearMap.ofClass (since := "2026-06-10")]

def PositiveLinearMapClass.toPositiveLinearMap {F : Type u_1} {R : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [FunLike F E₁ E₂] [LinearMapClass F R E₁ E₂] [OrderHomClass F E₁ E₂] (f : F) : E₁ →ₚ[R] E₂

Alias of PositiveLinearMap.ofClass.

---

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

Equations

• @PositiveLinearMapClass.toPositiveLinearMap = @PositiveLinearMap.ofClass

theorem OrderHomClass.of_addMonoidHom {F' : Type u_5} {E₁' : Type u_6} {E₂' : Type u_7} [FunLike F' E₁' E₂'] [AddGroup E₁'] [LE E₁'] [AddRightMono E₁'] [AddGroup E₂'] [LE E₂'] [AddRightMono E₂'] [AddMonoidHomClass F' E₁' E₂'] (h : ∀ (f : F') (x : E₁'), 0 ≤ x → 0 ≤ f x) : OrderHomClass F' E₁' E₂'

A type of additive group homomorphisms that map nonnegative elements to nonnegative elements is also a type of order homomorphisms.

@[implicit_reducible]

instance PositiveLinearMap.instFunLike {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] : FunLike (E₁ →ₚ[R] E₂) E₁ E₂

Equations

• PositiveLinearMap.instFunLike = { coe := fun (f : E₁ →ₚ[R] E₂) => f.toFun, coe_injective := ⋯ }

theorem PositiveLinearMap.ext {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] {f g : E₁ →ₚ[R] E₂} (h : ∀ (x : E₁), f x = g x) : f = g

theorem PositiveLinearMap.ext_iff {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] {f g : E₁ →ₚ[R] E₂} : f = g ↔ ∀ (x : E₁), f x = g x

def PositiveLinearMap.id (R : Type u_1) (E₁ : Type u_2) [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [Module R E₁] : E₁ →ₚ[R] E₁

The identity as a positive linear map.

Equations

• PositiveLinearMap.id R E₁ = { toLinearMap := LinearMap.id, monotone' := ⋯ }

@[simp]

theorem PositiveLinearMap.toLinearMap_id (R : Type u_1) (E₁ : Type u_2) [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [Module R E₁] : (PositiveLinearMap.id R E₁).toLinearMap = LinearMap.id

@[simp]

theorem PositiveLinearMap.id_apply (R : Type u_1) (E₁ : Type u_2) [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [Module R E₁] (x : E₁) : (PositiveLinearMap.id R E₁) x = x

@[simp]

theorem PositiveLinearMap.toOrderHom_id {R : Type u_1} {E₁ : Type u_2} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [Module R E₁] : (PositiveLinearMap.id R E₁).toOrderHom = OrderHom.id

def PositiveLinearMap.comp {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₁] [Module R E₂] [Module R E₃] (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) : E₁ →ₚ[R] E₃

The composition of positive linear maps is again a positive linear map.

Equations

• g.comp f = { toLinearMap := g.toLinearMap ∘ₗ f.toLinearMap, monotone' := ⋯ }

@[simp]

theorem PositiveLinearMap.comp_apply {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₁] [Module R E₂] [Module R E₃] (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) (x : E₁) : (g.comp f) x = g.toLinearMap (f.toLinearMap x)

@[simp]

theorem PositiveLinearMap.toLinearMap_comp {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₁] [Module R E₂] [Module R E₃] (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) : (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

@[simp]

theorem PositiveLinearMap.toOrderHom_comp {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [AddCommMonoid E₃] [PartialOrder E₃] [Module R E₁] [Module R E₂] [Module R E₃] (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) : (g.comp f).toOrderHom = g.toOrderHom.comp f.toOrderHom

@[simp]

theorem PositiveLinearMap.comp_id {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] (f : E₁ →ₚ[R] E₂) : f.comp (PositiveLinearMap.id R E₁) = f

@[simp]

theorem PositiveLinearMap.id_comp {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] (f : E₁ →ₚ[R] E₂) : (PositiveLinearMap.id R E₂).comp f = f

instance PositiveLinearMap.instLinearMapClass {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] : LinearMapClass (E₁ →ₚ[R] E₂) R E₁ E₂

instance PositiveLinearMap.instOrderHomClass {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] : OrderHomClass (E₁ →ₚ[R] E₂) E₁ E₂

@[simp]

theorem PositiveLinearMap.map_smul_of_tower {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] {S : Type u_5} [SMul S E₁] [SMul S E₂] [LinearMap.CompatibleSMul E₁ E₂ S R] (f : E₁ →ₚ[R] E₂) (c : S) (x : E₁) : f (c • x) = c • f x

theorem PositiveLinearMap.map_nonneg {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] (f : E₁ →ₚ[R] E₂) {x : E₁} (hx : 0 ≤ x) : 0 ≤ f x

@[simp]

theorem PositiveLinearMap.coe_toLinearMap {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] (f : E₁ →ₚ[R] E₂) : ⇑f.toLinearMap = ⇑f

theorem PositiveLinearMap.toLinearMap_injective {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] : Function.Injective toLinearMap

@[simp]

theorem PositiveLinearMap.toLinearMap_inj {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] {f g : E₁ →ₚ[R] E₂} : f.toLinearMap = g.toLinearMap ↔ f = g

@[implicit_reducible]

instance PositiveLinearMap.instZero {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] : Zero (E₁ →ₚ[R] E₂)

Equations

• PositiveLinearMap.instZero = { zero := { toLinearMap := 0, monotone' := ⋯ } }

@[simp]

theorem PositiveLinearMap.toLinearMap_zero {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] : toLinearMap 0 = 0

@[simp]

theorem PositiveLinearMap.zero_apply {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] (x : E₁) : 0 x = 0

@[implicit_reducible]

instance PositiveLinearMap.instAdd {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [IsOrderedAddMonoid E₂] : Add (E₁ →ₚ[R] E₂)

Equations

• PositiveLinearMap.instAdd = { add := fun (f g : E₁ →ₚ[R] E₂) => { toLinearMap := f.toLinearMap + g.toLinearMap, monotone' := ⋯ } }

@[simp]

theorem PositiveLinearMap.toLinearMap_add {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [IsOrderedAddMonoid E₂] (f g : E₁ →ₚ[R] E₂) : (f + g).toLinearMap = f.toLinearMap + g.toLinearMap

@[simp]

theorem PositiveLinearMap.add_apply {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [IsOrderedAddMonoid E₂] (f g : E₁ →ₚ[R] E₂) (x : E₁) : (f + g) x = f x + g x

@[implicit_reducible]

instance PositiveLinearMap.instSMulNat {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [IsOrderedAddMonoid E₂] : SMul ℕ (E₁ →ₚ[R] E₂)

Equations

• PositiveLinearMap.instSMulNat = { smul := fun (n : ℕ) (f : E₁ →ₚ[R] E₂) => { toLinearMap := n • f.toLinearMap, monotone' := ⋯ } }

@[simp]

theorem PositiveLinearMap.toLinearMap_nsmul {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [IsOrderedAddMonoid E₂] (f : E₁ →ₚ[R] E₂) (n : ℕ) : (n • f).toLinearMap = n • f.toLinearMap

@[simp]

theorem PositiveLinearMap.nsmul_apply {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [IsOrderedAddMonoid E₂] (f : E₁ →ₚ[R] E₂) (n : ℕ) (x : E₁) : (n • f) x = n • f x

@[implicit_reducible]

instance PositiveLinearMap.instAddCommMonoid {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] [Module R E₁] [Module R E₂] [IsOrderedAddMonoid E₂] : AddCommMonoid (E₁ →ₚ[R] E₂)

Equations

• PositiveLinearMap.instAddCommMonoid = Function.Injective.addCommMonoid PositiveLinearMap.toLinearMap ⋯ ⋯ ⋯ ⋯

def PositiveLinearMap.mk₀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [Semiring R] [AddCommGroup E₁] [PartialOrder E₁] [IsOrderedAddMonoid E₁] [AddCommGroup E₂] [PartialOrder E₂] [IsOrderedAddMonoid E₂] [Module R E₁] [Module R E₂] (f : E₁ →ₗ[R] E₂) (hf : ∀ (x : E₁), 0 ≤ x → 0 ≤ f x) : E₁ →ₚ[R] E₂

Define a positive map from a linear map that maps nonnegative elements to nonnegative elements

Equations

• PositiveLinearMap.mk₀ f hf = { toLinearMap := f, monotone' := ⋯ }