English
Under separability, the same basis maps to a basis after raising to q^n.
Русский
При разделяемости тот же базис отображается в базис после возведения в q^n.
LaTeX
$$$\text{Basis}.map\_pow\_expChar\_pow\_of\_isSeparable$$$
Lean4
/-- If `E / F` is a separable extension of exponential characteristic `q`, if `{ u_i }` is a
family of 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 [Algebra.IsSeparable F E] (h : LinearIndependent F v) :
LinearIndependent F (v · ^ q ^ n) := by
classical
rw [linearIndependent_iff_finset_linearIndependent] at h ⊢
intro s
let E' := adjoin F (s.image v : Set E)
haveI : FiniteDimensional F E' := finiteDimensional_adjoin fun x _ ↦ Algebra.IsIntegral.isIntegral x
haveI : Algebra.IsSeparable F E' := Algebra.isSeparable_tower_bot_of_isSeparable F E' E
let v' (i : s) : E' := ⟨v i.1, subset_adjoin F _ (Finset.mem_image.2 ⟨i.1, i.2, rfl⟩)⟩
have h' : LinearIndependent F v' := (h s).of_comp E'.val.toLinearMap
exact
(h'.map_pow_expChar_pow_of_fd_isSeparable q n).map' E'.val.toLinearMap
(LinearMap.ker_eq_bot_of_injective E'.val.injective)
