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 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

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

theorem Nimber.IsGroup.sum_lt {x : Nimber} (h : x.IsGroup) (hx₀ : x ≠ 0) {ι : 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) (hx₀ : x ≠ 0) : AddSubgroup Nimber

Iio x as a subgroup of Nimber.

Equations

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

@[simp]

theorem Nimber.val_toAddSubgroup_lt {x : Nimber} (h : x.IsGroup) (hx₀ : x ≠ 0) (y : ↥(h.toAddSubgroup hx₀)) : ↑y < 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.

@[simp, 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.

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 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

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

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

def Nimber.IsRing.toSubring {x : Nimber} (h : x.IsRing) (hx₁ : 1 < x) : Subring Nimber

Iio x as a subring of Nimber.

Equations

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

@[simp]

theorem Nimber.val_toSubring_lt {x : Nimber} (h : x.IsRing) (hx₁ : 1 < x) (y : ↥(h.toSubring hx₁)) : ↑y < 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.IsGroup.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.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 < 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 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

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

def Nimber.IsField.toSubfield {x : Nimber} (h : x.IsField) (hx₁ : 1 < x) : Subfield Nimber

Iio x as a subring of Nimber.

Equations

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

@[simp]

theorem Nimber.val_toSubfield_lt {x : Nimber} (h : x.IsField) (hx₁ : 1 < x) (y : ↥(h.toSubfield hx₁)) : ↑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.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.