English
For a finite set L over K, the order of Frobenius endomorphism equals the finite rank (finrank) of L as a K-vector space.
Русский
Порядок Фробениуса как линейного отображения равен конечной размерности L как пространства над K.
LaTeX
$$orderOf (frobeniusAlgHom K L) = Module.finrank K L$$
Lean4
theorem orderOf_frobeniusAlgHom : orderOf (frobeniusAlgHom K L) = Module.finrank K L :=
(orderOf_eq_iff Module.finrank_pos).mpr <| by
have := Fintype.ofFinite L
refine ⟨DFunLike.ext _ _ fun x ↦ ?_, fun m lt pos eq ↦ ?_⟩
·
simp_rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply, ← Module.card_eq_pow_finrank,
pow_card]
have :=
card_le_degree_of_subset_roots (R := L) (p := X ^ q ^ m - X) (Z := univ) fun x _ ↦
by
simp_rw [mem_roots', IsRoot, eval_sub, eval_pow, eval_X]
have := DFunLike.congr_fun eq x
rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply, ← sub_eq_zero] at this
refine ⟨fun h ↦ ?_, this⟩
simpa [if_neg (Nat.one_lt_pow pos.ne' Fintype.one_lt_card).ne] using congr_arg (coeff · 1) h
refine
this.not_gt
(((natDegree_sub_le ..).trans_eq ?_).trans_lt <|
(Nat.pow_lt_pow_right Fintype.one_lt_card lt).trans_eq Module.card_eq_pow_finrank.symm)
simp [Nat.one_le_pow _ _ Fintype.card_pos]
