Presheaves adapted to a basis

A presheaf F on a topological space X is adapted to a set B of opens if, for every open V, the restriction maps F(V) ⟶ F(U) to the members U ∈ B with U ≤ V exhibit F(V) as the limit of the F(U). In the language of Kan extensions, F is the pointwise right Kan extension of its restriction to B along the inclusion of B into the opens of X. This is the sense in which the structure presheaf of an adic spectrum, defined on rational opens and extended to all opens by limits, is determined by its values on the rational opens.

When B is a basis of the topology, an adapted presheaf is a sheaf exactly when its restriction to B is a sheaf for the topology restricted to B; this is what makes sheaf conditions checkable on a basis for presheaves defined by such limits. Only the direction from B to X uses adaptedness; the other direction holds for every sheaf. Conversely, when the target category has limits, every sheaf is adapted to every basis: a sheaf is determined on an open V by its values on the basic opens contained in V. So, for a basis, being a sheaf is the same as being adapted and a sheaf on the basis.

Main definitions

• TopCat.Presheaf.IsAdapted: F is adapted to B.

Main results

• TopCat.Presheaf.isSheaf_of_isAdapted_of_isSheaf_restrictedTopology: an adapted presheaf whose restriction to B is a sheaf for the restricted topology is a sheaf.
• TopCat.Presheaf.IsSheaf.isSheaf_restrictedTopology: the restriction of a sheaf to a basis is a sheaf for the restricted topology.
• TopCat.Presheaf.isSheaf_iff_of_isAdapted: for a presheaf adapted to a basis, the two sheaf conditions are equivalent.
• TopCat.Presheaf.IsSheaf.isAdapted: a sheaf with values in a category with limits is adapted to every basis.
• TopCat.Presheaf.isSheaf_iff_isAdapted_and_isSheaf_restrictedTopology: for a basis, a presheaf is a sheaf exactly when it is adapted to the basis and a sheaf on the basis.
• TopCat.Presheaf.IsAdapted.mono: a presheaf adapted to B is adapted to every B' ⊇ B. This is how adaptedness to the rational opens of an adic spectrum yields adaptedness to its open affinoid subspaces.
• TopCat.Presheaf.IsAdapted.of_iso, TopCat.Presheaf.IsAdapted.pushforward_of_iso: adaptedness is invariant under isomorphism of presheaves and under homeomorphism, for the family of opens whose preimages lie in B.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Remark and Definition 8.9.
• M. Artin, A. Grothendieck, J.-L. Verdier, Théorie des topos et cohomologie étale des schémas (SGA 4), Tome 1, Exposé III, 2.2, for the passage from a sheaf on the basis to a sheaf on the space, which is Mathlib's CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork.

def TopCat.Presheaf.IsAdapted {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : Presheaf C X) (B : Set (TopologicalSpace.Opens ↑X)) : Prop

A presheaf F on X is adapted to a set B of opens if, at every open V, the restriction maps to the members of B contained in V make F.obj (op V) the limit of F over them: F is the pointwise right Kan extension of its restriction to B.

Equations

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

Enlarging the family

