English
There is a natural equivalence between monoid homomorphisms from PushoutI φ to K and pairs (f, k) with f_i: G_i → K and k: H → K satisfying f_i ∘ φ_i = k for all i.
Русский
Существует естественное эквивалентное отображение между моноид-гомоморфизмами PushoutI φ →* K и парами (f, k), где f_i: G_i → K и k: H → K удовлетворяют f_i ∘ φ_i = k для всех i.
LaTeX
$$$Hom(PushoutI(\varphi),K) \cong { (f: Π_i G_i →* K) × (H →* K) \;|\; ∀ i, (f_i) ∘ φ_i = k }$$$
Lean4
@[ext high]
theorem hom_ext_nonempty [hn : Nonempty ι] {f g : PushoutI φ →* K}
(h : ∀ i, f.comp (of i : G i →* _) = g.comp (of i : G i →* _)) : f = g :=
hom_ext h <| by
cases hn with
| intro i =>
ext
rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]
