Documentation

Mathlib.CategoryTheory.GradedObject.Single

The graded object in a single degree #

In this file, we define the functor GradedObject.single j : C ⥤ GradedObject J C which sends an object X : C to the graded object which is X in degree j and the initial object of C in other degrees.

source
noncomputable def CategoryTheory.GradedObject.single {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) :
Functor C (GradedObject J C)

The functor which sends X : C to the graded object which is X in degree j and the initial object in other degrees.

Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev CategoryTheory.GradedObject.single₀ (J : Type u_1) {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] [Zero J] :
      Functor C (GradedObject J C)

      The functor which sends X : C to the graded object which is X in degree 0 and the initial object in nonzero degrees.

      Equations
        Instances For
          source
          noncomputable def CategoryTheory.GradedObject.singleObjApplyIsoOfEq {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) (i : J) (h : i = j) :
          (single j).obj X i ≅ X

          The canonical isomorphism (single j).obj X i ≅ X when i = j.

          Equations
            Instances For
              source
              @[reducible, inline]
              noncomputable abbrev CategoryTheory.GradedObject.singleObjApplyIso {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) :
              (single j).obj X j ≅ X

              The canonical isomorphism (single j).obj X j ≅ X.

              Equations
                Instances For
                  source
                  noncomputable def CategoryTheory.GradedObject.isInitialSingleObjApply {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) (i : J) (h : i ≠ j) :
                  Limits.IsInitial ((single j).obj X i)

                  The object (single j).obj X i is initial when i ≠ j.

                  Equations
                    Instances For
                      source
                      theorem CategoryTheory.GradedObject.singleObjApplyIsoOfEq_inv_single_map {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) (i : J) (h : i = j) :
                      CategoryStruct.comp (singleObjApplyIsoOfEq j X i h).inv ((single j).map f i) = CategoryStruct.comp f (singleObjApplyIsoOfEq j Y i h).inv
                      source
                      theorem CategoryTheory.GradedObject.single_map_singleObjApplyIsoOfEq_hom {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) (i : J) (h : i = j) :
                      CategoryStruct.comp ((single j).map f i) (singleObjApplyIsoOfEq j Y i h).hom = CategoryStruct.comp (singleObjApplyIsoOfEq j X i h).hom f
                      source
                      @[simp]
                      theorem CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) :
                      CategoryStruct.comp (singleObjApplyIso j X).inv ((single j).map f j) = CategoryStruct.comp f (singleObjApplyIso j Y).inv
                      source
                      @[simp]
                      theorem CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map_assoc {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (single j).obj Y j ⟶ Z) :
                      CategoryStruct.comp (singleObjApplyIso j X).inv (CategoryStruct.comp ((single j).map f j) h) = CategoryStruct.comp f (CategoryStruct.comp (singleObjApplyIso j Y).inv h)
                      source
                      @[simp]
                      theorem CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) :
                      CategoryStruct.comp ((single j).map f j) (singleObjApplyIso j Y).hom = CategoryStruct.comp (singleObjApplyIso j X).hom f
                      source
                      @[simp]
                      theorem CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom_assoc {J : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) :
                      CategoryStruct.comp ((single j).map f j) (CategoryStruct.comp (singleObjApplyIso j Y).hom h) = CategoryStruct.comp (singleObjApplyIso j X).hom (CategoryStruct.comp f h)
                      source
                      noncomputable def CategoryTheory.GradedObject.singleCompEval {J : Type u_1} (C : Type u_2) [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) :
                      (single j).comp (eval j) ≅ Functor.id C

                      The composition of the single functor single j : C ⥤ GradedObject J C and the evaluation functor eval j identifies to the identity functor.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.GradedObject.singleCompEval_hom_app {J : Type u_1} (C : Type u_2) [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) :
                          (singleCompEval C j).hom.app X = (singleObjApplyIso j X).hom
                          source
                          @[simp]
                          theorem CategoryTheory.GradedObject.singleCompEval_inv_app {J : Type u_1} (C : Type u_2) [Category.{u_3, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) :
                          (singleCompEval C j).inv.app X = (singleObjApplyIso j X).inv