algebra.category.Group.Z_Module_equivalence

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[protected, instance]

def Module.forget₂_AddCommGroup_full :

category_theory.full (category_theory.forget₂ (Module ℤ) AddCommGroup)

The forgetful functor from ℤ modules to AddCommGroup is full.

Equations

Module.forget₂_AddCommGroup_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' := Module.forget₂_AddCommGroup_full._proof_3}

source

@[protected, instance]

def Module.forget₂_AddCommGroup_ess_surj :

category_theory.ess_surj (category_theory.forget₂ (Module ℤ) AddCommGroup)

The forgetful functor from ℤ modules to AddCommGroup is essentially surjective.

source

@[protected, instance]

noncomputable def Module.forget₂_AddCommGroup_is_equivalence :

category_theory.is_equivalence (category_theory.forget₂ (Module ℤ) AddCommGroup)

Equations

Module.forget₂_AddCommGroup_is_equivalence = category_theory.equivalence.of_fully_faithfully_ess_surj (category_theory.forget₂ (Module ℤ) AddCommGroup)