The exponent of a finite purely inseparable extension is bounded by its degree

Let L / K be a finite purely inseparable extension in exponential characteristic p. If [L : K] ≤ p ^ n, then every p ^ n-th power of L lies in K, and so the exponent of L / K is at most n. In particular a purely inseparable extension of degree p ^ n is cut out by p ^ n-th powers.

Mathlib's IsPurelyInseparable.hasExponent_of_finiteDimensional shows that a finite purely inseparable extension has an exponent, but keeps the bound inside the instance proof. This file states the bound, in the pointwise form a caller holding a degree uses and as a bound on IsPurelyInseparable.exponent.

Main results

• TauCeti.IsPurelyInseparable.pow_mem_of_finrank_le_pow: if [L : K] ≤ p ^ n, every p ^ n-th power of L lies in K.
• TauCeti.IsPurelyInseparable.exponent_le_of_finrank_le_pow: if [L : K] ≤ p ^ n, the exponent of L / K is at most n.

theorem TauCeti.IsPurelyInseparable.pow_mem_of_finrank_le_pow (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] [FiniteDimensional K L] (p : ℕ) [ExpChar K p] {n : ℕ} (h : Module.finrank K L ≤ p ^ n) (a : L) : a ^ p ^ n ∈ (algebraMap K L).range

A purely inseparable extension of degree at most p ^ n is cut out by p ^ n-th powers: every a ^ p ^ n lies in the base field.

theorem TauCeti.IsPurelyInseparable.exponent_le_of_finrank_le_pow (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsPurelyInseparable K L] [FiniteDimensional K L] (p : ℕ) [ExpChar K p] {n : ℕ} (h : Module.finrank K L ≤ p ^ n) : IsPurelyInseparable.exponent K L ≤ n

The exponent of a purely inseparable extension of degree at most p ^ n is at most n.