Theorems · Theorem · category theory

CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_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 C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y').HasMap
      p]
  {Z : CategoryTheory.GradedObject J D}
  (h : CategoryTheory.GradedObject.mapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.mapBifunctorMapMap F p
          (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
        h)

Defined in

Mathlib.CategoryTheory.GradedObject.Unitor

Cited by

0 results in Mathlib

Foundations

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

Assumes

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