isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits

English

If C is finitely cocomplete and A: C^{op} ⥤ Type is a presheaf that preserves finite limits, then CostructuredArrow yoneda A is filtered.

Русский

Пусть C — конечнокомплектная категория, A: C^{op} ⥤ Type — предобраз, сохраняющий конечные пределы; тогда CostructuredArrow yoneda A является фильтрованной.

LaTeX

$$$\operatorname{IsFiltered}(\operatorname{CostructuredArrow}(\mathrm{yoneda}, A))$$$

Lean4

/-- If `C` is a finitely cocomplete category and `A : Cᵒᵖ ⥤ Type u` is a presheaf that preserves
finite limits, then `CostructuredArrow yoneda A` is filtered.

One direction of Proposition 3.3.13 of [Kashiwara2006].
-/
theorem isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits [PreservesFiniteLimits A] :
    IsFiltered (CostructuredArrow yoneda A) :=
  by
  suffices IsCofiltered A.Elements from
    IsFiltered.of_equivalence (CategoryOfElements.costructuredArrowYonedaEquivalence _)
  suffices HasFiniteLimits A.Elements from IsCofiltered.of_hasFiniteLimits A.Elements
  exact ⟨fun J _ _ => inferInstance⟩

Похожие утверждения