The adic spectrum of a topological localization

For a rational subset R(T/s) of Spa(A, A⁺), Wedhorn first equips the algebraic localization Aₛ with a topology for which the fractions t/s are power-bounded. Its plus ring is the integral closure of A⁺[T/s] in Aₛ. This file identifies the adic spectrum of that topological localization with the rational subset:

Spa(A(T/s), A(T/s)⁺) ≃ₜ R(T/s).

Pullback along A → Aₛ is an embedding because pullback embeds the whole valuation spectrum of a localization. Surjectivity is the extension theorem from Localization.Surjective. The completed coordinate ring A⟨T/s⟩ requires a further extension of continuous valuations along the dense completion map and is intentionally not identified here.

Main definitions

• TauCeti.ValuationSpectrum.spaLocalizationToRationalSubset: pullback from the adic spectrum of A(T/s) to R(T/s).
• TauCeti.ValuationSpectrum.spaLocalizationHomeomorph: the resulting canonical homeomorphism.

Main results

• TauCeti.ValuationSpectrum.spaLocalizationHomeomorph_apply_val: the forward map is pullback along A → A(T/s).
• TauCeti.ValuationSpectrum.val_comp_spaLocalizationHomeomorph: composing the homeomorphism with the inclusion into Spa(A, A⁺) is spaComap.
• TauCeti.ValuationSpectrum.comap_spaLocalizationHomeomorph_symm_apply: the inverse extends a point of the rational subset.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Proposition and Definition 5.51 and §8.1.

Provenance

The construction combines this repository's localization embedding and valuation-extension results. It follows no external formalization.

noncomputable def TauCeti.ValuationSpectrum.spaLocalizationToRationalSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (s : A) (S : Type u_3) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : ↑(spa (integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S).toSubring) → ↑(Subtype.val ⁻¹' rationalSubset Aplus T s)

Pullback along A → A(T/s), corestricted from the adic spectrum of the topological localization to the rational subset R(T/s).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ValuationSpectrum.spaLocalizationToRationalSubset_apply_val {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (s : A) (S : Type u_3) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (v : ↑(spa (integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S).toSubring)) : ↑↑(spaLocalizationToRationalSubset P Aplus T s S hden v) = comap (algebraMap A S) ↑v

The map to the rational subset is pullback along A → A(T/s) on underlying valuations.

theorem TauCeti.ValuationSpectrum.isEmbedding_spaLocalizationToRationalSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (s : A) (S : Type u_3) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : Topology.IsEmbedding (spaLocalizationToRationalSubset P Aplus T s S hden)

The canonical map from the localization spectrum to the rational subset is a topological embedding.

theorem TauCeti.ValuationSpectrum.surjective_spaLocalizationToRationalSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_3) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : Function.Surjective (spaLocalizationToRationalSubset P Aplus T s S hden)

Every point of R(T/s) is extended by the canonical map from the localization spectrum.

noncomputable def TauCeti.ValuationSpectrum.spaLocalizationHomeomorph {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_3) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : ↑(spa (integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S).toSubring) ≃ₜ ↑(Subtype.val ⁻¹' rationalSubset Aplus T s)

The adic spectrum of the topological localization A(T/s), with plus ring the integral closure of A⁺[T/s], is canonically homeomorphic to the rational subset R(T/s).

The hypothesis A₀ ≤ A⁺ ensures that extending a continuous valuation to the localization is continuous; a pair of definition satisfying it exists for every ring of integral elements.

Equations

• TauCeti.ValuationSpectrum.spaLocalizationHomeomorph P Aplus hP T s S hden = ⋯.toHomeomorphOfSurjective ⋯

@[simp]

theorem TauCeti.ValuationSpectrum.spaLocalizationHomeomorph_apply_val {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_3) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (v : ↑(spa (integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S).toSubring)) : ↑↑((spaLocalizationHomeomorph P Aplus hP T s S hden) v) = comap (algebraMap A S) ↑v

The forward map of spaLocalizationHomeomorph is pullback along A → A(T/s).

theorem TauCeti.ValuationSpectrum.val_comp_spaLocalizationHomeomorph {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : Subtype.val ∘ ⇑(spaLocalizationHomeomorph P Aplus hP T s S hden) = spaComap (algebraMap A S) ⋯ Aplus (integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S).toSubring ⋯

The homeomorphism of spaLocalizationHomeomorph, followed by the inclusion of R(T/s) into Spa(A, A⁺), is pullback along A → A(T/s).

@[simp]

theorem TauCeti.ValuationSpectrum.comap_spaLocalizationHomeomorph_symm_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_3) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (v : ↑(Subtype.val ⁻¹' rationalSubset Aplus T s)) : comap (algebraMap A S) ↑((spaLocalizationHomeomorph P Aplus hP T s S hden).symm v) = ↑↑v

Pulling the valuation supplied by the inverse homeomorphism back to A recovers the original point of R(T/s).