Theorems · Theorem · category theory

CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app

∀ {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.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux A K).hom.app = fun X =>
    CategoryTheory.CategoryStruct.id (Opposite.unop (CategoryTheory.Limits.limit K) ⟶ X.left)

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.Limits.HasFiniteColimitsCategoryTheory.SmallCategoryCategoryTheory.FinCategory