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.

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) : { 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

• 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) : { 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

• @AlgEquiv.separableClosure = @separableClosure.algEquivOfAlgEquiv

instance separableClosure.isAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Algebra.IsAlgebraic F { x : E // x ∈ separableClosure 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] : Algebra.IsSeparable F { x : E // x ∈ separableClosure 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) : 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 { x : E // x ∈ 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 { x : E // x ∈ 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 { x : E // x ∈ 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 { x : E // x ∈ 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 { 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

• ⋯ = ⋯

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 { 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] : 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 = { x : AlgebraicClosure F // x ∈ 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 { x : E // x ∈ IntermediateField.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 : 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] : 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 { x : E // x ∈ 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 { x : E // x ∈ 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 { x : E // x ∈ 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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

• ⋯ = ⋯

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 { 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

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 { x : K // x ∈ ⊥ }) = 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 { x : K // x ∈ ⊥ }) = 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 { x : K // x ∈ ⊥ } = 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 { 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] : Field.insepDegree F { x : K // x ∈ ⊤ } = 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 { x : K // x ∈ ⊤ } = 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 { 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] : Field.insepDegree F { x : K // x ∈ ⊥ } = Field.insepDegree F E

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.