Completion matches rational subsets

For a Huber ring A with a compatible uniform structure and any subring A⁺ ⊆ A, the homeomorphism

Spa (Â, Â⁺) ≃ₜ Spa (A, A⁺)

of spaCompletionHomeomorph identifies the rational subsets of the two sides. Together with spaCompletionHomeomorph this completes Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.48.

Both directions go through the description of the homeomorphism as pullback along the completion map ι : A → Â. Pushing a rational subset of Spa (Â, Â⁺) down is available for any continuous map with dense range, as exists_mem_spaRationalFamily_spaComap_preimage_eq_of_denseRange, which produces a rational subset downstairs whose preimage it is; the homeomorphism is surjective, so that preimage description turns into an image description. Pulling a rational subset of Spa (A, A⁺) up sends R(T/s) to R(ι(T)/ι(s)) by spaComap_preimage_rationalSubset, and the side condition that the numerator ideal ι(T) · Â be open — which is part of what membership in spaRationalFamily means — is TauCeti.Huber.isOpen_map_coeRingHom: the ideal of Â generated by the image of an open ideal of A is open.

As for spaCompletionHomeomorph itself, no completeness, Tate or Noetherian hypothesis is needed and A⁺ is an arbitrary subring.

Main results

• TauCeti.ValuationSpectrum.spaCompletionHomeomorph_preimage_mem_spaRationalFamily: the preimage of a rational subset of Spa (A, A⁺) is a rational subset of Spa (Â, Â⁺).
• TauCeti.ValuationSpectrum.spaCompletionHomeomorph_image_mem_spaRationalFamily: the image of a rational subset of Spa (Â, Â⁺) is a rational subset of Spa (A, A⁺).
• TauCeti.ValuationSpectrum.spaCompletionHomeomorph_preimage_mem_spaRationalFamily_iff: the two directions combined, which is the rational clause of Proposition 7.48.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.48.

theorem TauCeti.ValuationSpectrum.spaCompletionHomeomorph_preimage_mem_spaRationalFamily {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) {U : Set ↑(spa Aplus)} (hU : U ∈ spaRationalFamily Aplus) : ⇑(spaCompletionHomeomorph Aplus) ⁻¹' U ∈ spaRationalFamily (completionPlus Aplus)

Rational subsets pull back to rational subsets under completion. The preimage under the homeomorphism of Wedhorn Proposition 7.48 of a rational subset of Spa (A, A⁺) is a rational subset of Spa (Â, Â⁺). A presentation R(T/s) downstairs is carried to R(ι(T)/ι(s)) upstairs.

theorem TauCeti.ValuationSpectrum.spaCompletionHomeomorph_image_mem_spaRationalFamily {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) {V : Set ↑(spa (completionPlus Aplus))} (hV : V ∈ spaRationalFamily (completionPlus Aplus)) : ⇑(spaCompletionHomeomorph Aplus) '' V ∈ spaRationalFamily Aplus

Rational subsets push forward to rational subsets under completion. The image under the homeomorphism of Wedhorn Proposition 7.48 of a rational subset of Spa (Â, Â⁺) is a rational subset of Spa (A, A⁺).

theorem TauCeti.ValuationSpectrum.spaCompletionHomeomorph_preimage_mem_spaRationalFamily_iff {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) {U : Set ↑(spa Aplus)} : ⇑(spaCompletionHomeomorph Aplus) ⁻¹' U ∈ spaRationalFamily (completionPlus Aplus) ↔ U ∈ spaRationalFamily Aplus

Wedhorn Proposition 7.48, rational clause: the homeomorphism Spa (Â, Â⁺) ≃ₜ Spa (A, A⁺) matches rational subsets. A subset of Spa (A, A⁺) is rational exactly when its preimage in Spa (Â, Â⁺) is.