Inseparable nimber extensions

Let t be an algebraically closed nimber, and let t(t) denote the smallest nimber field larger than t. Then the next few fields after t(t) are t(t) ^ 2 ^ n as n ranges over ℕ, and these are all purely inseparable extensions over t(t) obtained by adjoining the 2 ^ n-th root of t. After these then t(t) ^ ω is a perfect field and so all further extensions are too until the next algebraically closed nimber.

@[simp]

theorem RingEquiv.coe_subfieldCongr_apply {K : Type u} [DivisionRing K] {s t : Subfield K} (x : ↥s) (h : s = t) : ↑((subfieldCongr h) x) = ↑x

theorem Nimber.IsAlgClosed.leastNoRoots_fieldClosure_succ {t : Nimber} (ht : t.IsAlgClosed) : (Order.succ t).fieldClosure.leastNoRoots = ↑(Polynomial.X ^ 2 + Polynomial.C t)

theorem Nimber.IsAlgClosed.fieldClosure_succ_pow_two {t : Nimber} (ht : t.IsAlgClosed) : (Order.succ t).fieldClosure ^ 2 = t

theorem Nimber.IsAlgClosed.sqrt_eq {t : Nimber} (ht : t.IsAlgClosed) : sqrt t = (Order.succ t).fieldClosure

theorem Nimber.IsAlgClosed.isField_fieldClosure_succ_pow_two_pow {t : Nimber} (ht : t.IsAlgClosed) (n : ℕ) : (of (val (Order.succ t).fieldClosure ^ 2 ^ n)).IsField

theorem Nimber.IsAlgClosed.leastNoRoots_fieldClosure_succ_pow_two_pow_succ {t : Nimber} (ht : t.IsAlgClosed) (n : ℕ) : (of (val (Order.succ t).fieldClosure ^ 2 ^ (n + 1))).leastNoRoots = ↑(Polynomial.X ^ 2 + Polynomial.C (of (val (Order.succ t).fieldClosure ^ 2 ^ n)))

theorem Nimber.IsAlgClosed.fieldClosure_succ_pow_two_pow_succ_pow_two {t : Nimber} (ht : t.IsAlgClosed) (n : ℕ) : of (val (Order.succ t).fieldClosure ^ 2 ^ (n + 1)) ^ 2 = of (val (Order.succ t).fieldClosure ^ 2 ^ n)

theorem Nimber.IsAlgClosed.sqrt_map_fieldClosure_succ_pow_two_pow_succ {t : Nimber} (ht : t.IsAlgClosed) (n : ℕ) : Subfield.map sqrt.toRingHom ⋯.toSubfield = ⋯.toSubfield

theorem Nimber.IsAlgClosed.sqrt_fieldClosure_succ_pow_two_pow {t : Nimber} (ht : t.IsAlgClosed) (n : ℕ) : sqrt (of (val (Order.succ t).fieldClosure ^ 2 ^ n)) = of (val (Order.succ t).fieldClosure ^ 2 ^ (n + 1))

theorem Nimber.IsAlgClosed.isField_fieldClosure_succ_pow_omega0 {t : Nimber} (ht : t.IsAlgClosed) : (of (val (Order.succ t).fieldClosure ^ Ordinal.omega0)).IsField

theorem Nimber.IsAlgClosed.exists_fieldClosure_succ_pow_two_pow_eq_of_isField_of_btwn {t : Nimber} (ht : t.IsAlgClosed) {x : Nimber} (hx : x.IsField) (htx : (Order.succ t).fieldClosure ≤ x) (hxt : x < of (val (Order.succ t).fieldClosure ^ Ordinal.omega0)) : ∃ (n : ℕ), of (val (Order.succ t).fieldClosure ^ 2 ^ n) = x

theorem Nimber.IsAlgClosed.perfectField_fieldClosure_succ_pow_omega0 {t : Nimber} (ht : t.IsAlgClosed) : PerfectField ↥⋯.toSubfield

theorem Nimber.IsAlgClosed.not_perfectField_fieldClosure_succ_pow_two_pow {t : Nimber} (ht : t.IsAlgClosed) (n : ℕ) : ¬PerfectField ↥⋯.toSubfield

theorem Nimber.IsField.not_perfectField_iff {x : Nimber} (hx : x.IsField) : ¬PerfectField ↥hx.toSubfield ↔ ∃ (t : Nimber), t.IsAlgClosed ∧ ∃ (n : ℕ), of (val (Order.succ t).fieldClosure ^ 2 ^ n) = x