The associator for actions of bifunctors on graded objects

Given functors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂, G : C₁₂ ⥤ C₃ ⥤ C₄, F : C₁ ⥤ C₂₃ ⥤ C₄, G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃ equipped with an isomorphism associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃ (which informally means that we have natural isomorphisms G(F₁₂(X₁, X₂), X₃) ≅ F(X₁, G₂₃(X₂, X₃))), a map r : I₁ × I₂ × I₃ → J, and data ρ₁₂ : BifunctorComp₁₂IndexData r and ρ₂₃ : BifunctorComp₂₃IndexData r, then if X₁ : GradedObject I₁ C₁, X₂ : GradedObject I₂ C₂ and X₃ : GradedObject I₃ C₃ satisfy suitable assumptions, we construct an isomorphism mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃ between mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ and mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) in the category GradedObject J C₄.

This construction shall be used in the definition of the monoidal category structure on graded objects indexed by an additive monoid.

noncomputable def CategoryTheory.GradedObject.mapBifunctorAssociator {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [Category.{u_11, u_1} C₁] [Category.{u_12, u_2} C₂] [Category.{u_13, u_5} C₃] [Category.{u_14, u_6} C₄] [Category.{u_15, u_3} C₁₂] [Category.{u_16, u_4} C₂₃] {F₁₂ : Functor C₁ (Functor C₂ C₁₂)} {G : Functor C₁₂ (Functor C₃ C₄)} {F : Functor C₁ (Functor C₂₃ C₄)} {G₂₃ : Functor C₂ (Functor C₃ C₂₃)} (associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : BifunctorComp₁₂IndexData r) (ρ₂₃ : BifunctorComp₂₃IndexData r) (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) [(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ ≅ mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)

Associator isomorphism for the action of bifunctors on graded objects.

Equations

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

@[simp]

theorem CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [Category.{u_15, u_1} C₁] [Category.{u_14, u_2} C₂] [Category.{u_12, u_5} C₃] [Category.{u_11, u_6} C₄] [Category.{u_13, u_3} C₁₂] [Category.{u_17, u_4} C₂₃] {F₁₂ : Functor C₁ (Functor C₂ C₁₂)} {G : Functor C₁₂ (Functor C₃ C₄)} {F : Functor C₁ (Functor C₂₃ C₄)} {G₂₃ : Functor C₂ (Functor C₃ C₂₃)} (associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : BifunctorComp₁₂IndexData r) (ρ₂₃ : BifunctorComp₂₃IndexData r) (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) [(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j) = CategoryStruct.comp (((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)

@[simp]

theorem CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [Category.{u_15, u_1} C₁] [Category.{u_14, u_2} C₂] [Category.{u_12, u_5} C₃] [Category.{u_11, u_6} C₄] [Category.{u_13, u_3} C₁₂] [Category.{u_17, u_4} C₂₃] {F₁₂ : Functor C₁ (Functor C₂ C₁₂)} {G : Functor C₁₂ (Functor C₃ C₄)} {F : Functor C₁ (Functor C₂₃ C₄)} {G₂₃ : Functor C₂ (Functor C₃ C₂₃)} (associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : BifunctorComp₁₂IndexData r) (ρ₂₃ : BifunctorComp₂₃IndexData r) (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) [(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ Z) : CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryStruct.comp ((mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j) h✝) = CategoryStruct.comp (((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝)

@[simp]

theorem CategoryTheory.GradedObject.ι_mapBifunctorAssociator_inv {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [Category.{u_13, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_14, u_5} C₃] [Category.{u_11, u_6} C₄] [Category.{u_17, u_3} C₁₂] [Category.{u_12, u_4} C₂₃] {F₁₂ : Functor C₁ (Functor C₂ C₁₂)} {G : Functor C₁₂ (Functor C₃ C₄)} {F : Functor C₁ (Functor C₂₃ C₄)} {G₂₃ : Functor C₂ (Functor C₃ C₂₃)} (associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : BifunctorComp₁₂IndexData r) (ρ₂₃ : BifunctorComp₂₃IndexData r) (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) [(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) : CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j) = CategoryStruct.comp (((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)

@[simp]

theorem CategoryTheory.GradedObject.ι_mapBifunctorAssociator_inv_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [Category.{u_13, u_1} C₁] [Category.{u_15, u_2} C₂] [Category.{u_14, u_5} C₃] [Category.{u_11, u_6} C₄] [Category.{u_17, u_3} C₁₂] [Category.{u_12, u_4} C₂₃] {F₁₂ : Functor C₁ (Functor C₂ C₁₂)} {G : Functor C₁₂ (Functor C₃ C₄)} {F : Functor C₁ (Functor C₂₃ C₄)} {G₂₃ : Functor C₂ (Functor C₃ C₂₃)} (associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : BifunctorComp₁₂IndexData r) (ρ₂₃ : BifunctorComp₂₃IndexData r) (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) [(((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p] [(((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q] [(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p] [(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q] [H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] [H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h✝ : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ Z) : CategoryStruct.comp (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryStruct.comp ((mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j) h✝) = CategoryStruct.comp (((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryStruct.comp (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝)