isSheaf_iff_of_isGeneratedByOneHypercovers

English

IsSheaf J P is equivalent to IsSheaf under the assumption that J is generated by one-hypercovers.

Русский

IsSheaf J P эквивалентно IsSheaf при предположении, что J порождается одной гиперковер-структурой.

LaTeX

$$$ IsSheaf(J,P) \\iff \\forall E, IsSheafIff.IsGenerating.le J P$$$

Lean4

theorem isSheaf_iff_of_isGeneratedByOneHypercovers [GrothendieckTopology.IsGeneratedByOneHypercovers.{w} J]
    (P : Cᵒᵖ ⥤ A) :
    IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : GrothendieckTopology.OneHypercover.{w} J X), Nonempty (IsLimit (E.multifork P)) := by
  simpa using GrothendieckTopology.OneHypercoverFamily.isSheaf_iff.{w} ⊤ P

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