Separable closure

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

Main definitions

• separableClosure: 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.

• SeparableClosure: the absolute separable closure, defined to be the relative separable closure inside the algebraic closure.

• Field.sepDegree F E: the (infinite) separable degree $[E:F{]}_s$ of an algebraic extension E / F of fields, defined to be the degree of separableClosure F E / F. Later we will show that (Field.finSepDegree_eq, not in this file), if Field.Emb F E is finite, then this coincides with Field.finSepDegree F E.

• Field.insepDegree F E: the (infinite) inseparable degree $[E:F{]}_i$ of an algebraic extension E / F of fields, defined to be the degree of E / separableClosure F E.

• Field.finInsepDegree F E: the finite inseparable degree $[E:F{]}_i$ of an algebraic extension E / F of fields, defined to be the degree of E / separableClosure F E as a natural number. It is zero if such field extension is not finite.

Main results

• le_separableClosure_iff: 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.

• separableClosure.normalClosure_eq_self: the normal closure of the separable closure of F in E is equal to itself.

• separableClosure.isGalois: the separable closure in a normal extension is Galois (namely, normal and separable).

• separableClosure.isSepClosure: the separable closure in a separably closed extension is a separable closure of the base field.

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

• separableClosure.eq_top_iff: the separable closure of F in E is equal to E if and only if E / F is separable.

Tags

separable degree, degree, separable closure

def separableClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : IntermediateField 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.

Stacks Tag 09HC

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} : x ∈ separableClosure F E ↔ IsSeparable F x

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} : i x ∈ separableClosure F K ↔ x ∈ separableClosure F 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.

theorem separableClosure.comap_eq_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) : IntermediateField.comap i (separableClosure F K) = 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) : IntermediateField.map i (separableClosure F E) ≤ separableClosure 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.

theorem separableClosure.map_eq_of_separableClosure_eq_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] (h : separableClosure E K = ⊥) : IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E) = 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) : IntermediateField.map (↑i) (separableClosure F E) = separableClosure 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) : ↥(separableClosure F E) ≃ₐ[F] ↥(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

• separableClosure.algEquivOfAlgEquiv i = (IntermediateField.intermediateFieldMap i (separableClosure F E)).trans (IntermediateField.equivOfEq ⋯)

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) : ↥(_root_.separableClosure F E) ≃ₐ[F] ↥(_root_.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

• @AlgEquiv.separableClosure = @separableClosure.algEquivOfAlgEquiv

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

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

instance separableClosure.isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Algebra.IsSeparable F ↥(separableClosure F E)

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

Stacks Tag 030K ($E_{sep}/F$ is separable)

theorem le_separableClosure' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {L : IntermediateField F E} (hs : ∀ (x : ↥L), IsSeparable F x) : L ≤ separableClosure F E

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 ↥L] : L ≤ separableClosure F E

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) : L ≤ separableClosure F E ↔ Algebra.IsSeparable F ↥L

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] : separableClosure (↥(separableClosure F E)) 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] : IntermediateField.normalClosure F (↥(separableClosure F E)) E = separableClosure 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 ↥(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.

Stacks Tag 0EXK

theorem IsSepClosed.separableClosure_eq_bot_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsSepClosed E] : separableClosure F E = ⊥ ↔ IsSepClosed F

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 ↥(separableClosure F E)

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

@[reducible, inline]

abbrev SeparableClosure (F : Type u) [Field F] : Type u

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

• SeparableClosure F = ↥(separableClosure F (AlgebraicClosure F))

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 ↥(adjoin F S) ↔ ∀ x ∈ S, IsSeparable F x

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

theorem separableClosure.eq_top_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : separableClosure F E = ⊤ ↔ Algebra.IsSeparable F E

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

theorem separableClosure.le_restrictScalars (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] : separableClosure F K ≤ IntermediateField.restrictScalars F (separableClosure E K)

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

theorem separableClosure.eq_restrictScalars_of_isSeparable (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] [Algebra.IsSeparable F E] : separableClosure F K = IntermediateField.restrictScalars F (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] : IntermediateField.adjoin E ↑(separableClosure F K) ≤ separableClosure 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 L2 : IntermediateField F E) [h1 : Algebra.IsSeparable F ↥L1] [h2 : Algebra.IsSeparable F ↥L2] : Algebra.IsSeparable F ↥(L1 ⊔ L2)

A compositum of two separable extensions is separable.

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 ↥(t i)] : Algebra.IsSeparable F ↥(⨆ (i : ι), t i)

