The space Cont A of continuous valuations

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.7 and Remark 7.9.

Cont A is the subspace of Spv A cut out by continuity. Wedhorn defines it in one line — "the subspace of Spv (A) of continuous valuations" — but that line only makes sense because continuity is a property of the equivalence class, not of a chosen representative. That is what this file supplies, and it is the reason the definition is meaningful at all. Two further results of Wedhorn's come with it: the discrete case (Remark 7.8(2)) and the pullback along a continuous ring homomorphism (Remark 7.9).

Why this is not automatic

A point of Spv A is a valuative relation, so a predicate on valuations descends to it only if equivalent valuations agree on the predicate. For continuity as Wedhorn states it — the quantifier running over the value group Γ_v — that holds, and Valuation.IsEquiv.isContinuous_iff says so. Had continuity instead been asked of every γ in the ambient codomain, it would not descend, and Cont A would not be well defined; the module docstring of TauCeti.RingTheory.Valuation.Continuous.Basic carries the counterexample.

So IsContinuous is defined here by testing the canonical valuation of the point, and isContinuous_ofValuation_iff says the test may equally be run on any representative.

Main definitions

• TauCeti.ValuationSpectrum.IsContinuous : continuity of a point of Spv A, in the attained-value sense.
• TauCeti.ValuationSpectrum.cont : Wedhorn's Cont A, the set of continuous points, cut out by the attained-value test — see its docstring for how that relates to Wedhorn's value-group quantifier.

Main results

• TauCeti.ValuationSpectrum.isContinuous_ofValuation_iff : continuity may be tested on any representative, not only the canonical one — the well-definedness making cont meaningful. Membership ofValuation w ∈ cont A reduces to it through the @[simp] mem_cont_iff.
• TauCeti.ValuationSpectrum.isContinuous_trivialSection_iff : the trivial valuation of a prime is a continuous point exactly when that prime is open — Remark 4.6, and the continuity input to Proposition 7.51.
• TauCeti.ValuationSpectrum.IsContinuous.comap : Remark 7.9, that a continuous ring homomorphism pulls continuous points back to continuous points. Combined with mem_cont_iff this is exactly the statement that comap φ restricts to a map Cont B → Cont A; no separate set-level lemma is kept for it, since that would be this one after unfolding.
• TauCeti.ValuationSpectrum.IsContinuous.quotientLift : continuity descends to the canonical lift through a quotient.
• TauCeti.ValuationSpectrum.closure_zero_subset_supp_of_isContinuous, closure_zero_le_supp_of_isContinuous: every continuous valuation kills the closure of zero.
• TauCeti.ValuationSpectrum.cont_eq_univ : Remark 7.8(2), Cont A = Spv A for discrete A.
• TauCeti.ValuationSpectrum.cont_eq_empty_of_one_mem_closure_zero : if 1 belongs to the closure of zero, then Cont A is empty.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Definition 7.7 and Remarks 7.8, 7.9; Remark 4.6 and Proposition 7.51 for the trivial valuation of an open prime.

Provenance

The corresponding development in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, project projects/AdicSpaces/, file Adic spaces/ContinuousValuations.lean, was consulted rather than copied. Its ValuationSpectrum.IsContinuous also tests the canonical valuation, but because its valuation-level predicate quantifies over the ambient codomain it can only offer the one-way isContinuous_ofValuation_of; the ↔ here is what makes cont well defined.

isContinuous_trivialSection_iff comes from a second file of that same project, Adic spaces/AdicSpectrum.lean, section Prop752, which runs the argument inline for maximal ideals on the way to Wedhorn 7.52(2). It is stated here for prime ideals as a named characterisation, so that the downstream development can cite it instead of repeating it.

def TauCeti.ValuationSpectrum.IsContinuous {A : Type u_1} [CommRing A] [TopologicalSpace A] (v : ValuationSpectrum A) : Prop

Continuity of a point of Spv A. A point is continuous when its canonical valuation is, in the attained-value sense of Valuation.IsContinuous. Any representative would do — that is isContinuous_ofValuation_iff — but the canonical one makes the definition depend on nothing chosen.

Under [ContinuousConstSMul Aᵐᵒᵖ A] this is Wedhorn's Definition 7.7; see cont.

Equations

• v.IsContinuous = v.valuation.IsContinuous

@[simp]

theorem TauCeti.ValuationSpectrum.isContinuous_def {A : Type u_1} [CommRing A] [TopologicalSpace A] (v : ValuationSpectrum A) : v.IsContinuous ↔ v.valuation.IsContinuous

Continuity of a point, unfolded to its canonical valuation.

def TauCeti.ValuationSpectrum.cont (A : Type u_2) [CommRing A] [TopologicalSpace A] : Set (ValuationSpectrum A)

