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₂AddCommGroupFull : CategoryTheory.Full (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGroupCat)

The forgetful functor from ℤ modules to AddCommGroup is full.

Equations

• One or more equations did not get rendered due to their size.

instance ModuleCat.forget₂_addCommGroupCat_essSurj : CategoryTheory.EssSurj (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGroupCat)

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

Equations

• ModuleCat.forget₂_addCommGroupCat_essSurj = (_ : CategoryTheory.EssSurj (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGroupCat))

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

Equations

• ModuleCat.forget₂AddCommGroupIsEquivalence = CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGroupCat)