English
If L/K is purely inseparable and L is finite dimensional over K, then there exists an exponent e such that for all a ∈ L, a^{ringExpChar(K)^{e - elemExponent(K,a)}} lies in the base-field range; this e is computable from ringExpChar(K) and [finrank_K L].
Русский
Если расширение L/K чисто нерасщепимо и L конечномерно над K, то существует экспонента e, такая что для всех a ∈ L, a^{ringExpChar(K)^{e - elemExponent(K,a)}} лежит в образе algebraMap_KL; вычисляется из ringExpChar(K) и размерности L над K.
LaTeX
$$$\\exists e:\\mathbb{N},\\ \\forall a\\in L:\\ a^{\\operatorname{ringExpChar}(K)^{\\left(e-\\operatorname{elemExponent}(K,a)\\right)}} \\in \\operatorname{range}(\\operatorname{algebraMap} K L)$$$
Lean4
instance hasExponent_of_finiteDimensional [IsPurelyInseparable K L] [FiniteDimensional K L] : HasExponent K L :=
by
let ⟨p, _⟩ := ExpChar.exists K
rcases ‹ExpChar K p› with _ | ⟨hp⟩
· exact ⟨0, fun a ↦ surjective_algebraMap_of_isSeparable K L _⟩
· let e := Nat.log (ringExpChar K) (Module.finrank K L)
refine ⟨e, fun a ↦ ⟨elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a), ?_⟩⟩
have h_elemexp_bound (a : L) : elemExponent K a ≤ e :=
Nat.le_log_of_pow_le (Nat.Prime.one_lt <| ringExpChar.eq K p ▸ hp)
(minpoly_natDegree_eq K a ▸ minpoly.natDegree_le a)
rw [RingHom.map_pow, algebraMap_elemReduct_eq, ← pow_mul, ← pow_add, Nat.add_sub_cancel' (h_elemexp_bound a)]
