English
If h is a monoid homomorphism and f,g are as above with commuting images, then h ∘ (f.noncommCoprod g) equals (h ∘ f).noncommCoprod (h ∘ g) with the induced commutation.
Русский
Если h — гомоморфизм моноидов, а f,g удовлетворяют условиям, то композиция h с копродуктом равна копродукту композиции своих компонентов с адаптированным условием коммютирования.
LaTeX
$$$ h \\circ (f.noncommCoprod g\\, comm) = (h \\circ f).noncommCoprod (h \\circ g) (\\lambda m n, (comm m n).map h). $$$
Lean4
@[to_additive]
theorem comp_noncommCoprod {Q : Type*} [Semigroup Q] (h : P →ₙ* Q) (comm : ∀ m n, Commute (f m) (g n)) :
h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) (fun m n ↦ (comm m n).map h) :=
ext fun _ => map_mul h _ _
