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!

Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean

riccardobrasca · 2026-04-14T12:46:09Z

Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean

+theorem not_vle_zero_of_isUnit [ValuativeRel A] {f : A} (hu : IsUnit f) :
+    ¬ f ≤ᵥ (0 : A) := by


Suggested change

theorem not_vle_zero_of_isUnit [ValuativeRel A] {f : A} (hu : IsUnit f) :

¬ f ≤ᵥ (0 : A) := by

theorem not_vle_zero_of_isUnit [ValuativeRel A] {f : A} (hu : IsUnit f) : ¬ f ≤ᵥ (0 : A) := by

Also, maybe a name that allows dot notation is a good idea.

Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean

Mathlib/RingTheory/Valuation/ValuationSpectrum.lean

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>

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(RingTheory/Valuation): define the valuation spectrum and its topology#38009

feat(RingTheory/Valuation): define the valuation spectrum and its topology#38009
CBirkbeck wants to merge 15 commits intoleanprover-community:masterfrom
CBirkbeck:feat/valuation-spectrum

CBirkbeck commented Apr 13, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Apr 13, 2026 •

edited

Loading

Declarations diff

Uh oh!

riccardobrasca left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca Apr 14, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		theorem not_vle_zero_of_isUnit [ValuativeRel A] {f : A} (hu : IsUnit f) :
		¬ f ≤ᵥ (0 : A) := by

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!

riccardobrasca Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

CBirkbeck commented Apr 13, 2026 •

edited

Loading

github-actions bot commented Apr 13, 2026 •

edited

Loading