Sums of squares

We introduce a predicate for sums of squares in a ring.

Main declarations

• IsSumSq : R → Prop: for a type R with addition, multiplication and a zero, 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 and Subsemiring.sumSq R: respectively the submonoid or subsemiring of sums of squares in an additive monoid or semiring R with multiplication.

inductive IsSumSq {R : Type u_1} [Mul R] [Add R] [Zero R] : R → Prop

The property of being a sum of squares is defined inductively by: 0 : R is a sum of squares and if s : R is a sum of squares, then for all a : R, a * a + s is a sum of squares in R.

• zero {R : Type u_1} [Mul R] [Add R] [Zero R] : IsSumSq 0
• sq_add {R : Type u_1} [Mul R] [Add R] [Zero R] (a : R) {s : R} (hs : IsSumSq s) : IsSumSq (a * a + s)

theorem isSumSq_iff {R : Type u_1} [Mul R] [Add R] [Zero R] (a✝ : R) : IsSumSq a✝ ↔ a✝ = 0 ∨ ∃ (a : R) (s : R), IsSumSq s ∧ a✝ = a * a + s

theorem IsSumSq.rec' {R : Type u_1} [Mul R] [Add R] [Zero R] {motive : (s : R) → IsSumSq s → Prop} (zero : motive 0 ⋯) (sq_add : ∀ {x s : R} (hx : IsSquare x) (hs : IsSumSq s), motive s hs → motive (x + s) ⋯) {s : R} (h : IsSumSq s) : motive s h

Alternative induction scheme for IsSumSq which uses IsSquare.

theorem IsSumSq.add {R : Type u_1} [AddMonoid R] [Mul R] {s₁ s₂ : R} (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) : IsSumSq (s₁ + s₂)

In an additive monoid with multiplication, if s₁ and s₂ are sums of squares, then s₁ + s₂ is a sum of squares.

def AddSubmonoid.sumSq (T : Type u_2) [AddMonoid T] [Mul T] : AddSubmonoid T

In an additive monoid with multiplication R, AddSubmonoid.sumSq R is the submonoid of sums of squares in R.

Equations