theorem TopCat.Presheaf.IsAdapted.mono {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {F : Presheaf C X} {B B' : Set (TopologicalSpace.Opens ↑X)} (hBB' : B ⊆ B') (hF : F.IsAdapted B) : F.IsAdapted B'

Adaptedness passes to a larger family. If F is adapted to B and B ⊆ B', then F is adapted to B': a compatible family on the members of B' below V is determined by its restriction to the members of B, and a compatible family on the members of B below V extends to the members U' ∈ B' below V through the limit description of F(U').

Transport along isomorphisms

theorem TopCat.Presheaf.IsAdapted.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {F : Presheaf C X} {B : Set (TopologicalSpace.Opens ↑X)} {G : Presheaf C X} (e : F ≅ G) (hF : F.IsAdapted B) : G.IsAdapted B

Adaptedness is invariant under isomorphism of presheaves.

theorem TopCat.Presheaf.IsAdapted.pushforward_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {F : Presheaf C X} {B : Set (TopologicalSpace.Opens ↑X)} {Y : TopCat} (f : X ≅ Y) (hF : F.IsAdapted B) : ((pushforward C f.hom).obj F).IsAdapted ((TopologicalSpace.Opens.map f.hom).obj ⁻¹' B)

Adaptedness is invariant under homeomorphism. If F is adapted to B and f : X ≅ Y is an isomorphism of topological spaces, the pushforward f_* F is adapted to the opens of Y whose preimages lie in B.

The sheaf condition on a basis

theorem TopCat.Presheaf.isSheaf_of_isAdapted_of_isSheaf_restrictedTopology {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : Presheaf C X) (B : Set (TopologicalSpace.Opens ↑X)) (hB : TopologicalSpace.Opens.IsBasis B) (hF : F.IsAdapted B) (h : CategoryTheory.Presheaf.IsSheaf ((CategoryTheory.inducedFunctor Subtype.val).restrictedTopology (Opens.grothendieckTopology ↑X)) ((CategoryTheory.inducedFunctor Subtype.val).op.comp F)) : F.IsSheaf

The sheaf condition on a basis B suffices for an adapted presheaf. If F is adapted to the basis B and its restriction to B is a sheaf for the topology restricted to B, then F is a sheaf. A sieve on a member of B covers for the restricted topology exactly when its image covers in X (Functor.mem_restrictedTopology_iff), so the hypothesis involves only covers of members of B by members of B. The inclusion of a basis is cocontinuous for the restricted topology, and a pointwise right Kan extension of a sheaf along a cocontinuous functor is a sheaf (SGA 4 III 2.2).

theorem TopCat.Presheaf.IsSheaf.isSheaf_restrictedTopology {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {B : Set (TopologicalSpace.Opens ↑X)} (hB : TopologicalSpace.Opens.IsBasis B) {F : Presheaf C X} (hF : F.IsSheaf) : CategoryTheory.Presheaf.IsSheaf ((CategoryTheory.inducedFunctor Subtype.val).restrictedTopology (Opens.grothendieckTopology ↑X)) ((CategoryTheory.inducedFunctor Subtype.val).op.comp F)

The restriction of a sheaf to a basis B is a sheaf for the restricted topology on B.

theorem TopCat.Presheaf.isSheaf_iff_of_isAdapted {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : Presheaf C X) (B : Set (TopologicalSpace.Opens ↑X)) (hB : TopologicalSpace.Opens.IsBasis B) (hF : F.IsAdapted B) : F.IsSheaf ↔ CategoryTheory.Presheaf.IsSheaf ((CategoryTheory.inducedFunctor Subtype.val).restrictedTopology (Opens.grothendieckTopology ↑X)) ((CategoryTheory.inducedFunctor Subtype.val).op.comp F)

A presheaf adapted to a basis is a sheaf exactly when it is a sheaf on the basis, for the topology restricted to the basis.

Sheaves are adapted to every basis

theorem TopCat.Presheaf.IsSheaf.isAdapted {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C] {B : Set (TopologicalSpace.Opens ↑X)} (hB : TopologicalSpace.Opens.IsBasis B) {F : Presheaf C X} (hF : F.IsSheaf) : F.IsAdapted B

A sheaf is adapted to every basis. If F takes values in a category with limits and is a sheaf, then for every basis B and every open V, the restriction maps exhibit F(V) as the limit of the F(U) over the members U ∈ B below V: a basis is a dense subsite of the opens, and a sheaf is the pointwise right Kan extension of its restriction to a dense subsite.

theorem TopCat.Presheaf.isSheaf_iff_isAdapted_and_isSheaf_restrictedTopology {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : Presheaf C X) (B : Set (TopologicalSpace.Opens ↑X)) [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C] (hB : TopologicalSpace.Opens.IsBasis B) : F.IsSheaf ↔ F.IsAdapted B ∧ CategoryTheory.Presheaf.IsSheaf ((CategoryTheory.inducedFunctor Subtype.val).restrictedTopology (Opens.grothendieckTopology ↑X)) ((CategoryTheory.inducedFunctor Subtype.val).op.comp F)

For a basis B, a presheaf is a sheaf exactly when it is adapted to B and a sheaf on B, for the topology restricted to B.