English
If f : M →⋆ P and g : N →⋆ P are monoid homomorphisms whose images commute pairwise, then the map (m,n) ↦ f(m) g(n) defines a monoid homomorphism from M × N to P.
Русский
Если f : M →* P и g : N →* P — гомоморфизмы моноидов, чьи образцы попарно commute, то отображение (m,n) ↦ f(m) g(n) задаёт гомоморфизм от прямого произведения M × N к P.
LaTeX
$$$\\text{If } f : M \\to\\!* P, \\; g : N \\to\\!* P \\text{ and } \\forall m,n,\\; \\mathrm{Commute}(f(m), g(n)), \\text{ then } f.noncommCoprod g comm:\\ M \\times N \\to P \\text{ is a monoid hom with } (m,n) \\mapsto f(m)g(n).$$$
Lean4
/-- Coproduct of two `MulHom`s with the same codomain with `Commute` assumption:
`f.noncommCoprod g _ (p : M × N) = f p.1 * g p.2`.
(For the commutative case, use `MulHom.coprod`) -/
@[to_additive (attr := simps) /-- Coproduct of two `AddHom`s with the same codomain with `AddCommute` assumption:
`f.noncommCoprod g _ (p : M × N) = f p.1 + g p.2`.
(For the commutative case, use `AddHom.coprod`) -/
]
def noncommCoprod (comm : ∀ m n, Commute (f m) (g n)) : M × N →ₙ* P
where
toFun mn := f mn.fst * g mn.snd
map_mul' mn mn' := by simpa using (comm _ _).mul_mul_mul_comm _ _
