Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.StronglyNoetherian

Sheafiness of strongly noetherian Tate pairs #

For a strongly noetherian Tate ring A and a ring of integral elements A⁺, the presentation-limit structure presheaf of Spa(A, A⁺) is a sheaf of complete separated topological rings. This is Wedhorn's Theorem 8.28(b) for the pair (A, A⁺); A itself need not be complete or Hausdorff.

Gluing for rational covers of rational opens, including the empty cover, holds both for sections (isSheafFor_ofArrows_spaRationalOpens_of_iSup_eq) and for continuous ring homomorphisms out of an arbitrary topological commutative ring (isSheafFor_ofArrows_spaRationalOpens_of_iSup_eq_topCommRingCat). Intersections of rational opens are rational, so either form is the sheaf condition on the basis of rational opens (isSheaf_rational_comp_of_isSheafFor_ofArrows), and it extends to all opens because the presheaf is the limit of its values on that basis.

Main results #

References #

source
theorem TauCeti.ValuationSpectrum.isSheaf_underlying_presentationLimitPresheaf_of_isStronglyNoetherian {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hP : P.ringOfDefinition ≤ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) :
CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa Aplus)) ((presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat)))

The presheaf of sets underlying the presentation-limit structure presheaf of a strongly noetherian Tate pair is a sheaf on all opens of Spa(A, A⁺). The ring need not be complete or Hausdorff. The ring of definition of P lies in A⁺, which consists of power-bounded elements. This is isSheaf_underlying_presentationLimitPresheaf_of_laurentGluing for strong noetherianness (laurentGluing_isStronglyNoetherian).

source
theorem TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_of_isStronglyNoetherian {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hP : P.ringOfDefinition ≤ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) :
CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa Aplus)) (presentationLimitPresheaf P Aplus)

Wedhorn's Theorem 8.28(b) for a pair: the structure presheaf of a strongly noetherian Tate pair is a sheaf. Let A be a strongly noetherian Tate ring, P a pair of definition whose ring of definition lies in A⁺, and A⁺ a subring of power-bounded elements. Then the presentation-limit structure presheaf of Spa(A, A⁺) is a sheaf of complete separated topological rings on all opens.

A itself need not be complete or Hausdorff.

source
theorem TauCeti.Huber.isSheafyForEveryPresentation_of_isStronglyNoetherian {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [IsTateRing A] [IsStronglyNoetherian A] {Aplus : Subring A} (hAplus : IsRingOfIntegralElements Aplus) :
IsSheafyForEveryPresentation Aplus

Strongly noetherian Tate pairs are sheafy: every ring of integral elements A⁺ of a strongly noetherian Tate ring A satisfies TauCeti.Huber.IsSheafyForEveryPresentation, so the structure presheaf of Spa(A, A⁺) is a sheaf of complete separated topological rings. This is Wedhorn's Theorem 8.28(b) for the pair (A, A⁺); A need not be complete or Hausdorff.

source
theorem TauCeti.Huber.isSheafyRing_of_isStronglyNoetherian {A : Type v} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsTateRing A] [IsStronglyNoetherian A] [CompleteSpace A] [T0Space A] :
IsSheafyRing A

A complete Hausdorff strongly noetherian Tate ring is sheafy in the sense of Wedhorn's Definition 8.26 (TauCeti.Huber.IsSheafyRing). This is Wedhorn's Theorem 8.28(b) for a complete Hausdorff ring.