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

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

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

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 ↔ 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.

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 = AlgEquiv.trans (IntermediateField.intermediateFieldMap i (separableClosure F E)) (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) :

↥(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

Instances For

source

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.

source

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

⋯ = ⋯

source

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.

source

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.

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 ↔ 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] :

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.

Equations

⋯ = ⋯

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.

Equations

⋯ = ⋯

source

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

Instances For

source

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.

source

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.

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] [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 : 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

⋯ = ⋯

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

IsSeparable F ↥(⨆ (i : ι), t i)

A compositum of separable extensions is separable.

Equations

⋯ = ⋯

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 = FiniteDimensional.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] :

Field.finInsepDegree F E = Cardinal.toNat (Field.insepDegree F E)

source

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

NeZero (Field.sepDegree F E)

Equations

⋯ = ⋯

source

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

NeZero (Field.insepDegree F E)

Equations

⋯ = ⋯

source

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

⋯ = ⋯

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} (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.

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

Field.sepDegree F E = Field.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] :

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.

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} (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.

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

Field.insepDegree F E = Field.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) :

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.

source

@[simp]

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

Field.sepDegree F F = 1

source

@[simp]

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

Field.insepDegree F F = 1

source

@[simp]

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

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

Field.sepDegree F E = Module.rank F E

A separable extension has separable degree equal to degree.

source

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

Field.insepDegree F E = 1

A separable extension has inseparable degree one.

source

theorem IsSeparable.finInsepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [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 #