preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda

English

For any K: J ⥤ C^{op}, limit.post K A is iso when IsFiltered holds.

Русский

Для любого K: J ⥤ C^{op}, limit.post K A является изоморфизмом при условии IsFiltered.

LaTeX

$$$\operatorname{IsIso}(\operatorname{limit.post}(K, A))$$$

Lean4

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

One direction of Proposition 3.3.13 of [Kashiwara2006].
-/
theorem preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda [IsFiltered (CostructuredArrow yoneda A)] :
    PreservesFiniteLimits A where preservesFiniteLimits _ _ _ := ⟨fun {_} => preservesLimit_of_isIso_post _ _⟩

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