refactor(Algebra/Star/Order): Use NonUnitalStarRingHom in Algebra.Star.Order (#13089)

Refactor `Algebra.Star.Order` to use the new non-unital *-ring homomorphisms / isomorphisms introduced in #12924



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>

Author: mans0954

Mathlib/Algebra/Star/Order.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.Star.SelfAdjoint
+import Mathlib.Algebra.Star.StarRingHom
 import Mathlib.Algebra.Regular.Basic
 
 #align_import algebra.star.order from "leanprover-community/mathlib"@"31c24aa72e7b3e5ed97a8412470e904f82b81004"
@@ -50,7 +51,8 @@ convenient to declare instances using `StarOrderedRing.of_nonneg_iff`.
 
 Porting note: dropped an unneeded assumption
 `add_le_add_left : ∀ {x y}, x ≤ y → ∀ z, z + x ≤ z + y` -/
-class StarOrderedRing (R : Type u) [NonUnitalSemiring R] [PartialOrder R] [StarRing R] : Prop where
+class StarOrderedRing (R : Type u) [NonUnitalSemiring R] [PartialOrder R]
+    [StarRing R] : Prop where
   /-- characterization of the order in terms of the `StarRing` structure. -/
   le_iff :
     ∀ x y : R, x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
@@ -320,38 +322,34 @@ end StarModule
 
 section OrderClass
 
-variable {F R S : Type*} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
+variable {F R S : Type*} [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
+  [StarOrderedRing R]
 variable [NonUnitalSemiring S] [PartialOrder S] [StarRing S] [StarOrderedRing S]
 
 -- we prove this auxiliary lemma in order to avoid duplicating the proof twice below.
-lemma NonUnitalRingHom.map_le_map_of_map_star (f : R →ₙ+* S) (hf : ∀ r, f (star r) = star (f r))
-    {x y : R} (hxy : x ≤ y) : f x ≤ f y := by
+lemma NonUnitalStarRingHom.map_le_map_of_map_star (f : R →⋆ₙ+* S) {x y : R} (hxy : x ≤ y) :
+    f x ≤ f y := by
   rw [StarOrderedRing.le_iff] at hxy ⊢
   obtain ⟨p, hp, rfl⟩ := hxy
   refine ⟨f p, ?_, map_add f _ _⟩
   induction hp using AddSubmonoid.closure_induction'
+  have hf : ∀ r, f (star r) = star (f r) := map_star _
   all_goals aesop
 
-instance (priority := 100) StarRingHomClass.instOrderHomClass [FunLike F R S] [StarHomClass F R S]
-    [NonUnitalRingHomClass F R S] : OrderHomClass F R S where
-  map_rel f := (f : R →ₙ+* S).map_le_map_of_map_star (map_star f)
+instance (priority := 100) StarRingHomClass.instOrderHomClass [FunLike F R S]
+    [NonUnitalSemiring R] [StarRing R] [StarOrderedRing R] [NonUnitalSemiring S]
+    [StarRing S] [StarOrderedRing S] [NonUnitalRingHomClass F R S]
+    [NonUnitalStarRingHomClass F R S] : OrderHomClass F R S where
+  map_rel f := (f : R →⋆ₙ+* S).map_le_map_of_map_star
 
--- This doesn't require any module structure, but the only morphism we currently have bundling
--- `star` is `starAlgHom`. So we have to build the inverse morphism by hand.
-instance (priority := 100) StarRingHomClass.instOrderIsoClass [EquivLike F R S] [StarHomClass F R S]
-    [RingEquivClass F R S] : OrderIsoClass F R S where
+instance (priority := 100) StarRingEquivClass.instOrderIsoClass [EquivLike F R S]
+    [StarRingEquivClass F R S] : OrderIsoClass F R S where
   map_le_map_iff f x y := by
     refine ⟨fun h ↦ ?_, map_rel f⟩
-    let f_inv : S →ₙ+* R :=
-      { toFun := EquivLike.inv f
-        map_mul' := fun _ _ ↦ EmbeddingLike.injective f <| by simp
-        map_add' := fun _ _ ↦ EmbeddingLike.injective f <| by simp
-        map_zero' := EmbeddingLike.injective f <| by simp }
-    have f_inv_star (s : S) : f_inv (star s) = star (f_inv s) := EmbeddingLike.injective f <| by
-      simp only [map_star f, show ∀ s, f (f_inv s) = s from EquivLike.apply_inv_apply f]
+    let f_inv : S →⋆ₙ+* R := (f : R ≃⋆+* S).symm
     have f_inv_f (r : R) : f_inv (f r) = r := EquivLike.inv_apply_apply f r
     rw [← f_inv_f x, ← f_inv_f y]
-    exact f_inv.map_le_map_of_map_star f_inv_star h
+    exact NonUnitalStarRingHom.map_le_map_of_map_star f_inv h
 
 end OrderClass