English
Any two morphisms f,g: AddCommGrpCat.of ℤ ⟶ G are equal if and only if they agree on 1; i.e., the map from ℤ determines a morphism to G.
Русский
Любые две гомоморфизмы f,g: AddCommGrpCat.of ℤ ⟶ G равны тогда и только тогда, когда они согласны на 1; то есть образ ℤ полностью определяет гомоморфизм в G.
LaTeX
$$$$ \forall G:\mathrm{AddCommGrpCat},\ f,g:\mathrm{AddCommGrpCat.of} \mathbb{Z} \to G,\ w: f(1) = g(1) \Rightarrow f = g. $$$$
Lean4
@[ext]
theorem int_hom_ext {G : AddCommGrpCat.{0}} (f g : AddCommGrpCat.of ℤ ⟶ G) (w : f (1 : ℤ) = g (1 : ℤ)) : f = g :=
hom_ext
(AddMonoidHom.ext_int w)
-- TODO: this argument should be generalised to the situation where
-- the forgetful functor is representable.
