Theorems · Theorem · category theory

CategoryTheory.GradedObject.mapBifunctorRightUnitor_naturality_assoc

∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) {Y : C}
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X X' : CategoryTheory.GradedObject J D) (φ : X ⟶ X')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  {Z : CategoryTheory.GradedObject J D} (h : X' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom
      (CategoryTheory.CategoryStruct.comp φ h)

Defined in

Mathlib.CategoryTheory.GradedObject.Unitor

Cited by

0 results in Mathlib

Foundations

Depth 43 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryZeroDecidableEqCategoryTheory.Limits.HasInitialCategoryTheory.Limits.PreservesColimitCategoryTheory.GradedObject.HasMapCategoryTheory.GradedObject.HasMap