The exponent of purely inseparable extensions

This file defines the exponent of a purely inseparable extension (if one exists) and some related results.

Most results are stated using ringExpChar K rather than using [ExpChar K p] parameter because it gives cleaner API. To use the results in a context with [ExpChar K p], consider using ringExpChar.eq K p for substitution.

Main definitions

• IsPurelyInseparable.HasExponent: typeclass to assert a purely inseparable field extension L / K has an exponent, that is a smallest natural number e such that a ^ ringExpChar K ^ e ∈ K for all a ∈ L.
• IsPurelyInseparable.exponent: the exponent of a purely inseparable field extension.
• IsPurelyInseparable.elemExponent: the exponent of an element of a purely inseparable field extension, that is the smallest natural number e such that a ^ ringExpChar K ^ e ∈ K.
• IsPurelyInseparable.iterateFrobenius: the iterated Frobenius map (ring homomorphism) L →+* K for purely inseparable field extension L / K with exponent; for n ≥ exponent K L, it acts like x ↦ x ^ p ^ n but the codomain is the base field K.
• IsPurelyInseparable.iterateFrobeniusₛₗ: version of iterateFrobenius as a semilinear map over a subfield F of K, wrt the iterated Frobenius homomorphism on F.

Tags

purely inseparable

class IsPurelyInseparable.HasExponent (K : Type u_2) (L : Type u_3) [CommRing K] [Ring L] [Algebra K L] : Prop

A predicate class on a ring extension saying that there is a natural number e such that a ^ ringExpChar K ^ e ∈ K for all a ∈ L.

• has_exponent : ∃ (e : ℕ), ∀ (a : L), a ^ ringExpChar K ^ e ∈ (algebraMap K L).range

theorem IsPurelyInseparable.hasExponent_iff (K : Type u_2) (L : Type u_3) [CommRing K] [Ring L] [Algebra K L] : HasExponent K L ↔ ∃ (e : ℕ), ∀ (a : L), a ^ ringExpChar K ^ e ∈ (algebraMap K L).range

theorem IsPurelyInseparable.hasExponent_iff' (K : Type u_2) (L : Type u_3) [CommRing K] [Ring L] [Algebra K L] (p : ℕ) [ExpChar K p] : HasExponent K L ↔ ∃ (e : ℕ), ∀ (a : L), a ^ p ^ e ∈ (algebraMap K L).range

Version of hasExponent_iff using ExpChar.

noncomputable def IsPurelyInseparable.exponent (K : Type u_2) (L : Type u_3) [CommRing K] [Ring L] [Algebra K L] [HasExponent K L] : ℕ

The exponent of a purely inseparable extension is the smallest natural number e such that a ^ ringExpChar K ^ e ∈ K for all a ∈ L.

theorem IsPurelyInseparable.exponent_def (K : Type u_2) {L : Type u_3} [CommRing K] [Ring L] [Algebra K L] [HasExponent K L] (a : L) : a ^ ringExpChar K ^ exponent K L ∈ (algebraMap K L).range

theorem IsPurelyInseparable.exponent_def' (K : Type u_2) {L : Type u_3} [CommRing K] [Ring L] [Algebra K L] [HasExponent K L] (p : ℕ) [ExpChar K p] (a : L) : a ^ p ^ exponent K L ∈ (algebraMap K L).range

Version of exponent_def using ExpChar.

theorem IsPurelyInseparable.exponent_min {K : Type u_2} {L : Type u_3} [CommRing K] [Ring L] [Algebra K L] [HasExponent K L] {e : ℕ} (h : e < exponent K L) : ∃ (a : L), a ^ ringExpChar K ^ e ∉ (algebraMap K L).range

theorem IsPurelyInseparable.exponent_min' {K : Type u_2} {L : Type u_3} [CommRing K] [Ring L] [Algebra K L] [HasExponent K L] (p : ℕ) [ExpChar K p] {e : ℕ} (h : e < exponent K L) : ∃ (a : L), a ^ p ^ e ∉ (algebraMap K L).range

Version of exponent_min using ExpChar.

instance IsPurelyInseparable.instOfHasExponent (K : Type u_2) (L : Type u_3) [Field K] [Ring L] [IsDomain L] [Algebra K L] [HasExponent K L] : IsPurelyInseparable K L

