Documentation

Mathlib.FieldTheory.SeparableClosure

Separable closure #

This file contains basics about the (relative) separable closure of a field extension.

Main definitions #

Main results #

Tags #

separable degree, degree, separable closure

def separableClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

The (relative) separable closure of F in E, or called maximal separable subextension of E / F, is defined to be the intermediate field of E / F consisting of all separable elements. The previous results prove that these elements are closed under field operations.

Equations
  • separableClosure F E = { carrier := {x : E | IsSeparable F x}, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := , inv_mem' := }
theorem mem_separableClosure_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} :

An element is contained in the separable closure of F in E if and only if it is a separable element.

theorem map_mem_separableClosure_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E →ₐ[F] K) {x : E} :

If i is an F-algebra homomorphism from E to K, then i x is contained in separableClosure F K if and only if x is contained in separableClosure F E.

If i is an F-algebra homomorphism from E to K, then the preimage of separableClosure F K under the map i is equal to separableClosure F E.

theorem separableClosure.map_le_of_algHom {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E →ₐ[F] K) :

If i is an F-algebra homomorphism from E to K, then the image of separableClosure F E under the map i is contained in separableClosure F K.

If K / E / F is a field extension tower, such that K / E has no non-trivial separable subextensions (when K / E is algebraic, this means that it is purely inseparable), then the image of separableClosure F E in K is equal to separableClosure F K.

