English
Given a separable extension, the basis after powering remains a basis.
Русский
Для разделяемого расширения базис после подъема сохраняет свойство базиса.
LaTeX
$$$\text{Basis}.map\_pow\_expChar\_pow\_of\_isSeparable$$$
Lean4
/-- If `E / F` is a field extension of exponential characteristic `q`, if `{ u_i }` is a
family of separable elements of `E` which is `F`-linearly independent, then `{ u_i ^ (q ^ n) }`
is also `F`-linearly independent for any natural number `n`. -/
theorem map_pow_expChar_pow_of_isSeparable' (hsep : ∀ i : ι, IsSeparable F (v i)) (h : LinearIndependent F v) :
LinearIndependent F (v · ^ q ^ n) := by
let E' := adjoin F (Set.range v)
haveI : Algebra.IsSeparable F E' := (isSeparable_adjoin_iff_isSeparable F _).2 <| by rintro _ ⟨y, rfl⟩; exact hsep y
let v' (i : ι) : E' := ⟨v i, subset_adjoin F _ ⟨i, rfl⟩⟩
have h' : LinearIndependent F v' := h.of_comp E'.val.toLinearMap
exact
(h'.map_pow_expChar_pow_of_isSeparable q n).map' E'.val.toLinearMap
(LinearMap.ker_eq_bot_of_injective E'.val.injective)
