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_separable: 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.

Equations

• One or more equations did not get rendered due to their size.

theorem mem_separableClosure_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} : x ∈ separableClosure F E ↔ Polynomial.Separable (minpoly 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

• One or more equations did not get rendered due to their size.

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

theorem 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] : IsSeparable F ↥(separableClosure F E)

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

Equations

• (_ : IsSeparable F ↥(separableClosure F E)) = (_ : IsSeparable F ↥(separableClosure F E))

theorem le_separableClosure' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {L : IntermediateField F E} (hs : ∀ (x : ↥L), Polynomial.Separable (minpoly 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) [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 ↔ 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] : 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.

Equations

• (_ : IsGalois F ↥(separableClosure F E)) = (_ : IsGalois F ↥(separableClosure F E))

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.

Equations

• (_ : IsSepClosure F ↥(separableClosure F E)) = (_ : IsSepClosure F ↥(separableClosure F E))

@[inline, reducible]

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_separable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {S : Set E} : IsSeparable F ↥(IntermediateField.adjoin F S) ↔ ∀ x ∈ S, Polynomial.Separable (minpoly 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 = ⊤ ↔ 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] [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 : IntermediateField F E) (L2 : IntermediateField F E) [h1 : IsSeparable F ↥L1] [h2 : IsSeparable F ↥L2] : IsSeparable F ↥(L1 ⊔ L2)

A compositum of two separable extensions is separable.

Equations

• (_ : IsSeparable F ↥(L1 ⊔ L2)) = (_ : IsSeparable F ↥(L1 ⊔ L2))

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

A compositum of separable extensions is separable.

Equations

• (_ : IsSeparable F ↥(⨆ (i : ι), t i)) = (_ : IsSeparable F ↥(⨆ (i : ι), t i))

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.

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.

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 = FiniteDimensional.finrank (↥(separableClosure F E)) E

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] : NeZero (Field.sepDegree F E)

Equations

• (_ : NeZero (Field.sepDegree F E)) = (_ : NeZero (Field.sepDegree F E))

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

Equations

• (_ : NeZero (Field.insepDegree F E)) = (_ : NeZero (Field.insepDegree F E))

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

Equations

• (_ : NeZero (Field.finInsepDegree F E)) = (_ : NeZero (Field.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} (Field.sepDegree F E) = Cardinal.lift.{v, w} (Field.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) : Field.sepDegree F E = Field.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] : Field.sepDegree F E * Field.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.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} (Field.insepDegree F E) = Cardinal.lift.{v, w} (Field.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) : Field.insepDegree F E = Field.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) : Field.finInsepDegree F E = Field.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] : Field.sepDegree F F = 1

@[simp]

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

@[simp]

theorem Field.finInsepDegree_self (F : Type u) [Field F] : Field.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