English
The forgetful functor from the category of Z-modules to AddCommGrpCat is full; every additive group hom between underlying abelian groups lifts to a Z-linear map.
Русский
Функтор забывания из категории Z-модулей в AddCommGrpCat полно; каждый аддитивный гомоморфизм между базовыми абелевыми группами поднимается до Z-линейного отображения.
LaTeX
$$$\forall A,B : \mathrm{ModuleCat}_\mathbb{Z},\; \mathrm{Hom}_{\mathrm{AddCommGrpCat}}(A,B) \\ni f \\exists \tilde f : \mathrm{Hom}_{\mathrm{ModuleCat}_\mathbb{Z}}(A,B) \\text{such that forget}(\tilde f) = f$$$
Lean4
/-- The forgetful functor from `ℤ` modules to `AddCommGrpCat` is full. -/
instance forget₂_addCommGroup_full : (forget₂ (ModuleCat ℤ) AddCommGrpCat.{u}).Full where
map_surjective
{A B}
-- `AddMonoidHom.toIntLinearMap` doesn't work here because `A` and `B` are not
-- definitionally equal to the canonical `AddCommGroup.toIntModule` module
-- instances it expects.
f :=
⟨@ModuleCat.ofHom _ _ _ _ _ A.isModule _ B.isModule <|
@LinearMap.mk _ _ _ _ _ _ _ _ _ A.isModule B.isModule { toFun := f, map_add' := AddMonoidHom.map_add f.hom }
(fun n x => by convert AddMonoidHom.map_zsmul f.hom x n <;> ext <;> apply int_smul_eq_zsmul),
rfl⟩
