Theorems · Theorem · category theory

CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_hom

∀ {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ᵒᵖ)
  [inst_4 : CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)],
  (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso A K).hom =
    CategoryTheory.Limits.limit.post K A

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.Limits.HasFiniteColimitsCategoryTheory.SmallCategoryCategoryTheory.FinCategoryCategoryTheory.IsFiltered