Continuous valuations extend to the completion

Let A be a commutative topological ring with a compatible uniform structure, and let ι : A → Â be its Hausdorff completion. Every continuous point of Spv A is the pullback along ι of a continuous point of Spv Â, and consequently pullback along ι maps Spa (Â, Â⁺) onto Spa (A, A⁺), where Â⁺ is the closure of ι(A⁺).

This is the surjectivity half of Wedhorn's Proposition 7.48, for an arbitrary subring A⁺ of an arbitrary commutative topological ring A with a compatible uniform structure: no Huber, Hausdorff or completeness hypothesis is needed, and A⁺ need not be a ring of integral elements. For an affinoid ring, closure (ι A⁺) is Wedhorn's Â⁺ (Lemma 7.47). Together with the corresponding statement for rational subsets, this surjectivity feeds the identification of the adic spectrum of a completed rational localisation with the rational subset it comes from; that identification is a homeomorphism only once the map is also shown to be inducing and injective, the latter through the T0 separation of the adic spectrum.

Main results

• TauCeti.ValuationSpectrum.exists_isContinuous_comap_coeRingHom_eq : a continuous point of Spv A is the pullback of a continuous point of Spv Â.
• TauCeti.ValuationSpectrum.spaComap_coeRingHom_surjective : pullback along A → Â maps Spa (Â, closure (ι A⁺)) onto Spa (A, A⁺).

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 7.47 and Proposition 7.48.
• R. Huber, Continuous valuations, Math. Z. 212 (1993), 445–477, Proposition 3.9, which Wedhorn cites for Proposition 7.48.

Provenance

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, file projects/AdicSpaces/Adic spaces/SpaRationalOpenComparison.lean, was consulted: its scResHom, scResHom_val, scResHom_continuous, comap_coeRingHom_extensionHom_ofValuation_eq and spa_completion_of_spa_localization extend a point along the completion of a rational localisation through the completed residue field. Nothing was copied. Here the ring is an arbitrary commutative uniform topological ring rather than a rational localisation, continuity is the attained-value predicate of Valuation.IsContinuous, and the plus ring of the completion is the closure of the image of A⁺.

theorem TauCeti.ValuationSpectrum.exists_isContinuous_comap_coeRingHom_eq {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {v : ValuationSpectrum A} (hv : v.IsContinuous) : ∃ (w : ValuationSpectrum (UniformSpace.Completion A)), w.IsContinuous ∧ comap UniformSpace.Completion.coeRingHom w = v

Continuous valuations extend to the completion. Every continuous point of Spv A is the pullback along A → Â of a continuous point of Spv Â, where Â is the Hausdorff completion UniformSpace.Completion A.

theorem TauCeti.ValuationSpectrum.spaComap_coeRingHom_surjective {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] (Aplus : Subring A) : Function.Surjective (spaComap UniformSpace.Completion.coeRingHom ⋯ Aplus (Subring.map UniformSpace.Completion.coeRingHom Aplus).topologicalClosure ⋯)

The surjectivity half of Wedhorn Proposition 7.48, for any subring A⁺. Pullback along A → Â maps Spa (Â, Â⁺) onto Spa (A, A⁺), where Â⁺ is the closure of the image of A⁺. This is the adic-spectrum form of exists_isContinuous_comap_coeRingHom_eq.