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

source

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' := ⋯ }

Instances For

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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 ⋯)

Instances For

source

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

Instances For

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

@[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))

Instances For

source

instance SeparableClosure.isSepClosed (F : Type u) [Field F] :

IsSepClosed (SeparableClosure F)

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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)

Instances For

source

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

Instances For

source

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

Instances For

source

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)

source

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

NeZero (sepDegree F E)

source

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

NeZero (insepDegree F E)

source

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

NeZero (finInsepDegree F E)

source

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.

source

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.

source

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.

source

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

source

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

source

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.

source

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.

source

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.

source

@[simp]

theorem Field.sepDegree_self (F : Type u) [Field F] :

sepDegree F F = 1

source

@[simp]

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

insepDegree F F = 1

source

@[simp]

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

finInsepDegree F F = 1

source

@[simp]

theorem IntermediateField.sepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

Field.sepDegree F ↥⊥ = 1

source

@[simp]

theorem IntermediateField.insepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

Field.insepDegree F ↥⊥ = 1

source

@[simp]

theorem IntermediateField.finInsepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

Field.finInsepDegree F ↥⊥ = 1

source

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)

source

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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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.

Documentation

Mathlib.FieldTheory.SeparableClosure

Separable closure #

Main definitions #

Main results #

Tags #