A compositum of separable extensions is separable.

def Field.sepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Cardinal.{v}

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

Stacks Tag 030L (Part 1)

Equations

• Field.sepDegree F E = Module.rank F ↥(separableClosure F E)

def Field.insepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Cardinal.{v}

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

Stacks Tag 030L (Part 2)

Equations

• Field.insepDegree F E = Module.rank (↥(separableClosure F E)) E

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

• Field.finInsepDegree F E = Module.finrank (↥(separableClosure F E)) E

theorem Field.finInsepDegree_def' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : finInsepDegree F E = Cardinal.toNat (insepDegree F E)

instance Field.instNeZeroSepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : NeZero (sepDegree F E)

instance Field.instNeZeroInsepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : NeZero (insepDegree F E)

instance Field.instNeZeroFinInsepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] : NeZero (finInsepDegree F E)

theorem Field.lift_sepDegree_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) : Cardinal.lift.{w, v} (sepDegree F E) = Cardinal.lift.{v, w} (sepDegree F K)

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) : sepDegree F E = sepDegree F K

The same-universe version of Field.lift_sepDegree_eq_of_equiv.

theorem Field.sepDegree_mul_insepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : sepDegree F E * insepDegree F E = Module.rank F E

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

theorem Field.sepDegree_le_rank (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : sepDegree F E ≤ Module.rank F E

theorem Field.insepDegree_le_rank (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : insepDegree F E ≤ Module.rank F E

theorem Field.lift_insepDegree_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) : Cardinal.lift.{w, v} (insepDegree F E) = Cardinal.lift.{v, w} (insepDegree F K)

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) : insepDegree F E = insepDegree 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) : finInsepDegree F E = finInsepDegree 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] : sepDegree F F = 1

@[simp]

theorem Field.insepDegree_self (F : Type u) [Field F] : insepDegree F F = 1

@[simp]

theorem Field.finInsepDegree_self (F : Type u) [Field F] : finInsepDegree F F = 1

@[simp]

theorem IntermediateField.sepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Field.sepDegree F ↥⊥ = 1

@[simp]

theorem IntermediateField.insepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Field.insepDegree F ↥⊥ = 1

@[simp]

theorem IntermediateField.finInsepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Field.finInsepDegree F ↥⊥ = 1

theorem IntermediateField.lift_sepDegree_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] : Cardinal.lift.{v, w} (Field.sepDegree F ↥⊥) = Cardinal.lift.{w, v} (Field.sepDegree F E)

theorem IntermediateField.lift_insepDegree_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] : Cardinal.lift.{v, w} (Field.insepDegree F ↥⊥) = Cardinal.lift.{w, v} (Field.insepDegree F E)

@[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] : Field.finInsepDegree F ↥⊥ = Field.finInsepDegree F E

@[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 ↥⊤ = 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] : Field.insepDegree F ↥⊤ = Field.insepDegree F 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] : Field.finInsepDegree F ↥⊤ = Field.finInsepDegree F 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 ↥⊥ = 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] : Field.insepDegree F ↥⊥ = Field.insepDegree F E

theorem Field.insepDegree_top_le_insepDegree_of_isScalarTower (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] : insepDegree E K ≤ insepDegree F K

theorem Field.insepDegree_le_of_left_le {F : Type u} [Field F] {K : Type v} [Field K] [Algebra F K] {E₁ E₂ : IntermediateField F K} (H : E₁ ≤ E₂) : insepDegree (↥E₂) K ≤ insepDegree (↥E₁) K

theorem Field.finInsepDegree_top_le_finInsepDegree_of_isScalarTower (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] [Module.Finite F K] : finInsepDegree E K ≤ finInsepDegree F K

theorem IntermediateField.finInsepDegree_le_of_left_le {F : Type u} [Field F] {K : Type v} [Field K] [Algebra F K] {E₁ E₂ : IntermediateField F K} (H : E₁ ≤ E₂) [Module.Finite (↥E₁) K] : Field.finInsepDegree (↥E₂) K ≤ Field.finInsepDegree (↥E₁) K

theorem Algebra.IsSeparable.sepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsSeparable F E] : Field.sepDegree F E = Module.rank F E

A separable extension has separable degree equal to degree.

theorem Algebra.IsSeparable.insepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsSeparable F E] : Field.insepDegree F E = 1

A separable extension has inseparable degree one.

theorem Algebra.IsSeparable.finInsepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsSeparable F E] : Field.finInsepDegree F E = 1

A separable extension has finite inseparable degree one.