isSheaf_iff_preservesFiniteProducts

English

A derived simplification of the IsSheaf_iff_preservesFiniteProducts for subsingleton index sets.

Русский

Упрощение леммы IsSheaf_iff_preservesFiniteProducts для индексов с единственным элементом.

LaTeX

$$$\text{(simplified)}$$$

Lean4

/-- A presheaf on a category which is `FinitaryExtensive` is a sheaf iff it preserves finite products.
-/
theorem isSheaf_iff_preservesFiniteProducts (F : Cᵒᵖ ⥤ D) :
    IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F :=
  by
  constructor
  · intro h
    rw [IsSheaf] at h
    refine ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
    constructor
    apply coyonedaJointlyReflectsLimits
    intro ⟨E⟩
    specialize h E
    rw [Presieve.isSheaf_iff_preservesFiniteProducts] at h
    exact isLimitOfPreserves (F.comp (coyoneda.obj ⟨E⟩)) hc
  · intro _ E
    rw [Presieve.isSheaf_iff_preservesFiniteProducts]
    exact ⟨inferInstance⟩

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