isSheaf_iff — Mathlib

English

IsSheaf J P is equivalent to the existence of limits for all OneHypercovers in J.

Русский

IsSheaf J P эквивалентно существованию пределов для всех OneHypercover в J.

LaTeX

$$$\\text{IsSheaf}(J,P) \\;\\iff\\; \\forall X\\; \\forall E\\; E\\text{ is OneHypercover}, Nonempty(IsLimit(E.multifork P))$$$

Lean4

theorem isSheaf_iff [H.IsGenerating] :
    Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X) (_ : H E), Nonempty (IsLimit (E.multifork P)) :=
  by
  constructor
  · intro hP X E _
    exact ⟨E.isLimitMultifork ⟨_, hP⟩⟩
  · intro hP
    rw [Presheaf.isSheaf_iff_multifork]
    rintro X ⟨S, hS⟩
    obtain ⟨E, hE, le⟩ := H.exists_oneHypercover S hS
    exact ⟨IsSheafIff.isLimit hP hE le⟩

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