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.

The simplest extension theorem states:

• 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 closed, then x is the root of some polynomial with coefficients < x.

This file proves the first 3/4 parts of the theorem. The last part will be proven in CombinatorialGames.Nimber.SimplestExtension.Algebraic.

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

Mathlib lemmas

Order lemmas

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

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 nonzero nimber x is a group when Iio x is closed under addition.

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

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

theorem Nimber.IsGroup.neZero {x : Nimber} (h : x.IsGroup) : NeZero x

theorem Nimber.IsGroup.zero_lt {x : Nimber} (h : x.IsGroup) : 0 < x

theorem Nimber.IsGroup.pos {x : Nimber} (h : x.IsGroup) : 0 < x

Alias of Nimber.IsGroup.zero_lt.

theorem Nimber.IsGroup.sum_lt {x : Nimber} (h : x.IsGroup) {ι : Type u_2} {s : Finset ι} {f : ι → Nimber} (hs : ∀ y ∈ s, f y < x) : s.sum f < x

def Nimber.IsGroup.toAddSubgroup {x : Nimber} (h : x.IsGroup) : AddSubgroup Nimber

Iio x as a subgroup of Nimber.

Equations

• h.toAddSubgroup = { carrier := Set.Iio x, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Nimber.val_toAddSubgroup_lt {x : Nimber} (h : x.IsGroup) (y : ↥h.toAddSubgroup) : ↑y < x

@[simp]

theorem Nimber.mem_toAddSubgroup_iff {x y : Nimber} (h : x.IsGroup) : y ∈ h.toAddSubgroup ↔ y < x

theorem Nimber.IsGroup.closure_Iio {x : Nimber} (h : x.IsGroup) : AddSubgroup.closure (Set.Iio x) = h.toAddSubgroup

@[simp]

theorem Nimber.IsGroup.one : IsGroup 1

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

theorem Nimber.IsGroup.iSup {ι : Sort u_1} [Nonempty ι] {f : ι → Nimber} (H : ∀ (i : ι), (f i).IsGroup) (bdd : BddAbove (Set.range f) := by apply Nimber.bddAbove_of_small) : (⨆ (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) (ne : x ≠ 0) : ∃ y < x, ∃ z < x, y + z = x

The first simplest extension theorem: if x ≠ 0 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.

@[simp, irreducible]

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

@[simp]

theorem Nimber.IsGroup.two : (of 2).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_mem_range_two_opow {x : Nimber} : x.IsGroup ↔ x ∈ Set.range fun (y : Ordinal.{u_1}) => of (2 ^ y)

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

theorem Nimber.isGroup_iff_zero_or_mem_range_two_opow' {x : Ordinal.{u_1}} : (of x).IsGroup ↔ 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.

theorem Nimber.IsGroup.opow {x : Nimber} (h : x.IsGroup) (a : Ordinal.{u_1}) : (of (val x ^ a)).IsGroup

theorem Nimber.IsGroup.pow {x : Nimber} (h : x.IsGroup) (n : ℕ) : (of (val x ^ n)).IsGroup

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 1 < x and Iio x is closed under addition and multiplication.

• add_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y + z < x
• ne_zero : x ≠ 0
• mul_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y * z < x
• ne_one : x ≠ 1

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

theorem Nimber.IsRing.one_lt {x : Nimber} (h : x.IsRing) : 1 < x

theorem Nimber.IsRing.pow_lt {x y : Nimber} (h : x.IsRing) {n : ℕ} (hy : y < x) : y ^ n < x

@[simp]

theorem Nimber.IsRing.two : (of 2).IsRing

def Nimber.IsRing.toSubring {x : Nimber} (h : x.IsRing) : Subring Nimber

Iio x as a subring of Nimber.

Equations

• h.toSubring = { carrier := ⋯.toAddSubgroup.carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Nimber.val_toSubring_lt {x : Nimber} (h : x.IsRing) (y : ↥h.toSubring) : ↑y < x

@[simp]

theorem Nimber.mem_toSubring_iff {x y : Nimber} (h : x.IsRing) : y ∈ h.toSubring ↔ y < x

theorem Nimber.IsRing.closure_Iio {x : Nimber} (h : x.IsRing) : Subring.closure (Set.Iio x) = h.toSubring

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

theorem Nimber.IsRing.iSup {ι : Sort u_1} [Nonempty ι] {f : ι → Nimber} (H : ∀ (i : ι), (f i).IsRing) (bdd : BddAbove (Set.range f) := by apply Nimber.bddAbove_of_small) : (⨆ (i : ι), f i).IsRing

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

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

@[irreducible]

theorem Nimber.IsGroup.mul_eq_of_lt' {x y z w : Ordinal.{u_1}} (hx : (of x).IsGroup) (hy : (of y).IsGroup) (hw : (of w).IsGroup) (hyx : y ≤ x) (hzy : z < y) (hyw : y ≤ w) (H : ∀ z < y, (of z)⁻¹ < of w) (H' : ∀ ⦃a b : Ordinal.{u_1}⦄, a < x → b < w → of a * of b < of x) : x * z = val (of x * of z)

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

theorem Nimber.IsGroup.mul_eq_of_lt {x y z w : Nimber} (hx : x.IsGroup) (hy : y.IsGroup) (hw : w.IsGroup) (hyx : y ≤ x) (hzy : z < y) (hyw : y ≤ w) (H : ∀ z < y, z⁻¹ < w) (H' : ∀ ⦃a b : Nimber⦄, a < x → b < w → a * b < x) : of (val x * val z) = x * z

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 1 < x and Iio x is closed under addition, multiplication, and division.

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
• ne_zero : x ≠ 0
• mul_lt ⦃y z : Nimber⦄ (hy : y < x) (hz : z < x) : y * z < x
• ne_one : x ≠ 1
• 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

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

@[simp]

theorem Nimber.IsField.two : (of 2).IsField

def Nimber.IsField.toSubfield {x : Nimber} (h : x.IsField) : Subfield Nimber

Iio x as a subring of Nimber.

Equations

• h.toSubfield = { toSubring := ⋯.toSubring, inv_mem' := ⋯ }

@[simp]

theorem Nimber.val_toSubfield_lt {x : Nimber} (h : x.IsField) (y : ↥h.toSubfield) : ↑y < x

@[simp]

theorem Nimber.mem_toSubfield_iff {x y : Nimber} (h : x.IsField) : y ∈ h.toSubfield ↔ y < x

theorem Nimber.IsField.closure_Iio {x : Nimber} (h : x.IsField) : Subfield.closure (Set.Iio x) = h.toSubfield

theorem Nimber.IsField.mul_eq_of_lt {x y z : Nimber} (hx : x.IsRing) (hy : y.IsField) (hyx : y ≤ x) (hzy : z < y) : of (val x * val z) = x * z

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

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

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

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

theorem Nimber.IsRing.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.