feat(algebra/star/basic): refactor star_ordered_ring to include add_submonoid.closure (#18854)

Per [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Star.20ordered.20ring), this refactors `star_ordered_ring` so that the condition `star_ordered_ring.nonneg_iff` is changed from `∀ r : R, 0 ≤ r ↔ ∃ s, r = star s * s` to something morally equivalent to `∀ x : R, 0 ≤ x ↔ x ∈ add_submonoid.closure (set.range (λ s : R, star s * s))`.

In fact, we actually change the structure field `nonneg_iff` to `le_iff`, which characterizes `· ≤ ·` instead of just `0 ≤ ·`. When `R` is a `non_unital_ring`, there is effectively no change (see how we recover `star_ordered_ring.nonneg_iff` and also `star_ordered_ring.of_nonneg_iff`), but it gives a more useful and sensible condition when `R` is only a `non_unital_semiring`. For instance, now `conjugate_le_conjugate` holds for `non_unital_semiring`. 

There are essentially two reasons for this change.
1. It would be nice if things like `ℚ` could be `star_ordered_ring`s. This is a minor reason, but it should be a nice convenience. This instance is added in this PR in a new file.
2. Much more importantly, we want to declare the positive elements in a `star_ordered_ring` as an `add_submonoid`, but to accomplish this with the previous definition requires much more stringent type class assumptions (e.g., C⋆-algebras) and sophisticated machinery (the continuous functional calculus) in order to show that the sum of positive elements is positive. This change essentially allows us to defer that proof obligation to the settings where it will matter that a positive element really does have the form `star s * s`.

We remark that even for C⋆-algebras, the fact that the sum of positive elements (i.e., those of the form `star s * s`) is positive is a deep result which was first shown in 1952 by [Fukamiya](http://www.sci.kumamoto-u.ac.jp/~kjm/BKS/kjmpdf/KJSM/v1-4-fukamiya.pdf), and then again in 1953 by [Kelley and Vaught](https://www.ams.org/journals/tran/1953-074-01/S0002-9947-1953-0054175-2/S0002-9947-1953-0054175-2.pdf). These proofs are in essence very similar, but the latter is more aesthetically pleasing, and it is this proof that appears in all the textbooks. I went looking and did not see another proof anywhere in the literature.

We provide a few convenience constructors for `star_ordered_ring` in the form of reducible definitions which can apply when `R` is either a `non_unital_ring` (so we only need to characterize nonnegativity), and / or when positive elements have exactly the form `star s * s`. In this way, we can effectively maintain the status quo (see the instances for `real` and `complex`).

Author: j-loreaux

docs/references.bib

@@ -1473,6 +1473,18 @@ @Book{            kechris1995
   url           = {https://doi.org/10.1007/978-1-4612-4190-4}
 }
 
+@Article{         kelleyVaught1953,
+  author        = {Kelley, J. L. and Vaught, R. L.},
+  title         = {The positive cone in {Banach} algebras},
+  journal       = {Trans. Am. Math. Soc.},
+  issn          = {0002-9947},
+  volume        = {74},
+  pages         = {44--55},
+  year          = {1953},
+  language      = {English},
+  doi           = {10.2307/1990847}
+}
+
 @Article{         kleiman1979,
   author        = {Kleiman, Steven Lawrence},
   title         = {Misconceptions about {$K\_X$}},

src/algebra/star/basic.lean

@@ -22,23 +22,12 @@ These are implemented as "mixin" typeclasses, so to summon a star ring (for exam
 one needs to write `(R : Type) [ring R] [star_ring R]`.
 This avoids difficulties with diamond inheritance.
 
-We also define the class `star_ordered_ring R`, which says that the order on `R` respects the
-star operation, i.e. an element `r` is nonnegative iff there exists an `s` such that
-`r = star s * s`.
-
 For now we simply do not introduce notations,
 as different users are expected to feel strongly about the relative merits of
 `r^*`, `r†`, `rᘁ`, and so on.
 
 Our star rings are actually star semirings, but of course we can prove
 `star_neg : star (-r) = - star r` when the underlying semiring is a ring.
-
-## TODO
-
-* In a Banach star algebra without a well-defined square root, the natural ordering is given by the
-positive cone which is the closure of the sums of elements `star r * r`. A weaker version of
-`star_ordered_ring` could be defined for this case. Note that the current definition has the
-advantage of not requiring a topology.
 -/
 
 assert_not_exists finset
@@ -365,62 +354,6 @@ def star_ring_of_comm {R : Type*} [comm_semiring R] : star_ring R :=
   star_add := λ x y, rfl,
   ..star_semigroup_of_comm }
 
-/--
-An ordered `*`-ring is a ring which is both an `ordered_add_comm_group` and a `*`-ring,
-and `0 ≤ r ↔ ∃ s, r = star s * s`.
--/
-class star_ordered_ring (R : Type u) [non_unital_semiring R] [partial_order R]
-  extends star_ring R :=
-(add_le_add_left       : ∀ a b : R, a ≤ b → ∀ c : R, c + a ≤ c + b)
-(nonneg_iff            : ∀ r : R, 0 ≤ r ↔ ∃ s, r = star s * s)
-
-namespace star_ordered_ring
-
-@[priority 100] -- see note [lower instance priority]
-instance [non_unital_ring R] [partial_order R] [star_ordered_ring R] : ordered_add_comm_group R :=
-{ ..show non_unital_ring R, by apply_instance,
-  ..show partial_order R, by apply_instance,
-  ..show star_ordered_ring R, by apply_instance }
-
-end star_ordered_ring
-
-section non_unital_semiring
-
-variables [non_unital_semiring R] [partial_order R] [star_ordered_ring R]
-
-lemma star_mul_self_nonneg {r : R} : 0 ≤ star r * r :=
-(star_ordered_ring.nonneg_iff _).mpr ⟨r, rfl⟩
-
-lemma star_mul_self_nonneg' {r : R} : 0 ≤ r * star r :=
-by { nth_rewrite_rhs 0 [←star_star r], exact star_mul_self_nonneg }
-
-lemma conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c :=
-begin
-  obtain ⟨x, rfl⟩ := (star_ordered_ring.nonneg_iff _).1 ha,
-  exact (star_ordered_ring.nonneg_iff _).2 ⟨x * c, by rw [star_mul, ←mul_assoc, mul_assoc _ _ c]⟩,
-end
-
-lemma conjugate_nonneg' {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c :=
-by simpa only [star_star] using conjugate_nonneg ha (star c)
-
-end non_unital_semiring
-
-section non_unital_ring
-
-variables [non_unital_ring R] [partial_order R] [star_ordered_ring R]
-
-lemma conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) : star c * a * c ≤ star c * b * c :=
-begin
-  rw ←sub_nonneg at hab ⊢,
-  convert conjugate_nonneg hab c,
-  simp only [mul_sub, sub_mul],
-end
-
-lemma conjugate_le_conjugate' {a b : R} (hab : a ≤ b) (c : R) : c * a * star c ≤ c * b * star c :=
-by simpa only [star_star] using conjugate_le_conjugate hab (star c)
-
-end non_unital_ring
-
 /--
 A star module `A` over a star ring `R` is a module which is a star add monoid,
 and the two star structures are compatible in the sense

src/algebra/star/chsh.lean

@@ -133,7 +133,7 @@ begin
         T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa, mul_comm B₀, mul_comm B₁], },
     rw idem',
     conv_rhs { congr, skip, congr, rw ←sa, },
-    convert smul_le_smul_of_nonneg (star_mul_self_nonneg : 0 ≤ star P * P) _,
+    convert smul_le_smul_of_nonneg (star_mul_self_nonneg P) _,
     { simp, },
     { apply_instance, },
     { norm_num, } },
