isIndObject_iff_preservesFiniteLimits

English

For a presheaf A on a small category C with finite colimits, A is Ind-object iff A preserves finite limits.

Русский

Для прешепафета A над малой категорией C с конечными колимитами, A является Ind-объектом тогда и только тогда, когда A сохраняет конечные пределы.

LaTeX

$$$\mathrm{IsIndObject}(A) \iff \mathrm{PreservesFiniteLimits}(A)$$$

Lean4

/-- Presheaves over a small finitely cocomplete category `C : Type u` are Ind-objects if and only if
they are left-exact. -/
theorem isIndObject_iff_preservesFiniteLimits [HasFiniteColimits C] (A : Cᵒᵖ ⥤ Type u) :
    IsIndObject A ↔ PreservesFiniteLimits A :=
  (isIndObject_iff A).trans <| by
    refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩
    · apply preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda
    · exact isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A
    · have := essentiallySmallSelf (CostructuredArrow yoneda A)
      apply finallySmall_of_essentiallySmall

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