Basic results about relative perfect closure #

This file contains basic results about relative perfect closures.

Main definitions #

perfectClosure: the relative perfect closure of F in E, it consists of the elements x of E such that there exists a natural number n such that x ^ (ringExpChar F) ^ n is contained in F, where ringExpChar F is the exponential characteristic of F. It is also the maximal purely inseparable subextension of E / F (le_perfectClosure_iff).

Main results #

le_perfectClosure_iff: an intermediate field of E / F is contained in the relative perfect closure of F in E if and only if it is purely inseparable over F.
perfectClosure.perfectRing, perfectClosure.perfectField: if E is a perfect field, then the (relative) perfect closure perfectClosure F E is perfect.
IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem: if F is of exponential characteristic q, then F(S) / F is a purely inseparable extension if and only if for any x ∈ S, x ^ (q ^ n) is contained in F for some n : ℕ.

Tags #

separable degree, degree, separable closure, purely inseparable

source

def perfectClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

IntermediateField F E

The relative perfect closure of F in E, consists of the elements x of E such that there exists a natural number n such that x ^ (ringExpChar F) ^ n is contained in F, where ringExpChar F is the exponential characteristic of F. It is also the maximal purely inseparable subextension of E / F (le_perfectClosure_iff).

Stacks Tag 09HH

Equations

Instances For

source

theorem mem_perfectClosure_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} :

x ∈ perfectClosure F E ↔ ∃ (n : ℕ), x ^ ringExpChar F ^ n ∈ (algebraMap F E).range

source

theorem mem_perfectClosure_iff_pow_mem {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] {x : E} :

x ∈ perfectClosure F E ↔ ∃ (n : ℕ), x ^ q ^ n ∈ (algebraMap F E).range

source

theorem mem_perfectClosure_iff_natSepDegree_eq_one {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} :

x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1

An element is contained in the relative perfect closure if and only if its minimal polynomial has separable degree one.

source

theorem isPurelyInseparable_iff_perfectClosure_eq_top {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] :

IsPurelyInseparable F E ↔ perfectClosure F E = ⊤

A field extension E / F is purely inseparable if and only if the relative perfect closure of F in E is equal to E.

source

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

IsPurelyInseparable F ↥(perfectClosure F E)

The relative perfect closure of F in E is purely inseparable over F.

source

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

Algebra.IsAlgebraic F ↥(perfectClosure F E)

The relative perfect closure of F in E is algebraic over F.

source

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

perfectClosure F E = ⊥

If E / F is separable, then the perfect closure of F in E is equal to F. Note that the converse is not necessarily true (see https://math.stackexchange.com/a/3009197) even when E / F is algebraic.

source

theorem le_perfectClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [h : IsPurelyInseparable F ↥L] :

L ≤ perfectClosure F E

An intermediate field of E / F is contained in the relative perfect closure of F in E if it is purely inseparable over F.

source

theorem le_perfectClosure_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) :

L ≤ perfectClosure F E ↔ IsPurelyInseparable F ↥L

An intermediate field of E / F is contained in the relative perfect closure of F in E if and only if it is purely inseparable over F.

source

theorem separableClosure_inf_perfectClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] :

separableClosure F E ⊓ perfectClosure F E = ⊥

source

theorem map_mem_perfectClosure_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 ∈ perfectClosure F K ↔ x ∈ perfectClosure F E

If i is an F-algebra homomorphism from E to K, then i x is contained in perfectClosure F K if and only if x is contained in perfectClosure F E.

source

theorem perfectClosure.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 (perfectClosure F K) = perfectClosure F E

If i is an F-algebra homomorphism from E to K, then the preimage of perfectClosure F K under the map i is equal to perfectClosure F E.

source

theorem perfectClosure.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 (perfectClosure F E) ≤ perfectClosure F K

If i is an F-algebra homomorphism from E to K, then the image of perfectClosure F E under the map i is contained in perfectClosure F K.

source

theorem perfectClosure.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) (perfectClosure F E) = perfectClosure F K

If i is an F-algebra isomorphism of E and K, then the image of perfectClosure F E under the map i is equal to in perfectClosure F K.

source

def perfectClosure.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) :

↥(perfectClosure F E) ≃ₐ[F] ↥(perfectClosure F K)

If E and K are isomorphic as F-algebras, then perfectClosure F E and perfectClosure F K are also isomorphic as F-algebras.

Equations

Instances For

source

