Documentation

Mathlib.CategoryTheory.GradedObject.Associator

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} [CategoryTheory.Category.{u_11, u_1} C₁] [CategoryTheory.Category.{u_12, u_2} C₂] [CategoryTheory.Category.{u_13, u_5} C₃] [CategoryTheory.Category.{u_14, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Category.{u_16, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {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) (ρ₂₃ : 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] [(((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₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ 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.
Instances For
    @[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} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_12, u_5} C₃] [CategoryTheory.Category.{u_11, u_6} C₄] [CategoryTheory.Category.{u_13, u_3} C₁₂] [CategoryTheory.Category.{u_17, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {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) (ρ₂₃ : 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] [(((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₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (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) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j) h) = CategoryTheory.CategoryStruct.comp (((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h)
    @[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} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_12, u_5} C₃] [CategoryTheory.Category.{u_11, u_6} C₄] [CategoryTheory.Category.{u_13, u_3} C₁₂] [CategoryTheory.Category.{u_17, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {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) (ρ₂₃ : 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] [(((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₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j) = CategoryTheory.CategoryStruct.comp (((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj 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} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_15, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_11, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Category.{u_12, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {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) (ρ₂₃ : 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] [(((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₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (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) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j) h) = CategoryTheory.CategoryStruct.comp (((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj 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} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_15, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_11, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Category.{u_12, u_4} C₂₃] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G CategoryTheory.bifunctorComp₂₃ F G₂₃) {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) (ρ₂₃ : 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] [(((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₃] [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j) = CategoryTheory.CategoryStruct.comp (((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)