Simplest extension theorems

We say that a nimber x is a group when the lower set Iio x is closed under addition. Likewise, we say that x is a ring when Iio x is closed under addition and multiplication, and we say that x is a field when it's closed under addition, multiplication, and division.

This file aims to prove the four parts of the simplest extension theorem:

• If x is not a group, then x can be written as y + z for some y, z < x.
• If x is a group but not a ring, then x can be written as y * z for some y, z < x.
• If x is a ring but not a field, then x can be written as y⁻¹ for some y < x.
• If x is a field that isn't algebraically complete, then x is the root of some polynomial with coefficients < x.

The proof follows Aaron Siegel's Combinatorial Games, pp. 440-444.

Todo

We are currently at 3/4.

Mathlib lemmas

Order lemmas

theorem le_of_forall_ne {α : Type u_1} [LinearOrder α] {x y : α} (h : ∀ z < x, z ≠ y) : x ≤ y

theorem lt_add_iff_lt_or_exists_lt {α : Type u_1} [Add α] [LinearOrder α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] {a b c : α} : a < b + c ↔ a < b ∨ ∃ d < c, a = b + d

theorem forall_lt_add {α : Type u_1} [Add α] [LinearOrder α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] {b c : α} {P : α → Prop} : (∀ a < b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ a < c, P (b + a)

theorem exists_lt_add {α : Type u_1} [Add α] [LinearOrder α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] {b c : α} {P : α → Prop} : (∃ a < b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ a < c, P (b + a)

theorem le_add_iff_lt_or_exists_le {α : Type u_1} [Add α] [LinearOrder α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] {a b c : α} : a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d

theorem forall_le_add {α : Type u_1} [Add α] [LinearOrder α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] {b c : α} {P : α → Prop} : (∀ a ≤ b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ a ≤ c, P (b + a)

theorem exists_le_add {α : Type u_1} [Add α] [LinearOrder α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] {b c : α} {P : α → Prop} : (∃ a ≤ b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ a ≤ c, P (b + a)

theorem Maximal.isGreatest {α : Type u_1} [LinearOrder α] {P : α → Prop} {x : α} (h : Maximal P x) : IsGreatest {y : α | P y} x

Ordinal lemmas

theorem Ordinal.div_two_opow_log {o : Ordinal.{u_1}} (ho : o ≠ 0) : o / 2 ^ log 2 o = 1

theorem Ordinal.two_opow_log_add {o : Ordinal.{u_1}} (ho : o ≠ 0) : 2 ^ log 2 o + o % 2 ^ log 2 o = o

theorem Ordinal.mul_two (o : Ordinal.{u_1}) : o * 2 = o + o

theorem Ordinal.lt_mul_iff {a b c : Ordinal.{u_1}} : a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

theorem Ordinal.forall_lt_mul {b c : Ordinal.{u_1}} {P : Ordinal.{u_1} → Prop} : (∀ a < b * c, P a) ↔ ∀ q < c, ∀ r < b, P (b * q + r)

theorem Ordinal.exists_lt_mul {b c : Ordinal.{u_1}} {P : Ordinal.{u_1} → Prop} : (∃ a < b * c, P a) ↔ ∃ q < c, ∃ r < b, P (b * q + r)

theorem Ordinal.mul_add_lt {a b c d : Ordinal.{u_1}} (h₁ : c < a) (h₂ : b < d) : a * b + c < a * d

theorem Ordinal.log_eq_zero' {b x : Ordinal.{u_1}} (hb : b ≤ 1) : log b x = 0

theorem Ordinal.log_eq_zero_iff {b x : Ordinal.{u_1}} : log b x = 0 ↔ b ≤ 1 ∨ x < b

instance Ordinal.instCanonicallyOrderedAdd_combinatorialGames : CanonicallyOrderedAdd Ordinal.{u_1}

theorem Ordinal.Principal.sSup {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} {s : Set Ordinal.{u_1}} (H : ∀ x ∈ s, Principal op x) : Principal op (sSup s)

theorem Ordinal.Principal.iSup {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} {ι : Sort u_2} {f : ι → Ordinal.{u_1}} (H : ∀ (i : ι), Principal op (f i)) : Principal op (⨆ (i : ι), f i)

Polynomial lemmas

@[simp]

theorem Polynomial.coeffs_nonempty_iff {R : Type u_1} [Semiring R] {p : Polynomial R} : p.coeffs.Nonempty ↔ p ≠ 0

theorem Polynomial.natDegree_eq_zero_iff {R : Type u_1} [Semiring R] {p : Polynomial R} : p.natDegree = 0 ↔ p = 0 ∨ p.degree = 0

theorem inv_eq_self_iff {α : Type u_1} [DivisionRing α] {a : α} : a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

theorem self_eq_inv_iff {α : Type u_1} [DivisionRing α] {a : α} : a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1

Groups

def Nimber.«term_+ₒ_» : Lean.TrailingParserDescr

Add two nimbers as ordinal numbers.

Equations

• Nimber.«term_+ₒ_» = Lean.ParserDescr.trailingNode `Nimber.«term_+ₒ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+ₒ") (Lean.ParserDescr.cat `term 66))

structure Nimber.IsGroup (x : Nimber) : Prop

A nimber x is a group when Iio x is closed under addition. Note that 0 is a group under this definition.

• add_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y + z < x

theorem Nimber.isGroup_iff (x : Nimber) : x.IsGroup ↔ ∀ ⦃y z : Nimber⦄, y < x → z < x → y + z < x

@[simp]

theorem Nimber.IsGroup.zero : IsGroup 0

@[simp]

theorem Nimber.IsGroup.one : IsGroup 1

theorem Nimber.IsGroup.of_le_one {x : Nimber} (h : x ≤ 1) : x.IsGroup

theorem Nimber.IsGroup.sSup {s : Set Nimber} (H : ∀ x ∈ s, x.IsGroup) : (sSup s).IsGroup

theorem Nimber.IsGroup.iSup {ι : Sort u_1} {f : ι → Nimber} (H : ∀ (i : ι), (f i).IsGroup) : (⨆ (i : ι), f i).IsGroup

theorem Nimber.IsGroup.le_add_self {x y : Nimber} (h : x.IsGroup) (hy : y < x) : x ≤ x + y

theorem Nimber.exists_add_of_not_isGroup {x : Nimber} (h : ¬x.IsGroup) : ∃ y < x, ∃ z < x, y + z = x

The first simplest extension theorem: if x is not a group, then x can be written as y + z for some y, z < x.

@[irreducible]

theorem Nimber.IsGroup.mul_add_eq_of_lt' {x y : Ordinal.{u_1}} (h : (of x).IsGroup) (hy : y < x) (z : Ordinal.{u_1}) : of (x * z + y) = of (x * z) + of y

A version of IsGroup.mul_add_eq_of_lt stated in terms of Ordinal.

theorem Nimber.IsGroup.mul_add_eq_of_lt {x y : Nimber} (h : x.IsGroup) (hy : y < x) (z : Ordinal.{u_1}) : of (val x * z + val y) = of (val x * z) + y

theorem Nimber.IsGroup.add_eq_of_lt {x y : Nimber} (h : x.IsGroup) (hy : y < x) : of (val x + val y) = x + y

theorem Nimber.IsGroup.add_eq_of_lt' {x y : Ordinal.{u_1}} (h : (of x).IsGroup) (hy : y < x) : x + y = val (of x + of y)

A version of IsGroup.add_eq_of_lt stated in terms of Ordinal.

@[irreducible]

theorem Nimber.IsGroup.two_opow (x : Ordinal.{u_1}) : (of (2 ^ x)).IsGroup

theorem Nimber.two_opow_log_add {o : Ordinal.{u_1}} (ho : o ≠ 0) : of (2 ^ Ordinal.log 2 o) + of (o % 2 ^ Ordinal.log 2 o) = of o

theorem Nimber.add_lt_of_log_eq {a b : Ordinal.{u_1}} (ha₀ : a ≠ 0) (hb₀ : b ≠ 0) (h : Ordinal.log 2 a = Ordinal.log 2 b) : of a + of b < of (2 ^ Ordinal.log 2 a)

theorem Nimber.exists_isGroup_add_lt {x : Nimber} (hx : x ≠ 0) : ∃ y ≤ x, y.IsGroup ∧ x + y < y

theorem Nimber.isGroup_iff_zero_or_mem_range_two_opow {x : Nimber} : x.IsGroup ↔ x = 0 ∨ x ∈ Set.range fun (y : Ordinal.{u_1}) => of (2 ^ y)

The nimbers that are groups are exactly 0 and the powers of 2.

theorem Nimber.isGroup_iff_zero_or_mem_range_two_opow' {x : Ordinal.{u_1}} : (of x).IsGroup ↔ x = 0 ∨ x ∈ Set.range fun (x : Ordinal.{u_1}) => 2 ^ x

A version of isGroup_iff_zero_or_mem_range_two_opow stated in terms of Ordinal.

Rings

def Nimber.«term_*ₒ_» : Lean.TrailingParserDescr

Multiply two nimbers as ordinal numbers.

Equations

• Nimber.«term_*ₒ_» = Lean.ParserDescr.trailingNode `Nimber.«term_*ₒ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*ₒ") (Lean.ParserDescr.cat `term 71))