noncomputable def IsPurelyInseparable.elemExponent (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (a : L) : ℕ

The exponent of an element a ∈ L of a purely inseparable field extension L / K is the smallest natural number e such that a ^ ringExpChar K ^ e ∈ K.

theorem IsPurelyInseparable.elemExponent_eq_zero_of_mem_range {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] {a : L} (h : a ∈ (algebraMap K L).range) : elemExponent K a = 0

theorem IsPurelyInseparable.elemExponent_eq_zero_of_charZero (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (a : L) [CharZero K] : elemExponent K a = 0

noncomputable def IsPurelyInseparable.elemReduct (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (a : L) : K

The element y of the base field K such that a ^ ringExpChar K ^ elemExponent K a = algebraMap K L y. See IsPurelyInseparable.algebraMap_elemReduct_eq.

theorem IsPurelyInseparable.minpoly_eq (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (a : L) : minpoly K a = Polynomial.X ^ ringExpChar K ^ elemExponent K a - Polynomial.C (elemReduct K a)

theorem IsPurelyInseparable.minpoly_eq' (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] (a : L) : minpoly K a = Polynomial.X ^ p ^ elemExponent K a - Polynomial.C (elemReduct K a)

Version of minpoly_eq using ExpChar.

theorem IsPurelyInseparable.minpoly_natDegree_eq (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (a : L) : (minpoly K a).natDegree = ringExpChar K ^ elemExponent K a

The degree of the minimal polynomial of an element a ∈ L equals ringExpChar K ^ elemExponent K a.

theorem IsPurelyInseparable.minpoly_natDegree_eq' (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] (a : L) : (minpoly K a).natDegree = p ^ elemExponent K a

Version of minpoly_natDegree_eq using ExpChar.

theorem IsPurelyInseparable.algebraMap_elemReduct_eq (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (a : L) : (algebraMap K L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a

theorem IsPurelyInseparable.algebraMap_elemReduct_eq' (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] (a : L) : (algebraMap K L) (elemReduct K a) = a ^ p ^ elemExponent K a

Version of algebraMap_elemReduct_eq using ExpChar.

theorem IsPurelyInseparable.elemExponent_def (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (a : L) : a ^ ringExpChar K ^ elemExponent K a ∈ (algebraMap K L).range

theorem IsPurelyInseparable.elemExponent_def' (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] (a : L) : a ^ p ^ elemExponent K a ∈ (algebraMap K L).range

Version of elemExponent_def using ExpChar.

theorem IsPurelyInseparable.elemExponent_le_of_pow_mem {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] {a : L} {n : ℕ} (h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range) : elemExponent K a ≤ n

theorem IsPurelyInseparable.elemExponent_le_of_pow_mem' {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] {a : L} {n : ℕ} (h : a ^ p ^ n ∈ (algebraMap K L).range) : elemExponent K a ≤ n

Version of elemExponent_le_of_pow_mem using ExpChar.

theorem IsPurelyInseparable.elemExponent_min {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] {a : L} {n : ℕ} (h : n < elemExponent K a) : a ^ ringExpChar K ^ n ∉ (algebraMap K L).range

theorem IsPurelyInseparable.elemExponent_min' (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] {a : L} {n : ℕ} (h : n < elemExponent K a) : a ^ p ^ n ∉ (algebraMap K L).range

Version of elemExponent_min using ExpChar.

theorem IsPurelyInseparable.elemExponent_le_exponent (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] [HasExponent K L] (a : L) : elemExponent K a ≤ exponent K L

An exponent of an element is less or equal than exponent of the extension.

instance IsPurelyInseparable.hasExponent_of_finiteDimensional {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] [FiniteDimensional K L] : HasExponent K L

noncomputable def IsPurelyInseparable.iterateFrobenius (K : Type u_2) (L : Type u_3) [Field K] [Field L] [Algebra K L] [HasExponent K L] (p : ℕ) [ExpChar K p] {n : ℕ} (hn : exponent K L ≤ n) : L →+* K

Iterated Frobenius map (ring homomorphism) for purely inseparable field extension with exponent. If n ≥ exponent K L, it acts like x ↦ x ^ p ^ n but the codomain is the base field K.

theorem IsPurelyInseparable.algebraMap_iterateFrobenius (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [HasExponent K L] (p : ℕ) [ExpChar K p] {n : ℕ} (hn : exponent K L ≤ n) (a : L) : (algebraMap K L) ((iterateFrobenius K L p hn) a) = a ^ p ^ n

Action of iterateFrobenius on the top field.

theorem IsPurelyInseparable.iterateFrobenius_algebraMap {K : Type u_2} (L : Type u_3) [Field K] [Field L] [Algebra K L] [HasExponent K L] (p : ℕ) [ExpChar K p] {n : ℕ} (hn : exponent K L ≤ n) (a : K) : (iterateFrobenius K L p hn) ((algebraMap K L) a) = a ^ p ^ n

Action of iterateFrobenius on the bottom field.

noncomputable def IsPurelyInseparable.iterateFrobeniusₛₗ (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field K] [Field L] [Algebra K L] [HasExponent K L] (p : ℕ) [ExpChar K p] [Field F] [Algebra F K] [Algebra F L] [IsScalarTower F K L] [ExpChar F p] {n : ℕ} (hn : exponent K L ≤ n) : L →ₛₗ[_root_.iterateFrobenius F p n] K

Version of iterateFrobenius as a semilinear map over a subfield F of K, wrt the iterated Frobenius homomorphism on F.

theorem IsPurelyInseparable.algebraMap_iterateFrobeniusₛₗ (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field K] [Field L] [Algebra K L] [HasExponent K L] (p : ℕ) [ExpChar K p] [Field F] [Algebra F K] [Algebra F L] [IsScalarTower F K L] [ExpChar F p] {n : ℕ} (hn : exponent K L ≤ n) (a : L) : (algebraMap K L) ((iterateFrobeniusₛₗ F K L p hn) a) = a ^ p ^ n

Action of iterateFrobeniusₛₗ on the top field.

theorem IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field K] [Field L] [Algebra K L] [HasExponent K L] (p : ℕ) [ExpChar K p] [Field F] [Algebra F K] [Algebra F L] [IsScalarTower F K L] [ExpChar F p] {n : ℕ} (hn : exponent K L ≤ n) (a : K) : (iterateFrobeniusₛₗ F K L p hn) ((algebraMap K L) a) = a ^ p ^ n

Action of iterateFrobeniusₛₗ on the bottom field.

theorem IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap_base (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field K] [Field L] [Algebra K L] [HasExponent K L] (p : ℕ) [ExpChar K p] [Field F] [Algebra F K] [Algebra F L] [IsScalarTower F K L] [ExpChar F p] {n : ℕ} (hn : exponent K L ≤ n) (a : F) : (iterateFrobeniusₛₗ F K L p hn) ((algebraMap F L) a) = (algebraMap F K) a ^ p ^ n

Action of iterateFrobeniusₛₗ on the base field.