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 #

Tags #

separable closure, separably closed

TODO #

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

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

    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_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
    class IsSepClosure (k : Type u) [Field k] (K : Type v) [Field K] [Algebra k K] :

    Typeclass for an extension being a separable closure.

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