theorem separableClosure.map_eq_of_algEquiv {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :

If i is an F-algebra isomorphism of E and K, then the image of separableClosure F E under the map i is equal to separableClosure F K.

def separableClosure.algEquivOfAlgEquiv {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :
{ x : E // x separableClosure F E } ≃ₐ[F] { x : K // x separableClosure F K }

If E and K are isomorphic as F-algebras, then separableClosure F E and separableClosure F K are also isomorphic as F-algebras.

Equations
def AlgEquiv.separableClosure {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :
{ x : E // x separableClosure F E } ≃ₐ[F] { x : K // x separableClosure F K }

Alias of separableClosure.algEquivOfAlgEquiv.


If E and K are isomorphic as F-algebras, then separableClosure F E and separableClosure F K are also isomorphic as F-algebras.

Equations
instance separableClosure.isAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

The separable closure of F in E is algebraic over F.

Equations
  • =
instance separableClosure.isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

The separable closure of F in E is separable over F.

Equations
  • =
theorem le_separableClosure' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {L : IntermediateField F E} (hs : ∀ (x : { x : E // x L }), IsSeparable F x) :

An intermediate field of E / F is contained in the separable closure of F in E if all of its elements are separable over F.

theorem le_separableClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [Algebra.IsSeparable F { x : E // x L }] :

An intermediate field of E / F is contained in the separable closure of F in E if it is separable over F.

theorem le_separableClosure_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) :

An intermediate field of E / F is contained in the separable closure of F in E if and only if it is separable over F.

theorem separableClosure.separableClosure_eq_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

The separable closure in E of the separable closure of F in E is equal to itself.

theorem separableClosure.normalClosure_eq_self (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

The normal closure in E/F of the separable closure of F in E is equal to itself.

instance separableClosure.isGalois (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Normal F E] :
IsGalois F { x : E // x separableClosure F E }

If E is normal over F, then the separable closure of F in E is Galois (i.e. normal and separable) over F.

Equations
  • =

If E / F is a field extension and E is separably closed, then the separable closure of F in E is equal to F if and only if F is separably closed.

instance separableClosure.isSepClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsSepClosed E] :
IsSepClosure F { x : E // x separableClosure F E }

If E is separably closed, then the separable closure of F in E is an absolute separable closure of F.

Equations
  • =
@[reducible, inline]
abbrev SeparableClosure (F : Type u) [Field F] :

The absolute separable closure is defined to be the relative separable closure inside the algebraic closure. It is indeed a separable closure (IsSepClosure) by separableClosure.isSepClosure, and it is Galois (IsGalois) by separableClosure.isGalois or IsSepClosure.isGalois, and every separable extension embeds into it (IsSepClosed.lift).

Equations
theorem IntermediateField.isSeparable_adjoin_iff_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {S : Set E} :
Algebra.IsSeparable F { x : E // x IntermediateField.adjoin F S } xS, IsSeparable F x

F(S) / F is a separable extension if and only if all elements of S are separable elements.

The separable closure of F in E is equal to E if and only if E / F is separable.

If K / E / F is a field extension tower, then separableClosure F K is contained in separableClosure E K.

If K / E / F is a field extension tower, such that E / F is separable, then separableClosure F K is equal to separableClosure E K.

theorem separableClosure.adjoin_le (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :

If K / E / F is a field extension tower, then E adjoin separableClosure F K is contained in separableClosure E K.

instance IntermediateField.isSeparable_sup (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L1 : IntermediateField F E) (L2 : IntermediateField F E) [h1 : Algebra.IsSeparable F { x : E // x L1 }] [h2 : Algebra.IsSeparable F { x : E // x L2 }] :
Algebra.IsSeparable F { x : E // x L1 L2 }

A compositum of two separable extensions is separable.

Equations
  • =
instance IntermediateField.isSeparable_iSup (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {ι : Type u_1} {t : ιIntermediateField F E} [h : ∀ (i : ι), Algebra.IsSeparable F { x : E // x t i }] :
Algebra.IsSeparable F { x : E // x ⨆ (i : ι), t i }

A compositum of separable extensions is separable.

Equations
  • =
def Field.sepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

The (infinite) separable degree for a general field extension E / F is defined to be the degree of separableClosure F E / F.

Equations
Instances For
def Field.insepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

The (infinite) inseparable degree for a general field extension E / F is defined to be the degree of E / separableClosure F E.

Equations
Instances For
def Field.finInsepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

The finite inseparable degree for a general field extension E / F is defined to be the degree of E / separableClosure F E as a natural number. It is defined to be zero if such field extension is infinite.

Equations
Instances For
theorem Field.finInsepDegree_def' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
Field.finInsepDegree F E = Cardinal.toNat (Field.insepDegree F E)
instance Field.instNeZeroSepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
Equations
  • =
instance Field.instNeZeroInsepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
Equations
  • =
Equations
  • =

If E and K are isomorphic as F-algebras, then they have the same separable degree over F.

theorem Field.sepDegree_eq_of_equiv (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :

The same-universe version of Field.lift_sepDegree_eq_of_equiv.

The separable degree multiplied by the inseparable degree is equal to the (infinite) field extension degree.

If E and K are isomorphic as F-algebras, then they have the same inseparable degree over F.

theorem Field.insepDegree_eq_of_equiv (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :

The same-universe version of Field.lift_insepDegree_eq_of_equiv.

theorem Field.finInsepDegree_eq_of_equiv (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :

If E and K are isomorphic as F-algebras, then they have the same finite inseparable degree over F.

@[simp]
theorem Field.sepDegree_self (F : Type u) [Field F] :
@[simp]
@[simp]
theorem IntermediateField.sepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
Field.sepDegree F { x : E // x } = 1
@[simp]
theorem IntermediateField.insepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
Field.insepDegree F { x : E // x } = 1
@[simp]
theorem IntermediateField.finInsepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :
Field.finInsepDegree F { x : E // x } = 1
@[simp]
theorem IntermediateField.finInsepDegree_bot' {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
@[simp]
theorem IntermediateField.sepDegree_top {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
Field.sepDegree F { x : K // x } = Field.sepDegree F K
@[simp]
theorem IntermediateField.insepDegree_top {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
@[simp]
theorem IntermediateField.finInsepDegree_top {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
@[simp]
theorem IntermediateField.sepDegree_bot' {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
Field.sepDegree F { x : K // x } = Field.sepDegree F E
@[simp]
theorem IntermediateField.insepDegree_bot' {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :

A separable extension has separable degree equal to degree.

A separable extension has inseparable degree one.

A separable extension has finite inseparable degree one.