English
For a group action, we obtain a representation of G in the automorphism group of A.V, i.e., a monoid hom G → Aut(A.V).
Русский
Для групповского действия получаем отображение группы в группу автоморфизмов A.V, то есть гомоморфизм моноида G → Aut(A.V).
LaTeX
$$$\rho_{\mathrm{Aut}}: G \to^* \mathrm{Aut}(A.V)$ is a monoid hom$$
Lean4
/-- When a group acts, we can lift the action to the group of automorphisms. -/
@[simps]
def ρAut {G : Type*} [Group G] (A : Action V G) : G →* Aut A.V
where
toFun
g :=
{ hom := A.ρ g
inv := A.ρ (g⁻¹ : G)
hom_inv_id := (A.ρ.map_mul (g⁻¹ : G) g).symm.trans (by rw [inv_mul_cancel, ρ_one])
inv_hom_id := (A.ρ.map_mul g (g⁻¹ : G)).symm.trans (by rw [mul_inv_cancel, ρ_one]) }
map_one' := Aut.ext A.ρ.map_one
map_mul' x y := Aut.ext (A.ρ.map_mul x y)
