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.

For Mathlib

@[simp]

theorem Ordinal.one_lt_opow {x y : Ordinal.{u_1}} (h : 1 < x) : 1 < x ^ y ↔ y ≠ 0

@[simp]

theorem Ordinal.one_lt_pow {x : Ordinal.{u_1}} {n : ℕ} (h : 1 < x) : 1 < x ^ n ↔ n ≠ 0

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.

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.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
• exists_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.exists_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

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

theorem Nimber.IsNthDegreeClosed.iSup {n : ℕ} {ι : Sort u_1} [Nonempty ι] {f : ι → Nimber} (H : ∀ (i : ι), IsNthDegreeClosed n (f i)) (bdd : BddAbove (Set.range f) := by apply Nimber.bddAbove_of_small) : 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) (ne : s.Nonempty) (bdd : BddAbove s) : (sSup s).IsField

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

theorem Nimber.IsNthDegreeClosed.X_pow_lt_leastNoRoots {n : ℕ} {x : Nimber} (h : IsNthDegreeClosed n x) : ↑(Polynomial.X ^ (n + 1)) < x.leastNoRoots

theorem Nimber.isNthDegreeClosed_iff_X_pow_lt_leastNoRoots {n : ℕ} {x : Nimber} (h : x.IsRing) : IsNthDegreeClosed n x ↔ ↑(Polynomial.X ^ (n + 1)) < x.leastNoRoots

theorem Nimber.isNthDegreeClosed_iff_X_pow_le_leastNoRoots {n : ℕ} {x : Nimber} (h : x.IsRing) : IsNthDegreeClosed n x ↔ ↑(Polynomial.X ^ (n + 1)) ≤ x.leastNoRoots

theorem Nimber.IsField.X_sq_lt_leastNoRoots {x : Nimber} (h : x.IsField) : ↑(Polynomial.X ^ 2) < x.leastNoRoots

theorem Nimber.IsNthDegreeClosed.root_lt {n : ℕ} {x r : Nimber} (h : IsNthDegreeClosed n x) {p : Polynomial Nimber} (hpn : p.degree ≤ ↑n) (hpk : ∀ (k : ℕ), p.coeff k < x) (hr : r ∈ p.roots) : r < x

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

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

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

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.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
• exists_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.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.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.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.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.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.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

Nimbers are algebraically closed

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

Returns the smallest IsAlgClosed that's at least x.

Equations

• x.algClosure = ⨆ (n : ℕ), (fun (y : Nimber) => (sSup (Order.succ '' Nimber.rootSet✝ y)).fieldClosure)^[n] x.fieldClosure

@[simp]

theorem Nimber.le_algClosure (x : Nimber) : x ≤ x.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