Formally real rings

A ring R is formally real if, whenever ∑ i, x i ^ 2 = 0, in fact x i = 0 for all i.

We define formally real rings in an index-free manner using the inductive predicate IsSumNonzeroSq, which asserts that an element is a finite sum of squares of nonzero elements. A ring is then formally real if ¬ IsSumNonzeroSq 0.

Main declaration

• IsFormallyReal: typeclass stating that a ring is formally real.

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

The property of being a sum of squares of nonzero elements (S) is defined inductively by: a * a : R is (S) for all nonzero a, and if s : R is (S), and a ≠ 0, then a * a + s is (S).

• sq {R : Type u_1} [Mul R] [Add R] [Zero R] {a : R} (ha : a ≠ 0) : IsSumNonzeroSq (a * a)
• sq_add {R : Type u_1} [Mul R] [Add R] [Zero R] {a s : R} (ha : a ≠ 0) (hs : IsSumNonzeroSq s) : IsSumNonzeroSq (a * a + s)

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

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

theorem IsSumNonzeroSq.isSumSq {R : Type u_1} [AddMonoid R] [Mul R] {s : R} (h : IsSumNonzeroSq s) : IsSumSq s

theorem isSumNonzeroSq_iff_isSumSq {R : Type u_1} [NonUnitalNonAssocSemiring R] {s : R} (hs : s ≠ 0) : IsSumNonzeroSq s ↔ IsSumSq s

theorem IsSumSq.isSumNonzeroSq_of_ne_zero {R : Type u_1} [NonUnitalNonAssocSemiring R] {s : R} (hs : s ≠ 0) : IsSumSq s → IsSumNonzeroSq s

Alias of the reverse direction of isSumNonzeroSq_iff_isSumSq.

def AddSubsemigroup.sumNonzeroSq (R : Type u_1) [AddMonoid R] [Mul R] : AddSubsemigroup R

The subsemigroup of sums of squares of nonzero elements.

@[simp]

theorem AddSubsemigroup.coe_sumNonzeroSq (R : Type u_1) [AddMonoid R] [Mul R] : ↑(sumNonzeroSq R) = {s : R | IsSumNonzeroSq s}

@[simp]

theorem AddSubsemigroup.mem_sumNonzeroSq {R : Type u_1} [AddMonoid R] [Mul R] {s : R} : s ∈ sumNonzeroSq R ↔ IsSumNonzeroSq s

@[simp]

theorem AddSubsemigroup.closure_mul_self {R : Type u_1} [AddMonoid R] [Mul R] : closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x} = sumNonzeroSq R

class IsFormallyReal (R : Type u_1) [AddCommMonoid R] [Mul R] : Prop

A ring is formally real if, whenever ∑ i, x i ^ 2 = 0, we in fact have x i = 0 for all i.

• not_isSumNonzeroSq_zero : ¬IsSumNonzeroSq 0

theorem IsFormallyReal.of_eq_zero_of_mul_self_of_eq_zero_of_add {R : Type u_1} [AddCommMonoid R] [Mul R] (hz : ∀ {a : R}, a * a = 0 → a = 0) (ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0) : IsFormallyReal R

theorem IsFormallyReal.of_eq_zero_of_eq_zero_of_mul_self_add {R : Type u_1} [NonUnitalNonAssocSemiring R] (h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0) : IsFormallyReal R

instance IsFormallyReal.instOfIsStrictOrderedRing {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] : IsFormallyReal R

instance IsFormallyReal.instIsReduced {R : Type u_1} [Ring R] [IsFormallyReal R] : IsReduced R

theorem IsFormallyReal.eq_zero_of_add_right {R : Type u_1} [NonUnitalNonAssocSemiring R] [IsFormallyReal R] {s₁ s₂ : R} (hs₁ : IsSumSq s₁) (hs₂ : IsSumSq s₂) (h : s₁ + s₂ = 0) : s₁ = 0

theorem IsFormallyReal.eq_zero_of_add_left {R : Type u_1} [NonUnitalNonAssocSemiring R] [IsFormallyReal R] {s₁ s₂ : R} (hs₁ : IsSumSq s₁) (hs₂ : IsSumSq s₂) (h : s₁ + s₂ = 0) : s₂ = 0

theorem IsFormallyReal.eq_zero_of_isSumSq_of_neg_isSumSq {R : Type u_1} [NonUnitalNonAssocRing R] [IsFormallyReal R] {s : R} (h₁ : IsSumSq s) (h₂ : IsSumSq (-s)) : s = 0