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.HasMap (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃)
ρ₁₂.q]
[CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃) ρ₂₃.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃))
ρ₂₃.q]
[H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
[H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
:
CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)
X₃ ≅ CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
(CategoryTheory.GradedObject.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.
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.HasMap (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃)
ρ₁₂.q]
[CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃) ρ₂₃.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃))
ρ₂₃.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.HasMap (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃)
ρ₁₂.q]
[CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃) ρ₂₃.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃))
ρ₂₃.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.HasMap (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃)
ρ₁₂.q]
[CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃) ρ₂₃.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃))
ρ₂₃.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.HasMap (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂) ρ₁₂.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
X₃)
ρ₁₂.q]
[CategoryTheory.GradedObject.HasMap (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃) ρ₂₃.p]
[CategoryTheory.GradedObject.HasMap
(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
(CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃))
ρ₂₃.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)