feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings (#16094)

* Generalise definition of a semireal ring, as discussed at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Formally.20real.20fields
* Add facts about multiplicative structure of sums of squares -- preserved under multiplication, form a semiring, set of sums of squares is the semiring generated by the squares.
* Add some lemmas to simpset
* Update documentation

Deletions:
* `mem_sumSq_of_isSquare` (statement changed to `IsSquare.isSumSq`)

Author: artie2000

Mathlib/Algebra/Ring/Semireal/Defs.lean

@@ -1,15 +1,14 @@
 /-
 Copyright (c) 2024 Florent Schaffhauser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Florent Schaffhauser
+Authors: Florent Schaffhauser, Artie Khovanov
 -/
 import Mathlib.Algebra.Ring.SumsOfSquares
 
 /-!
 # Semireal rings
 
-A semireal ring is a non-trivial commutative ring (with unit) in which `-1` is *not* a
-sum of squares.
+A semireal ring is a commutative ring (with unit) in which `-1` is *not* a sum of squares.
 
 For instance, linearly ordered rings are semireal, because sums of squares are positive and `-1` is
 not.
@@ -24,22 +23,31 @@ not.
 [lam_1984](https://doi.org/10.1216/RMJ-1984-14-4-767)
 -/
 
-variable (R : Type*)
+variable {R : Type*}
 
+variable (R) in
 /--
-A semireal ring is a non-trivial commutative ring (with unit) in which `-1` is *not* a sum of
-squares. We define the class `IsSemireal R`
-for all additive monoids `R` equipped with a multiplication, a multiplicative unit and a negation.
+A semireal ring is a commutative ring (with unit) in which `-1` is *not* a sum of
+squares. We define the predicate `IsSemireal R` for structures `R` equipped with
+a multiplication, an addition, a multiplicative unit and an additive unit.
 -/
 @[mk_iff]
-class IsSemireal [AddMonoid R] [Mul R] [One R] [Neg R] : Prop where
-  non_trivial         : (0 : R) ≠ 1
-  not_isSumSq_neg_one : ¬IsSumSq (-1 : R)
+class IsSemireal [Add R] [Mul R] [One R] [Zero R] : Prop where
+  one_add_ne_zero {s : R} (hs : IsSumSq s) : 1 + s ≠ 0
 
 @[deprecated (since := "2024-08-09")] alias isSemireal := IsSemireal
+
+/-- In a semireal ring, `-1` is not a sum of squares. -/
+theorem IsSemireal.not_isSumSq_neg_one [AddGroup R] [One R] [Mul R] [IsSemireal R]:
+    ¬ IsSumSq (-1 : R) := (by simpa using one_add_ne_zero ·)
+
 @[deprecated (since := "2024-08-09")] alias isSemireal.neg_one_not_SumSq :=
   IsSemireal.not_isSumSq_neg_one
 
-instance [LinearOrderedRing R] : IsSemireal R where
-  non_trivial := zero_ne_one
-  not_isSumSq_neg_one := fun h ↦ (not_le (α := R)).2 neg_one_lt_zero h.nonneg
+/--
+Linearly ordered semirings with the property `a ≤ b → ∃ c, a + c = b` (e.g. `ℕ`)
+are semireal.
+-/
+instance [LinearOrderedSemiring R] [ExistsAddOfLE R] : IsSemireal R where
+  one_add_ne_zero hs amo := zero_ne_one' R (le_antisymm zero_le_one
+                              (le_of_le_of_eq (le_add_of_nonneg_right hs.nonneg) amo))

Mathlib/Algebra/Ring/SumsOfSquares.lean

@@ -1,12 +1,12 @@
 /-
 Copyright (c) 2024 Florent Schaffhauser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Florent Schaffhauser
+Authors: Florent Schaffhauser, Artie Khovanov
 -/
-import Mathlib.Algebra.BigOperators.Group.Finset.Basic
-import Mathlib.Algebra.Group.Submonoid.Basic
-import Mathlib.Algebra.Order.Ring.Defs
-
+import Mathlib.Algebra.Group.Subgroup.Even
+import Mathlib.Algebra.Order.Ring.Basic
+import Mathlib.Algebra.Ring.Subsemiring.Basic
+import Mathlib.Tactic.ApplyFun
 /-!
 # Sums of squares
 
@@ -18,7 +18,8 @@ We introduce a predicate for sums of squares in a ring.
   an inductive predicate defining the property of being a sum of squares in `R`.
   `0 : R` is a sum of squares and if `S` is a sum of squares, then, for all `a : R`,
   `a * a + s` is a sum of squares.
-- `AddMonoid.sumSq R`: the submonoid of sums of squares in an additive monoid `R`
+- `AddMonoid.sumSq R` and `Subsemiring.sumSq R`: respectively
+  the submonoid or subsemiring of sums of squares in an additive monoid or semiring `R`
   with multiplication.
 
 -/
@@ -37,6 +38,17 @@ inductive IsSumSq [Mul R] [Add R] [Zero R] : R → Prop
 
 @[deprecated (since := "2024-08-09")] alias isSumSq := IsSumSq
 
+/-- Alternative induction scheme for `IsSumSq` which uses `IsSquare`. -/
+theorem IsSumSq.rec' [Mul R] [Add R] [Zero R]
+    {motive : (s : R) → (h : IsSumSq s) → Prop}
+    (zero : motive 0 zero)
+    (sq_add : ∀ {x s}, (hx : IsSquare x) → (hs : IsSumSq s) → motive s hs →
+      motive (x + s) (by rcases hx with ⟨_, rfl⟩; exact sq_add _ hs))
+    {s : R} (h : IsSumSq s) : motive s h :=
+  match h with
+  | .zero        => zero
+  | .sq_add _ hs => sq_add (.mul_self _) hs (rec' zero sq_add _)
+
 /--
 In an additive monoid with multiplication,
 if `s₁` and `s₂` are sums of squares, then `s₁ + s₂` is a sum of squares.
@@ -71,50 +83,133 @@ end AddSubmonoid
 @[deprecated (since := "2025-01-03")] alias sumSqIn := AddSubmonoid.sumSq
 @[deprecated (since := "2025-01-06")] alias sumSq := AddSubmonoid.sumSq
 
+/-- In an additive unital magma with multiplication, `x * x` is a sum of squares for all `x`. -/
+@[simp] theorem IsSumSq.mul_self [AddZeroClass R] [Mul R] (a : R) : IsSumSq (a * a) := by
+  simpa using sq_add a zero
+
 /--
-In an additive monoid with multiplication, squares are sums of squares
+In an additive unital magma with multiplication, squares are sums of squares
 (see Mathlib.Algebra.Group.Even).
 -/
-theorem mem_sumSq_of_isSquare [AddMonoid R] [Mul R] {x : R} (hx : IsSquare x) :
-    x ∈ AddSubmonoid.sumSq R := by
-  rcases hx with ⟨y, hy⟩
-  rw [hy, ← AddMonoid.add_zero (y * y)]
-  exact IsSumSq.sq_add _ IsSumSq.zero
-
-@[deprecated (since := "2024-08-09")] alias SquaresInSumSq := mem_sumSq_of_isSquare
-@[deprecated (since := "2025-01-03")] alias mem_sumSqIn_of_isSquare := mem_sumSq_of_isSquare
+theorem IsSquare.isSumSq [AddZeroClass R] [Mul R] {x : R} (hx : IsSquare x) :
+    IsSumSq x := by rcases hx with ⟨_, rfl⟩; apply IsSumSq.mul_self
 
 /--
 In an additive monoid with multiplication `R`, the submonoid generated by the squares is the set of
 sums of squares in `R`.
 -/
+@[simp]
 theorem AddSubmonoid.closure_isSquare [AddMonoid R] [Mul R] :
     closure {x : R | IsSquare x} = sumSq R := by
-  refine le_antisymm (closure_le.2 (fun x hx ↦ mem_sumSq_of_isSquare hx)) (fun x hx ↦ ?_)
-  induction hx <;> aesop
+  refine closure_eq_of_le (fun x hx ↦ IsSquare.isSumSq hx) (fun x hx ↦ ?_)
+  induction hx with
+  | zero => apply zero_mem
+  | sq_add a hs ih => exact add_mem (subset_closure (IsSquare.mul_self a)) ih
 
 @[deprecated (since := "2024-08-09")] alias SquaresAddClosure := AddSubmonoid.closure_isSquare
 
+/--
+In an additive commutative monoid with multiplication, a finite sum of sums of squares
+is a sum of squares.
+-/
+theorem IsSumSq.sum [AddCommMonoid R] [Mul R] {ι : Type*} {I : Finset ι} {s : ι → R}
+    (hs : ∀ i ∈ I, IsSumSq <| s i) : IsSumSq (∑ i ∈ I, s i) := by
+  simpa using sum_mem (S := AddSubmonoid.sumSq _) hs
+
+/--
+In an additive commutative monoid with multiplication,
+`∑ i ∈ I, x i`, where each `x i` is a square, is a sum of squares.
+-/
+theorem IsSumSq.sum_isSquare [AddCommMonoid R] [Mul R] {ι : Type*} (I : Finset ι) {x : ι → R}
+    (hx : ∀ i ∈ I, IsSquare <| x i) : IsSumSq (∑ i ∈ I, x i) :=
+  .sum fun _ hi => IsSquare.isSumSq (hx _ hi)
+
 /--
 In an additive commutative monoid with multiplication,
 `∑ i ∈ I, a i * a i` is a sum of squares.
 -/
+@[simp]
 theorem IsSumSq.sum_mul_self [AddCommMonoid R] [Mul R] {ι : Type*} (I : Finset ι) (a : ι → R) :
-    IsSumSq (∑ i ∈ I, a i * a i) := by
-  induction I using Finset.cons_induction with
-  | empty         => simpa using IsSumSq.zero
-  | cons i _ hi h => exact (Finset.sum_cons (β := R) hi) ▸ IsSumSq.sq_add (a i) h
+    IsSumSq (∑ i ∈ I, a i * a i) := .sum fun _ _ => .mul_self _
 
 @[deprecated (since := "2024-12-27")] alias isSumSq_sum_mul_self := IsSumSq.sum_mul_self
 
+namespace NonUnitalSubsemiring
+variable {T : Type*} [NonUnitalCommSemiring T]
+
+variable (T) in
+/--
+In a commutative (possibly non-unital) semiring `R`, `NonUnitalSubsemiring.sumSq R` is
+the (possibly non-unital) subsemiring of sums of squares in `R`.
+-/
+def sumSq : NonUnitalSubsemiring T := (Subsemigroup.square T).nonUnitalSubsemiringClosure
+
+@[simp] theorem sumSq_toAddSubmonoid : (sumSq T).toAddSubmonoid = .sumSq T := by
+  simp [sumSq, ← AddSubmonoid.closure_isSquare,
+    Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid]
+
+@[simp]
+theorem mem_sumSq {s : T} : s ∈ sumSq T ↔ IsSumSq s := by
+  simp [← NonUnitalSubsemiring.mem_toAddSubmonoid]
+
+@[simp, norm_cast] theorem coe_sumSq : sumSq T = {s : T | IsSumSq s} := by ext; simp
+
+@[simp] theorem closure_isSquare : closure {x : T | IsSquare x} = sumSq T := by
+  simp [sumSq, Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]
+
+end NonUnitalSubsemiring
+
+/--
+In a commutative (possibly non-unital) semiring,
+if `s₁` and `s₂` are sums of squares, then `s₁ * s₂` is a sum of squares.
+-/
+theorem IsSumSq.mul [NonUnitalCommSemiring R] {s₁ s₂ : R}
+    (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) : IsSumSq (s₁ * s₂) := by
+  simpa using mul_mem (by simpa : _ ∈ NonUnitalSubsemiring.sumSq R) (by simpa)
+
+private theorem Submonoid.square_subsemiringClosure {T : Type*} [CommSemiring T] :
+    (Submonoid.square T).subsemiringClosure = .closure {x : T | IsSquare x} := by
+  simp [Submonoid.subsemiringClosure_eq_closure]
+
+namespace Subsemiring
+variable {T : Type*} [CommSemiring T]
+
+variable (T) in
+/--
+In a commutative semiring `R`, `Subsemiring.sumSq R` is the subsemiring of sums of squares in `R`.
+-/
+def sumSq : Subsemiring T where
+  __ := NonUnitalSubsemiring.sumSq T
+  one_mem' := by simpa using IsSquare.one.isSumSq
+
+@[simp] theorem sumSq_toNonUnitalSubsemiring :
+    (sumSq T).toNonUnitalSubsemiring = .sumSq T := rfl
+
+@[simp]
+theorem mem_sumSq {s : T} : s ∈ sumSq T ↔ IsSumSq s := by
+  simp [← Subsemiring.mem_toNonUnitalSubsemiring]
+
+@[simp, norm_cast] theorem coe_sumSq : sumSq T = {s : T | IsSumSq s} := by ext; simp
+
+@[simp] theorem closure_isSquare : closure {x : T | IsSquare x} = sumSq T := by
+  apply_fun toNonUnitalSubsemiring using toNonUnitalSubsemiring_injective
+  simp [← Submonoid.square_subsemiringClosure]
+
+end Subsemiring
+
+/-- In a commutative semiring, a finite product of sums of squares is a sum of squares. -/
+theorem IsSumSq.prod [CommSemiring R] {ι : Type*} {I : Finset ι} {x : ι → R}
+    (hx : ∀ i ∈ I, IsSumSq <| x i) : IsSumSq (∏ i ∈ I, x i) := by
+  simpa using prod_mem (S := Subsemiring.sumSq R) (by simpa)
+
 /--
 In a linearly ordered semiring with the property `a ≤ b → ∃ c, a + c = b` (e.g. `ℕ`),
 sums of squares are non-negative.
 -/
 theorem IsSumSq.nonneg {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] {s : R}
     (hs : IsSumSq s) : 0 ≤ s := by
-  induction hs with
-  | zero           => simp only [le_refl]
-  | sq_add x _ ih  => apply add_nonneg ?_ ih; simp only [← pow_two x, sq_nonneg]
+  induction hs using IsSumSq.rec' with
+  | zero          => simp
+  | sq_add hx _ h => exact add_nonneg (IsSquare.nonneg hx) h
 
 @[deprecated (since := "2024-08-09")] alias isSumSq.nonneg := IsSumSq.nonneg