English
There is a natural action of M on Subring R defined pointwise by a • S = map of S via a RingHom.
Русский
Существуют естественные действия M на Subring R, заданные точечно: a • S = отображение S через соответствующее кольцевое однородное отображение.
LaTeX
$$$\text{pointwiseMulAction}: M \curvearrowright \mathrm{Subring}(R)$$$
Lean4
/-- The action on a subring corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulAction : MulAction M (Subring R)
where
smul a S := S.map (MulSemiringAction.toRingHom _ _ a)
one_smul S := (congr_arg (fun f => S.map f) (RingHom.ext <| one_smul M)).trans S.map_id
mul_smul _ _ S := (congr_arg (fun f => S.map f) (RingHom.ext <| mul_smul _ _)).trans (S.map_map _ _).symm
