Documentation

Mathlib.FieldTheory.IsSepClosed

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) [] :
• splits_of_separable : ∀ (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.

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

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} [] {K : Type v} [] [] {f : k →+* K} (p : ) (h : ) :

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} [] [] (p : ) (hp : ) (hsep : ) :
x,
theorem IsSepClosed.exists_pow_nat_eq {k : Type u} [] [] (x : k) (n : ) [hn : NeZero n] :
z, z ^ n = x
theorem IsSepClosed.exists_eq_mul_self {k : Type u} [] [] (x : k) [h2 : ] :
z, x = z * z
theorem IsSepClosed.roots_eq_zero_iff {k : Type u} [] [] {p : } (hsep : ) :
p = Polynomial.C ()
theorem IsSepClosed.exists_eval₂_eq_zero {k : Type u} [] {K : Type v} [] [] (f : k →+* K) (p : ) (hp : ) (hsep : ) :
x, = 0
theorem IsSepClosed.exists_aeval_eq_zero (k : Type u) [] {K : Type v} [] [] [Algebra k K] (p : ) (hp : ) (hsep : ) :
x, ↑() p = 0
theorem IsSepClosed.of_exists_root (k : Type u) [] (H : ∀ (p : ), x, = 0) :
theorem IsSepClosed.degree_eq_one_of_irreducible (k : Type u) [] [] {p : } (hp : ) (hsep : ) :
theorem IsSepClosed.algebraMap_surjective {k : Type u} [] {K : Type v} [] [] [Algebra k K] [] :
class IsSepClosure (k : Type u) [] (K : Type v) [] [Algebra k K] :
• sep_closed :
• separable :

Typeclass for an extension being a separable closure.

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