• AddSubmonoid.sumSq T = { carrier := {s : T | IsSumSq s}, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem AddSubmonoid.coe_sumSq (T : Type u_2) [AddMonoid T] [Mul T] : ↑(sumSq T) = {s : T | IsSumSq s}

@[simp]

theorem AddSubmonoid.mem_sumSq {T : Type u_2} [AddMonoid T] [Mul T] {s : T} : s ∈ sumSq T ↔ IsSumSq s

@[simp]

theorem IsSumSq.mul_self {R : Type u_1} [AddZeroClass R] [Mul R] (a : R) : IsSumSq (a * a)

In an additive unital magma with multiplication, x * x is a sum of squares for all x.

theorem IsSquare.isSumSq {R : Type u_1} [AddZeroClass R] [Mul R] {x : R} (hx : IsSquare x) : IsSumSq x

In an additive unital magma with multiplication, squares are sums of squares (see Mathlib.Algebra.Group.Even).

@[simp]

theorem IsSumSq.one {R : Type u_1} [AddZeroClass R] [MulOneClass R] : IsSumSq 1

@[simp]

theorem AddSubmonoid.closure_isSquare {R : Type u_1} [AddMonoid R] [Mul R] : closure {x : R | IsSquare x} = sumSq R

In an additive monoid with multiplication R, the submonoid generated by the squares is the set of sums of squares in R.

theorem IsSumSq.sum {R : Type u_1} [AddCommMonoid R] [Mul R] {ι : Type u_2} {I : Finset ι} {s : ι → R} (hs : ∀ i ∈ I, IsSumSq (s i)) : IsSumSq (∑ i ∈ I, s i)

In an additive commutative monoid with multiplication, a finite sum of sums of squares is a sum of squares.

theorem IsSumSq.sum_isSquare {R : Type u_1} [AddCommMonoid R] [Mul R] {ι : Type u_2} (I : Finset ι) {x : ι → R} (hx : ∀ i ∈ I, IsSquare (x i)) : IsSumSq (∑ i ∈ I, x i)

In an additive commutative monoid with multiplication, ∑ i ∈ I, x i, where each x i is a square, is a sum of squares.

@[simp]

theorem IsSumSq.sum_mul_self {R : Type u_1} [AddCommMonoid R] [Mul R] {ι : Type u_2} (I : Finset ι) (a : ι → R) : IsSumSq (∑ i ∈ I, a i * a i)

In an additive commutative monoid with multiplication, ∑ i ∈ I, a i * a i is a sum of squares.

@[simp]

theorem IsSumSq.sum_sq {R : Type u_1} [CommSemiring R] {ι : Type u_2} (I : Finset ι) (a : ι → R) : IsSumSq (∑ i ∈ I, a i ^ 2)

def NonUnitalSubsemiring.sumSq (T : Type u_2) [NonUnitalCommSemiring T] : NonUnitalSubsemiring T

In a commutative (possibly non-unital) semiring R, NonUnitalSubsemiring.sumSq R is the (possibly non-unital) subsemiring of sums of squares in R.

Equations

• NonUnitalSubsemiring.sumSq T = (Subsemigroup.square T).nonUnitalSubsemiringClosure

@[simp]

theorem NonUnitalSubsemiring.sumSq_toAddSubmonoid {T : Type u_2} [NonUnitalCommSemiring T] : (sumSq T).toAddSubmonoid = AddSubmonoid.sumSq T

@[simp]

theorem NonUnitalSubsemiring.mem_sumSq {T : Type u_2} [NonUnitalCommSemiring T] {s : T} : s ∈ sumSq T ↔ IsSumSq s

@[simp]

theorem NonUnitalSubsemiring.coe_sumSq {T : Type u_2} [NonUnitalCommSemiring T] : ↑(sumSq T) = {s : T | IsSumSq s}

@[simp]

theorem NonUnitalSubsemiring.closure_isSquare {T : Type u_2} [NonUnitalCommSemiring T] : closure {x : T | IsSquare x} = sumSq T

@[simp]

theorem IsSumSq.natCast {R : Type u_2} [NonAssocSemiring R] (n : ℕ) : IsSumSq ↑n

@[simp]

theorem Nat.isSumSq (n : ℕ) : IsSumSq n

theorem IsSumSq.mul {R : Type u_1} [NonUnitalCommSemiring R] {s₁ s₂ : R} (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) : IsSumSq (s₁ * s₂)

In a commutative (possibly non-unital) semiring, if s₁ and s₂ are sums of squares, then s₁ * s₂ is a sum of squares.

def Subsemiring.sumSq (T : Type u_2) [CommSemiring T] : Subsemiring T

In a commutative semiring R, Subsemiring.sumSq R is the subsemiring of sums of squares in R.

Equations

• Subsemiring.sumSq T = { carrier := (NonUnitalSubsemiring.sumSq T).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Subsemiring.sumSq_toNonUnitalSubsemiring {T : Type u_2} [CommSemiring T] : (sumSq T).toNonUnitalSubsemiring = NonUnitalSubsemiring.sumSq T

@[simp]

theorem Subsemiring.mem_sumSq {T : Type u_2} [CommSemiring T] {s : T} : s ∈ sumSq T ↔ IsSumSq s

@[simp]

theorem Subsemiring.coe_sumSq {T : Type u_2} [CommSemiring T] : ↑(sumSq T) = {s : T | IsSumSq s}

@[simp]

theorem Subsemiring.closure_isSquare {T : Type u_2} [CommSemiring T] : closure {x : T | IsSquare x} = sumSq T

theorem IsSumSq.prod {R : Type u_1} [CommSemiring R] {ι : Type u_2} {I : Finset ι} {x : ι → R} (hx : ∀ i ∈ I, IsSumSq (x i)) : IsSumSq (∏ i ∈ I, x i)

In a commutative semiring, a finite product of sums of squares is a sum of squares.

theorem IsSumSq.nonneg {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {s : R} (hs : IsSumSq s) : 0 ≤ s

In a linearly ordered semiring with the property a ≤ b → ∃ c, a + c = b (e.g. ℕ), sums of squares are non-negative.