Wedhorn's Cont A: the continuous points of Spv A, as a Set (Spv A). Wedhorn calls it a subspace; here it is the underlying set, and the subspace topology is the one the coercion ↥(cont A) carries as a subtype of Spv A.

Membership is the attained-value test of Valuation.IsContinuous, which is Wedhorn's Definition 7.7 once right multiplication is continuous — isContinuous_iff_forall_isOpen_lt_div is that step, and it is where [ContinuousConstSMul Aᵐᵒᵖ A] is asked for. It is not asked for here: an unused instance argument is a lint violation, and every setting Cont A is used in — a Huber ring, and Spa beyond it — is a topological ring, which supplies it at the point of use.

Equations

• TauCeti.ValuationSpectrum.cont A = {v : TauCeti.ValuationSpectrum A | v.IsContinuous}

@[simp]

theorem TauCeti.ValuationSpectrum.mem_cont_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] (v : ValuationSpectrum A) : v ∈ cont A ↔ v.IsContinuous

theorem TauCeti.ValuationSpectrum.isContinuous_ofValuation_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation A Γ₀) : (ofValuation w).IsContinuous ↔ w.IsContinuous

Continuity may be tested on any representative. This is what makes cont well defined: the point ofValuation w is continuous exactly when w is, for every w in the class, not merely for the canonical one. It rests on Valuation.IsEquiv.isContinuous_iff, and would fail for a continuity predicate quantified over the ambient codomain.

Not @[simp]: isContinuous_def already rewrites the left-hand side, so this would not be in simp-normal form.

theorem TauCeti.ValuationSpectrum.isContinuous_trivialSection_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] (p : PrimeSpectrum A) : (trivialSection p).IsContinuous ↔ IsOpen ↑p.asIdeal

A trivial-valuation point is continuous exactly when its prime ideal is open. Every value set of trivialSection p is ∅ (testing below a vanishing value) or p.asIdeal itself (testing below a surviving value), so continuity amounts to openness of the prime; conversely the test below 1 recovers the ideal. This is the continuity interface of the sealed trivialSection — it rests on trivialSection_vle_iff, not on the definition's body.

This is the continuity half of Wedhorn Remark 4.6, and the input Proposition 7.51 needs to exhibit an open prime as a support. The argument is AINTLIB's, from the Prop752 section cited in this file's Provenance, separated out here as a standalone characterisation.

@[simp]

theorem TauCeti.ValuationSpectrum.cont_eq_univ {A : Type u_1} [CommRing A] [TopologicalSpace A] [DiscreteTopology A] : cont A = Set.univ

Wedhorn Remark 7.8(2). Over a discrete ring every point is continuous.

theorem TauCeti.ValuationSpectrum.closure_zero_subset_supp_of_isContinuous {A : Type u_1} [CommRing A] [TopologicalSpace A] [SeparatelyContinuousAdd A] {v : ValuationSpectrum A} (hv : v.IsContinuous) : closure {0} ⊆ ↑v.supp

The support of every continuous valuation contains the closure of zero. This is the set-level form, needing only separately continuous addition; over a topological ring, closure_zero_le_supp_of_isContinuous states it for the ideal Ideal.closure ⊥.

theorem TauCeti.ValuationSpectrum.cont_eq_empty_of_one_mem_closure_zero {A : Type u_1} [CommRing A] [TopologicalSpace A] [SeparatelyContinuousAdd A] (h : 1 ∈ closure {0}) : cont A = ∅

The 1 ∈ closure {0} → Cont A = ∅ half of Wedhorn Proposition 7.49(1). If 1 ∈ closure {0} in a commutative ring A with separately continuous addition, then Cont A = ∅.

theorem TauCeti.ValuationSpectrum.closure_zero_le_supp_of_isContinuous {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {v : ValuationSpectrum A} (hv : v.IsContinuous) : ⊥.closure ≤ v.supp

The support of every continuous valuation contains the closure of the zero ideal. Equivalently, every continuous valuation factors through the separation quotient.

theorem TauCeti.ValuationSpectrum.IsContinuous.comap {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Type u_2} [CommRing B] [TopologicalSpace B] {φ : A →+* B} (hφ : Continuous ⇑φ) {v : ValuationSpectrum B} (hv : v.IsContinuous) : (ValuationSpectrum.comap φ v).IsContinuous

Wedhorn Remark 7.9. A continuous ring homomorphism pulls continuous points back to continuous points, so it restricts to a map Cont B → Cont A.

theorem TauCeti.ValuationSpectrum.IsContinuous.quotientLift {A : Type u_1} [CommRing A] [TopologicalSpace A] (J : Ideal A) ⦃v : ValuationSpectrum A⦄ (hJ : J ≤ v.supp) (hv : v.IsContinuous) : (ValuationSpectrum.quotientLift J hJ).IsContinuous

Continuity of the lifted valuation on the quotient ring A ⧸ J.