Documentation

Mathlib.CategoryTheory.GradedObject.Trifunctor

The action of trifunctors on graded objects #

Given a trifunctor F. C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ and types I₁, I₂ and I₃, we define a functor GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject (I₁ × I₂ × I₃) C₄ (see mapTrifunctor). When we have a map p : I₁ × I₂ × I₃ → J and suitable coproducts exists, we define a functor GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject J C₄ (see mapTrifunctorMap) which sends graded objects X₁, X₂, X₃ to the graded object which sets j to the coproduct of the objects ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) for p ⟨i₁, i₂, i₃⟩ = j.

This shall be used in order to construct the associator isomorphism for the monoidal category structure on GradedObject I C induced by a monoidal structure on C and an additive monoid structure on I (TODO @joelriou).

@[simp]
theorem CategoryTheory.GradedObject.mapTrifunctorObj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_13, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} (X₁ : CategoryTheory.GradedObject I₁ C₁) (I₂ : Type u_8) (I₃ : Type u_9) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (x : I₁ × I₂ × I₃) :
((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃ x = ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).obj (X₃ x.2.2)
@[simp]
theorem CategoryTheory.GradedObject.mapTrifunctorObj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_13, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} (X₁ : CategoryTheory.GradedObject I₁ C₁) (I₂ : Type u_8) (I₃ : Type u_9) {X₂ : CategoryTheory.GradedObject I₂ C₂} {Y₂ : CategoryTheory.GradedObject I₂ C₂} (φ : X₂ Y₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (x : I₁ × I₂ × I₃) :
((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).map φ).app X₃ x = ((F.obj (X₁ x.1)).map (φ x.2.1)).app (X₃ x.2.2)
@[simp]
theorem CategoryTheory.GradedObject.mapTrifunctorObj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_13, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} (X₁ : CategoryTheory.GradedObject I₁ C₁) (I₂ : Type u_8) (I₃ : Type u_9) (X₂ : CategoryTheory.GradedObject I₂ C₂) {X₃ : CategoryTheory.GradedObject I₃ C₃} {Y₃ : CategoryTheory.GradedObject I₃ C₃} (φ : X₃ Y₃) (x : I₁ × I₂ × I₃) :
((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).map φ x = ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).map (φ x.2.2)

