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

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_of_separable {k : Type u} [Field k] [self : IsSepClosed k] (p : Polynomial k) :
    p.SeparablePolynomial.Splits (RingHom.id k) p

    An algebraically closed field is also separably closed.

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

    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 : p.Separable) :

    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 : p.degree 0) (hsep : p.Separable) :
    ∃ (x : k), p.IsRoot x
    @[instance 100]

    A separably closed perfect field is also algebraically closed.

    Equations
    • =
    theorem IsSepClosed.exists_pow_nat_eq {k : Type u} [Field k] [IsSepClosed k] (x : k) (n : ) [hn : NeZero n] :
    ∃ (z : k), z ^ n = x
    theorem IsSepClosed.exists_eq_mul_self {k : Type u} [Field k] [IsSepClosed k] (x : k) [h2 : NeZero 2] :
    ∃ (z : k), x = z * z
    theorem IsSepClosed.roots_eq_zero_iff {k : Type u} [Field k] [IsSepClosed k] {p : Polynomial k} (hsep : p.Separable) :
    p.roots = 0 p = Polynomial.C (p.coeff 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 : p.degree 0) (hsep : p.Separable) :
    ∃ (x : K), 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 : p.degree 0) (hsep : p.Separable) :
    ∃ (x : K), (Polynomial.aeval x) p = 0
    theorem IsSepClosed.of_exists_root (k : Type u) [Field k] (H : ∀ (p : Polynomial k), p.MonicIrreducible pp.Separable∃ (x : k), Polynomial.eval x p = 0) :
    theorem IsSepClosed.degree_eq_one_of_irreducible (k : Type u) [Field k] [IsSepClosed k] {p : Polynomial k} (hp : Irreducible p) (hsep : p.Separable) :
    p.degree = 1

    If k is separably closed, K / k is a field extension, L / k is an intermediate field which is separable, then L is equal to k. A corollary of IsSepClosed.algebraMap_surjective.

    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.sep_closed (k : Type u) [Field k] {K : Type v} [Field K] [Algebra k K] [self : IsSepClosure k K] :
      theorem IsSepClosure.separable {k : Type u} [Field k] {K : Type v} [Field K] [Algebra k K] [self : IsSepClosure k K] :

      A separably closed field is its separable closure.

      Equations
      • =
      @[instance 100]

      If K is perfect and is a separable closure of k, then it is also an algebraic closure of k.

      Equations
      • =
      @[instance 100]

      If k is perfect, K is a separable closure of k, then it is also an algebraic closure of k.

      Equations
      • =
      @[instance 100]

      If k is perfect, K is an algebraic closure of k, then it is also a separable closure of k.

      Equations
      • =
      instance IsSepClosure.isSeparable {k : Type u} [Field k] {K : Type v} [Field K] [Algebra k K] [IsSepClosure k K] :
      Equations
      • =
      @[instance 100]
      instance IsSepClosure.isGalois {k : Type u} [Field k] {K : Type v} [Field K] [Algebra k K] [IsSepClosure k K] :
      Equations
      • =
      theorem IsSepClosed.surjective_comp_algebraMap_of_isSeparable {K : Type u} (L : Type v) {M : Type w} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [IsSepClosed M] {E : Type u_1} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsSeparable L E] :
      Function.Surjective fun (φ : E →ₐ[K] M) => φ.comp (IsScalarTower.toAlgHom K L E)
      @[irreducible]
      noncomputable def IsSepClosed.lift {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [IsSepClosed M] [Algebra.IsSeparable K L] :

      A (random) homomorphism from a separable extension L of K into a separably closed extension M of K.

      Equations
      Instances For
        theorem IsSepClosed.lift_def {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [IsSepClosed M] [Algebra.IsSeparable K L] :
        IsSepClosed.lift = Classical.choice
        noncomputable def IsSepClosure.equiv (K : Type u) [Field K] (L : Type v) (M : Type w) [Field L] [Field M] [Algebra K M] [IsSepClosure K M] [Algebra K L] [IsSepClosure K L] :

        A (random) isomorphism between two separable closures of K.

        Equations
        Instances For