def AlgEquiv.perfectClosure {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_.perfectClosure F E) ≃ₐ[F] ↥(_root_.perfectClosure F K)

Alias of perfectClosure.algEquivOfAlgEquiv.

If E and K are isomorphic as F-algebras, then perfectClosure F E and perfectClosure F K are also isomorphic as F-algebras.

Equations

Instances For

source

instance perfectClosure.perfectRing (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (p : ℕ) [ExpChar E p] [PerfectRing E p] :

PerfectRing (↥(perfectClosure F E)) p

If E is a perfect field of exponential characteristic p, then the (relative) perfect closure perfectClosure F E is perfect.

source

instance perfectClosure.perfectField (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [PerfectField E] :

PerfectField ↥(perfectClosure F E)

If E is a perfect field, then the (relative) perfect closure perfectClosure F E is perfect.

source

theorem IntermediateField.isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {x : E} :

IsPurelyInseparable F ↥F⟮x⟯ ↔ (minpoly F x).natSepDegree = 1

F⟮x⟯ / F is a purely inseparable extension if and only if the minimal polynomial of x has separable degree one.

source

theorem IntermediateField.isPurelyInseparable_adjoin_simple_iff_pow_mem (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] {x : E} :

IsPurelyInseparable F ↥F⟮x⟯ ↔ ∃ (n : ℕ), x ^ q ^ n ∈ (algebraMap F E).range

If F is of exponential characteristic q, then F⟮x⟯ / F is a purely inseparable extension if and only if x ^ (q ^ n) is contained in F for some n : ℕ.

source

theorem IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] {S : Set E} :

IsPurelyInseparable F ↥(adjoin F S) ↔ ∀ x ∈ S, ∃ (n : ℕ), x ^ q ^ n ∈ (algebraMap F E).range

If F is of exponential characteristic q, then F(S) / F is a purely inseparable extension if and only if for any x ∈ S, x ^ (q ^ n) is contained in F for some n : ℕ.

source

instance IntermediateField.isPurelyInseparable_sup (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L1 L2 : IntermediateField F E) [h1 : IsPurelyInseparable F ↥L1] [h2 : IsPurelyInseparable F ↥L2] :

IsPurelyInseparable F ↥(L1 ⊔ L2)

A compositum of two purely inseparable extensions is purely inseparable.

source

instance IntermediateField.isPurelyInseparable_iSup (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {ι : Sort u_1} {t : ι → IntermediateField F E} [h : ∀ (i : ι), IsPurelyInseparable F ↥(t i)] :

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

A compositum of purely inseparable extensions is purely inseparable.

source

theorem IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (S : Set E) [Algebra.IsSeparable F ↥(adjoin F S)] (q : ℕ) [ExpChar F q] (n : ℕ) :

adjoin F S = adjoin F ((fun (x : E) => x ^ q ^ n) '' S)

If F is a field of exponential characteristic q, F(S) / F is separable, then F(S) = F(S ^ (q ^ n)) for any natural number n.

source

theorem IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsSeparable F E] (S : Set E) (q : ℕ) [ExpChar F q] (n : ℕ) :

adjoin F S = adjoin F ((fun (x : E) => x ^ q ^ n) '' S)

If E / F is a separable field extension of exponential characteristic q, then F(S) = F(S ^ (q ^ n)) for any subset S of E and any natural number n.

source

theorem IntermediateField.adjoin_eq_adjoin_pow_expChar_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (S : Set E) [Algebra.IsSeparable F ↥(adjoin F S)] (q : ℕ) [ExpChar F q] :

adjoin F S = adjoin F ((fun (x : E) => x ^ q) '' S)

If F is a field of exponential characteristic q, F(S) / F is separable, then F(S) = F(S ^ q).

source

theorem IntermediateField.adjoin_eq_adjoin_pow_expChar_of_isSeparable' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsSeparable F E] (S : Set E) (q : ℕ) [ExpChar F q] :

adjoin F S = adjoin F ((fun (x : E) => x ^ q) '' S)

If E / F is a separable field extension of exponential characteristic q, then F(S) = F(S ^ q) for any subset S of E.

source

theorem IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {a : E} (ha : IsSeparable F a) (q : ℕ) [ExpChar F q] (n : ℕ) :

F⟮a⟯ = F⟮a ^ q ^ n⟯

If F is a field of exponential characteristic q, a : E is separable over F, then F⟮a⟯ = F⟮a ^ q ^ n⟯ for any natural number n.

source

theorem IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsSeparable F E] (a : E) (q : ℕ) [ExpChar F q] (n : ℕ) :

