English
Given a monoid hom f: M →* N, the map compHom'(f): (N →* P) →* M →* P sends a monoid hom g: N →* P to the composite g ∘ f: M →* P. This construction is itself a monoid hom (upon suitable commutativity assumptions on N and P).
Русский
Для гомоморфизма моноидов f: M →* N отображение compHom'(f): (N →* P) →* M →* P отправляет гомоморфизм g: N →* P в композицию g ∘ f: M →* P. Это построение само по себе образует моноидоморфизм (при соответствующих условиях на коммутативность N и P).
LaTeX
$$$\\mathrm{compHom}'(f) : (N \\to^* P) \\to^* M \\to^* P \\quad\\text{with}\\quad (\\mathrm{compHom}'(f))(g) = g \\circ f.$$$
Lean4
/-- The expression `fun g m ↦ g (f m)` as a `MonoidHom`.
Equivalently, `(fun g ↦ MonoidHom.comp g f)` as a `MonoidHom`. -/
@[to_additive (attr := simps!) /-- The expression `fun g m ↦ g (f m)` as an `AddMonoidHom`.
Equivalently, `(fun g ↦ AddMonoidHom.comp g f)` as an `AddMonoidHom`.
This also exists in a `LinearMap` version, `LinearMap.lcomp`. -/
]
def compHom' [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* N) : (N →* P) →* M →* P :=
flip <| eval.comp f
