Theorems · Definition · category theory

CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux

{C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteColimits C] →
      (A : CategoryTheory.Functor Cᵒᵖ (Type u)) →
        {J : Type} →
          [inst_2 : CategoryTheory.SmallCategory J] →
            [inst_3 : CategoryTheory.FinCategory J] →
              (K : CategoryTheory.Functor J Cᵒᵖ) →
                (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A).comp
                    (CategoryTheory.yoneda.comp
                      ((CategoryTheory.evaluation Cᵒᵖ (Type u)).obj (CategoryTheory.Limits.limit K))) ≅
                  (CategoryTheory.coyoneda.comp
                        ((CategoryTheory.Functor.whiskeringLeft
                              (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) C (Type u)).obj
                          (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A))).obj
                    (CategoryTheory.Limits.limit K)

(Implementation) A natural isomorphism we will need to construct iso.

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.Limits.HasFiniteColimitsCategoryTheory.SmallCategoryCategoryTheory.FinCategory