Auxiliary definition for mapTrifunctor.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.GradedObject.mapTrifunctor_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_13, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) (I₁ : Type u_7) (I₂ : Type u_8) (I₃ : Type u_9) {X₁ : CategoryTheory.GradedObject I₁ C₁} {Y₁ : CategoryTheory.GradedObject I₁ C₁} (φ : X₁ Y₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (x : I₁ × I₂ × I₃) :
    (((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).map φ).app X₂).app X₃ x = ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2)

    Given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ and types I₁, I₂, I₃, this is the obvious functor GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject (I₁ × I₂ × I₃) C₄.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.GradedObject.mapTrifunctorMapNatTrans_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_13, u_4} C₄] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} {F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} (α : F F') (I₁ : Type u_7) (I₂ : Type u_8) (I₃ : Type u_9) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (i : I₁ × I₂ × I₃) :
      (((CategoryTheory.GradedObject.mapTrifunctorMapNatTrans α I₁ I₂ I₃).app X₁).app X₂).app X₃ i = ((α.app (X₁ i.1)).app (X₂ i.2.1)).app (X₃ i.2.2)

      The natural transformation mapTrifunctor F I₁ I₂ I₃ ⟶ mapTrifunctor F' I₁ I₂ I₃ induced by a natural transformation F ⟶ F of trifunctors.

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

        The natural isomorphism mapTrifunctor F I₁ I₂ I₃ ≅ mapTrifunctor F' I₁ I₂ I₃ induced by a natural isomorphism F ≅ F of trifunctors.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def CategoryTheory.GradedObject.mapTrifunctorMapObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] :

          Given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₃, graded objects X₁ : GradedObject I₁ C₁, X₂ : GradedObject I₂ C₂, X₃ : GradedObject I₃ C₃, and a map p : I₁ × I₂ × I₃ → J, this is the J-graded object sending j to the coproduct of ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) for p ⟨i₁, i₂, i₃⟩ = k.

          Equations
          Instances For
            noncomputable def CategoryTheory.GradedObject.ιMapTrifunctorMapObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : p (i₁, i₂, i₃) = j) [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] :
            ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j

            The obvious inclusion ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p X₁ X₂ X₃ j when p ⟨i₁, i₂, i₃⟩ = j.

            Equations
            Instances For
              noncomputable def CategoryTheory.GradedObject.mapTrifunctorMapMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) {X₁ : CategoryTheory.GradedObject I₁ C₁} {Y₁ : CategoryTheory.GradedObject I₁ C₁} (f₁ : X₁ Y₁) {X₂ : CategoryTheory.GradedObject I₂ C₂} {Y₂ : CategoryTheory.GradedObject I₂ C₂} (f₂ : X₂ Y₂) {X₃ : CategoryTheory.GradedObject I₃ C₃} {Y₃ : CategoryTheory.GradedObject I₃ C₃} (f₃ : X₃ Y₃) [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p] :

              The maps mapTrifunctorMapObj F p X₁ X₂ X₃ ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ which express the functoriality of mapTrifunctorMapObj, see mapTrifunctorMap

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.GradedObject.ι_mapTrifunctorMapMap_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) {X₁ : CategoryTheory.GradedObject I₁ C₁} {Y₁ : CategoryTheory.GradedObject I₁ C₁} (f₁ : X₁ Y₁) {X₂ : CategoryTheory.GradedObject I₂ C₂} {Y₂ : CategoryTheory.GradedObject I₂ C₂} (f₂ : X₂ Y₂) {X₃ : CategoryTheory.GradedObject I₃ C₃} {Y₃ : CategoryTheory.GradedObject I₃ C₃} (f₃ : X₃ Y₃) [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : p (i₁, i₂, i₃) = j) {Z : C₄} (h : CategoryTheory.GradedObject.mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j Z) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapTrifunctorMapMap F p f₁ f₂ f₃ j) h) = CategoryTheory.CategoryStruct.comp (((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h✝) h)))
                @[simp]
                theorem CategoryTheory.GradedObject.ι_mapTrifunctorMapMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) {X₁ : CategoryTheory.GradedObject I₁ C₁} {Y₁ : CategoryTheory.GradedObject I₁ C₁} (f₁ : X₁ Y₁) {X₂ : CategoryTheory.GradedObject I₂ C₂} {Y₂ : CategoryTheory.GradedObject I₂ C₂} (f₂ : X₂ Y₂) {X₃ : CategoryTheory.GradedObject I₃ C₃} {Y₃ : CategoryTheory.GradedObject I₃ C₃} (f₃ : X₃ Y₃) [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : p (i₁, i₂, i₃) = j) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.GradedObject.mapTrifunctorMapMap F p f₁ f₂ f₃ j) = CategoryTheory.CategoryStruct.comp (((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)))
                theorem CategoryTheory.GradedObject.mapTrifunctorMapObj_ext {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} {Y : C₄} (j : J) [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] {φ : CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j Y} {φ' : CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j Y} (h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h) φ') :
                φ = φ'
                instance CategoryTheory.GradedObject.instHasMapProdObjFunctorMapTrifunctorObjOfMapTrifunctor {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [h : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] :
                (((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃).HasMap p
                Equations
                • = h
                @[simp]
                theorem CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) (X₁ : CategoryTheory.GradedObject I₁ C₁) [∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] (X₂ : CategoryTheory.GradedObject I₂ C₂) {X₃ : CategoryTheory.GradedObject I₃ C₃} {Y₃ : CategoryTheory.GradedObject I₃ C₃} (φ : X₃ Y₃) (i : J) :
                @[simp]
                theorem CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) (X₁ : CategoryTheory.GradedObject I₁ C₁) [∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) :
                @[simp]
                theorem CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) (X₁ : CategoryTheory.GradedObject I₁ C₁) [∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] {X₂ : CategoryTheory.GradedObject I₂ C₂} {Y₂ : CategoryTheory.GradedObject I₂ C₂} (φ : X₂ Y₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (i : J) :
                noncomputable def CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) (X₁ : CategoryTheory.GradedObject I₁ C₁) [∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] :

                Given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄, a map p : I₁ × I₂ × I₃ → J, and graded objects X₁ : GradedObject I₁ C₁, X₂ : GradedObject I₂ C₂ and X₃ : GradedObject I₃ C₃, this is the J-graded object sending j to the coproduct of ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) for p ⟨i₁, i₂, i₃⟩ = j.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.GradedObject.mapTrifunctorMap_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) [∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] (X₁ : CategoryTheory.GradedObject I₁ C₁) :
                  @[simp]
                  theorem CategoryTheory.GradedObject.mapTrifunctorMap_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) [∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] {X₁ : CategoryTheory.GradedObject I₁ C₁} {Y₁ : CategoryTheory.GradedObject I₁ C₁} (φ : X₁ Y₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (i : J) :
                  noncomputable def CategoryTheory.GradedObject.mapTrifunctorMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃J) [∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃), ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p] :

                  Given a trifunctor F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ and a map p : I₁ × I₂ × I₃ → J, this is the functor GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject J C₄ sending X₁ : GradedObject I₁ C₁, X₂ : GradedObject I₂ C₂ and X₃ : GradedObject I₃ C₃ to the J-graded object sending j to the coproduct of ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) for p ⟨i₁, i₂, i₃⟩ = j.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    structure CategoryTheory.GradedObject.BifunctorComp₁₂IndexData {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (r : I₁ × I₂ × I₃J) :
                    Type (max (max (max (max u_10 (u_11 + 1)) u_7) u_8) u_9)

                    Given a map r : I₁ × I₂ × I₃ → J, a BifunctorComp₁₂IndexData r consists of the data of a type I₁₂, maps p : I₁ × I₂ → I₁₂ and q : I₁₂ × I₃ → J, such that r is obtained by composition of p and q.

                    • I₁₂ : Type u_11

                      an auxiliary type

                    • p : I₁ × I₂self.I₁₂

                      a map I₁ × I₂ → I₁₂

                    • q : self.I₁₂ × I₃J

                      a map I₁₂ × I₃ → J

                    • hpq : ∀ (i : I₁ × I₂ × I₃), self.q (self.p (i.1, i.2.1), i.2.2) = r i
                    Instances For
                      theorem CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.hpq {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (self : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (i : I₁ × I₂ × I₃) :
                      self.q (self.p (i.1, i.2.1), i.2.2) = r i
                      @[reducible, inline]
                      abbrev CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) :
                      Type (max (max (max (max (max (max u_9 u_16) u_4) u_5) u_14) u_15) u_7 u_8)

                      Given bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂, G : C₁₂ ⥤ C₃ ⥤ C₄, graded objects X₁ : GradedObject I₁ C₁, X₂ : GradedObject I₂ C₂, X₃ : GradedObject I₃ C₃ and ρ₁₂ : BifunctorComp₁₂IndexData r, this asserts that for all i₁₂ : ρ₁₂.I₁₂ and i₃ : I₃, the functor G(-, X₃ i₃) commutes wich the coproducts of the F₁₂(X₁ i₁, X₂ i₂) such that ρ₁₂.p ⟨i₁, i₂⟩ = i₁₂.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        noncomputable def CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
                        (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j

                        The inclusion of (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) in mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j when r (i₁, i₂, i₃) = j.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj_eq_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_15, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_12, u_4} C₄] [CategoryTheory.Category.{u_14, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₁₂ : ρ₁₂.I₁₂) (h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂) {Z : C₄} (h : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j Z) :
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h = CategoryTheory.CategoryStruct.comp ((G.map (CategoryTheory.GradedObject.ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ) h)
                          theorem CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_15, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_12, u_4} C₄] [CategoryTheory.Category.{u_14, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₁₂ : ρ₁₂.I₁₂) (h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂) :
                          CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp ((G.map (CategoryTheory.GradedObject.ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j )
                          noncomputable def CategoryTheory.GradedObject.cofan₃MapBifunctor₁₂BifunctorMapObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] (j : J) :
                          ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).CofanMapObjFun r j

                          The cofan consisting of the inclusions given by ιMapBifunctor₁₂BifunctorMapObj.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            noncomputable def CategoryTheory.GradedObject.isColimitCofan₃MapBifunctor₁₂BifunctorMapObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] (j : J) :

                            The cofan cofan₃MapBifunctor₁₂BifunctorMapObj is a colimit, see the induced isomorphism mapBifunctorComp₁₂MapObjIso.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj.hasMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_15, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] :
                              ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
                              noncomputable def CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] :

                              The action on graded objects of a trifunctor obtained by composition of two bifunctors can be computed as a composition of the actions of these two bifunctors.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_hom_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_15, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j Z) :
                                @[simp]
                                theorem CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_hom {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_15, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
                                @[simp]
                                theorem CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_inv_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_13, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ j Z) :
                                @[simp]
                                theorem CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_inv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_13, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
                                theorem CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_13, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r} {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄} (f : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j A) (g : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j A) (h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g) :
                                f = g
                                structure CategoryTheory.GradedObject.BifunctorComp₂₃IndexData {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (r : I₁ × I₂ × I₃J) :
                                Type (max (max (max (max u_10 (u_11 + 1)) u_7) u_8) u_9)

                                Given a map r : I₁ × I₂ × I₃ → J, a BifunctorComp₂₃IndexData r consists of the data of a type I₂₃, maps p : I₂ × I₃ → I₂₃ and q : I₁ × I₂₃ → J, such that r is obtained by composition of p and q.

                                • I₂₃ : Type u_11

                                  an auxiliary type

                                • p : I₂ × I₃self.I₂₃

                                  a map I₂ × I₃ → I₂₃

                                • q : I₁ × self.I₂₃J

                                  a map I₁ × I₂₃ → J

                                • hpq : ∀ (i : I₁ × I₂ × I₃), self.q (i.1, self.p i.2) = r i
                                Instances For
                                  theorem CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.hpq {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (self : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (i : I₁ × I₂ × I₃) :
                                  self.q (i.1, self.p i.2) = r i
                                  @[reducible, inline]
                                  abbrev CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) :
                                  Type (max (max (max (max (max (max u_7 u_16) u_4) u_6) u_14) u_15) u_8 u_9)

                                  Given bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄, G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃, graded objects X₁ : GradedObject I₁ C₁, X₂ : GradedObject I₂ C₂, X₃ : GradedObject I₃ C₃ and ρ₂₃ : BifunctorComp₂₃IndexData r, this asserts that for all i₁ : I₁ and i₂₃ : ρ₂₃.I₂₃, the functor F(X₁ i₁, _) commutes wich the coproducts of the G₂₃(X₂ i₂, X₃ i₃) such that ρ₂₃.p ⟨i₂, i₃⟩ = i₂₃.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    noncomputable def CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
                                    (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j

                                    The inclusion of (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) in mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j when r (i₁, i₂, i₃) = j.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj_eq_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_15, u_3} C₃] [CategoryTheory.Category.{u_12, u_4} C₄] [CategoryTheory.Category.{u_13, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₂₃ : ρ₂₃.I₂₃) (h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃) {Z : C₄} (h : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j Z) :
                                      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h = CategoryTheory.CategoryStruct.comp ((F.obj (X₁ i₁)).map (CategoryTheory.GradedObject.ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ) h)
                                      theorem CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_15, u_3} C₃] [CategoryTheory.Category.{u_12, u_4} C₄] [CategoryTheory.Category.{u_13, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₂₃ : ρ₂₃.I₂₃) (h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃) :
                                      CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp ((F.obj (X₁ i₁)).map (CategoryTheory.GradedObject.ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j )
                                      noncomputable def CategoryTheory.GradedObject.cofan₃MapBifunctorBifunctor₂₃MapObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] (j : J) :
                                      ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).CofanMapObjFun r j

                                      The cofan consisting of the inclusions given by ιMapBifunctorBifunctor₂₃MapObj.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        noncomputable def CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (j : J) :

                                        The cofan cofan₃MapBifunctorBifunctor₂₃MapObj is a colimit, see the induced isomorphism mapBifunctorComp₁₂MapObjIso.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          theorem CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj.hasMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_15, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] :
                                          ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
                                          noncomputable def CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₃] [CategoryTheory.Category.{u_14, u_4} C₄] [CategoryTheory.Category.{u_15, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] :

                                          The action on graded objects of a trifunctor obtained by composition of two bifunctors can be computed as a composition of the actions of these two bifunctors.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_hom_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_15, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j Z) :
                                            @[simp]
                                            theorem CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_hom {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_14, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_15, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
                                            @[simp]
                                            theorem CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_inv_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_15, u_2} C₂] [CategoryTheory.Category.{u_14, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_12, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j Z) :
                                            @[simp]
                                            theorem CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_inv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_15, u_2} C₂] [CategoryTheory.Category.{u_14, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_12, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] [((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
                                            theorem CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_15, u_2} C₂] [CategoryTheory.Category.{u_16, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} C₄] [CategoryTheory.Category.{u_14, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} [(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄} (f : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j A) (g : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j A) (h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) g) :
                                            f = g