Theorems · Definition · category theory

CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.compYonedaColimitIsoColimitCompYoneda

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type v} →
      [inst_1 : CategoryTheory.SmallCategory I] →
        (F : CategoryTheory.Functor I (CategoryTheory.Functor Cᵒᵖ (Type v))) →
          {J : Type v} →
            [inst_2 : CategoryTheory.SmallCategory J] →
              (G :
                  CategoryTheory.Functor J
                    (CategoryTheory.CostructuredArrow CategoryTheory.yoneda (CategoryTheory.Limits.colimit F))) →
                {K : Type v} →
                  [inst_3 : CategoryTheory.SmallCategory K] →
                    (H : CategoryTheory.Functor K (CategoryTheory.Over (CategoryTheory.Limits.colimit F))) →
                      (G.op.comp
                              (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda
                                  (CategoryTheory.Limits.colimit F)).op).comp
                          (CategoryTheory.yoneda.obj (CategoryTheory.Limits.colimit H)) ≅
                        CategoryTheory.Limits.colimit
                          (H.comp
                            (CategoryTheory.yoneda.comp
                              ((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ
                                    (CategoryTheory.Over (CategoryTheory.Limits.colimit F))ᵒᵖ (Type (max u v))).obj
                                (G.op.comp
                                  (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda
                                      (CategoryTheory.Limits.colimit F)).op))))

(implementation) Pulling out a colimit out of a hom functor is one half of the key lemma. Note that all of the heavy lifting actually happens in CostructuredArrow.toOverCompYonedaColimit and yonedaYonedaColimit.

Defined in

Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.SmallCategoryCategoryTheory.SmallCategoryCategoryTheory.SmallCategory