English
The Frobenius K-algebra endomorphism on R is given by the map r ↦ r^q.
Русский
Фробениус-алгебра-одномерность на R задаётся отображением r ↦ r^q.
LaTeX
$$frobeniusAlgHom K R = (λ r, r^q)$$
Lean4
/-- If `R` is an algebra over a finite field `K`, the Frobenius `K`-algebra endomorphism of `R` is
given by raising every element of `R` to its `#K`-th power. -/
@[simps!]
def frobeniusAlgHom : R →ₐ[K] R where
__ := powMonoidHom q
map_zero' := zero_pow Fintype.card_pos.ne'
map_add' _
_ := by
obtain ⟨p, _, _, hp, card_eq⟩ := card' K
nontriviality R
have : CharP R p := charP_of_injective_algebraMap' K R p
have : ExpChar R p := .prime hp
simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, powMonoidHom_apply, card_eq]
exact add_pow_expChar_pow ..
commutes' _ := by simp [← RingHom.map_pow, pow_card]
