English
For a finite field extension L/K, the map n ↦ frobeniusAlgHom^n is bijective from Fin (Module.finrank K L) to the automorphisms of L over K.
Русский
Для конечного расширения L/K отображение n ↦ frobeniusAlgHom^n является биекции между Fin (Module.finrank K L) и автоморфизмами L над K.
LaTeX
$$Function.Bijective fun n : Fin (Module.finrank K L) ↦ frobeniusAlgHom K L ^ n.1$$
Lean4
/-- The sum of `x ^ i` as `x` ranges over the units of a finite field of cardinality `q`
is equal to `0` unless `(q - 1) ∣ i`, in which case the sum is `q - 1`. -/
theorem sum_pow_units [DecidableEq K] (i : ℕ) : (∑ x : Kˣ, (x ^ i : K)) = if q - 1 ∣ i then -1 else 0 :=
by
let φ : Kˣ →* K :=
{ toFun := fun x => x ^ i
map_one' := by simp
map_mul' := by simp [mul_pow] }
have : Decidable (φ = 1) := by classical infer_instance
calc
(∑ x : Kˣ, φ x) = if φ = 1 then Fintype.card Kˣ else 0 := sum_hom_units φ
_ = if q - 1 ∣ i then -1 else 0 :=
by
suffices q - 1 ∣ i ↔ φ = 1 by
simp only [this]
split_ifs; swap
· exact Nat.cast_zero
· rw [Fintype.card_units, Nat.cast_sub, cast_card_eq_zero, Nat.cast_one, zero_sub]
show 1 ≤ q; exact Fintype.card_pos_iff.mpr ⟨0⟩
rw [← forall_pow_eq_one_iff, DFunLike.ext_iff]
apply forall_congr'; intro x; simp [φ, Units.ext_iff]
