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 sayingk
is a separably closed field, i.e. every separable polynomial ink
splits. -
IsSepClosure k K
is the typeclass sayingK
is a separable closure ofk
, wherek
is a field. This means thatK
is separably closed and separable overk
.
Tags #
separable closure, separably closed
TODO #
-
IsSepClosed.lift
is a map from a separable extensionL
ofk
, into any separably closed extension ofk
. -
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) containingk
, then all elements ofK
which are separable overk
form a separable closure ofk
. -
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 ...
- 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
.
Instances
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.
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.
- sep_closed : IsSepClosed K
- separable : IsSeparable k K
Typeclass for an extension being a separable closure.