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.
Equations
- category_theory.forget₂.category_theory.ess_surj = {obj_preimage := λ (A : AddCommGroup), Module.of ℤ ↥A, iso' := λ (A : AddCommGroup), {hom := 𝟙 A, inv := 𝟙 A, hom_inv_id' := _, inv_hom_id' := _}}
@[instance]