English
There is a functor from pairwise intersections to OpensLeCover U, respecting the inclusions of single and pairwise opens.
Русский
Существует функтор от парных пересечений к OpensLeCover U, сохраняющий включения одиночных и парных открытых множеств.
LaTeX
$$$\text{pairwiseToOpensLeCover}: \text{Pairwise } ι \to OpensLeCover U$$$
Lean4
/-- A presheaf `(opens X)ᵒᵖ ⥤ C` on a topological space `X` is a sheaf on the site `opens X` iff
it satisfies the `IsSheafOpensLeCover` sheaf condition. The latter is not the
official definition of sheaves on spaces, but has the advantage that it does not
require `has_products C`. -/
theorem isSheaf_iff_isSheafOpensLeCover : F.IsSheaf ↔ F.IsSheafOpensLeCover :=
by
refine ⟨fun h _ ↦ h.isSheafOpensLeCover, fun h ↦ (Presheaf.isSheaf_iff_isLimit _ _).mpr fun Y S ↦ ?_⟩
rw [← Sieve.generate_sieve S]
intro hS
rw [← (isLimitOpensLeEquivGenerate₂ F S.1 hS).nonempty_congr]
apply h
