mathlib documentation

algebra.category.Group.Z_Module_equivalence

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]

The forgetful functor from modules to AddCommGroup is full.

Equations
@[instance]

The forgetful functor from modules to AddCommGroup is essentially surjective.