English
If E/F is separable with q-characteristic, then raising basis elements to q^n yields another F-basis of E.
Русский
Если расширение E/F разделяемое с характеристикой q, то возведение элементов базиса в степень q^n дает новый базис над F.
LaTeX
$$$\text{Basis}\; b\;\to\; \text{basis }(b^{q^n})$$$
Lean4
/-- If `E / F` is a separable extension of exponential characteristic `q`, if `{ u_i }` is a family
of elements of `E` which `F`-linearly spans `E`, then `{ u_i ^ (q ^ n) }` also `F`-linearly spans
`E` for any natural number `n`. -/
theorem span_map_pow_expChar_pow_eq_top_of_isSeparable [Algebra.IsSeparable F E]
(h : Submodule.span F (Set.range v) = ⊤) : Submodule.span F (Set.range (v · ^ q ^ n)) = ⊤ :=
by
rw [← Algebra.top_toSubmodule, ← top_toSubalgebra, ← adjoin_univ,
adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' F E _ q n,
adjoin_algebraic_toSubalgebra fun x _ ↦ Algebra.IsAlgebraic.isAlgebraic x, Set.image_univ, Algebra.adjoin_eq_span]
have := (MonoidHom.mrange (powMonoidHom (α := E) (q ^ n))).closure_eq
simp only [MonoidHom.mrange, powMonoidHom, MonoidHom.coe_mk, OneHom.coe_mk, Submonoid.coe_copy] at this
rw [this]
refine (Submodule.span_mono <| Set.range_comp_subset_range _ _).antisymm (Submodule.span_le.2 ?_)
rw [Set.range_comp, ← Set.image_univ]
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
apply h ▸ Submodule.image_span_subset_span (LinearMap.iterateFrobenius F E q n) _
