Proper ideals supplied by continuous valuations survive completion

Let v be a continuous valuation on a topological ring A. Its support is closed because v is locally constant away from its support.

This closedness has an algebraic consequence needed for rational covers. The ideal generated by the image of supp v in the separated completion Â is proper. Indeed, the map A → (A / supp v)̂ extends through Â because its target is complete and Hausdorff. Closedness of supp v makes the quotient separated and its completion nonzero. The resulting map  → (A / supp v)̂ kills the extended support but not 1.

Main results

• TauCeti.map_supp_completion_ne_top_of_isContinuous: the support remains proper after extension to the separated completion.

References

• T. Wedhorn, Adic Spaces, Definition 7.7 and Corollary 8.32.

Provenance

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, file projects/AdicSpaces/Adic spaces/IdealLocalizationCompletion.lean, was consulted to compare the completion prerequisites used by its conditional approach to Corollary 8.32. It does not contain the closed-support argument here; no code is ported.

theorem TauCeti.map_supp_completion_ne_top_of_isContinuous {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] {v : Valuation A Γ₀} (hv : v.IsContinuous) : Ideal.map UniformSpace.Completion.coeRingHom v.supp ≠ ⊤

The support of a continuous valuation remains proper in the separated completion.

The ideal generated by the image of supp v under the completion map is not the unit ideal. No completeness or Hausdorff assumption on the original ring is required. The value monoid must be nontrivial so that the support is proper.