English
The expression g ∘ f m n, with f : M →* N →* P and g : P →* Q, can be packaged as a single monoid homomorphism compr₂ f g : M →* N →* Q, given by compr₂(f,g)(m)(n) = g(f(m)(n)).
Русский
Выражение g ∘ f m n с f: M →* N →* P и g: P →* Q может быть представлено как один моноидоморфизм compr₂ f g : M →* N →* Q, задаваемый compr₂(f,g)(m)(n) = g(f(m)(n)).
LaTeX
$$$\\mathrm{compr}_2(f,g) : M \\to^* N \\to^* Q, \\quad (\\mathrm{compr}_2(f,g))(m)(n) = g(f(m)(n)).$$$
Lean4
/-- The expression `fun m n ↦ g (f m n)` as a `MonoidHom`. -/
@[to_additive /-- The expression `fun m n ↦ g (f m n)` as an `AddMonoidHom`.
This also exists as a `LinearMap` version, `LinearMap.compr₂` -/
]
def compr₂ [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M →* N →* P) (g : P →* Q) : M →* N →* Q :=
(compHom g).comp f