structure Nimber.IsRing (x : Nimber) extends x.IsGroup : Prop

A nimber x is a ring when Iio x is closed under addition and multiplication. Note that 0 is a ring under this definition.

• add_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y + z < x
• mul_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y * z < x

theorem Nimber.isRing_iff (x : Nimber) : x.IsRing ↔ x.IsGroup ∧ ∀ ⦃y z : Nimber⦄, y < x → z < x → y * z < x

@[simp]

theorem Nimber.IsRing.zero : IsRing 0

@[simp]

theorem Nimber.IsRing.one : IsRing 1

theorem Nimber.IsRing.of_le_one {x : Nimber} (h : x ≤ 1) : x.IsRing

theorem Nimber.IsRing.sSup {s : Set Nimber} (H : ∀ x ∈ s, x.IsRing) : (sSup s).IsRing

theorem Nimber.IsRing.iSup {ι : Sort u_1} {f : ι → Nimber} (H : ∀ (i : ι), (f i).IsRing) : (⨆ (i : ι), f i).IsRing

theorem Nimber.exists_mul_of_not_isRing {x : Nimber} (h' : x.IsGroup) (h : ¬x.IsRing) : ∃ y < x, ∃ z < x, y * z = x

The second simplest extension theorem: if x is a group but not a ring, then x can be written as y * z for some y, z < x.

@[irreducible]

theorem Nimber.IsRing.mul_eq_of_lt' {x y z : Ordinal.{u_1}} (hx : (of x).IsRing) (hy : (of y).IsGroup) (hyx : y ≤ x) (hzy : z < y) (H : ∀ z < y, (of z)⁻¹ < of x) : x * z = val (of x * of z)

A version of IsRing.mul_eq_of_lt stated in terms of Ordinal.

theorem Nimber.IsRing.mul_eq_of_lt {x y z : Nimber} (hx : x.IsRing) (hy : y.IsGroup) (hyx : y ≤ x) (hzy : z < y) (H : ∀ z < y, z⁻¹ < x) : of (val x * val z) = x * z

Fields

structure Nimber.IsField (x : Nimber) extends x.IsRing : Prop

A nimber x is a field when Iio x is closed under addition, multiplication, and division. Note that 0 and 1 are fields under this definition.

For simplicity, the constructor takes a redundant y ≠ 0 assumption. The lemma IsField.inv_lt proves that this theorem applies when y = 0 as well.

• add_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y + z < x
• mul_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y * z < x
• inv_lt' ⦃y : Nimber⦄ (hy₀ : y ≠ 0) (hy : y < x) : y⁻¹ < x

theorem Nimber.isField_iff (x : Nimber) : x.IsField ↔ x.IsRing ∧ ∀ ⦃y : Nimber⦄, y ≠ 0 → y < x → y⁻¹ < x

theorem Nimber.IsField.inv_lt {x y : Nimber} (h : x.IsField) (hy : y < x) : y⁻¹ < x

@[simp]

theorem Nimber.IsField.zero : IsField 0

@[simp]

theorem Nimber.IsField.one : IsField 1

theorem Nimber.IsField.of_le_one {x : Nimber} (h : x ≤ 1) : x.IsField

theorem Nimber.IsField.div_lt {x y z : Nimber} (h : x.IsField) (hy : y < x) (hz : z < x) : y / z < x

theorem Nimber.IsField.mul_eq_of_lt {x y : Nimber} (h : x.IsField) (hyx : y < x) : of (val x * val y) = x * y

theorem Nimber.IsField.mul_eq_of_lt' {x y : Ordinal.{u_1}} (hx : (of x).IsField) (hyx : y < x) : x * y = val (of x * of y)

A version of IsField.mul_eq_of_lt stated in terms of Ordinal.

theorem Nimber.inv_lt_of_not_isField {x y : Nimber} (h' : x.IsRing) (h : ¬x.IsField) (hy : y < x⁻¹) : y⁻¹ < x

theorem Nimber.inv_le_of_not_isField {x y : Nimber} (h' : x.IsRing) (h : ¬x.IsField) (hy : y ≤ x⁻¹) : y⁻¹ ≤ x

theorem Nimber.inv_lt_self_of_not_isField {x : Nimber} (h' : x.IsRing) (h : ¬x.IsField) : x⁻¹ < x

The third simplest extension theorem: if x is a ring but not a field, then x can be written as y⁻¹ for some y < x. In simpler wording, x⁻¹ < x.

n-th degree closed fields

structure Nimber.IsNthDegreeClosed (n : ℕ) (x : Nimber) extends x.IsRing : Prop

A nimber x is n-th degree closed when IsRing x, and every non-constant polynomial in the nimbers with degree less or equal to n and coefficients less than x has a root that's less than x. Note that 0 and 1 are n-th degree closed under this definition.

We don't extend IsField x, as for 1 ≤ n, this predicate implies it.

For simplicity, the constructor takes a 0 < p.degree assumption. The theorem IsNthDegreeClosed.has_root proves that this theorem applies (vacuously) when p = 0 as well.

• add_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y + z < x
• mul_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y * z < x
• has_root' ⦃p : Polynomial Nimber⦄ (hp₀ : 0 < p.degree) (hpn : p.degree ≤ ↑n) (hp : ∀ (k : ℕ), p.coeff k < x) : ∃ r < x, p.IsRoot r

theorem Nimber.isNthDegreeClosed_iff (n : ℕ) (x : Nimber) : IsNthDegreeClosed n x ↔ x.IsRing ∧ ∀ ⦃p : Polynomial Nimber⦄, 0 < p.degree → p.degree ≤ ↑n → (∀ (k : ℕ), p.coeff k < x) → ∃ r < x, p.IsRoot r

theorem Nimber.IsNthDegreeClosed.has_root {n : ℕ} {x : Nimber} (h : IsNthDegreeClosed n x) {p : Polynomial Nimber} (hp₀ : p.degree ≠ 0) (hpn : p.degree ≤ ↑n) (hp : ∀ (k : ℕ), p.coeff k < x) : ∃ r < x, p.IsRoot r

theorem Nimber.IsNthDegreeClosed.le {m n : ℕ} {x : Nimber} (h : IsNthDegreeClosed n x) (hmn : m ≤ n) : IsNthDegreeClosed m x

@[simp]

theorem Nimber.IsNthDegreeClosed.zero (n : ℕ) : IsNthDegreeClosed n 0

@[simp]

theorem Nimber.IsNthDegreeClosed.one (n : ℕ) : IsNthDegreeClosed n 1

theorem Nimber.IsNthDegreeClosed.of_le_one (n : ℕ) {x : Nimber} (h : x ≤ 1) : IsNthDegreeClosed n x

theorem Nimber.IsNthDegreeClosed.sSup {n : ℕ} {s : Set Nimber} (H : ∀ x ∈ s, IsNthDegreeClosed n x) : IsNthDegreeClosed n (sSup s)

theorem Nimber.IsNthDegreeClosed.iSup {n : ℕ} {ι : Sort u_1} {f : ι → Nimber} (H : ∀ (i : ι), IsNthDegreeClosed n (f i)) : IsNthDegreeClosed n (⨆ (i : ι), f i)

theorem Nimber.IsNthDegreeClosed.ofMonic {n : ℕ} {x : Nimber} (h : x.IsField) (hp : ∀ (p : Polynomial Nimber), p.Monic → 0 < p.degree → p.degree ≤ ↑n → (∀ (k : ℕ), p.coeff k < x) → ∃ r < x, p.IsRoot r) : IsNthDegreeClosed n x

If x is a field, to prove it n-th degree closed, it suffices to check monic polynomials of degree less or equal to n.

@[simp]

theorem Nimber.isNthDegreeClosed_zero_iff_isRing {x : Nimber} : IsNthDegreeClosed 0 x ↔ x.IsRing

theorem Nimber.IsNthDegreeClosed.toIsField {n : ℕ} {x : Nimber} (h : IsNthDegreeClosed n x) (hn : 1 ≤ n) : x.IsField

@[simp]

theorem Nimber.isNthDegreeClosed_one_iff_isField {x : Nimber} : IsNthDegreeClosed 1 x ↔ x.IsField

theorem Nimber.IsField.sSup {s : Set Nimber} (H : ∀ x ∈ s, x.IsField) : (sSup s).IsField

theorem Nimber.IsField.iSup {ι : Sort u_1} {f : ι → Nimber} (H : ∀ (i : ι), (f i).IsField) : (⨆ (i : ι), f i).IsField

Algebraically closed fields

structure Nimber.IsAlgClosed (x : Nimber) extends x.IsRing : Prop

A nimber x is algebraically closed when IsRing x, and every non-constant polynomial in the nimbers with coefficients less than x has a root that's less than x. Note that 0 and 1 are algebraically closed under this definition.

For simplicity, the constructor takes a 0 < p.degree assumption. The theorem IsAlgClosed.has_root proves that this theorem applies (vacuously) when p = 0 as well.

• add_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y + z < x
• mul_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y * z < x
• has_root' ⦃p : Polynomial Nimber⦄ (hp₀ : 0 < p.degree) (hp : ∀ (k : ℕ), p.coeff k < x) : ∃ r < x, p.IsRoot r

theorem Nimber.isAlgClosed_iff (x : Nimber) : x.IsAlgClosed ↔ x.IsRing ∧ ∀ ⦃p : Polynomial Nimber⦄, 0 < p.degree → (∀ (k : ℕ), p.coeff k < x) → ∃ r < x, p.IsRoot r

theorem Nimber.IsAlgClosed.toIsNthDegreeClosed {x : Nimber} (h : x.IsAlgClosed) (n : ℕ) : IsNthDegreeClosed n x

theorem Nimber.IsAlgClosed.toIsField {x : Nimber} (h : x.IsAlgClosed) : x.IsField

theorem Nimber.isAlgClosed_iff_forall {x : Nimber} : x.IsAlgClosed ↔ ∀ (n : ℕ), IsNthDegreeClosed n x

theorem Nimber.IsAlgClosed.has_root {x : Nimber} (h : x.IsAlgClosed) {p : Polynomial Nimber} (hp₀ : p.degree ≠ 0) (hp : ∀ (n : ℕ), p.coeff n < x) : ∃ r < x, p.IsRoot r

@[simp]

theorem Nimber.IsAlgClosed.zero : IsAlgClosed 0

@[simp]

theorem Nimber.IsAlgClosed.one : IsAlgClosed 1

theorem Nimber.IsAlgClosed.sSup {s : Set Nimber} (H : ∀ x ∈ s, x.IsAlgClosed) : (sSup s).IsAlgClosed

theorem Nimber.IsAlgClosed.iSup {ι : Sort u_1} {f : ι → Nimber} (H : ∀ (i : ι), (f i).IsAlgClosed) : (⨆ (i : ι), f i).IsAlgClosed

theorem Nimber.IsAlgClosed.ofMonic {x : Nimber} (h : x.IsField) (hp : ∀ (p : Polynomial Nimber), p.Monic → 0 < p.degree → (∀ (k : ℕ), p.coeff k < x) → ∃ r < x, p.IsRoot r) : x.IsAlgClosed

If x is a field, to prove it algebraically closed, it suffices to check monic polynomials.