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
    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.one_def {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] (X : C) :
    Mon_Class.one = 0
    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
      Instances For
        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
        @[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_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
        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
          Instances For
            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 X.X
            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 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
              Instances For
                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_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_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 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_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
                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 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_inverse_obj {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp_ C) :
                commGrpEquivalence.inverse.obj X = X.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