F⟮a⟯ = F⟮a ^ q ^ n⟯

If E / F is a separable field extension of exponential characteristic q, then F⟮a⟯ = F⟮a ^ q ^ n⟯ for any subset a : E and any natural number n.

source

theorem IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {a : E} (ha : IsSeparable F a) (q : ℕ) [ExpChar F q] :

F⟮a⟯ = F⟮a ^ q⟯

If F is a field of exponential characteristic q, a : E is separable over F, then F⟮a⟯ = F⟮a ^ q⟯.

source

theorem IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsSeparable F E] (a : E) (q : ℕ) [ExpChar F q] :

F⟮a⟯ = F⟮a ^ q⟯

If E / F is a separable field extension of exponential characteristic q, then F⟮a⟯ = F⟮a ^ q⟯ for any a : E.

source

theorem Field.span_map_pow_expChar_pow_eq_top_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q n : ℕ) [hF : ExpChar F q] {ι : Type u_1} {v : ι → E} [Algebra.IsSeparable F E] (h : Submodule.span F (Set.range v) = ⊤) :

Submodule.span F (Set.range fun (x : ι) => v x ^ q ^ n) = ⊤

If E / F is a separable extension of exponential characteristic q, if { u_i } is a family of elements of E which F-linearly spans E, then { u_i ^ (q ^ n) } also F-linearly spans E for any natural number n.

source

theorem LinearIndependent.map_pow_expChar_pow_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q n : ℕ) [hF : ExpChar F q] {ι : Type u_1} {v : ι → E} [Algebra.IsSeparable F E] (h : LinearIndependent F v) :

LinearIndependent F fun (x : ι) => v x ^ q ^ n

If E / F is a separable extension of exponential characteristic q, if { u_i } is a family of elements of E which is F-linearly independent, then { u_i ^ (q ^ n) } is also F-linearly independent for any natural number n.

source

theorem LinearIndependent.map_pow_expChar_pow_of_isSeparable' {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q n : ℕ) [hF : ExpChar F q] {ι : Type u_1} {v : ι → E} (hsep : ∀ (i : ι), IsSeparable F (v i)) (h : LinearIndependent F v) :

LinearIndependent F fun (x : ι) => v x ^ q ^ n

If E / F is a field extension of exponential characteristic q, if { u_i } is a family of separable elements of E which is F-linearly independent, then { u_i ^ (q ^ n) } is also F-linearly independent for any natural number n.

source

def Module.Basis.mapPowExpCharPowOfIsSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q n : ℕ) [hF : ExpChar F q] {ι : Type u_1} [Algebra.IsSeparable F E] (b : Basis ι F E) :

Basis ι F E

If E / F is a separable extension of exponential characteristic q, if { u_i } is an F-basis of E, then { u_i ^ (q ^ n) } is also an F-basis of E for any natural number n.

Equations

Instances For

source

theorem minpoly.iterateFrobenius_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] [ExpChar E q] (n : ℕ) {a : E} (hsep : IsSeparable F a) :

minpoly F ((iterateFrobenius E q n) a) = Polynomial.map (iterateFrobenius F q n) (minpoly F a)

For an extension E / F of exponential characteristic q and a separable element a : E, the minimal polynomial of a ^ q ^ n equals the minimal polynomial of a mapped via (⬝ ^ q ^ n).

source

theorem minpoly.frobenius_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] [ExpChar E q] {a : E} (hsep : IsSeparable F a) :

minpoly F ((frobenius E q) a) = Polynomial.map (frobenius F q) (minpoly F a)

For an extension E / F of exponential characteristic q and a separable element a : E, the minimal polynomial of a ^ q equals the minimal polynomial of a mapped via (⬝ ^ q).

source

theorem perfectField_of_perfectClosure_eq_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [h : PerfectField E] (eq : perfectClosure F E = ⊥) :

PerfectField F

source

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

PerfectField F

If E / F is a separable extension, E is perfect, then F is also perfect.

source

theorem perfectField_iff_isSeparable_algebraicClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsAlgClosure F E] :

PerfectField F ↔ Algebra.IsSeparable F E

If E is an algebraic closure of F, then F is perfect if and only if E / F is separable.

Documentation

Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Basic results about relative perfect closure #

Main definitions #

Main results #

Tags #