Documentation

Mathlib.CategoryTheory.Preadditive.CommGrp_

Commutative group objects in additive categories. #

We construct an inverse of the forgetful functor CommGrp_ C ⥤ C if C is an additive category.

This looks slightly strange because the additive structure of C maps to the multiplicative structure of the commutative group objects.

source
instance CategoryTheory.Preadditive.instGrp_Class {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] (X : C) :
Grp_Class X
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Preadditive.one_def {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] (X : C) :
Mon_Class.one = 0
source
@[simp]
theorem CategoryTheory.Preadditive.inv_def {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] (X : C) :
Grp_Class.inv = -CategoryStruct.id X
source
@[simp]
theorem CategoryTheory.Preadditive.mul_def {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] (X : C) :
Mon_Class.mul = CartesianMonoidalCategory.fst X X + CartesianMonoidalCategory.snd X X
source
instance CategoryTheory.Preadditive.instIsCommMon {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
IsCommMon X
source
def CategoryTheory.Preadditive.toCommGrp (C : Type u) [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] :
Functor C (CommGrp_ C)

The canonical functor from an additive category into its commutative group objects. This is always an equivalence, see commGrpEquivalence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Preadditive.toCommGrp_obj_grp (C : Type u) [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
    ((toCommGrp C).obj X).grp = instGrp_Class X
    source
    @[simp]
    theorem CategoryTheory.Preadditive.toCommGrp_map_hom (C : Type u) [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] {X Y : C} (f : X ⟶ Y) :
    ((toCommGrp C).map f).hom = f
    source
    @[simp]
    theorem CategoryTheory.Preadditive.toCommGrp_obj_X (C : Type u) [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
    ((toCommGrp C).obj X).X = X
    source
    def CategoryTheory.Preadditive.commGrpEquivalenceAux {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] :
    (CommGrp_.forget C).comp (toCommGrp C) ≅ Functor.id (CommGrp_ C)

    Auxiliary definition for commGrpEquivalence.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp_ C) :
      (commGrpEquivalenceAux.hom.app X).hom = CategoryStruct.id ((Grp_.forget₂Mon_ C).obj ((CommGrp_.forget₂Grp_ C).obj X)).X
      source
      @[simp]
      theorem CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp_ C) :
      (commGrpEquivalenceAux.inv.app X).hom = CategoryStruct.id ((Grp_.forget₂Mon_ C).obj ((CommGrp_.forget₂Grp_ C).obj X)).X
      source
      def CategoryTheory.Preadditive.commGrpEquivalence {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] :
      C ≌ CommGrp_ C

      An additive category is equivalent to its category of commutative group objects.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_inverse_obj {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp_ C) :
        commGrpEquivalence.inverse.obj X = ((Grp_.forget₂Mon_ C).obj ((CommGrp_.forget₂Grp_ C).obj X)).X
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
        Mon_Class.mul = CartesianMonoidalCategory.fst X X + CartesianMonoidalCategory.snd X X
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp_ C) :
        (commGrpEquivalence.counitIso.inv.app X).hom = CategoryStruct.id ((Grp_.forget₂Mon_ C).obj ((CommGrp_.forget₂Grp_ C).obj X)).X
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] {X Y : C} (f : X ⟶ Y) :
        (commGrpEquivalence.functor.map f).hom = f
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
        Mon_Class.one = 0
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp_ C) :
        (commGrpEquivalence.counitIso.hom.app X).hom = CategoryStruct.id ((Grp_.forget₂Mon_ C).obj ((CommGrp_.forget₂Grp_ C).obj X)).X
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_unitIso_hom_app {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
        commGrpEquivalence.unitIso.hom.app X = CategoryStruct.id X
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_X {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
        (commGrpEquivalence.functor.obj X).X = X
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_inverse_map {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : CommGrp_ C} (f : X✝ ⟶ Y✝) :
        commGrpEquivalence.inverse.map f = f.hom
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_unitIso_inv_app {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
        commGrpEquivalence.unitIso.inv.app X = CategoryStruct.id X
        source
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_inv {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
        Grp_Class.inv = -CategoryStruct.id X