@@ -221,11 +221,11 @@ begin
     have P2_nonneg : 0 ≤ P^2,
     { rw [sq],
       conv { congr, skip, congr, rw ←P_sa, },
-      convert (star_mul_self_nonneg : 0 ≤ star P * P), },
+      convert (star_mul_self_nonneg P), },
     have Q2_nonneg : 0 ≤ Q^2,
     { rw [sq],
       conv { congr, skip, congr, rw ←Q_sa, },
-      convert (star_mul_self_nonneg : 0 ≤ star Q * Q), },
+      convert (star_mul_self_nonneg Q), },
     convert smul_le_smul_of_nonneg (add_nonneg P2_nonneg Q2_nonneg)
       (le_of_lt (show 0 < √2⁻¹, by norm_num)), -- `norm_num` can't directly show `0 ≤ √2⁻¹`
     simp, },

src/algebra/star/order.lean

@@ -0,0 +1,179 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+
+import algebra.star.basic
+import group_theory.submonoid.basic
+
+/-! # Star ordered rings
+
+We define the class `star_ordered_ring R`, which says that the order on `R` respects the
+star operation, i.e. an element `r` is nonnegative iff it is in the `add_submonoid` generated by
+elements of the form `star s * s`. In many cases, including all C⋆-algebras, this can be reduced to
+`0 ≤ r ↔ ∃ s, r = star s * s`. However, this generality is slightly more convenient (e.g., it
+allows us to register a `star_ordered_ring` instance for `ℚ`), and more closely resembles the
+literature (see the seminal paper [*The positive cone in Banach algebras*][kelleyVaught1953])
+
+In order to accodomate `non_unital_semiring R`, we actually don't characterize nonnegativity, but
+rather the entire `≤` relation with `star_ordered_ring.le_iff`. However, notice that when `R` is a
+`non_unital_ring`, these are equivalent (see `star_ordered_ring.nonneg_iff` and
+`star_ordered_ring.of_nonneg_iff`).
+
+## TODO
+
+* In a Banach star algebra without a well-defined square root, the natural ordering is given by the
+positive cone which is the _closure_ of the sums of elements `star r * r`. A weaker version of
+`star_ordered_ring` could be defined for this case (again, see
+[*The positive cone in Banach algebras*][kelleyVaught1953]). Note that the current definition has
+the advantage of not requiring a topology.
+-/
+
+universe u
+variable {R : Type u}
+
+/--
+An ordered `*`-ring is a ring which is both an `ordered_add_comm_group` and a `*`-ring,
+and the nonnegative elements constitute precisely the `add_submonoid` generated by
+elements of the form `star s * s`.
+
+If you are working with a `non_unital_ring` and not a `non_unital_semiring`, it may be more
+convenient do declare instances using `star_ordered_ring.of_nonneg_iff'`. -/
+class star_ordered_ring (R : Type u) [non_unital_semiring R] [partial_order R]
+  extends star_ring R :=
+(add_le_add_left : ∀ a b : R, a ≤ b → ∀ c : R, c + a ≤ c + b)
+(le_iff          : ∀ x y : R,
+  x ≤ y ↔ ∃ p, p ∈ add_submonoid.closure (set.range $ λ s, star s * s) ∧ y = x + p)
+
+namespace star_ordered_ring
+
+@[priority 100] -- see note [lower instance priority]
+instance to_ordered_add_comm_monoid [non_unital_semiring R] [partial_order R]
+  [star_ordered_ring R] : ordered_add_comm_monoid R :=
+{ ..show non_unital_semiring R, by apply_instance,
+  ..show partial_order R, by apply_instance,
+  ..show star_ordered_ring R, by apply_instance }
+
+@[priority 100] -- see note [lower instance priority]
+instance to_has_exists_add_of_le [non_unital_semiring R] [partial_order R]
+  [star_ordered_ring R] : has_exists_add_of_le R :=
+{ exists_add_of_le := λ a b h, match (le_iff _ _).mp h with ⟨p, _, hp⟩ := ⟨p, hp⟩ end }
+
+@[priority 100] -- see note [lower instance priority]
+instance to_ordered_add_comm_group [non_unital_ring R] [partial_order R] [star_ordered_ring R] :
+  ordered_add_comm_group R :=
+{ ..show non_unital_ring R, by apply_instance,
+  ..show partial_order R, by apply_instance,
+  ..show star_ordered_ring R, by apply_instance }
+
+/-- To construct a `star_ordered_ring` instance it suffices to show that `x ≤ y` if and only if
+`y = x + star s * s` for some `s : R`.
+
+This is provided for convenience because it holds in some common scenarios (e.g.,`ℝ≥0`, `C(X, ℝ≥0)`)
+and obviates the hassle of `add_submonoid.closure_induction` when creating those instances.
+
+If you are working with a `non_unital_ring` and not a `non_unital_semiring`, see
+`star_ordered_ring.of_nonneg_iff` for a more convenient version. -/
+@[reducible] -- set note [reducible non-instances]
+def of_le_iff [non_unital_semiring R] [partial_order R] [star_ring R]
+  (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
+  (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) :
+  star_ordered_ring R :=
+{ add_le_add_left := @h_add,
+  le_iff := λ x y,
+  begin
+    refine ⟨λ h, _, _⟩,
+    { obtain ⟨p, hp⟩ := (h_le_iff x y).mp h,
+      exact ⟨star p * p, add_submonoid.subset_closure ⟨p, rfl⟩, hp⟩ },
+    { rintro ⟨p, hp, hpxy⟩,
+      revert x y hpxy,
+      refine add_submonoid.closure_induction hp _ (λ x y h, add_zero x ▸ h.ge) _,
+      { rintro _ ⟨s, rfl⟩ x y rfl,
+        nth_rewrite 0 [←add_zero x],
+        refine h_add _ x,
+        exact (h_le_iff _ _).mpr ⟨s, by rw [zero_add]⟩ },
+      { rintro a b ha hb x y rfl,
+        nth_rewrite 0 [←add_zero x],
+        refine h_add ((ha 0 _ (zero_add a).symm).trans (hb a _ rfl)) x } }
+  end,
+  .. ‹star_ring R› }
+
+/-- When `R` is a non-unital ring, to construct a `star_ordered_ring` instance it suffices to
+show that the nonnegative elements are precisely those elements in the `add_submonoid` generated
+by `star s * s` for `s : R`. -/
+@[reducible] -- set note [reducible non-instances]
+def of_nonneg_iff [non_unital_ring R] [partial_order R] [star_ring R]
+  (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
+  (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ x ∈ add_submonoid.closure (set.range $ λ s : R, star s * s)) :
+  star_ordered_ring R :=
+{ add_le_add_left := @h_add,
+  le_iff := λ x y,
+    begin
+      haveI : covariant_class R R (+) (≤) := ⟨λ _ _ _ h, h_add h _⟩,
+      simpa only [←sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x),
+    end,
+  .. ‹star_ring R› }
+
+/-- When `R` is a non-unital ring, to construct a `star_ordered_ring` instance it suffices to
+show that the nonnegative elements are precisely those elements of the form `star s * s`
+for `s : R`.
+
+This is provided for convenience because it holds in many common scenarios (e.g.,`ℝ`, `ℂ`, or
+any C⋆-algebra), and obviates the hassle of `add_submonoid.closure_induction` when creating those
+instances. -/
+@[reducible] -- set note [reducible non-instances]
+def of_nonneg_iff' [non_unital_ring R] [partial_order R] [star_ring R]
+  (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
+  (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ ∃ s, x = star s * s) :
+  star_ordered_ring R :=
+of_le_iff @h_add
+begin
+  haveI : covariant_class R R (+) (≤) := ⟨λ _ _ _ h, h_add h _⟩,
+  simpa [sub_eq_iff_eq_add', sub_nonneg] using λ x y, h_nonneg_iff (y - x),
+end
+
+lemma nonneg_iff [non_unital_semiring R] [partial_order R] [star_ordered_ring R]
+  {x : R} : 0 ≤ x ↔ x ∈ add_submonoid.closure (set.range $ λ s : R, star s * s) :=
+by simp only [le_iff, zero_add, exists_eq_right']
+
+end star_ordered_ring
+
+section non_unital_semiring
+
+variables [non_unital_semiring R] [partial_order R] [star_ordered_ring R]
+
+lemma star_mul_self_nonneg (r : R) : 0 ≤ star r * r :=
+star_ordered_ring.nonneg_iff.mpr $ add_submonoid.subset_closure ⟨r, rfl⟩
+
+lemma star_mul_self_nonneg' (r : R) : 0 ≤ r * star r :=
+by { nth_rewrite_rhs 0 [←star_star r], exact star_mul_self_nonneg (star r) }
+
+lemma conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c :=
+begin
+  rw star_ordered_ring.nonneg_iff at ha,
+  refine add_submonoid.closure_induction ha (λ x hx, _) (by rw [mul_zero, zero_mul])
+    (λ x y hx hy, _),
+  { obtain ⟨x, rfl⟩ := hx,
+    convert star_mul_self_nonneg (x * c) using 1,
+    rw [star_mul, ←mul_assoc, mul_assoc _ _ c] },
+  { calc 0 ≤ star c * x * c + 0 : by rw [add_zero]; exact hx
+     ...   ≤ star c * x * c + star c * y * c : star_ordered_ring.add_le_add_left _ _ hy _
+     ...   ≤ _ : by rw [mul_add, add_mul] }
+end
+
+lemma conjugate_nonneg' {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c :=
+by simpa only [star_star] using conjugate_nonneg ha (star c)
+
+lemma conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) : star c * a * c ≤ star c * b * c :=
+begin
+  rw [star_ordered_ring.le_iff] at hab ⊢,
+  obtain ⟨p, hp, rfl⟩ := hab,
+  simp_rw [←star_ordered_ring.nonneg_iff] at hp ⊢,
+  exact ⟨star c * p * c, conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩,
+end
+
+lemma conjugate_le_conjugate' {a b : R} (hab : a ≤ b) (c : R) : c * a * star c ≤ c * b * star c :=
+by simpa only [star_star] using conjugate_le_conjugate hab (star c)
+
+end non_unital_semiring

src/analysis/normed_space/star/continuous_functional_calculus.lean

@@ -100,7 +100,7 @@ begin
     rw [←spectrum.gelfand_transform_eq (star a' * a'), continuous_map.spectrum_eq_range],
     rintro - ⟨φ, rfl⟩,
     rw [gelfand_transform_apply_apply ℂ _ (star a' * a') φ, map_mul φ, map_star φ],
-    rw [complex.eq_coe_norm_of_nonneg star_mul_self_nonneg, ←map_star, ←map_mul],
+    rw [complex.eq_coe_norm_of_nonneg (star_mul_self_nonneg _), ←map_star, ←map_mul],
     exact ⟨complex.zero_le_real.2 (norm_nonneg _),
       complex.real_le_real.2 (alg_hom.norm_apply_le_self φ (star a' * a'))⟩, }
 end

src/data/complex/basic.lean

@@ -666,18 +666,19 @@ With `z ≤ w` iff `w - z` is real and nonnegative, `ℂ` is a star ordered ring
 (That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)
 -/
 protected def star_ordered_ring : star_ordered_ring ℂ :=
-{ nonneg_iff := λ r, by
-  { refine ⟨λ hr, ⟨real.sqrt r.re, _⟩, λ h, _⟩,
-    { have h₁ : 0 ≤ r.re := by { rw [le_def] at hr, exact hr.1 },
-      have h₂ : r.im = 0 := by { rw [le_def] at hr, exact hr.2.symm },
-      ext,
-      { simp only [of_real_im, star_def, of_real_re, sub_zero, conj_re, mul_re, mul_zero,
-                   ←real.sqrt_mul h₁ r.re, real.sqrt_mul_self h₁] },
-      { simp only [h₂, add_zero, of_real_im, star_def, zero_mul, conj_im,
-                   mul_im, mul_zero, neg_zero] } },
-    { obtain ⟨s, rfl⟩ := h,
-      simp only [←norm_sq_eq_conj_mul_self, norm_sq_nonneg, zero_le_real, star_def] } },
-  ..complex.strict_ordered_comm_ring }
+star_ordered_ring.of_nonneg_iff' (λ _ _, add_le_add_left) $ λ r,
+begin
+  refine ⟨λ hr, ⟨real.sqrt r.re, _⟩, λ h, _⟩,
+  { have h₁ : 0 ≤ r.re := by { rw [le_def] at hr, exact hr.1 },
+    have h₂ : r.im = 0 := by { rw [le_def] at hr, exact hr.2.symm },
+    ext,
+    { simp only [of_real_im, star_def, of_real_re, sub_zero, conj_re, mul_re, mul_zero,
+                 ←real.sqrt_mul h₁ r.re, real.sqrt_mul_self h₁] },
+    { simp only [h₂, add_zero, of_real_im, star_def, zero_mul, conj_im,
+                 mul_im, mul_zero, neg_zero] } },
+  { obtain ⟨s, rfl⟩ := h,
+    simp only [←norm_sq_eq_conj_mul_self, norm_sq_nonneg, zero_le_real, star_def] },
+end
 
 localized "attribute [instance] complex.star_ordered_ring" in complex_order