English
The expression f : M →* N →* P and g : Q →* N yields a two-argument composition described by compr₂. This is the monoid homomorphism M →* Q →* P sending m to the monoid hom q ↦ f(m)(g(q)).
Русский
Выражение f: M →* N →* P и g: Q →* N задают композицию двух аргументов, обозначаемую compr₂. Это моноидоморфизм M →* Q →* P, который отправляет m в моноидоморфизм q ↦ f(m)(g(q)).
LaTeX
$$$\\mathrm{compr}_2 : M \\to^* N \\to^* P \\;→\\; Q \\to^* N \\to^* P, \\quad \\mathrm{compr}_2(f,g)(m)(q) = g(f(m)(q)).$$$
Lean4
/-- The expression `fun m q ↦ f m (g q)` as a `MonoidHom`.
Note that the expression `fun q n ↦ f (g q) n` is simply `MonoidHom.comp`. -/
@[to_additive /-- The expression `fun m q ↦ f m (g q)` as an `AddMonoidHom`.
Note that the expression `fun q n ↦ f (g q) n` is simply `AddMonoidHom.comp`.
This also exists as a `LinearMap` version, `LinearMap.compl₂` -/
]
def compl₂ [MulOneClass M] [MulOneClass N] [CommMonoid P] [MulOneClass Q] (f : M →* N →* P) (g : Q →* N) :
M →* Q →* P :=
(compHom' g).comp f
