English
Coproduct of two MonoidHomorphisms with a commuting condition defines a monoid homomorphism on the product M × N sending (m,n) to f(m) g(n).
Русский
Копродукт двух MonoidHom с условием коммутирования задаёт гомоморфизм моноидов на произведение M × N, отправляющий (m,n) в f(m)g(n).
LaTeX
$$$\\text{noncommCoprod} : (M,N) \\to P \\\\text{defined by } (m,n) \\mapsto f(m)g(n) \\text{ with } \\forall m,n, f(m)g(n) = g(n)f(m) \\text{ when commuting holds.}$$$
Lean4
/-- Coproduct of two `MonoidHom`s with the same codomain,
with a commutation assumption:
`f.noncommCoprod g _ (p : M × N) = f p.1 * g p.2`.
(Noncommutative case; in the commutative case, use `MonoidHom.coprod`.) -/
@[to_additive (attr := simps) /-- Coproduct of two `AddMonoidHom`s with the same codomain,
with a commutation assumption:
`f.noncommCoprod g (p : M × N) = f p.1 + g p.2`.
(Noncommutative case; in the commutative case, use `AddHom.coprod`.) -/
]
def noncommCoprod : M × N →* P where
toFun := fun mn ↦ (f mn.fst) * (g mn.snd)
map_one' := by simp only [Prod.fst_one, Prod.snd_one, map_one, mul_one]
__ := f.toMulHom.noncommCoprod g.toMulHom comm
