English
Let σ: L →ₐ[K] L be a K-algebra endomorphism of finite order n. Then the minimal polynomial of σ considered as a K-linear map is X^n − 1.
Русский
Пусть σ: L →ₐ[K] L — концевой порядок конечной мощности алгебраически над K, тогда минимальный полином линейного отображения σ равен X^n − 1.
LaTeX
$$$\minpoly_K(\sigma^{\text{toLinearMap}}) = X^{\operatorname{orderOf}(\sigma)} - 1$$$
Lean4
/-- The minimal polynomial (over `K`) of `σ : Gal(L/K)` is `X ^ (orderOf σ) - 1`. -/
theorem minpoly_algHom_toLinearMap (σ : L →ₐ[K] L) (hσ : IsOfFinOrder σ) :
minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1 :=
by
have : orderOf σ = orderOf (AlgEquiv.algHomUnitsEquiv _ _ hσ.unit) :=
by
rw [← MonoidHom.coe_coe, orderOf_injective, ← orderOf_units, IsOfFinOrder.val_unit]
exact (AlgEquiv.algHomUnitsEquiv K L).injective
rw [this, ← minpoly_algEquiv_toLinearMap]
· apply congr_arg
ext
simp
· rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff]
