The coverage a topological basis induces on Opens X

A basis B of open sets induces a coverage on Opens X: a presieve covers U when all of its members lie in B and they cover U pointwise. basisCoverage_toGrothendieck identifies the Grothendieck topology it generates as Opens.grothendieckTopology X, the one the topology of X already defines, and isSheaf_iff_isSheafFor_basisCoverage reads off the consequence: a presheaf is a sheaf exactly when it satisfies the sheaf condition for covers by basis elements alone.

Mathlib names this construction as an open project in the module docstring of Mathlib/CategoryTheory/Sites/Coverage.lean:

A more concrete example: If ℬ is a basis for a topology on a type X (in the sense of TopologicalSpace.IsTopologicalBasis) then it naturally induces a coverage on Opens X whose associated Grothendieck topology is the one induced by the topology on X generated by ℬ. (Project: Formalize this!)

Main definitions

• TauCeti.TopologicalSpace.Opens.basisCoverage : the coverage on Opens X attached to a basis.

Main results

• TauCeti.TopologicalSpace.Opens.isBasisCover_iff, with IsBasisCover.mem_basis and IsBasisCover.exists_mem : the two clauses of a basis cover, for consumers that cannot unfold the definition.
• TauCeti.TopologicalSpace.Opens.basisCoverage_toGrothendieck : it generates Opens.grothendieckTopology X.
• TauCeti.TopologicalSpace.Opens.isSheaf_iff_isSheafFor_basisCoverage : a Type-valued presheaf is a sheaf for the space exactly when it is a sheaf for every basis cover.
• TauCeti.TopologicalSpace.Opens.isSheaf_iff_isSheafFor_basisCoverage_comp : the same criterion for a presheaf valued in an arbitrary category, which is the form TopCat.Presheaf.IsSheaf is stated in.
• TauCeti.TopologicalSpace.Opens.coverDense_inducedFunctor_subtypeVal : the inclusion of a basis into Opens X is cover-dense, Mathlib's TopCat.Opens.coverDense_inducedFunctor for a basis given as a set of opens.

Why a coverage and not a pretopology

A pretopology asks its covering families to be stable under pullback on the nose, and basis covers are not: intersecting two basis elements need not give a basis element. A coverage asks only that some covering family of the smaller object factors through the given one, which a basis supplies by shrinking each intersection to a basis neighbourhood of each of its points. That is exactly the weakening CategoryTheory.Coverage exists for.

def TauCeti.TopologicalSpace.Opens.IsBasisCover {X : Type u} [TopologicalSpace X] (B : Set (TopologicalSpace.Opens X)) {U : TopologicalSpace.Opens X} (R : CategoryTheory.Presieve U) : Prop

The presieves of a basis cover: every member lies in B, and together they cover U pointwise.

Equations

• TauCeti.TopologicalSpace.Opens.IsBasisCover B R = ((∀ ⦃V : TopologicalSpace.Opens X⦄ ⦃f : V ⟶ U⦄, R f → V ∈ B) ∧ ∀ x ∈ U, ∃ (V : TopologicalSpace.Opens X) (f : V ⟶ U), R f ∧ x ∈ V)

theorem TauCeti.TopologicalSpace.Opens.isBasisCover_iff {X : Type u} [TopologicalSpace X] {B : Set (TopologicalSpace.Opens X)} {U : TopologicalSpace.Opens X} {R : CategoryTheory.Presieve U} : IsBasisCover B R ↔ (∀ ⦃V : TopologicalSpace.Opens X⦄ ⦃f : V ⟶ U⦄, R f → V ∈ B) ∧ ∀ x ∈ U, ∃ (V : TopologicalSpace.Opens X) (f : V ⟶ U), R f ∧ x ∈ V

The two clauses of a basis cover. IsBasisCover is a definition and its body is not exposed, so this is how a consumer outside this module builds one or takes it apart.

theorem TauCeti.TopologicalSpace.Opens.IsBasisCover.mem_basis {X : Type u} [TopologicalSpace X] {B : Set (TopologicalSpace.Opens X)} {U : TopologicalSpace.Opens X} {R : CategoryTheory.Presieve U} (hR : IsBasisCover B R) ⦃V : TopologicalSpace.Opens X⦄ ⦃f : V ⟶ U⦄ (hf : R f) : V ∈ B

Every member of a basis cover lies in the basis.

