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 ℤ) AddCommGrp).Full

The forgetful functor from ℤ modules to AddCommGrp is full.

Equations

• ModuleCat.forget₂_addCommGroup_full = ⋯

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

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

Equations

• ModuleCat.forget₂_addCommGrp_essSurj = ⋯

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

Equations

• ModuleCat.forget₂AddCommGroupIsEquivalence = ⋯