Documentation

Mathlib.CategoryTheory.GradedObject

The category of graded objects #

For any type β, a β-graded object over some category C is just a function β → C into the objects of C. We put the "pointwise" category structure on these, as the non-dependent specialization of CategoryTheory.Pi.

We describe the comap functors obtained by precomposing with functions β → γ.

As a consequence a fixed element (e.g. 1) in an additive group β provides a shift functor on β-graded objects

When C has coproducts we construct the total functor GradedObject β C ⥤ C, show that it is faithful, and deduce that when C is concrete so is GradedObject β C.

A covariant functoriality of GradedObject β C with respect to the index set β is also introduced: if p : I → J is a map such that C has coproducts indexed by p ⁻¹' {j}, we have a functor map : GradedObject I C ⥤ GradedObject J C.

def CategoryTheory.GradedObject (β : Type w) (C : Type u) :
Type (max w u)

A type synonym for β → C, used for β-graded objects in a category C.

Equations
Instances For
    Equations
    @[reducible, inline]
    abbrev CategoryTheory.GradedObjectWithShift {β : Type w} [AddCommGroup β] :
    βType u → Type (max w u)

    A type synonym for β → C, used for β-graded objects in a category C with a shift functor given by translation by s.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.GradedObject.categoryOfGradedObjects_comp {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) :
      ∀ {X Y Z : (i : β) → (fun (x : β) => C) i} (f : X Y) (g : Y Z) (i : β), CategoryTheory.CategoryStruct.comp f g i = CategoryTheory.CategoryStruct.comp (f i) (g i)
      theorem CategoryTheory.GradedObject.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} {X : CategoryTheory.GradedObject β C} {Y : CategoryTheory.GradedObject β C} (f : X Y) (g : X Y) (h : ∀ (x : β), f x = g x) :
      f = g
      @[simp]

      The projection of a graded object to its i-th component.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.GradedObject.isoMk_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} (X : CategoryTheory.GradedObject β C) (Y : CategoryTheory.GradedObject β C) (e : (i : β) → X i Y i) (i : β) :
        (X.isoMk Y e).hom i = (e i).hom
        @[simp]
        theorem CategoryTheory.GradedObject.isoMk_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} (X : CategoryTheory.GradedObject β C) (Y : CategoryTheory.GradedObject β C) (e : (i : β) → X i Y i) (i : β) :
        (X.isoMk Y e).inv i = (e i).inv
        def CategoryTheory.GradedObject.isoMk {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} (X : CategoryTheory.GradedObject β C) (Y : CategoryTheory.GradedObject β C) (e : (i : β) → X i Y i) :
        X Y

        Constructor for isomorphisms in GradedObject

        Equations
        • X.isoMk Y e = { hom := fun (i : β) => (e i).hom, inv := fun (i : β) => (e i).inv, hom_inv_id := , inv_hom_id := }
        Instances For
          @[simp]
          theorem CategoryTheory.Iso.map_hom_inv_id_eval_app_assoc {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] {X : CategoryTheory.GradedObject J C} {Y : CategoryTheory.GradedObject J C} (e : X Y✝) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (j : J) (Y : D) {Z : E} (h : (F.obj (X j)).obj Y Z) :
          CategoryTheory.CategoryStruct.comp ((F.map (e.hom j)).app Y) (CategoryTheory.CategoryStruct.comp ((F.map (e.inv j)).app Y) h) = h
          @[simp]
          theorem CategoryTheory.Iso.map_inv_hom_id_eval_app_assoc {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] {X : CategoryTheory.GradedObject J C} {Y : CategoryTheory.GradedObject J C} (e : X Y✝) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (j : J) (Y : D) {Z : E} (h : (F.obj (Y✝ j)).obj Y Z) :
          CategoryTheory.CategoryStruct.comp ((F.map (e.inv j)).app Y) (CategoryTheory.CategoryStruct.comp ((F.map (e.hom j)).app Y) h) = h
          @[simp]
          @[reducible, inline]

          Pull back an I-graded object in C to a J-graded object along a function J → I.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.GradedObject.comapEq_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} {f : βγ} {g : βγ} (h : f = g) (X : CategoryTheory.GradedObject γ C) (b : β) :
            @[simp]
            theorem CategoryTheory.GradedObject.comapEq_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} {f : βγ} {g : βγ} (h : f = g) (X : CategoryTheory.GradedObject γ C) (b : β) :

            The natural isomorphism comparing between pulling back along two propositionally equal functions.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem CategoryTheory.GradedObject.eqToHom_apply (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {X : βC} {Y : βC} (h : X = Y) (b : β) :

              The equivalence between β-graded objects and γ-graded objects, given an equivalence between β and γ.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                @[simp]
                theorem CategoryTheory.GradedObject.shiftFunctor_obj_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} [AddCommGroup β] (s : β) (X : βC) (t : β) (n : ) :

                The total object of a graded object is the coproduct of the graded components.

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

                  The total functor taking a graded object to the coproduct of its graded components is faithful. To prove this, we need to know that the coprojections into the coproduct are monomorphisms, which follows from the fact we have zero morphisms and decidable equality for the grading.

                  Equations
                  • =
                  @[reducible, inline]
                  abbrev CategoryTheory.GradedObject.mapObjFun {I : Type u_1} {J : Type u_2} {C : Type u_4} (X : CategoryTheory.GradedObject I C) (p : IJ) (j : J) (i : (p ⁻¹' {j})) :
                  C

                  If X : GradedObject I C and p : I → J, X.mapObjFun p j is the family of objects X i for i : I such that p i = j.

                  Equations
                  • X.mapObjFun p j i = X i
                  Instances For
                    @[reducible, inline]

                    Given X : GradedObject I C and p : I → J, X.HasMap p is the condition that for all j : J, the coproduct of all X i such p i = j exists.

                    Equations
                    Instances For
                      theorem CategoryTheory.GradedObject.hasMap_of_iso {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (e : X Y) (p : IJ) [X.HasMap p] :
                      Y.HasMap p
                      noncomputable def CategoryTheory.GradedObject.mapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] :

                      Given X : GradedObject I C and p : I → J, X.mapObj p is the graded object by J which in degree j consists of the coproduct of the X i such that p i = j.

                      Equations
                      • X.mapObj p j = X.mapObjFun p j
                      Instances For
                        noncomputable def CategoryTheory.GradedObject.ιMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] (i : I) (j : J) (hij : p i = j) :
                        X i X.mapObj p j

                        The canonical inclusion X i ⟶ X.mapObj p j when i : I and j : J are such that p i = j.

                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev CategoryTheory.GradedObject.CofanMapObjFun {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) (j : J) :
                          Type (max (max u_4 u_5) u_1)

                          Given X : GradedObject I C, p : I → J and j : J, CofanMapObjFun X p j is the type Cofan (X.mapObjFun p j). The point object of such colimits cofans are isomorphic to X.mapObj p j, see CofanMapObjFun.iso.

                          Equations
                          Instances For
                            def CategoryTheory.GradedObject.CofanMapObjFun.mk {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) (j : J) (pt : C) (ι' : (i : I) → p i = j(X i pt)) :
                            X.CofanMapObjFun p j

                            Constructor for CofanMapObjFun X p j.

                            Equations
                            Instances For
                              noncomputable def CategoryTheory.GradedObject.cofanMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] (j : J) :
                              X.CofanMapObjFun p j

                              The tautological cofan corresponding to the coproduct decomposition of X.mapObj p j.

                              Equations
                              Instances For
                                noncomputable def CategoryTheory.GradedObject.isColimitCofanMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] (j : J) :

                                Given X : GradedObject I C, p : I → J and j : J, X.mapObj p j satisfies the universal property of the coproduct of those X i such that p i = j.

                                Equations
                                Instances For
                                  theorem CategoryTheory.GradedObject.mapObj_ext {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] {A : C} {j : J} (f : X.mapObj p j A) (g : X.mapObj p j A) (hfg : ∀ (i : I) (hij : p i = j), CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) f = CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) g) :
                                  f = g
                                  noncomputable def CategoryTheory.GradedObject.descMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j(X i A)) :
                                  X.mapObj p j A

                                  This is the morphism X.mapObj p j ⟶ A constructed from a family of morphisms X i ⟶ A for all i : I such that p i = j.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.GradedObject.ι_descMapObj_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j(X i A)) (i : I) (hi : p i = j) {Z : C} (h : A Z) :
                                    @[simp]
                                    theorem CategoryTheory.GradedObject.ι_descMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j(X i A)) (i : I) (hi : p i = j) :
                                    CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (X.descMapObj p φ) = φ i hi
                                    theorem CategoryTheory.GradedObject.CofanMapObjFun.hasMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) (c : (j : J) → X.CofanMapObjFun p j) (hc : (j : J) → CategoryTheory.Limits.IsColimit (c j)) :
                                    X.HasMap p
                                    noncomputable def CategoryTheory.GradedObject.CofanMapObjFun.iso {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {p : IJ} {j : J} {c : X.CofanMapObjFun p j} (hc : CategoryTheory.Limits.IsColimit c) [X.HasMap p] :
                                    c.pt X.mapObj p j

                                    If c : CofanMapObjFun X p j is a colimit cofan, this is the induced isomorphism c.pt ≅ X.mapObj p j.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {p : IJ} {j : J} {c : X.CofanMapObjFun p j} (hc : CategoryTheory.Limits.IsColimit c) [X.HasMap p] (i : I) (hi : p i = j) {Z : C} (h : X.mapObj p j Z) :
                                      @[simp]
                                      theorem CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {p : IJ} {j : J} {c : X.CofanMapObjFun p j} (hc : CategoryTheory.Limits.IsColimit c) [X.HasMap p] (i : I) (hi : p i = j) :
                                      @[simp]
                                      @[simp]
                                      theorem CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {p : IJ} {j : J} {c : X.CofanMapObjFun p j} (hc : CategoryTheory.Limits.IsColimit c) [X.HasMap p] (i : I) (hi : p i = j) :
                                      noncomputable def CategoryTheory.GradedObject.mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (φ : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] :
                                      X.mapObj p Y.mapObj p

                                      The canonical morphism of J-graded objects X.mapObj p ⟶ Y.mapObj p induced by a morphism X ⟶ Y of I-graded objects and a map p : I → J.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.GradedObject.ι_mapMap_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (φ : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] (i : I) (j : J) (hij : p i = j) {Z : C} (h : Y.mapObj p j Z) :
                                        @[simp]
                                        theorem CategoryTheory.GradedObject.ι_mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (φ : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] (i : I) (j : J) (hij : p i = j) :
                                        theorem CategoryTheory.GradedObject.congr_mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (p : IJ) [X.HasMap p] [Y.HasMap p] (φ₁ : X Y) (φ₂ : X Y) (h : φ₁ = φ₂) :
                                        @[simp]
                                        theorem CategoryTheory.GradedObject.mapIso_inv {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (e : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] (i : J) :
                                        @[simp]
                                        theorem CategoryTheory.GradedObject.mapIso_hom {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (e : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] (i : J) :
                                        noncomputable def CategoryTheory.GradedObject.mapIso {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (e : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] :
                                        X.mapObj p Y.mapObj p

                                        The isomorphism of J-graded objects X.mapObj p ≅ Y.mapObj p induced by an isomorphism X ≅ Y of graded objects and a map p : I → J.

                                        Equations
                                        Instances For

                                          Given a map p : I → J, this is the functor GradedObject I C ⥤ GradedObject J C which sends an I-object X to the graded object X.mapObj p which in degree j : J is given by the coproduct of those X i such that p i = j.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def CategoryTheory.GradedObject.cofanMapObjComp {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) (q : JK) (r : IK) (hpqr : ∀ (i : I), q (p i) = r i) (k : K) (c : (j : J) → q j = kX.CofanMapObjFun p j) (c' : CategoryTheory.Limits.Cofan fun (j : (q ⁻¹' {k})) => (c j ).pt) :
                                            X.CofanMapObjFun r k

                                            Given maps p : I → J, q : J → K and r : I → K such that q.comp p = r, X : GradedObject I C, k : K, the datum of cofans X.CofanMapObjFun p j for all j : J and of a cofan for all the points of these cofans, this is a cofan of type X.CofanMapObjFun r k, which is a colimit (see isColimitCofanMapObjComp) if the given cofans are.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def CategoryTheory.GradedObject.isColimitCofanMapObjComp {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) (q : JK) (r : IK) (hpqr : ∀ (i : I), q (p i) = r i) (k : K) (c : (j : J) → q j = kX.CofanMapObjFun p j) (hc : (j : J) → (hj : q j = k) → CategoryTheory.Limits.IsColimit (c j hj)) (c' : CategoryTheory.Limits.Cofan fun (j : (q ⁻¹' {k})) => (c j ).pt) (hc' : CategoryTheory.Limits.IsColimit c') :
                                              CategoryTheory.Limits.IsColimit (X.cofanMapObjComp p q r hpqr k c c')

                                              Given maps p : I → J, q : J → K and r : I → K such that q.comp p = r, X : GradedObject I C, k : K, the cofan constructed by cofanMapObjComp is a colimit. In other words, if we have, for all j : J such that hj : q j = k, a colimit cofan c j hj which computes the coproduct of the X i such that p i = j, and also a colimit cofan which computes the coproduct of the points of these c j hj, then the point of this latter cofan computes the coproduct of the X i such that r i = k.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem CategoryTheory.GradedObject.hasMap_comp {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) (q : JK) (r : IK) (hpqr : ∀ (i : I), q (p i) = r i) [X.HasMap p] [(X.mapObj p).HasMap q] :
                                                X.HasMap r
                                                noncomputable def CategoryTheory.GradedObject.ιMapObjOrZero {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) :
                                                X i X.mapObj p j

                                                The canonical inclusion X i ⟶ X.mapObj p j when p i = j, the zero morphism otherwise.

                                                Equations
                                                • X.ιMapObjOrZero p i j = if h : p i = j then X.ιMapObj p i j h else 0
                                                Instances For
                                                  theorem CategoryTheory.GradedObject.ιMapObjOrZero_eq {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) (h : p i = j) :
                                                  X.ιMapObjOrZero p i j = X.ιMapObj p i j h
                                                  theorem CategoryTheory.GradedObject.ιMapObjOrZero_eq_zero {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] (X : CategoryTheory.GradedObject I C) (p : IJ) [X.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) (h : p i j) :
                                                  X.ιMapObjOrZero p i j = 0
                                                  @[simp]
                                                  theorem CategoryTheory.GradedObject.ιMapObjOrZero_mapMap_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (φ : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) {Z : C} (h : Y.mapObj p j Z) :
                                                  @[simp]
                                                  theorem CategoryTheory.GradedObject.ιMapObjOrZero_mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] {X : CategoryTheory.GradedObject I C} {Y : CategoryTheory.GradedObject I C} (φ : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) :
                                                  CategoryTheory.CategoryStruct.comp (X.ιMapObjOrZero p i j) (CategoryTheory.GradedObject.mapMap φ p j) = CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObjOrZero p i j)