English
There is a natural action of R' on Subalgebra R A given by applying the action to every element; i.e., a • S = map (MulSemiringAction.toAlgHom a) S.
Русский
Существует естественное действие кольца R' на Subalgebra(R,A), задаваемое отображением каждого элемента посредством соответствующего гомоморфа, т.е. a • S = map (MulSemiringAction.toAlgHom a) S.
LaTeX
$$protected_def pointwiseMulAction : MulAction R' (Subalgebra R A)$$
Lean4
/-- The action on a subalgebra corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulAction : MulAction R' (Subalgebra R A)
where
smul a S := S.map (MulSemiringAction.toAlgHom _ _ a)
one_smul S := (congr_arg (fun f => S.map f) (AlgHom.ext <| one_smul R')).trans S.map_id
mul_smul _a₁ _a₂ S := (congr_arg (fun f => S.map f) (AlgHom.ext <| mul_smul _ _)).trans (S.map_map _ _).symm
