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

[CBirkbeck]

Draft / discussion PR — do not merge.

(In case its not obvious, this was all written by Claude).

This is an alternative design for #38009, prototyping the suggestion in this comment from @riccardobrasca:

I propose something like

structure ValuationSpectrum (A : Type*) [CommRing A] where
  ofValuativeRel ::
  toValuativeRel : ValuativeRel A

[...] points v : Spv A are not literally valuations (you need to do v.toValuativeRel to access the valuation) but I think this is the correct way of thinking. Points of Spv A are just points of Spv A, their interpretation as valuations should be needed for the API.

Tagging the others mentioned there for visibility: @mariainesdff @faenuccio @jjdishere @kbuzzard.

What this PR is

The same content as #38009 (all reviewer fixes already applied), but with ValuationSpectrum defined as a one-field structure instead of extends ValuativeRel A.

What changes vs #38009

1. Structure definition

@[ext]
structure ValuationSpectrum (A : Type*) [CommRing A] where
  ofValuativeRel ::
  /-- The underlying `ValuativeRel A` of a point `v : Spv A`. -/
  toValuativeRel : ValuativeRel A

A point of Spv A is no longer literally a ValuativeRel A; you must explicitly .toValuativeRel to access the relation. This makes the semantic distinction "points of Spv A" vs "valuative relations on A" explicit at the type level.

2. Wrapper API to recover dot notation (~16 lines)

With extends we got v.vle, v.vle_total, v.mul_vle_mul_left, etc. for free. Without it, those need to be introduced explicitly:

abbrev vle (v : Spv A) : A → A → Prop := v.toValuativeRel.vle
lemma vle_total (v : Spv A) (x y : A) : v.vle x y ∨ v.vle y x := v.toValuativeRel.vle_total x y
lemma vle_trans {v : Spv A} {x y z : A} (h₁ : v.vle x y) (h₂ : v.vle y z) : v.vle x z := ...
lemma vle_add ...
lemma mul_vle_mul_left ...
lemma vle_mul_cancel ...
lemma not_vle_one_zero (v : Spv A) : ¬ v.vle 1 0 := v.toValuativeRel.not_vle_one_zero

vle is an abbrev, so existing call sites like basicOpen f s := { v | v.vle f s ∧ ¬ v.vle s 0 } continue to work without modification.

3. Proof updates (4 places)

Some proofs that previously closed via ValuationSpectrum.ext chaining all the way down to vle = vle (via the extends-derived ext lemma) now need an extra apply ValuativeRel.ext step, since the new structure's @[ext] only descends to toValuativeRel = toValuativeRel. Affected: ofValuation_eq_of_isEquiv, ofValuation_valuation, quotientLift_comap, comap_injective.

A couple of proofs (comap_id, comap_comp) actually got cleaner — they no longer need a congr_arg (·.vle) ... projection trick.

Net stats vs #38009

	# 38009 (extends)	This PR (one-field)	Δ
File length	293 lines	322 lines	+29
Diff	—	+40 / −11	—
Wrapper boilerplate	0	~16 lines	+16
Proofs needing extra ValuativeRel.ext	0	4	+4
Proofs that got cleaner	0	2	(comap_id, comap_comp)
letI/@ count at the derived-API layer	unchanged	unchanged	0

What this design does NOT change

The letI/@ noise that triggered the original design discussion lives at the derived API layer (ValuativeRel.supp, ValuativeRel.valuation, ValuativeRel.supp_eq_valuation_supp, etc.), not at the structure level. Those operations take [ValuativeRel R] as a typeclass argument, so we still need letI := v.toValuativeRel to pass our specific relation. Both extends and the one-field design hit this wall.

The cleanest fix for the letI/@ noise (IMO) would be a separate PR adding term-mode versions of those operations to ValuativeRel/Basic.lean — e.g. ValuativeRel.supp' (v : ValuativeRel R) : Ideal R taking the relation as an explicit argument. That refactor is independent of which shape Spv takes here, and would benefit both designs equally.

[github-actions]

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
+ mul_vle_mul_left
+ not_vle_one_zero
+ 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
+ vle_add
+ vle_mul_cancel
+ vle_ofValuation
+ vle_total
+ vle_trans
++ 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).