English
Given a monoid hom h: H →* G and a slash action of β on α with respect to G, there is a canonical slash action of β on α coming from composing g ↦ h(g).
Русский
Для гомоморфизма моноидов h: H →* G существует естественное slash-действие β на α, получаемое за счёт композиции g ↦ h(g).
LaTeX
$$$\text{map}_h(k,g,a) = \text{SlashAction.map}(k, h(g), a)$ and the corresponding zero_slash, slash_one, slash_mul, add_slash are defined by composing with h.$$
Lean4
/-- Slash_action induced by a monoid homomorphism. -/
def monoidHomSlashAction {β G H α : Type*} [Monoid G] [AddMonoid α] [Monoid H] [SlashAction β G α] (h : H →* G) :
SlashAction β H α where
map k g := SlashAction.map k (h g)
zero_slash k g := SlashAction.zero_slash k (h g)
slash_one k a := by simp only [map_one, SlashAction.slash_one]
slash_mul k g gg a := by simp only [map_mul, SlashAction.slash_mul]
add_slash _ g _ _ := SlashAction.add_slash _ (h g) _ _
