Theorems · Theorem · category theory

CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj

∀ {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 : CategoryTheory.GradedObject J D) (j : J),
  CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
      (e.hom.app (Y j))

Defined in

Mathlib.CategoryTheory.GradedObject.Unitor

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryZeroDecidableEqCategoryTheory.Limits.HasInitialCategoryTheory.Limits.PreservesColimit