The residue field of a point as a topological field

residueFieldValuation v topologises the residue field κ(v) of a point v : Spv A, through Mathlib's type synonym WithVal. This file describes the canonical map A → κ(v) for that topology: the valuation it computes, and its continuity when v is a continuous point.

The algebraic content of κ(v) — the residue ring, the three valuations and their characteristic equations — is in TauCeti.AlgebraicGeometry.AdicSpace.ResidueField.Basic, which carries no topology. This file is where the topology enters, so that a consumer of κ(v) as a field need not depend on the continuous-valuation API.

Main results

• TauCeti.ValuationSpectrum.valued_algebraMap_residueFieldValuation: the valuation topologising κ(v) takes the image of a : A to v.valuation a.
• TauCeti.ValuationSpectrum.continuous_algebraMap_residueFieldValuation: for a continuous point of a ring with separately continuous operations, A → κ(v) is continuous.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §2.4 for the residue field and Definition 7.7 for continuity of a valuation.

@[simp]

theorem TauCeti.ValuationSpectrum.valued_algebraMap_residueFieldValuation {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) (a : A) : Valued.v ((algebraMap A (WithVal v.residueFieldValuation)) a) = v.valuation a

The valuation topologising κ(v) takes the image of a : A to v.valuation a. The residue field carries the topology of residueFieldValuation v through Mathlib's type synonym WithVal, and Valued.v is that valuation.

This is the characteristic equation of residueFieldValuation at the level of A itself, rather than of the residue ring A ⧸ supp v.

theorem TauCeti.ValuationSpectrum.continuous_algebraMap_residueFieldValuation {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsSemitopologicalRing A] {v : ValuationSpectrum A} (hv : v.IsContinuous) : Continuous ⇑(algebraMap A (WithVal v.residueFieldValuation))

A continuous point maps continuously to its residue field. If v : Spv A is continuous then the canonical map A → WithVal (residueFieldValuation v) is continuous, κ(v) carrying the topology of residueFieldValuation v.

Separate continuity of the ring operations is enough: the topology and the ring structure of A are related only through translations and multiplication by a constant. Continuity is what lets the map be extended along a completion of A.