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
- category_theory.forget₂.category_theory.full = {preimage := λ (A B : Module ℤ) (f : (category_theory.forget₂ (Module ℤ) AddCommGroup).obj A ⟶ (category_theory.forget₂ (Module ℤ) AddCommGroup).obj B), {to_fun := ⇑f, map_add' := _, map_smul' := _}, witness' := category_theory.forget₂.category_theory.full._proof_3}
@[instance]
The forgetful functor from ℤ modules to AddCommGroup is essentially surjective.
@[instance]