Transporting the sheaf property along isomorphisms and completion

This file compares the presentation-limit presheaves presentationLimitPresheaf of two topological rings, each with a pair of definition and a subring (the plus subring A⁺, B⁺), whose adic spectra correspond, and shows that one is a sheaf exactly when the other is. The plus subrings need not be rings of integral elements:

• along an isomorphism of topological rings e : A ≃+* B, continuous in both directions, carrying A⁺ onto B⁺. The pairs of definition of A and of B are arbitrary, and no condition is put on A⁺. At the identity of A this compares two pairs of definition of one ring.
• along the completion A → Â of a Huber ring A with a uniform structure, with Â⁺ the closure of the image of A⁺, when every element of A⁺ is power-bounded. The pairs of definition of A and of Â are arbitrary. The adic spectra are then identified by Wedhorn's Proposition 7.48 (spaCompletionHomeomorph), and Â⟨T/s⟩ with A⟨T/s⟩.

In both cases the presentation-limit presheaf of (A, A⁺) is isomorphic to the pushforward of the other along the homeomorphism of adic spectra; its components are built from the base-change maps between completed rational localisations of TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.BaseChange.

The consequences for TauCeti.Huber.IsSheafyForEveryPresentation are in TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.SheafForEveryPresentation.

Main results

• TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_iff_of_ringEquiv : invariance of the sheaf property under isomorphism.
• TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_completionPlus_iff : invariance of the sheaf property under completion.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition and Definition 5.51 (the universal property of A⟨T/s⟩), Proposition 7.48 (the adic spectrum of the completion) and §8.1 (the structure presheaf).

The comparison maps of presentation limits along an isomorphism

The isomorphism of presheaves

theorem TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_iff_of_ringEquiv {A B : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] {P : Huber.PairOfDefinition A} {P' : Huber.PairOfDefinition B} {Aplus : Subring A} {Bplus : Subring B} (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hplus : Subring.map (↑e) Aplus = Bplus) : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa Aplus)) (presentationLimitPresheaf P Aplus) ↔ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa Bplus)) (presentationLimitPresheaf P' Bplus)

Sheafhood of the presentation limit is invariant under isomorphism. If e : A ≃+* B is an isomorphism of topological rings carrying A⁺ onto B⁺, then the presentation-limit presheaf of Spa(A, A⁺) for a pair of definition P of A is a sheaf exactly when that of Spa(B, B⁺) for a pair of definition P' of B is. The two pairs of definition are arbitrary.

Maps between A⟨T/s⟩ and Â⟨T/s⟩

Invariance under completion

theorem TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_completionPlus_iff {A : Type v} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [Huber.IsHuberRing A] (P : Huber.PairOfDefinition A) (P' : Huber.PairOfDefinition (UniformSpace.Completion A)) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa (completionPlus Aplus))) (presentationLimitPresheaf P' (completionPlus Aplus)) ↔ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa Aplus)) (presentationLimitPresheaf P Aplus)

Sheafhood of the presentation limit is invariant under completion. If A⁺ consists of power-bounded elements and Â⁺ is the closure of its image in the completion Â, the presentation-limit presheaf of Spa(Â, Â⁺) for a pair of definition P' of Â is a sheaf exactly when that of Spa(A, A⁺) for a pair of definition P of A is.