feat(RingTheory/Valuation): define the valuation spectrum and its topology by CBirkbeck · Pull Request #38009 · leanprover-community/mathlib4

CBirkbeck · 2026-04-13T15:42:51Z

Summary

Define the valuation spectrum Spv A of a commutative ring and equip it with the topology generated by basic open sets, following Wedhorn's Adic Spaces. Also define the pullback (comap) of a ValuativeRel along a ring homomorphism. This is preparation for later defining adic spaces.

Note the code was generated by claude code, but I have cleaned up and pre-reviewed the work.

…ology Define the valuation spectrum `Spv A` of a commutative ring as the type of valuative relations on `A`, following Definition 4.1 of Wedhorn's *Adic Spaces*. Equip it with the topology generated by basic open sets `{ v | v(f) ≤ v(s) ∧ v(s) ≠ 0 }`. ## New files * `ValuativeRel/Comap.lean`: Pullback of a `ValuativeRel` along a ring homomorphism, and the lemma that units cannot map to zero. * `ValuationSpectrum.lean`: The valuation spectrum with: - basic open sets and their properties - contravariant functoriality (`comap`) and its continuity - support map `Spv A → Spec A` and its continuity - quotient lifting and topological embedding - localization lifting and range characterization Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

github-actions · 2026-04-13T15:43:57Z

