Transitivity of the sheaf condition along a cover of an open set

Let W be an open set, Y i ≤ W opens for which a presheaf of types F satisfies the sheaf condition, and S a sieve on W whose members each lie in some Y i. If F is a sheaf for the restriction of S to each Y i and separated for the restriction of S to each Y i ⊓ Y j, then F is a sheaf for S: sections over the members of S glue first over each Y i, the gluings agree on the overlaps Y i ⊓ Y j, and so glue over W.

Mathlib's CategoryTheory.Presieve.isSheafFor_trans proves a transitivity statement of this kind for sieves on an arbitrary category, but it asks for the sheaf condition of S restricted to every open contained in some Y i. Since there is at most one morphism between two opens, two sections over Y i and Y j are compatible as soon as they agree on Y i ⊓ Y j, so here the hypotheses concern only the opens Y i and Y i ⊓ Y j. This makes the statement usable when the sheaf condition is known only on a basis of opens closed under finite intersections, such as the rational subsets of an adic spectrum, where a cover is refined by covering each of its members.

Main results

• TauCeti.TopologicalSpace.Opens.isSheafFor_trans : the transitivity statement.

theorem TauCeti.TopologicalSpace.Opens.isSheafFor_trans {X : Type u} [TopologicalSpace X] {F : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ (Type w)} {W : TopologicalSpace.Opens X} {ι : Type u_1} (Y : ι → TopologicalSpace.Opens X) (hY : ∀ (i : ι), Y i ≤ W) (S : CategoryTheory.Sieve W) (hR : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Y fun (i : ι) => CategoryTheory.homOfLE ⋯)) (hS : ∀ (i : ι), CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Sieve.pullback (CategoryTheory.homOfLE ⋯) S).arrows) (hS₂ : ∀ (i j : ι), CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Sieve.pullback (CategoryTheory.homOfLE ⋯) S).arrows) (hSY : ∀ ⦃V : TopologicalSpace.Opens X⦄ (f : V ⟶ W), S.arrows f → ∃ (i : ι), V ≤ Y i) : CategoryTheory.Presieve.IsSheafFor F S.arrows

Transitivity of the sheaf condition along a cover of an open set. Let Y i ≤ W be opens covering W in the sense that F is a sheaf for the family of inclusions Y i ⟶ W, and let S be a sieve on W each of whose members lies in some Y i. If F is a sheaf for the restriction of S to every Y i, and separated for the restriction of S to every Y i ⊓ Y j, then F is a sheaf for S.

Compare CategoryTheory.Presieve.isSheafFor_trans, which instead asks for the sheaf condition of the restriction of S to every open contained in some Y i.