Continuous gluing for finite Laurent covers

For a strongly noetherian Tate ring, sections on a rational open carry the topology induced by restriction to the sieve of any finite Laurent cover. Consequently, Laurent gluing is valid for continuous ring homomorphisms, not just for elements: compatible continuous homomorphisms into the rings of sections glue to a unique continuous homomorphism.

This is the topological form of finite Laurent gluing needed to pass from Laurent covers to standard rational covers. Neither completeness nor Hausdorffness of the original ring is required; the rings of sections are complete and separated by construction.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 8.34(i) and Remark 8.20.
• S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis, §8.2.2, Lemma 2.

theorem TauCeti.ValuationSpectrum.isInducing_presentationLimitPresheafMap_laurentSieve {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) {W : TopologicalSpace.Opens ↑(spa Aplus)} (hW : W ∈ spaRationalOpens Aplus) : Topology.IsInducing fun (x : ((presentationLimitPresheaf P Aplus).obj (Opposite.op W)).obj.α) (g : (V : TopologicalSpace.Opens ↑(spa Aplus)) × { f : V ⟶ W // (laurentSieve Aplus T W).arrows f }) => ↑((presentationLimitPresheaf P Aplus).map (↑g.snd).op).hom x

Sections on a rational open have the topology induced by their restrictions to the sieve of a finite Laurent cover. This is the topological assertion in finite Laurent gluing.

theorem TauCeti.ValuationSpectrum.isSheafFor_laurentSieve_topCommRingCat {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) {W : TopologicalSpace.Opens ↑(spa Aplus)} (hW : W ∈ spaRationalOpens Aplus) (E : TopCommRingCat) : CategoryTheory.Presieve.IsSheafFor ((presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))) (laurentSieve Aplus T W).arrows

The presentation-limit presheaf, viewed as a presheaf of topological commutative rings, satisfies the sheaf condition for every finite Laurent cover of a rational open. Equivalently, compatible continuous ring homomorphisms from any topological commutative ring into the sections on the cover glue uniquely to a continuous ring homomorphism into sections on the original open.