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]