The forgetful functor (C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v) is an equivalence

This is true as long as C is additive.

Here, C ⥤ₗ D is the category of finite-limits-preserving functors from C to D.

To construct a functor from C ⥤ₗ Type v to C ⥤ₗ AddCommGrp.{v}, notice that a left-exact functor F : C ⥤ Type v induces a functor CommGrp_ C ⥤ CommGrp_ (Type v). But CommGrp_ C is equivalent to C, and CommGrp_ (Type v) is equivalent to AddCommGrp.{v}, so we turn this into a functor C ⥤ AddCommGrp.{v}. By construction, composing with with the forgetful functor recovers the functor we started with, so since the forgetful functor reflects finite limits and F preserves finite limits, our constructed functor also preserves finite limits. It can be shown that this construction gives a quasi-inverse to the whiskering operation (C ⥤ₗ AddCommGrp.{v}) ⥤ (C ⥤ₗ Type v).

noncomputable def AddCommGrp.leftExactFunctorForgetEquivalence.inverseAux {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Functor (C ⥤ₗ Type v) (CategoryTheory.Functor C AddCommGrp)

Implementation, see leftExactFunctorForgetEquivalence.

Equations

• One or more equations did not get rendered due to their size.

instance AddCommGrp.leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (F : C ⥤ₗ Type v) : CategoryTheory.Limits.PreservesFiniteLimits (inverseAux.obj F)

noncomputable def AddCommGrp.leftExactFunctorForgetEquivalence.inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Functor (C ⥤ₗ Type v) (C ⥤ₗ AddCommGrp)

Implementation, see leftExactFunctorForgetEquivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommGrp.leftExactFunctorForgetEquivalence.unitIsoAux {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (F : CategoryTheory.Functor C AddCommGrp) [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) : commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X)) ≅ (F.comp (CategoryTheory.forget AddCommGrp)).mapCommGrp.obj (CategoryTheory.Preadditive.commGrpEquivalence.functor.obj X)

Implementation, see leftExactFunctorForgetEquivalence. This is the complicated bit, where we show that forgetting the group structure in the image of F and then reconstructing it recovers the group structure we started with.

Equations

• AddCommGrp.leftExactFunctorForgetEquivalence.unitIsoAux F X = CommGrp_.mkIso Multiplicative.toAdd.toIso ⋯ ⋯

noncomputable def AddCommGrp.leftExactFunctorForgetEquivalence.unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Functor.id (C ⥤ₗ AddCommGrp) ≅ ((CategoryTheory.LeftExactFunctor.whiskeringRight C AddCommGrp (Type v)).obj (CategoryTheory.LeftExactFunctor.of (CategoryTheory.forget AddCommGrp))).comp inverse

Implementation, see leftExactFunctorForgetEquivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommGrp.leftExactFunctorForgetEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : C ⥤ₗ AddCommGrp ≌ C ⥤ₗ Type v

If C is an additive category, the forgetful functor (C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v) is an equivalence.

Equations

• One or more equations did not get rendered due to their size.