feat: clean up PositiveLinearMap and add API (leanprover-community#40492)

Among other things, this removes the coercion from the morphism class into the morphism type, and renames the underlying convenience constructor to `PositiveLinearMap.ofClass`.

Author: j-loreaux

Mathlib/Algebra/Order/Module/PositiveLinearMap.lean

@@ -38,24 +38,23 @@ add_decl_doc PositiveLinearMap.toOrderHom
 /-- Notation for a `PositiveLinearMap`. -/
 notation:25 E " →ₚ[" R:25 "] " F:0 => PositiveLinearMap R E F
 
-namespace PositiveLinearMapClass
+section PositiveLinearMapClass
 
 variable {F R E₁ E₂ : Type*} [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₂]
 
 /-- Reinterpret an element of a type of positive linear maps as a positive linear map. -/
-def toPositiveLinearMap (f : F) : E₁ →ₚ[R] E₂ :=
+def PositiveLinearMap.ofClass (f : F) : E₁ →ₚ[R] E₂ :=
   { (f : E₁ →ₗ[R] E₂), (f : E₁ →o E₂) with }
 
-/-- Reinterpret an element of a type of positive linear maps as a positive linear map. -/
-instance instCoeToLinearMap : CoeHead F (E₁ →ₚ[R] E₂) where
-  coe f := toPositiveLinearMap f
+@[deprecated (since := "2026-06-10")]
+alias PositiveLinearMapClass.toPositiveLinearMap := PositiveLinearMap.ofClass
 
-/-- An additive group homomorphism that maps nonnegative elements to nonnegative elements
-is an order homomorphism. -/
-lemma _root_.OrderHomClass.of_addMonoidHom {F' E₁' E₂' : Type*} [FunLike F' E₁' E₂'] [AddGroup E₁']
+/-- A type of additive group homomorphisms that map nonnegative elements to nonnegative elements
+is also a type of order homomorphisms. -/
+lemma OrderHomClass.of_addMonoidHom {F' E₁' E₂' : Type*} [FunLike F' E₁' E₂'] [AddGroup E₁']
     [LE E₁'] [AddRightMono E₁'] [AddGroup E₂'] [LE E₂'] [AddRightMono E₂']
     [AddMonoidHomClass F' E₁' E₂']
     (h : ∀ f : F', ∀ x, 0 ≤ x → 0 ≤ f x) : OrderHomClass F' E₁' E₂' where
@@ -67,9 +66,11 @@ namespace PositiveLinearMap
 
 section general
 
-variable {R E₁ E₂ : Type*} [Semiring R]
-  [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂]
-  [Module R E₁] [Module R E₂]
+variable {R E₁ E₂ E₃ : Type*} [Semiring R]
+    [AddCommMonoid E₁] [PartialOrder E₁]
+    [AddCommMonoid E₂] [PartialOrder E₂]
+    [AddCommMonoid E₃] [PartialOrder E₃]
+    [Module R E₁] [Module R E₂] [Module R E₃]
 
 instance : FunLike (E₁ →ₚ[R] E₂) E₁ E₂ where
   coe f := f.toFun
@@ -80,10 +81,33 @@ instance : FunLike (E₁ →ₚ[R] E₂) E₁ E₂ where
     apply DFunLike.coe_injective
     exact h
 
+initialize_simps_projections PositiveLinearMap (toFun → apply, as_prefix toLinearMap)
+
 @[ext]
 lemma ext {f g : E₁ →ₚ[R] E₂} (h : ∀ x, f x = g x) : f = g :=
   DFunLike.ext f g h
 
+variable (R E₁) in
+/-- The identity as a positive linear map. -/
+@[simps! apply toLinearMap] protected def id : E₁ →ₚ[R] E₁ where
+  __ := LinearMap.id
+  __ := OrderHom.id
+
+@[simp] lemma toOrderHom_id : (PositiveLinearMap.id R E₁).toOrderHom = .id := rfl
+
+/-- The composition of positive linear maps is again a positive linear map. -/
+@[simps! apply toLinearMap]
+def comp (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) : E₁ →ₚ[R] E₃ where
+  toLinearMap := g.toLinearMap.comp f.toLinearMap
+  monotone' := g.monotone'.comp f.monotone'
+
+@[simp] lemma toOrderHom_comp (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) :
+    (g.comp f).toOrderHom = g.toOrderHom.comp f.toOrderHom :=
+  rfl
+
+@[simp] lemma comp_id (f : E₁ →ₚ[R] E₂) : f.comp (.id R E₁) = f := rfl
+@[simp] lemma id_comp (f : E₁ →ₚ[R] E₂) : (PositiveLinearMap.id R E₂).comp f = f := rfl
+
 instance : LinearMapClass (E₁ →ₚ[R] E₂) R E₁ E₂ where
   map_add f := map_add f.toLinearMap
   map_smulₛₗ f := f.toLinearMap.map_smul'

Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean

@@ -130,7 +130,7 @@ instance {F : Type*} [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [Ord
     ContinuousLinearMapClass F ℂ A₁ A₂ where
   map_continuous f := by
     have hbound : ∃ C : ℝ, ∀ a, ‖f a‖ ≤ C * ‖a‖ := by
-      obtain ⟨C, h⟩ := exists_norm_apply_le (f : A₁ →ₚ[ℂ] A₂)
+      obtain ⟨C, h⟩ := exists_norm_apply_le (.ofClass f)
       exact ⟨C, h⟩
     exact (LinearMap.mkContinuousOfExistsBound (f : A₁ →ₗ[ℂ] A₂) hbound).continuous