Spectral maps of adic spectra

A continuous morphism of Huber pairs induces a continuous map of adic spectra. The map is spectral when the image of every open ideal again generates an open ideal: the preimage of each rational open is then rational, hence quasi-compact. For a Tate source, every open ideal is the unit ideal, so this condition holds for every morphism into a Huber ring. These statements give the compact-open control needed when pulling back the rational basis along morphisms.

It suffices to test openness on the image of one ideal of definition of the source. The criterion does not require the underlying ring map to be open or surjective.

Main results

• spaComap_preimage_mem_spaRationalFamily_of_isOpen_map_extendedIdealOfDefinition: the rational-preimage result under the ideal-of-definition criterion.
• spaComap_preimage_mem_spaRationalFamily_of_isTateRing: the rational-preimage result for a Tate source.
• isSpectralMap_spaComap: the resulting map on adic spectra is spectral.
• isSpectralMap_spaComap_of_isOpen_map_extendedIdealOfDefinition: it suffices to test one extended ideal of definition.
• isSpectralMap_spaComap_of_isTateRing: every morphism from a Tate Huber pair is spectral.

The unbundled rational-preimage criterion is in Spa/RationalSubset/Basis.lean.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, §6.5 for related adic homomorphisms and Proposition 6.25 on maps from Tate rings, Definition 7.14(4) for morphisms of Huber pairs, Remark and Definition 7.28 for their induced maps on Spa, and Theorem 7.35 for the rational basis of quasi-compact opens used here.
• R. Huber, Continuous valuations, Math. Z. 212 (1993), §3, for adic spectra and their rational subsets.

theorem TauCeti.Huber.Pair.Hom.spaComap_preimage_mem_spaRationalFamily {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) (hopen : ∀ (J : Ideal A), IsOpen ↑J → IsOpen ↑(Ideal.map f.toRingHom J)) {U : Set ↑(ValuationSpectrum.spa S.plus)} (hU : U ∈ ValuationSpectrum.spaRationalFamily S.plus) : f.spaComap ⁻¹' U ∈ ValuationSpectrum.spaRationalFamily T.plus

Under the openness hypothesis, the preimage of a rational open under a Huber-pair morphism is again rational.

theorem TauCeti.Huber.Pair.Hom.isSpectralMap_spaComap {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) (hopen : ∀ (J : Ideal A), IsOpen ↑J → IsOpen ↑(Ideal.map f.toRingHom J)) : IsSpectralMap f.spaComap

The adic-spectrum map of a Huber-pair morphism is spectral when images of open ideals are open.

theorem TauCeti.Huber.Pair.Hom.spaComap_preimage_mem_spaRationalFamily_of_isOpen_map_extendedIdealOfDefinition {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) (P : PairOfDefinition A) (hP : IsOpen ↑(Ideal.map f.toRingHom P.extendedIdealOfDefinition)) {U : Set ↑(ValuationSpectrum.spa S.plus)} (hU : U ∈ ValuationSpectrum.spaRationalFamily S.plus) : f.spaComap ⁻¹' U ∈ ValuationSpectrum.spaRationalFamily T.plus

It is enough to check openness on the image of one ideal of definition: openness of every other source ideal then transports along the ring homomorphism. Rational opens therefore pull back to rational opens.

theorem TauCeti.Huber.Pair.Hom.isSpectralMap_spaComap_of_isOpen_map_extendedIdealOfDefinition {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) (P : PairOfDefinition A) (hP : IsOpen ↑(Ideal.map f.toRingHom P.extendedIdealOfDefinition)) : IsSpectralMap f.spaComap

Openness of the image of one ideal of definition makes the induced map spectral.

theorem TauCeti.Huber.Pair.Hom.spaComap_preimage_mem_spaRationalFamily_of_isTateRing {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) {U : Set ↑(ValuationSpectrum.spa S.plus)} (hU : U ∈ ValuationSpectrum.spaRationalFamily S.plus) : f.spaComap ⁻¹' U ∈ ValuationSpectrum.spaRationalFamily T.plus

Rational opens pull back to rational opens for a morphism from a Tate Huber pair. No Tate assumption is needed on the target.

theorem TauCeti.Huber.Pair.Hom.isSpectralMap_spaComap_of_isTateRing {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {S : Pair A} {T : Pair B} (f : S.Hom T) : IsSpectralMap f.spaComap

A morphism from a Tate Huber pair induces a spectral map of adic spectra.