Documentation

CombinatorialGames.Nimber.SimplestExtension.Algebraic

Nimbers are algebraically closed #

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

n-th degree closed fields #

source
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.exists_root proves that this theorem applies (vacuously) when p = 0 as well.

Instances For
    source
    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
    source
    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
    source
    theorem Nimber.IsNthDegreeClosed.le {m n : ℕ} {x : Nimber} (h : IsNthDegreeClosed n x) (hmn : m ≤ n) :
    IsNthDegreeClosed m x
    source
    @[simp]
    theorem Nimber.IsNthDegreeClosed.zero (n : ℕ) :
    IsNthDegreeClosed n 0
    source
    @[simp]
    theorem Nimber.IsNthDegreeClosed.one (n : ℕ) :
    IsNthDegreeClosed n 1
    source
    theorem Nimber.IsNthDegreeClosed.of_le_one (n : ℕ) {x : Nimber} (h : x ≤ 1) :
    IsNthDegreeClosed n x
    source
    theorem Nimber.IsNthDegreeClosed.sSup {n : ℕ} {s : Set Nimber} (H : ∀ x ∈ s, IsNthDegreeClosed n x) :
    IsNthDegreeClosed n (sSup s)
    source
    theorem Nimber.IsNthDegreeClosed.iSup {n : ℕ} {ι : Sort u_1} {f : ι → Nimber} (H : ∀ (i : ι), IsNthDegreeClosed n (f i)) :
    IsNthDegreeClosed n (⨆ (i : ι), f i)
    source
    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.

    source
    @[simp]
    theorem Nimber.isNthDegreeClosed_zero_iff_isRing {x : Nimber} :
    IsNthDegreeClosed 0 x ↔ x.IsRing
    source
    theorem Nimber.IsNthDegreeClosed.toIsField {n : ℕ} {x : Nimber} (h : IsNthDegreeClosed n x) (hn : 1 ≤ n) :
    x.IsField
    source
    @[simp]
    theorem Nimber.isNthDegreeClosed_one_iff_isField {x : Nimber} :
    IsNthDegreeClosed 1 x ↔ x.IsField
    source
    theorem Nimber.IsField.sSup {s : Set Nimber} (H : ∀ x ∈ s, x.IsField) :
    (sSup s).IsField
    source
    theorem Nimber.IsField.iSup {ι : Sort u_1} {f : ι → Nimber} (H : ∀ (i : ι), (f i).IsField) :
    (⨆ (i : ι), f i).IsField

    Algebraically closed fields #

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

    Instances For
      source
      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
      source
      theorem Nimber.IsAlgClosed.toIsNthDegreeClosed {x : Nimber} (h : x.IsAlgClosed) (n : ℕ) :
      IsNthDegreeClosed n x
      source
      theorem Nimber.IsAlgClosed.toIsField {x : Nimber} (h : x.IsAlgClosed) :
      x.IsField
      source
      theorem Nimber.isAlgClosed_iff_forall {x : Nimber} :
      x.IsAlgClosed ↔ ∀ (n : ℕ), IsNthDegreeClosed n x
      source
      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
      source
      @[simp]
      theorem Nimber.IsAlgClosed.zero :
      IsAlgClosed 0
      source
      @[simp]
      theorem Nimber.IsAlgClosed.one :
      IsAlgClosed 1
      source
      theorem Nimber.IsAlgClosed.sSup {s : Set Nimber} (H : ∀ x ∈ s, x.IsAlgClosed) :
      (sSup s).IsAlgClosed
      source
      theorem Nimber.IsAlgClosed.iSup {ι : Sort u_1} {f : ι → Nimber} (H : ∀ (i : ι), (f i).IsAlgClosed) :
      (⨆ (i : ι), f i).IsAlgClosed
      source
      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.