PR summary bc7bce2142

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Valuation.ValuativeRel.Comap` (new file)	1163
`Mathlib.RingTheory.Valuation.ValuationSpectrum` (new file)	1798

Declarations diff

+ IsUnit.not_vle_zero
+ ValuationSpectrum
+ basicOpen
+ basicOpen_mul_subset
+ basicOpen_one
+ basicOpen_self
+ comap_continuous
+ comap_injective
+ comap_localizationLift
+ comap_localization_range
+ comap_ofValuation
+ comap_preimage_basicOpen
+ comap_quotientLift
+ comap_quotient_isEmbedding
+ comap_quotient_range
+ ideal_le_supp_comap_mk
+ instIsPrimeSupp
+ instTopologicalSpace
+ localizationLift
+ mem_supp_iff
+ not_vle_zero_of_isUnit
+ ofValuation
+ ofValuation_eq_of_isEquiv
+ ofValuation_valuation
+ quotientLift
+ quotientLift_comap
+ submonoid_le_supp_primeCompl_comap_algebraMap
+ supp
+ suppFun
+ suppFun_asIdeal
+ suppFun_comap
+ suppFun_continuous
+ suppFun_preimage_basicOpen
+ supp_eq_valuation_supp
+ supp_ofValuation
+ valuation
+ vle_ofValuation
++ comap
++ comap_comp
++ comap_id
++ comap_vle

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…cstrings Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…rings The module docstring already references Wedhorn; no need to repeat it on individual declarations. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Both files were missing the `module` keyword, `public import`, and `@[expose] public section` required by the Lean 4 module system. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

riccardobrasca

I stopped around line 150 of ValuationSpectrum.lean. In my opinion something is not optimal with the design, there too many let and @. I will have a closer look after the various easy comments are taken into account.

Anyway this is surely a great addition!

Comap.lean: - @[reducible] → @[implicit_reducible] - use ≤ᵥ notation in comap field body - comap_vle now returns ↔ / Iff.rfl (these are Props) - rename ValuativeRel.not_vle_zero_of_isUnit → IsUnit.not_vle_zero (enables dot notation hu.not_vle_zero) - golf not_vle_zero proof to a single simpa ValuationSpectrum.lean: - fix Wedhorn bib key (wedhorn_adic) - basicOpen_mul_subset: refactor with refine + simpa - docstrings: Spv(φ) → comap φ, v ∈ Spv A → v : Spv A - comap_id, comap_comp: by ext; rfl - instIsPrimeSupp: term-mode inferInstanceAs - add @[simp] rfl lemma vle_ofValuation and eliminate change in supp_ofValuation - replace let := with letI := for typeclass instance bindings Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Add ValuativeRel.comap_id and ValuativeRel.comap_comp in Comap.lean as named rfl lemmas. Use them in ValuationSpectrum.comap_id / comap_comp via congr_arg (·.vle), rather than closing the underlying goal with a bare rfl. Addresses reviewer comment on line 117. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

adamtopaz · 2026-04-15T15:06:19Z

Pinging @dagurtomas and @chrisflav since they have been working on similar things.

dagurtomas · 2026-04-15T15:21:12Z

All that we have done so far lives in the draft PR #30978. I haven't touched it in a while, but it certainly contains the definition of Spv, the topology, and comap.

CBirkbeck · 2026-04-15T15:28:56Z

All that we have done so far lives in the draft PR #30978. I haven't touched it in a while, but it certainly contains the definition of Spv, the topology, and comap.

Oh interesting, I didnt know about this PR. I'm working towards proving Tate acyclicity and defining the adic Fargues--Fontaine curve, so there will likely be lots of overlap, so maybe we should coordinate. I see that in #30978 the Spv definition is def Spv (R : Type u) [CommRing R] : Type u := ValuativeRel R is this what we would want then?

chrisflav · 2026-04-15T15:32:29Z

I think your definition is strictly better, it has better def-eq hygiene and it is what we have been doing with all the recent refactors, e.g. WithVal.

Concerning scope: I was mostly interested in testing a framework for analytification of schemes, for which adic spaces would provide one target category. But I am quite busy with other things at the moment, so I also did not work more on this.

riccardobrasca · 2026-04-15T15:36:44Z

On the other hand I don't have an opinion wrt the type synonym, the two approached should be more or less equivalent.

faenuccio

Some comments on my side as well.

faenuccio · 2026-04-15T15:29:54Z

+
+/-- The topology on `Spv A` generated by the basic open sets `basicOpen f s`
+for `f, s : A`. -/
+instance instTopologicalSpace : TopologicalSpace (Spv A) :=


Suggested change

instance instTopologicalSpace : TopologicalSpace (Spv A) :=

instance : TopologicalSpace (Spv A) :=

Why do you want to give it an explicit name (which coincides with the automatically generated one, btw)?

faenuccio · 2026-04-15T15:33:27Z

+    ofValuation v₁ = ofValuation v₂ :=
+  ValuationSpectrum.ext (funext₂ fun x y ↦ propext (h x y))
+
+/-- The basic open subset `Spv(A)(f/s) = { v ∈ Spv A | v(f) ≤ v(s) ∧ v(s) ≠ 0 }`. -/


Suggested change

/-- The basic open subset `Spv(A)(f/s) = { v ∈ Spv A | v(f) ≤ v(s) ∧ v(s) ≠ 0 }`. -/

/-- The basic open subset `Spv(A)(f/s) = { v ∈ Spv A | f ≤ᵥ s ∧ ¬ s =ᵥ 0 }`. -/

Change also all other occurrencies please.

faenuccio · 2026-04-15T15:34:29Z

+
+@[expose] public section
+
+-- This is defined as a structure extending `ValuativeRel A` rather than a type synonym, since we


I still think that @riccardobrasca's point makes sense: we want also to discourage copying the API for ValuativeRel to ValuationSpectrum, IMHO. Otherwise it will be a sort of "defeq under the hood".

faenuccio · 2026-04-15T15:35:41Z

+  ValuativeRel.supp_def x
+
+/-- The support of a point `v : Spv A` is a prime ideal. -/
+instance instIsPrimeSupp (v : Spv A) : v.supp.IsPrime :=


do you need a name?

faenuccio · 2026-04-15T15:36:37Z

+end Quotient
+
+/-- If `f` is a unit, then no valuative relation sends `f` to zero. -/
+lemma not_vle_zero_of_isUnit {f : A} (hu : IsUnit f) (v : Spv A) : ¬ v.vle f 0 :=


This kind of statements seems to abuse defeq, no?

CBirkbeck · 2026-04-15T15:42:48Z

Ok so do you prefer what the draft does here #38042 ?

CBirkbeck · 2026-04-15T16:05:00Z

One thing to note is that we maybe still want to think of elements of Spv as valuations, not points, since when it comes to defining Spa(A,A^+) we need to add that they are continuous (and <= 1 on A^+), and defining a point to be continuous feels weird.

github-actions bot added the t-ring-theory Ring theory label Apr 13, 2026

CBirkbeck and others added 9 commits April 13, 2026 16:46

doc(ValuationSpectrum): explain the design choice to extend ValuativeRel

7588fb1

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

chore(ValuationSpectrum): remove redundant Wedhorn references from do…

5ad9051

…cstrings Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

style(ValuationSpectrum): move design note from docstring to comment

001627e

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

style(ValuationSpectrum): remove inline Wedhorn references from docst…

47bdca9

…rings The module docstring already references Wedhorn; no need to repeat it on individual declarations. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

some golfs

e7df5bd

style(ValuationSpectrum): remove subsection headers

42f18e9

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

style(ValuativeRel/Comap): fix line length in docstring

f5ac855

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

style(ValuationSpectrum): use ↦ instead of => for consistency

2f5d095

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

fix(ValuationSpectrum): add module declarations for Lean 4 module system

31c5cfb

Both files were missing the `module` keyword, `public import`, and `@[expose] public section` required by the Lean 4 module system. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

CBirkbeck added the LLM-generated PRs with substantial input from LLMs - review accordingly label Apr 14, 2026

CBirkbeck added 3 commits April 14, 2026 12:38

save

4c379ca

cleanup

6f14d30

cleanup@

7815f38

CBirkbeck marked this pull request as ready for review April 14, 2026 11:57

CBirkbeck requested review from mariainesdff and riccardobrasca April 14, 2026 11:57

riccardobrasca self-assigned this Apr 14, 2026

riccardobrasca reviewed Apr 14, 2026

View reviewed changes

CBirkbeck and others added 2 commits April 14, 2026 15:11

CBirkbeck mentioned this pull request Apr 14, 2026

WIP/Discussion: ValuationSpectrum as one-field structure (alternative to #38009) #38042

Draft

faenuccio reviewed Apr 15, 2026

View reviewed changes

	instance instTopologicalSpace : TopologicalSpace (Spv A) :=
	instance : TopologicalSpace (Spv A) :=

	/-- The basic open subset `Spv(A)(f/s) = { v ∈ Spv A \| v(f) ≤ v(s) ∧ v(s) ≠ 0 }`. -/
	/-- The basic open subset `Spv(A)(f/s) = { v ∈ Spv A \| f ≤ᵥ s ∧ ¬ s =ᵥ 0 }`. -/


		@[expose] public section

		-- This is defined as a structure extending `ValuativeRel A` rather than a type synonym, since we

Conversation

CBirkbeck commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Uh oh!

github-actions bot commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary bc7bce2142

Import changes for modified files

Declarations diff

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

adamtopaz commented Apr 15, 2026

Uh oh!

dagurtomas commented Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

CBirkbeck commented Apr 15, 2026

Uh oh!

chrisflav commented Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

riccardobrasca commented Apr 15, 2026

Uh oh!

faenuccio left a comment

Choose a reason for hiding this comment

Uh oh!

faenuccio Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

faenuccio Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

faenuccio Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

faenuccio Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

faenuccio Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

CBirkbeck commented Apr 15, 2026

Uh oh!

CBirkbeck commented Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

CBirkbeck commented Apr 13, 2026 •

edited

Loading

github-actions bot commented Apr 13, 2026 •

edited

Loading

dagurtomas commented Apr 15, 2026 •

edited

Loading

chrisflav commented Apr 15, 2026 •

edited

Loading

CBirkbeck commented Apr 15, 2026 •

edited

Loading