Separably Closed Field

In this file we define the typeclass for separably closed fields and separable closures, and prove some of their properties.

Main Definitions

• IsSepClosed k is the typeclass saying k is a separably closed field, i.e. every separable polynomial in k splits.

• IsSepClosure k K is the typeclass saying K is a separable closure of k, where k is a field. This means that K is separably closed and separable over k.

Tags

separable closure, separably closed

TODO

• IsSepClosed.lift is a map from a separable extension L of k, into any separably closed extension of k.

• IsSepClosed.equiv is a proof that any two separable closures of the same field are isomorphic.

• If K is a separably closed field (or algebraically closed field) containing k, then all elements of K which are separable over k form a separable closure of k.

• Using the above result, construct a separable closure as a subfield of an algebraic closure.

• If k is a perfect field, then its separable closure coincides with its algebraic closure.

• An algebraic extension of a separably closed field is purely inseparable.

• Maximal separable subextension ...

class IsSepClosed (k : Type u) [Field k] : Prop

• splits_of_separable : ∀ (p : Polynomial k), Polynomial.Separable p → Polynomial.Splits (RingHom.id k) p

Typeclass for separably closed fields.

To show Polynomial.Splits p f for an arbitrary ring homomorphism f, see IsSepClosed.splits_codomain and IsSepClosed.splits_domain.

theorem IsSepClosed.splits_codomain {k : Type u} [Field k] {K : Type v} [Field K] [IsSepClosed K] {f : k →+* K} (p : Polynomial k) (h : Polynomial.Separable p) : Polynomial.Splits f p

Every separable polynomial splits in the field extension f : k →+* K if K is separably closed.

See also IsSepClosed.splits_domain for the case where k is separably closed.

theorem IsSepClosed.splits_domain {k : Type u} [Field k] {K : Type v} [Field K] [IsSepClosed k] {f : k →+* K} (p : Polynomial k) (h : Polynomial.Separable p) : Polynomial.Splits f p

Every separable polynomial splits in the field extension f : k →+* K if k is separably closed.

See also IsSepClosed.splits_codomain for the case where k is separably closed.

theorem IsSepClosed.exists_root {k : Type u} [Field k] [IsSepClosed k] (p : Polynomial k) (hp : Polynomial.degree p ≠ 0) (hsep : Polynomial.Separable p) : ∃ x, Polynomial.IsRoot p x

theorem IsSepClosed.exists_pow_nat_eq {k : Type u} [Field k] [IsSepClosed k] (x : k) (n : ℕ) [hn : NeZero ↑n] : ∃ z, z ^ n = x

theorem IsSepClosed.exists_eq_mul_self {k : Type u} [Field k] [IsSepClosed k] (x : k) [h2 : NeZero 2] : ∃ z, x = z * z

theorem IsSepClosed.roots_eq_zero_iff {k : Type u} [Field k] [IsSepClosed k] {p : Polynomial k} (hsep : Polynomial.Separable p) : Polynomial.roots p = 0 ↔ p = ↑Polynomial.C (Polynomial.coeff p 0)

theorem IsSepClosed.exists_eval₂_eq_zero {k : Type u} [Field k] {K : Type v} [Field K] [IsSepClosed K] (f : k →+* K) (p : Polynomial k) (hp : Polynomial.degree p ≠ 0) (hsep : Polynomial.Separable p) : ∃ x, Polynomial.eval₂ f x p = 0

theorem IsSepClosed.exists_aeval_eq_zero (k : Type u) [Field k] {K : Type v} [Field K] [IsSepClosed K] [Algebra k K] (p : Polynomial k) (hp : Polynomial.degree p ≠ 0) (hsep : Polynomial.Separable p) : ∃ x, ↑(Polynomial.aeval x) p = 0

theorem IsSepClosed.of_exists_root (k : Type u) [Field k] (H : ∀ (p : Polynomial k), Polynomial.Monic p → Irreducible p → Polynomial.Separable p → ∃ x, Polynomial.eval x p = 0) : IsSepClosed k

theorem IsSepClosed.degree_eq_one_of_irreducible (k : Type u) [Field k] [IsSepClosed k] {p : Polynomial k} (hp : Irreducible p) (hsep : Polynomial.Separable p) : Polynomial.degree p = 1

theorem IsSepClosed.algebraMap_surjective {k : Type u} [Field k] {K : Type v} [Field K] [IsSepClosed k] [Algebra k K] [IsSeparable k K] : Function.Surjective ↑(algebraMap k K)

class IsSepClosure (k : Type u) [Field k] (K : Type v) [Field K] [Algebra k K] : Prop

• sep_closed : IsSepClosed K
• separable : IsSeparable k K

Typeclass for an extension being a separable closure.

theorem isSepClosure_iff {k : Type u} [Field k] {K : Type v} [Field K] [Algebra k K] : IsSepClosure k K ↔ IsSepClosed K ∧ IsSeparable k K

instance IsSepClosure.normal {k : Type u} [Field k] {K : Type v} [Field K] [Algebra k K] [IsSepClosure k K] : Normal k K