Rational subsets descend along dense maps of Huber rings

A generalization of the rational half of Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.48. Wedhorn states that for an affinoid ring A the canonical map Spa  → Spa A is a homeomorphism which maps rational subsets to rational subsets. This file proves the preimage direction, and the inducing property it gives, for an arbitrary continuous ring homomorphism φ : A → B with dense image between Huber rings: every rational subset of Spa(B, B⁺) is the preimage under spaComap φ of a rational subset of Spa(A, A⁺). Wedhorn's image statement additionally needs spaComap φ to be surjective, which is not proved here. Neither ring is assumed complete, and the plus rings A⁺ ⊆ A and B⁺ ⊆ B are arbitrary subrings with φ(A⁺) ⊆ B⁺.

Main results

• TauCeti.ValuationSpectrum.exists_mem_spaRationalFamily_spaComap_preimage_eq_of_denseRange: every member of the rational family of Spa(B, B⁺) is the preimage under spaComap φ of a member of the rational family of Spa(A, A⁺).
• TauCeti.ValuationSpectrum.isInducing_spaComap_of_denseRange: spaComap φ is inducing.
• TauCeti.Huber.Pair.Hom.exists_mem_spaRationalFamily_spaComap_preimage_eq_of_denseRange and TauCeti.Huber.Pair.Hom.isInducing_spaComap_of_denseRange: the same two results for a morphism of Huber pairs whose underlying ring homomorphism has dense range.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.48, proved there by reference to R. Huber, Continuous valuations, Math. Z. 212 (1993), Proposition 3.9.
• C. Birkbeck, AINTLIB, branch dev/adic-spaces, commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, Apache-2.0, projects/AdicSpaces/Adic spaces/.

Provenance

Adapted from AINTLIB, not ported (C. Birkbeck; github.com/CBirkbeck/AINTLIB, Apache-2.0, branch dev/adic-spaces, commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, projects/AdicSpaces/Adic spaces/). AINTLIB proves the corresponding descent only for the canonical map from a complete Tate ring to a completed rational localisation of it, as part of its Wedhorn 8.2(2) comparison. The correspondence is:

• SpaRationalSubsetCorrespondence.lean, exists_downstairs_rationalDatum — AINTLIB's form of exists_mem_spaRationalFamily_spaComap_preimage_eq_of_denseRange;
• SpaParameterPerturbation.lean, exists_uniform_spanning_bound and indexedRationalSet_perturb_eq — its padding and perturbation steps, which correspond to TauCeti.Huber.exists_isOpen_span_forall_sub_mem_of_denseRange and exists_finset_subset_isOpen_span in TauCeti/RingTheory/Huber/OpenIdeal.lean;
• SpaRationalOpenHomeomorph.lean, exists_A_level_open_presentation and spaPresheafValueEquivRationalOpen_isOpenMap — its open-presentation and open-map steps.

What changed: the rings are Huber rather than Tate and neither is complete; the map is any continuous ring homomorphism with dense range rather than the canonical map to a completed rational localisation; the plus rings are arbitrary subrings where AINTLIB requires rings of integral elements; numerator ideals are only open where AINTLIB asks for the unit ideal; the descended numerators are enlarged by a finite set generating an open ideal of A where AINTLIB pads by a power of a topologically nilpotent unit; and the perturbation step is TauCeti's Huber-ring form of Proposition 7.34. No code is copied.

theorem TauCeti.ValuationSpectrum.exists_mem_spaRationalFamily_spaComap_preimage_eq_of_denseRange {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [Huber.IsHuberRing A] [Huber.IsHuberRing B] {φ : A →+* B} (hφc : Continuous ⇑φ) (hφ : DenseRange ⇑φ) (Aplus : Subring A) (Bplus : Subring B) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) {U : Set ↑(spa Bplus)} (hU : U ∈ spaRationalFamily Bplus) : ∃ W ∈ spaRationalFamily Aplus, spaComap φ hφc Aplus Bplus hplus ⁻¹' W = U

Rational subsets descend along a dense map (a generalization of the rational half of Wedhorn Proposition 7.48). If φ : A → B is a continuous homomorphism of Huber rings with dense image, every member R(T/s) of the rational family of Spa(B, B⁺) is the preimage under spaComap φ of a member R(T'/s') of the rational family of Spa(A, A⁺); that is, R(T/s) = R(φ(T')/φ(s')) with T' · A open.

As the rational family is a basis of Spa(B, B⁺), this makes spaComap φ inducing (isInducing_spaComap_of_denseRange).

theorem TauCeti.ValuationSpectrum.isInducing_spaComap_of_denseRange {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [Huber.IsHuberRing A] [Huber.IsHuberRing B] {φ : A →+* B} (hφc : Continuous ⇑φ) (hφ : DenseRange ⇑φ) (Aplus : Subring A) (Bplus : Subring B) (hplus : ∀ a ∈ Aplus, φ a ∈ Bplus) : Topology.IsInducing (spaComap φ hφc Aplus Bplus hplus)

Pullback of adic spectra along a continuous homomorphism of Huber rings with dense image is inducing. For the completion A → Â this is the inducing part of Wedhorn Proposition 7.48; here neither ring needs to be complete, and A⁺, B⁺ are arbitrary subrings with φ(A⁺) ⊆ B⁺.

Since spa Bplus is T0, Topology.IsInducing.isEmbedding upgrades this to an embedding. Unlike isEmbedding_spaComap, this assumes no embedding of the full valuation spectra along comap φ.

theorem TauCeti.Huber.Pair.Hom.exists_mem_spaRationalFamily_spaComap_preimage_eq_of_denseRange {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) (hf : DenseRange ⇑f.toRingHom) {U : Set ↑(ValuationSpectrum.spa T.plus)} (hU : U ∈ ValuationSpectrum.spaRationalFamily T.plus) : ∃ W ∈ ValuationSpectrum.spaRationalFamily S.plus, f.spaComap ⁻¹' W = U

Rational subsets descend along a morphism of Huber pairs with dense image. Every member of the rational family of Spa(T) is the preimage under f.spaComap of a member of the rational family of Spa(S).

theorem TauCeti.Huber.Pair.Hom.isInducing_spaComap_of_denseRange {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) (hf : DenseRange ⇑f.toRingHom) : Topology.IsInducing f.spaComap

The map of adic spectra induced by a morphism of Huber pairs with dense image is inducing. For the completion morphism this is the inducing part of Wedhorn Proposition 7.48.