English
Let F: J ⥤ AddCommGrpCat and α an AddMonoid. Then any two additive monoid homomorphisms f, g: Quot F →+ α are equal provided they agree on all generators, i.e., for every j ∈ J and every x ∈ F.obj j, f (Quot.ι F j x) = g (Quot.ι F j x).
Русский
Пусть F: J ⥤ AddCommGrpCat и α — добавочная моноидная группа. Тогда любые два моноид-хомоморфизма f, g: Quot F →+ α равны, если они совпадают на всех генераторах, т.е. для каждого j ∈ J и каждого x ∈ F.obj j выполняется f(Quot.ι F j x) = g(Quot.ι F j x).
LaTeX
$$$ f = g $ \quad\text{если}\quad \forall j:\!J,\forall x:\!F.obj j,\ f(\mathrm{Quot}.\mathrm{ι} F j x) = g(\mathrm{Quot}.\mathrm{ι} F j x). $$$
Lean4
theorem addMonoidHom_ext [DecidableEq J] {α : Type*} [AddMonoid α] {f g : Quot F →+ α}
(h : ∀ (j : J) (x : F.obj j), f (Quot.ι F j x) = g (Quot.ι F j x)) : f = g :=
QuotientAddGroup.addMonoidHom_ext _ (DFinsupp.addHom_ext h)
