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
🔸 coverage
@[implicit_reducible]
instance CategoryTheory.Preadditive.instGrpObj {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] (X : C) :
GrpObj X
source
📐 coverage
@[simp]
theorem CategoryTheory.Preadditive.one_def {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] (X : C) :
MonObj.one = 0
source
📐 coverage
@[simp]
theorem CategoryTheory.Preadditive.inv_def {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] (X : C) :
GrpObj.inv = -CategoryStruct.id X
source
📐 coverage
@[simp]
theorem CategoryTheory.Preadditive.mul_def {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] (X : C) :
MonObj.mul = SemiCartesianMonoidalCategory.fst X X + SemiCartesianMonoidalCategory.snd X X
source
📐 coverage
instance CategoryTheory.Preadditive.instIsCommMonObj {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
IsCommMonObj X
source
🔸 coverage
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.

Instances For
    source
    📐 coverage
    @[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
    📐 coverage
    @[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 = instGrpObj X
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.Preadditive.toCommGrp_map (C : Type u) [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] {X Y : C} (f : X ⟶ Y) :
    (toCommGrp C).map f = InducedCategory.homMk (Grp.homMk'' f ⋯ ⋯)
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp C) :
      (commGrpEquivalenceAux.hom.app X).hom.hom.hom = CategoryStruct.id X.X
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp C) :
      (commGrpEquivalenceAux.inv.app X).hom.hom.hom = CategoryStruct.id X.X
      source
      🔸 coverage
      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.

      Instances For
        source
        📐 coverage
        @[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.hom.hom
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_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.hom.hom = f
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
        MonObj.mul = SemiCartesianMonoidalCategory.fst X X + SemiCartesianMonoidalCategory.snd X X
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
        MonObj.one = 0
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp C) :
        (commGrpEquivalence.counitIso.inv.app X).hom.hom.hom = CategoryStruct.id X.X
        source
        📐 coverage
        @[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
        📐 coverage
        @[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
        📐 coverage
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp C) :
        (commGrpEquivalence.counitIso.hom.app X).hom.hom.hom = CategoryStruct.id X.X
        source
        📐 coverage
        @[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
        📐 coverage
        @[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
        📐 coverage
        @[simp]
        theorem CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_inv {C : Type u} [Category.{v, u} C] [Preadditive C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) :
        GrpObj.inv = -CategoryStruct.id X