English
Under separability, powering basis elements preserves linear independence and spanning.
Русский
При разделяемости возведение элементов базиса сохраняет линейную независимость и пространство порождений.
LaTeX
$$$\text{linearIndependent} \bigl( \text{pow}^{q^n} (b) \bigr)$ and spanning property$$
Lean4
/-- 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)`. -/
theorem iterateFrobenius_of_isSeparable [ExpChar E q] (n : ℕ) {a : E} (hsep : IsSeparable F a) :
minpoly F (iterateFrobenius E q n a) = (minpoly F a).map (iterateFrobenius F q n) :=
by
have hai : IsIntegral F a := hsep.isIntegral
have hapi : IsIntegral F (iterateFrobenius E q n a) := hai.pow _
symm
refine
Polynomial.eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic hapi) (minpoly.monic hai |>.map _)
(minpoly.dvd F (a ^ q ^ n) ?haeval) ?hdeg
· simpa using Eq.symm <| (minpoly F a).map_aeval_eq_aeval_map (RingHom.iterateFrobenius_comm _ q n) a
·
rw [(minpoly F a).natDegree_map_eq_of_injective (iterateFrobenius F q n).injective, ←
IntermediateField.adjoin.finrank hai,
IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable F E hsep q n, ←
IntermediateField.adjoin.finrank hapi, iterateFrobenius_def]
