The structure presheaf is the limit of its values on rational opens

Wedhorn §8.1 defines 𝒪_X(V), for an open V ⊆ Spa(A, A⁺), as the limit of 𝒪_X(W) over the rational opens W ⊆ V. This file proves that presentationLimitPresheaf, whose value at V is a limit over presentations, has this property naturally in V: it is the pointwise right Kan extension of its restriction to the rational opens (rationalOpensFunctor). Since the rational opens form a basis, a right Kan extension along their inclusion of a sheaf for the restricted topology is a sheaf, so the sheaf condition on Spa(A, A⁺) reduces to the rational opens, as in the proof of Wedhorn's Proposition A.4.

Main definitions

• TauCeti.ValuationSpectrum.presentationLimitPresheafIsPointwiseRightKanExtension : presentationLimitPresheaf is the pointwise right Kan extension of its restriction to the rational opens.

Main results

• TauCeti.ValuationSpectrum.isAdapted_presentationLimitPresheaf : presentationLimitPresheaf is adapted to the rational opens, in the sense of TopCat.Presheaf.IsAdapted.
• TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_of_isSheaf_rational : presentationLimitPresheaf is a sheaf once its restriction to the rational opens is a sheaf for the restricted topology.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1 and Proposition A.4.
• 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: a right Kan extension of a sheaf along a cocontinuous functor is a sheaf. This is Mathlib's CategoryTheory.ran_isSheaf_of_isCocontinuous; see also The Stacks Project, Tag 00XK.

Indices as rational opens

Cones over the rational opens

The Kan extension and the sheaf condition

noncomputable def TauCeti.ValuationSpectrum.presentationLimitPresheafIsPointwiseRightKanExtension {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} : (CategoryTheory.Functor.RightExtension.mk (presentationLimitPresheaf P Aplus) (CategoryTheory.CategoryStruct.id ((rationalOpensFunctor Aplus).op.comp (presentationLimitPresheaf P Aplus)))).IsPointwiseRightKanExtension

presentationLimitPresheaf is the right Kan extension of its restriction to the rational opens, pointwise: at every open V, its value with the restriction maps to the rational opens W ⊆ V is a limit cone over those W. This is Wedhorn §8.1's description of 𝒪_X(V) as the limit of 𝒪_X(W) over the rational W ⊆ V.

Equations

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

theorem TauCeti.ValuationSpectrum.presentationLimitPresheaf_coneAt_π_app {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (V : TopologicalSpace.Opens ↑(spa Aplus)) (g : CategoryTheory.StructuredArrow (Opposite.op V) (rationalOpensFunctor Aplus).op) : ((CategoryTheory.Functor.RightExtension.mk (presentationLimitPresheaf P Aplus) (CategoryTheory.CategoryStruct.id ((rationalOpensFunctor Aplus).op.comp (presentationLimitPresheaf P Aplus)))).coneAt (Opposite.op V)).π.app g = (presentationLimitPresheaf P Aplus).map (CategoryTheory.homOfLE ⋯).op

The legs of the Kan-extension cone are the restriction maps: at an open V, the leg of the cone of presentationLimitPresheafIsPointwiseRightKanExtension indexed by a rational open W ⊆ V (an object g of the category of rational opens over V) is the restriction map from V to W.

theorem TauCeti.ValuationSpectrum.isAdapted_presentationLimitPresheaf {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} : TopCat.Presheaf.IsAdapted (presentationLimitPresheaf P Aplus) (spaRationalOpens Aplus)

presentationLimitPresheaf is adapted to the rational opens: at every open V, it is the limit of its values on the rational opens W ⊆ V. This is Wedhorn §8.1's description of 𝒪_X(V) in the sense of Wedhorn's Remark and Definition 8.9.

theorem TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_of_isSheaf_rational {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (h : CategoryTheory.Presheaf.IsSheaf ((rationalOpensFunctor Aplus).restrictedTopology (Opens.grothendieckTopology ↑(spa Aplus))) ((rationalOpensFunctor Aplus).op.comp (presentationLimitPresheaf P Aplus))) : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa Aplus)) (presentationLimitPresheaf P Aplus)

The sheaf condition on the rational opens suffices: if the restriction of presentationLimitPresheaf to the rational opens is a sheaf for the restricted topology, then presentationLimitPresheaf is a sheaf on Spa(A, A⁺). With the rational opens as the basis, this is the step in the proof of Wedhorn's Proposition A.4 from a sheaf on the basis to a sheaf on the whole space: presentationLimitPresheaf is adapted to the basis of rational opens, and a presheaf adapted to a basis is a sheaf once it is a sheaf on the basis (TopCat.Presheaf.isSheaf_of_isAdapted_of_isSheaf_restrictedTopology). A sieve on a rational open covers for the restricted topology exactly when its image covers in Spa(A, A⁺) (Functor.mem_restrictedTopology_iff), so the hypothesis only involves covers of rational opens by rational opens.