theorem TauCeti.TopologicalSpace.Opens.IsBasisCover.exists_mem {X : Type u} [TopologicalSpace X] {B : Set (TopologicalSpace.Opens X)} {U : TopologicalSpace.Opens X} {R : CategoryTheory.Presieve U} (hR : IsBasisCover B R) {x : X} (hx : x ∈ U) : ∃ (V : TopologicalSpace.Opens X) (f : V ⟶ U), R f ∧ x ∈ V

A basis cover covers its object pointwise.

def TauCeti.TopologicalSpace.Opens.basisCoverage {X : Type u} [TopologicalSpace X] {B : Set (TopologicalSpace.Opens X)} (hB : TopologicalSpace.Opens.IsBasis B) : CategoryTheory.Coverage (TopologicalSpace.Opens X)

The coverage a basis induces on Opens X. Its covering presieves are the basis covers.

The pullback condition is where the basis property is used: the intersection of a basis element with a smaller open need not be a basis element, so the covering family of the smaller open is obtained by shrinking to a basis neighbourhood inside each intersection.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.TopologicalSpace.Opens.mem_basisCoverage {X : Type u} [TopologicalSpace X] {B : Set (TopologicalSpace.Opens X)} (hB : TopologicalSpace.Opens.IsBasis B) {U : TopologicalSpace.Opens X} {R : CategoryTheory.Presieve U} : R ∈ (basisCoverage hB).coverings U ↔ IsBasisCover B R

Membership in the basis coverage is being a basis cover; this is the normal form.

theorem TauCeti.TopologicalSpace.Opens.basisCoverage_toGrothendieck {X : Type u} [TopologicalSpace X] {B : Set (TopologicalSpace.Opens X)} (hB : TopologicalSpace.Opens.IsBasis B) : (basisCoverage hB).toGrothendieck = Opens.grothendieckTopology X

The basis coverage generates the topology of the space. Every basis cover is a cover in Opens.grothendieckTopology X, and conversely every covering sieve contains the basis cover made of the basis elements it already contains.

theorem TauCeti.TopologicalSpace.Opens.isSheaf_iff_isSheafFor_basisCoverage {X : Type u} [TopologicalSpace X] {B : Set (TopologicalSpace.Opens X)} (hB : TopologicalSpace.Opens.IsBasis B) (P : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf (Opens.grothendieckTopology X) P ↔ ∀ ⦃U : TopologicalSpace.Opens X⦄ (R : CategoryTheory.Presieve U), IsBasisCover B R → CategoryTheory.Presieve.IsSheafFor P R

The basis sheaf criterion. A presheaf on X is a sheaf exactly when it satisfies the sheaf condition for covers by basis elements. This is the criterion the structure presheaf of an adic space is checked against, where the basis is the rational subsets.

theorem TauCeti.TopologicalSpace.Opens.isSheaf_iff_isSheafFor_basisCoverage_comp {X : Type u} [TopologicalSpace X] {B : Set (TopologicalSpace.Opens X)} (hB : TopologicalSpace.Opens.IsBasis B) {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ C) : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P ↔ ∀ (E : C) ⦃U : TopologicalSpace.Opens X⦄ (R : CategoryTheory.Presieve U), IsBasisCover B R → CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E))) R

The basis sheaf criterion in an arbitrary target category. Presheaf.IsSheaf is by definition the Type-valued condition on P ⋙ coyoneda.obj (op E) for every object E, so the criterion transfers objectwise.

This is the form the structure presheaf of an adic space is checked in: TopCat.Presheaf.IsSheaf F unfolds to Presheaf.IsSheaf (Opens.grothendieckTopology X) F, and its target category is CompleteSeparatedTopCommRingCat.

theorem TauCeti.TopologicalSpace.Opens.coverDense_inducedFunctor_subtypeVal {X : Type u} [TopologicalSpace X] {B : Set (TopologicalSpace.Opens X)} (hB : TopologicalSpace.Opens.IsBasis B) : (CategoryTheory.inducedFunctor Subtype.val).IsCoverDense (Opens.grothendieckTopology X)

The inclusion of a basis B, given as a set of opens, into Opens X is cover-dense for the Grothendieck topology of X: every open is covered by the members of B it contains. This is Mathlib's TopCat.Opens.coverDense_inducedFunctor for a Set-indexed basis.