Documentation

Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence

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.

The forgetful functor from modules to AddCommGroupCat is essentially surjective.

Equations