Sheaves of topological rings from sheaves of sets

A presheaf F of topological commutative rings on a site is a sheaf as soon as its underlying presheaf of sets is a sheaf and, for every covering sieve S on X, the map sending x ∈ F(X) to its family of restrictions along the arrows of S is inducing for the product topology. The topological half of the sheaf condition is thereby reduced to one statement about the topology of each F(X).

For a presheaf with values in a full subcategory of TopCommRingCat, such as the complete separated rings in which the adic structure presheaf takes its values, the sheaf property descends along the inclusion by CategoryTheory.Presheaf.isSheaf_of_isSheaf_comp, since a fully faithful functor reflects limits.

Main results

• TauCeti.TopCommRingCat.isInducing_restrictionMap_ofArrows_iff: for a generated sieve, it is enough to test the topology against the generating restriction maps.
• TauCeti.TopCommRingCat.isSheafFor_of_isSheafFor_forget: the sheaf condition for a single sieve, tested against every topological commutative ring.
• TauCeti.TopCommRingCat.isSheaf_of_isSheaf_forget: the sheaf property for a Grothendieck topology.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Remark 8.20, which characterises sheaves of topological rings on a topological space by the sheaf condition on rings together with topological embeddings into products. isSheaf_of_isSheaf_forget is the sufficient direction, for presheaves on an arbitrary site.

theorem TauCeti.TopCommRingCat.isInducing_restrictionMap_ofArrows_iff {C : Type u} [CategoryTheory.Category.{w, u} C] (F : CategoryTheory.Functor Cᵒᵖ TopCommRingCat) {X : C} {I : Type u_1} (Y : I → C) (f : (i : I) → Y i ⟶ X) : (Topology.IsInducing fun (x : (F.obj (Opposite.op X)).α) (g : (Z : C) × { h : Z ⟶ X // (CategoryTheory.Sieve.ofArrows Y f).arrows h }) => ↑(F.map (↑g.snd).op) x) ↔ Topology.IsInducing fun (x : (F.obj (Opposite.op X)).α) (i : I) => ↑(F.map (f i).op) x

The topology induced by restriction along every arrow of a sieve generated by a family is equivalently induced by restriction along the generating family itself.

theorem TauCeti.TopCommRingCat.isSheafFor_of_isSheafFor_forget {C : Type u} [CategoryTheory.Category.{w, u} C] (F : CategoryTheory.Functor Cᵒᵖ TopCommRingCat) {X : C} (S : CategoryTheory.Sieve X) (hS : CategoryTheory.Presieve.IsSheafFor (F.comp (CategoryTheory.forget TopCommRingCat)) S.arrows) (hind : Topology.IsInducing fun (x : (F.obj (Opposite.op X)).α) (g : (Y : C) × { f : Y ⟶ X // S.arrows f }) => ↑(F.map (↑g.snd).op) x) (E : TopCommRingCat) : CategoryTheory.Presieve.IsSheafFor (F.comp (CategoryTheory.coyoneda.obj (Opposite.op E))) S.arrows

The sheaf condition for one sieve. Let S be a sieve on X for which the presheaf of sets underlying F satisfies the sheaf condition, and such that the map sending x ∈ F(X) to its restrictions along the arrows Y ⟶ X of S is inducing for the product topology. Then, for every topological commutative ring E, the presheaf F ⋙ coyoneda.obj (op E) of morphisms out of E satisfies the sheaf condition for S. See isSheaf_of_isSheaf_forget for the sheaf property over a Grothendieck topology.

theorem TauCeti.TopCommRingCat.isSheaf_of_isSheaf_forget {C : Type u} [CategoryTheory.Category.{w, u} C] (F : CategoryTheory.Functor Cᵒᵖ TopCommRingCat) (J : CategoryTheory.GrothendieckTopology C) (hF : CategoryTheory.Presheaf.IsSheaf J (F.comp (CategoryTheory.forget TopCommRingCat))) (hind : ∀ ⦃X : C⦄, ∀ S ∈ J X, Topology.IsInducing fun (x : (F.obj (Opposite.op X)).α) (g : (Y : C) × { f : Y ⟶ X // S.arrows f }) => ↑(F.map (↑g.snd).op) x) : CategoryTheory.Presheaf.IsSheaf J F

Sheaves from sheaves of sets. A presheaf F of topological commutative rings on a site (C, J) is a sheaf once its underlying presheaf of sets is a sheaf and, for every covering sieve S on X, the map sending x ∈ F(X) to its restrictions along the arrows Y ⟶ X of S is inducing for the product topology. The single-sieve form is isSheafFor_of_isSheafFor_forget. Compare CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget, which covers forgetful functors that preserve limits and reflect isomorphisms; here the inducing hypothesis hind supplies the topological half of the sheaf condition.