Nimbers are algebraically closed

This file proves the last part of the simplest extension theorem (see CombinatorialGames.Nimber.SimplestExtension.Basic), and deduces as a corollary that the nimbers are algebraically closed.

Lemmas relating rings to leastNoRoots

theorem Nimber.IsRing.eval_eq_of_lt {n : ℕ} {x : Nimber} (h : x.IsRing) (h' : ↑(Polynomial.X ^ n) ≤ x.leastNoRoots) {p : Polynomial Nimber} (hpn : p.degree < ↑n) (hpk : ∀ (k : ℕ), p.coeff k < x) : Polynomial.eval x p = x.oeval p

theorem Nimber.IsRing.pow_mul_eq {n : ℕ} {x y : Nimber} (h : x.IsRing) (h' : ↑(Polynomial.X ^ (n + 1)) ≤ x.leastNoRoots) (hy : y < x) : x ^ n * y = of (val x ^ n * val y)

theorem Nimber.IsRing.pow_eq {n : ℕ} {x : Nimber} (h : x.IsRing) (h' : ↑(Polynomial.X ^ (n + 1)) ≤ x.leastNoRoots) : x ^ n = of (val x ^ n)

Algebraically closed fields

structure Nimber.IsAlgClosed (x : Nimber) extends x.IsField : 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.exists_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
• 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
• exists_root' ⦃p : Polynomial Nimber⦄ (hp₀ : 0 < p.degree) (hp : ∀ (k : ℕ), p.coeff k < x) : ∃ r < x, p.IsRoot r

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

theorem Nimber.IsAlgClosed.leastNoRoots_eq_top {x : Nimber} (h : x.IsAlgClosed) : x.leastNoRoots = ⊤

theorem Nimber.isAlgClosed_iff_leastNoRoots_eq_top {x : Nimber} (h : x.IsRing) : x.IsAlgClosed ↔ x.leastNoRoots = ⊤

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

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

theorem Nimber.IsAlgClosed.eval_eq_of_lt {x : Nimber} (h : x.IsAlgClosed) {p : Polynomial Nimber} (hpk : ∀ (k : ℕ), p.coeff k < x) : Polynomial.eval x p = x.oeval p

theorem Nimber.IsAlgClosed.pow_mul_eq {n : ℕ} {x y : Nimber} (h : x.IsAlgClosed) (hy : y < x) : x ^ n * y = of (val x ^ n * val y)

theorem Nimber.IsAlgClosed.pow_eq {n : ℕ} {x : Nimber} (h : x.IsAlgClosed) : x ^ n = of (val x ^ n)

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.

theorem Nimber.IsRing.isRoot_leastNoRoots {x : Nimber} (h : x.IsRing) (ht : x.leastNoRoots ≠ ⊤) : (x.leastNoRoots.untop ht).IsRoot x

The fourth simplest extension theorem: if x is a ring that isn't algebraically closed, then x is the root of some polynomial with coefficients < x.

theorem Nimber.IsRing.pow_degree_leastNoRoots {x : Nimber} (h : x.IsRing) (ht : x.leastNoRoots ≠ ⊤) {n : ℕ} (hn : (x.leastNoRoots.untop ht).degree = ↑n) : (of (val x ^ n)).IsRing

theorem Nimber.IsField.pow_degree_leastNoRoots {x : Nimber} (hf : x.IsField) (ht : x.leastNoRoots ≠ ⊤) {n : ℕ} (hn : (x.leastNoRoots.untop ht).degree = ↑n) : (of (val x ^ n)).IsField

theorem Nimber.IsAlgClosed.isRing_opow_omega0 {t : Nimber} (ht : t.IsAlgClosed) : (of (val t ^ Ordinal.omega0)).IsRing

Nimbers are algebraically closed

noncomputable def Nimber.algClosure (x : Nimber) : Nimber

Returns the smallest IsAlgClosed that's at least x.

Equations

• x.algClosure = sSup (Order.succ '' Nimber.rootSet✝ x.fieldClosure)

theorem Nimber.lt_algClosure_iff_isAlgebraic {x y : Nimber} : y < x.algClosure ↔ IsAlgebraic (↥⋯.toSubfield) y

@[simp]

theorem Nimber.le_algClosure (x : Nimber) : x ≤ x.algClosure

theorem Nimber.IsAlgClosed.algClosure (x : Nimber) : x.algClosure.IsAlgClosed

theorem Nimber.IsAlgClosed.algClosure_le_iff {x y : Nimber} (h : x.IsAlgClosed) : y.algClosure ≤ x ↔ y ≤ x

theorem Nimber.IsAlgClosed.lt_algClosure_iff {x y : Nimber} (h : x.IsAlgClosed) : x < y.algClosure ↔ x < y

theorem Nimber.algClosure_mono : Monotone algClosure

instance Nimber.instIsAlgClosed : _root_.IsAlgClosed Nimber

The nimbers are an algebraically closed field.

Square roots

noncomputable def Nimber.sqrt : Nimber ≃+* Nimber

The square root of a nimber x is the unique value with (√x)^2 = x.

Conventions for notations in identifiers:

• The recommended spelling of √ in identifiers is sqrt.

Equations

• Nimber.sqrt = (frobeniusEquiv Nimber 2).symm

def Nimber.«term√_» : Lean.ParserDescr

The square root of a nimber x is the unique value with (√x)^2 = x.

Conventions for notations in identifiers:

• The recommended spelling of √ in identifiers is sqrt.

Equations

• Nimber.«term√_» = Lean.ParserDescr.node `Nimber.«term√_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "√") (Lean.ParserDescr.cat `term 1024))

theorem Nimber.sqrt_zero : sqrt 0 = 0

theorem Nimber.sqrt_one : sqrt 1 = 1

theorem Nimber.sqrt_add (x y : Nimber) : sqrt (x + y) = sqrt x + sqrt y

theorem Nimber.sqrt_mul (x y : Nimber) : sqrt (x * y) = sqrt x * sqrt y

theorem Nimber.sqrt_inj {x y : Nimber} : sqrt x = sqrt y ↔ x = y

@[simp]

theorem Nimber.sqrt_sq (x : Nimber) : sqrt (x ^ 2) = x

@[simp]

theorem Nimber.sq_sqrt (x : Nimber) : sqrt x ^ 2 = x

@[simp]

theorem Nimber.sqrt_self_mul_self (x : Nimber) : sqrt (x * x) = x

@[simp]

theorem Nimber.sqrt_mul_sqrt_self (x : Nimber) : sqrt x * sqrt x = x

theorem Nimber.sqrt_eq_iff {x y : Nimber} : sqrt y = x ↔ x ^ 2 = y

theorem Nimber.sqrt_eq {x y : Nimber} : x ^ 2 = y → sqrt y = x

Alias of the reverse direction of Nimber.sqrt_eq_iff.

theorem Nimber.IsField.sqrt_lt {x y : Nimber} (h : x.IsField) (hy : y < x) (hx : ↑(Polynomial.X ^ 2 + Polynomial.C y) < x.leastNoRoots) : sqrt y < x

theorem Nimber.IsField.sqrt_lt' {x y : Nimber} (h : x.IsField) (hy : y < x) (hx : ↑(Polynomial.X ^ 2 + Polynomial.X) ≤ x.leastNoRoots) : sqrt y < x