English
For small C with finite colimits and A: C^{op} ⥤ Type, IsFiltered(CostructuredArrow yoneda A) is equivalent to A preserving finite limits.
Русский
Для малой C с конечными колимитами и A: C^{op} ⥤ Type, IsFiltered(CostructuredArrow yoneda A) эквивалентно тому, что A сохраняет конечные пределы.
LaTeX
$$$\operatorname{IsFiltered}(\operatorname{CostructuredArrow}(\mathrm{yoneda}, A)) \iff \operatorname{PreservesFiniteLimits}(A)$$$
Lean4
/-- If `C` is a small finitely cocomplete category and `A : Cᵒᵖ ⥤ Type u` is a presheaf, then
`CostructuredArrow yoneda A` is filtered if and only if `A` preserves finite limits.
Proposition 3.3.13 of [Kashiwara2006].
-/
theorem isFiltered_costructuredArrow_yoneda_iff_nonempty_preservesFiniteLimits :
IsFiltered (CostructuredArrow yoneda A) ↔ PreservesFiniteLimits A :=
⟨fun _ => preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda A, fun _ =>
isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A⟩
