English
Let K and L be fields with K finite and L finite over K. Then the map from Fin(finrank_K L) to Aut_K(L) given by n ↦ (frobeniusAlgEquivOfAlgebraic K L)^{n.1} is bijective, i.e., the powers of Frobenius enumerate all K-algebra automorphisms of L.
Русский
Пусть K и L — поля, над которыми K конечно, и L конечно как расширение над K. Тогда отображение из Fin(finrank_K L) в Aut_K(L), заданное n ↦ (frobeniusAlgEquivOfAlgebraic K L)^{n.1}, биективно: степени Фробениуса образуют всю группе автоморфизмов над K.
LaTeX
$$$\\operatorname{Bijective}\\left( n \\mapsto \\operatorname{frobeniusAlgEquivOfAlgebraic}(K,L)^{n.1} \\right)$$$
Lean4
theorem bijective_frobeniusAlgEquivOfAlgebraic_pow :
Function.Bijective fun n : Fin (Module.finrank K L) ↦ frobeniusAlgEquivOfAlgebraic K L ^ n.1 :=
((Algebra.IsAlgebraic.algEquivEquivAlgHom K L).bijective.of_comp_iff' _).mp <| by
simpa only [Function.comp_def, map_pow] using bijective_frobeniusAlgHom_pow K L
