English
The action of a monoid α on Subgroup G is given by mapping each subgroup S to S.map(f) where f is the endomorphism corresponding to α.
Русский
Действие моноида α на Subgroup G задается отображением S → S.map(f), где f — отображение-автоморфизм, соответствующее α.
LaTeX
$$$\\text{The action is } (a,S)\\mapsto S.map(\\text{MulDistribMulAction.toMonoidEnd } a)$.$$
Lean4
/-- The action on a subgroup corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulAction : MulAction α (Subgroup G)
where
smul a S := S.map (MulDistribMulAction.toMonoidEnd _ _ a)
one_smul
S := by
change S.map _ = S
simpa only [map_one] using S.map_id
mul_smul _ _ S := (congr_arg (fun f : Monoid.End G => S.map f) (MonoidHom.map_mul _ _ _)).trans (S.map_map _ _).symm
