English
For any p and a, if a^{p^{n}} lies in the range, then a^{p^{n}} is outside the range whenever n < elemExponent(K,a).
Русский
Для любого p и a, если a^{p^{n}} лежит в образе, то при n < elemExponent(K,a) оно не лежит в образе.
LaTeX
$$$\text{If } n < \operatorname{elemExponent}(K,a),\ a^{p^{n}} \notin \operatorname{range}(\operatorname{algebraMap} K L)$$$
Lean4
/-- 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`. -/
noncomputable def iterateFrobenius {n : ℕ} (hn : exponent K L ≤ n) : L →+* K
where
toFun := iterateFrobeniusAux K L p n
map_zero' := by
apply (algebraMap K L).injective
rw [(algebraMap K L).map_zero, algebraMap_iterateFrobeniusAux K p hn 0, zero_pow]
exact Nat.pos_iff_ne_zero.mp <| expChar_pow_pos K p n
map_add' a
b := by
have inj := (algebraMap K L).injective
have : ExpChar L p := expChar_of_injective_ringHom inj p
apply inj
rw [(algebraMap K L).map_add, algebraMap_iterateFrobeniusAux K p hn a, algebraMap_iterateFrobeniusAux K p hn b,
algebraMap_iterateFrobeniusAux K p hn (a + b), add_pow_expChar_pow a b]
map_one' := by
apply (algebraMap K L).injective
rw [(algebraMap K L).map_one, algebraMap_iterateFrobeniusAux K p hn 1, one_pow]
map_mul' a
b := by
apply (algebraMap K L).injective
rw [(algebraMap K L).map_mul, algebraMap_iterateFrobeniusAux K p hn a, algebraMap_iterateFrobeniusAux K p hn b,
algebraMap_iterateFrobeniusAux K p hn (a * b), mul_pow]
