The forgetful functor from ℤ-modules to additive commutative groups is an equivalence of categories.

TODO: either use this equivalence to transport the monoidal structure from Module ℤ to Ab, or, having constructed that monoidal structure directly, show this functor is monoidal.

instance ModuleCat.forget₂_addCommGroup_full : (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGrpCat).Full

The forgetful functor from ℤ modules to AddCommGrpCat is full.

instance ModuleCat.forget₂_addCommGrp_essSurj : (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGrpCat).EssSurj

The forgetful functor from ℤ modules to AddCommGrpCat is essentially surjective.

instance ModuleCat.forget₂AddCommGroupIsEquivalence : (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGrpCat).IsEquivalence