Basic results about relative perfect closure #
This file contains basic results about relative perfect closures.
Main definitions #
perfectClosure: the relative perfect closure ofFinE, it consists of the elementsxofEsuch that there exists a natural numbernsuch thatx ^ (ringExpChar F) ^ nis contained inF, whereringExpChar Fis the exponential characteristic ofF. It is also the maximal purely inseparable subextension ofE / F(le_perfectClosure_iff).
Main results #
le_perfectClosure_iff: an intermediate field ofE / Fis contained in the relative perfect closure ofFinEif and only if it is purely inseparable overF.perfectClosure.perfectRing,perfectClosure.perfectField: ifEis a perfect field, then the (relative) perfect closureperfectClosure F Eis perfect.IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem: ifFis of exponential characteristicq, thenF(S) / Fis a purely inseparable extension if and only if for anyx ∈ S,x ^ (q ^ n)is contained inFfor somen : ℕ.
Tags #
separable degree, degree, separable closure, purely inseparable
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).
Equations
- perfectClosure F E = { toSubalgebra := have this := ⋯; Subalgebra.perfectClosure F E (ringExpChar F), inv_mem' := ⋯ }
Instances For
The relative perfect closure of F in E is purely inseparable over F.
The relative perfect closure of F in E is algebraic over F.
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.
An intermediate field of E / F is contained in the relative perfect closure of F in E
if it is purely inseparable over F.
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.
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.
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.
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.
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.
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
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.
Instances For
If E is a perfect field of exponential characteristic p, then the (relative) perfect closure
perfectClosure F E is perfect.
If E is a perfect field, then the (relative) perfect closure
perfectClosure F E is perfect.
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 : ℕ.
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 : ℕ.
A compositum of two purely inseparable extensions is purely inseparable.
A compositum of purely inseparable extensions is purely inseparable.
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.
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.
If E / F is a separable field extension of exponential characteristic q, then
F(S) = F(S ^ q) for any subset S of E.
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.
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.
If F is a field of exponential characteristic q, a : E is separable over F, then
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.
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.
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.
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.
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
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).
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).
If E / F is a separable extension, E is perfect, then F is also perfect.
If E is an algebraic closure of F, then F is perfect if and only if E / F is
separable.