English
Let M →* N and N →* P be monoid homomorphisms with M a MulOneClass, N and P CommMonoids. Then the map compHom: (N →* P) →* (M →* N) →* M →* P given by toFun g := { toFun := g ∘ -, map_one' := comp_one g, map_mul' := comp_mul g } defines a monoid homomorphism. Equivalently, g ↦ (− ↦ g ∘ (−)) is a monoid homomorphism.
Русский
Пусть существуют моноидоморофизмы M →* N и N →* P; тогда отображение compHom: (N →* P) →* (M →* N) →* M →* P, задаваемое toFun g := { toFun := g ∘ -, ... }, образует моноидоморфизм. Эквивалентно: g ↦ (h ↦ g ∘ h) образует моноидоморфизм.
LaTeX
$$$\\mathrm{compHom} : (N \\to^* P) \\to^* (M \\to^* N) \\to^* M \\to^* P, \\quad (\\mathrm{compHom}(g))(f) = g \\circ f.$$$
Lean4
/-- Composition of monoid morphisms (`MonoidHom.comp`) as a monoid morphism.
Note that unlike `MonoidHom.comp_hom'` this requires commutativity of `N`. -/
@[to_additive (attr := simps) /-- Composition of additive monoid morphisms (`AddMonoidHom.comp`) as an additive
monoid morphism.
Note that unlike `AddMonoidHom.comp_hom'` this requires commutativity of `N`.
This also exists in a `LinearMap` version, `LinearMap.llcomp`. -/
]
def compHom [MulOneClass M] [CommMonoid N] [CommMonoid P] : (N →* P) →* (M →* N) →* M →* P
where
toFun g := { toFun := g.comp, map_one' := comp_one g, map_mul' := comp_mul g }
map_one' := by
ext1 f
exact one_comp f
map_mul' g₁
g₂ := by
ext1 f
exact mul_comp g₁ g₂ f
