From 4d0e202fdc82fbaab7145bfb1f7b56779e750c11 Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 16:42:38 +0100
Subject: [PATCH 01/15] feat(RingTheory/Valuation): define the valuation
 spectrum and its topology
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 Mathlib.lean                                  |   2 +
 .../Valuation/ValuationSpectrum.lean          | 297 ++++++++++++++++++
 .../Valuation/ValuativeRel/Comap.lean         |  53 ++++
 3 files changed, 352 insertions(+)
 create mode 100644 Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
 create mode 100644 Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 6ef6211ab06657..3652561e0deb34 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6824,8 +6824,10 @@ public import Mathlib.RingTheory.Valuation.Quotient
 public import Mathlib.RingTheory.Valuation.RamificationGroup
 public import Mathlib.RingTheory.Valuation.RankOne
 public import Mathlib.RingTheory.Valuation.ValuationRing
+public import Mathlib.RingTheory.Valuation.ValuationSpectrum
 public import Mathlib.RingTheory.Valuation.ValuationSubring
 public import Mathlib.RingTheory.Valuation.ValuativeRel.Basic
+public import Mathlib.RingTheory.Valuation.ValuativeRel.Comap
 public import Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
 public import Mathlib.RingTheory.WittVector.Basic
 public import Mathlib.RingTheory.WittVector.Compare
diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
new file mode 100644
index 00000000000000..0d706220f0a0d5
--- /dev/null
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -0,0 +1,297 @@
+/-
+Copyright (c) 2026 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+import Mathlib.RingTheory.Valuation.ValuativeRel.Comap
+import Mathlib.RingTheory.Valuation.Quotient
+import Mathlib.RingTheory.Valuation.ExtendToLocalization
+import Mathlib.Topology.Order
+import Mathlib.RingTheory.Spectrum.Prime.Topology
+
+/-!
+# The Valuation Spectrum of a Ring
+
+We define the valuation spectrum `Spv A` following Definition 4.1 of Wedhorn.
+
+## Main definitions
+
+* `ValuationSpectrum A` : The valuation spectrum, the type of `ValuativeRel` instances on `A`.
+* `ValuationSpectrum.basicOpen f s` : The basic open set `{ v ∈ Spv A | v(f) ≤ v(s) ≠ 0 }`.
+* `ValuationSpectrum.comap φ` : The continuous map `Spv B → Spv A` induced by `φ : A →+* B`.
+* `ValuationSpectrum.supp v` : The support prime ideal `{ a ∈ A | v(a) = 0 }`.
+* `ValuationSpectrum.quotientLift 𝔞 v h` : Lift `v` with `𝔞 ≤ supp v` to `Spv (A ⧸ 𝔞)`.
+* `ValuationSpectrum.localizationLift S B v hS` : Lift `v` to a localization `Spv B`.
+
+## References
+
+* [T. Wedhorn, *Adic Spaces*][wedhorn2019adic], Definition 4.1, Remark 4.3, Remark 4.4,
+  Proposition 4.7(2)
+-/
+
+/-- The *valuation spectrum* `Spv A` of a commutative ring `A` (Definition 4.1 of Wedhorn). -/
+@[ext]
+structure ValuationSpectrum (A : Type*) [CommRing A] extends ValuativeRel A
+
+@[inherit_doc] notation "Spv" => ValuationSpectrum
+
+namespace ValuationSpectrum
+
+variable {A : Type*} [CommRing A]
+
+/-- Construct a point of `Spv A` from a valuation `v : Valuation A Γ₀`. -/
+def ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+    (v : Valuation A Γ₀) : Spv A :=
+  ⟨ValuativeRel.ofValuation v⟩
+
+/-- Two equivalent valuations define the same point of `Spv A`. -/
+lemma ofValuation_eq_of_isEquiv {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+    {Γ'₀ : Type*} [LinearOrderedCommGroupWithZero Γ'₀]
+    {v₁ : Valuation A Γ₀} {v₂ : Valuation A Γ'₀} (h : v₁.IsEquiv v₂) :
+    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 }`. -/
+def basicOpen (f s : A) : Set (Spv A) :=
+  { v | v.vle f s ∧ ¬ v.vle s 0 }
+
+/-- `Spv(A)(tf/ts) ⊆ Spv(A)(f/s)` (note after Definition 4.1 in Wedhorn). -/
+lemma basicOpen_mul_subset (t f s : A) :
+    basicOpen (t * f) (t * s) ⊆ basicOpen f s := by
+  intro v ⟨h1, h2⟩
+  have ht : ¬ v.vle t 0 := by
+    intro ht
+    exact h2 (by have := v.mul_vle_mul_left ht s; rwa [zero_mul] at this)
+  exact ⟨v.vle_mul_cancel ht (by rwa [mul_comm t f, mul_comm t s] at h1),
+    fun hs ↦ h2 (by have := v.mul_vle_mul_left hs t; rwa [zero_mul, mul_comm s t] at this)⟩
+
+/-- `Spv(A)(1/1) = Spv A`. Note after Definition 4.1 in Wedhorn. -/
+lemma basicOpen_one : basicOpen (1 : A) 1 = Set.univ :=
+  Set.eq_univ_iff_forall.mpr fun v ↦ ⟨(v.vle_total 1 1).elim id id, v.not_vle_one_zero⟩
+
+/-- `Spv(A)(s/s) = { v ∈ Spv A | v(s) ≠ 0 }`. Note after Definition 4.1 in Wedhorn. -/
+lemma basicOpen_self (s : A) :
+    basicOpen s s = { v : Spv A | ¬ v.vle s 0 } :=
+  Set.ext fun v ↦ ⟨fun ⟨_, h⟩ ↦ h, fun h ↦ ⟨(v.vle_total s s).elim id id, h⟩⟩
+
+/-- The topology on `Spv A` generated by the basic open sets `basicOpen f s`
+for `f, s : A`. -/
+instance instTopologicalSpace : TopologicalSpace (Spv A) :=
+  TopologicalSpace.generateFrom { U | ∃ f s : A, U = basicOpen f s }
+
+/-! ### Functoriality of Spv -/
+
+section Functoriality
+
+variable {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
+
+/-- Contravariant map `Spv B → Spv A` induced by `φ : A →+* B` (Remark 4.3 of Wedhorn). -/
+def comap (φ : A →+* B) (v : Spv B) : Spv A :=
+  ⟨ValuativeRel.comap φ v.toValuativeRel⟩
+
+@[simp]
+lemma comap_vle (φ : A →+* B) (v : Spv B) (a₁ a₂ : A) :
+    (comap φ v).vle a₁ a₂ = v.vle (φ a₁) (φ a₂) := rfl
+
+/-- `comap` is compatible with `ofValuation`. -/
+lemma comap_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+    (φ : A →+* B) (v : Valuation B Γ₀) :
+    comap φ (ofValuation v) = ofValuation (v.comap φ) := rfl
+
+/-- `Spv(φ)⁻¹(Spv(A)(f/s)) = Spv(B)(φ(f)/φ(s))` (Equation (4.1.1) of Wedhorn). -/
+lemma comap_preimage_basicOpen (φ : A →+* B) (f s : A) :
+    comap φ ⁻¹' basicOpen f s = basicOpen (φ f) (φ s) := by
+  ext v
+  simp only [Set.mem_preimage, basicOpen, Set.mem_setOf_eq, comap_vle, map_zero]
+
+/-- `Spv(φ)` is continuous (Remark 4.3 of Wedhorn). -/
+lemma comap_continuous (φ : A →+* B) : Continuous (comap φ) :=
+  continuous_generateFrom_iff.mpr fun _ ⟨f, s, hU⟩ ↦
+    hU ▸ comap_preimage_basicOpen φ f s ▸
+      TopologicalSpace.isOpen_generateFrom_of_mem ⟨φ f, φ s, rfl⟩
+
+/-- `Spv(id) = id`. -/
+@[simp]
+lemma comap_id : comap (RingHom.id A) = id := by ext v : 1; ext; rfl
+
+/-- `Spv(ψ ∘ φ) = Spv(φ) ∘ Spv(ψ)` (contravariant functoriality). -/
+lemma comap_comp (φ : A →+* B) (ψ : B →+* C) :
+    comap (ψ.comp φ) = comap φ ∘ comap ψ := by ext v : 1; ext; rfl
+
+/-- `comap φ` is injective when `φ` is surjective. -/
+lemma comap_injective {φ : A →+* B} (hφ : Function.Surjective φ) :
+    Function.Injective (comap φ) := by
+  intro v₁ v₂ h; apply ValuationSpectrum.ext; funext b₁ b₂
+  obtain ⟨a₁, rfl⟩ := hφ b₁; obtain ⟨a₂, rfl⟩ := hφ b₂
+  simpa only [comap_vle] using congr_arg (fun v ↦ v.vle a₁ a₂) h
+
+end Functoriality
+
+/-! ### Support of a point of `Spv A` -/
+
+/-- The support prime ideal `{ a ∈ A | v(a) = 0 }` of a point `v ∈ Spv A`. -/
+def supp (v : Spv A) : Ideal A :=
+  @ValuativeRel.supp A _ v.toValuativeRel
+
+@[simp]
+lemma mem_supp_iff (v : Spv A) (x : A) : x ∈ v.supp ↔ v.vle x 0 :=
+  @ValuativeRel.supp_def A _ v.toValuativeRel x
+
+/-- The support of a point `v ∈ Spv A` is a prime ideal. -/
+instance instIsPrimeSupp (v : Spv A) : v.supp.IsPrime := by
+  change (@ValuativeRel.supp A _ v.toValuativeRel).IsPrime
+  rw [@ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel]
+  infer_instance
+
+/-- The support of `ofValuation v` equals `v.supp`. -/
+lemma supp_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+    (v : Valuation A Γ₀) : (ofValuation v).supp = v.supp := by
+  ext x; rw [mem_supp_iff, Valuation.mem_supp_iff]
+  change v x ≤ v 0 ↔ _; rw [map_zero]; exact le_zero_iff
+
+/-- The canonical valuation gives back the same point of `Spv`. -/
+lemma ofValuation_valuation (v : Spv A) :
+    ofValuation (@ValuativeRel.valuation A _ v.toValuativeRel) = v := by
+  apply ValuationSpectrum.ext; funext x y
+  letI : ValuativeRel A := v.toValuativeRel
+  exact propext (ValuativeRel.valuation A).vle_iff_le.symm
+
+/-! ### Quotient -- Remark 4.4(2) of Wedhorn -/
+
+section Quotient
+
+variable (𝔞 : Ideal A)
+
+/-- `𝔞 ≤ supp(comap(mk 𝔞, w))` for all `w : Spv (A ⧸ 𝔞)`. -/
+lemma ideal_le_supp_comap_mk (w : Spv (A ⧸ 𝔞)) :
+    𝔞 ≤ (comap (Ideal.Quotient.mk 𝔞) w).supp := by
+  intro a ha
+  simp only [mem_supp_iff, comap_vle, map_zero]
+  rw [Ideal.Quotient.eq_zero_iff_mem.mpr ha]
+  exact (w.vle_total 0 0).elim id id
+
+/-- Lift a point `v ∈ Spv A` with `𝔞 ≤ supp v` to `Spv (A ⧸ 𝔞)`. -/
+noncomputable def quotientLift (v : Spv A) (h : 𝔞 ≤ v.supp) : Spv (A ⧸ 𝔞) :=
+  ofValuation ((@ValuativeRel.valuation A _ v.toValuativeRel).onQuot
+    (@ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel ▸ h))
+
+/-- `comap (mk 𝔞) (quotientLift 𝔞 v h) = v`. -/
+lemma comap_quotientLift (v : Spv A) (h : 𝔞 ≤ v.supp) :
+    comap (Ideal.Quotient.mk 𝔞) (quotientLift 𝔞 v h) = v := by
+  simp only [quotientLift, comap_ofValuation, Valuation.onQuot_comap_eq]
+  exact ofValuation_valuation v
+
+/-- `quotientLift 𝔞 (comap (mk 𝔞) w) _ = w`. -/
+lemma quotientLift_comap (w : Spv (A ⧸ 𝔞)) :
+    quotientLift 𝔞 (comap (Ideal.Quotient.mk 𝔞) w) (ideal_le_supp_comap_mk 𝔞 w) = w := by
+  apply ValuationSpectrum.ext; funext x y
+  obtain ⟨a₁, rfl⟩ := Ideal.Quotient.mk_surjective x
+  obtain ⟨a₂, rfl⟩ := Ideal.Quotient.mk_surjective y
+  letI : ValuativeRel A := ValuativeRel.comap (Ideal.Quotient.mk 𝔞) w.toValuativeRel
+  exact propext (ValuativeRel.valuation A).vle_iff_le.symm
+
+/-- The range of `comap (mk 𝔞)` is `{ v ∈ Spv A | 𝔞 ≤ supp v }`. -/
+lemma comap_quotient_range :
+    Set.range (comap (Ideal.Quotient.mk 𝔞)) = { v : Spv A | 𝔞 ≤ v.supp } := by
+  ext v
+  simp only [Set.mem_range, Set.mem_setOf_eq]
+  exact ⟨fun ⟨w, hw⟩ ↦ hw ▸ ideal_le_supp_comap_mk 𝔞 w,
+    fun h ↦ ⟨quotientLift 𝔞 v h, comap_quotientLift 𝔞 v h⟩⟩
+
+/-- `comap (mk 𝔞) : Spv (A ⧸ 𝔞) → Spv A` is a topological embedding. -/
+lemma comap_quotient_isEmbedding :
+    Topology.IsEmbedding (comap (Ideal.Quotient.mk 𝔞)) := by
+  constructor
+  · constructor
+    change ValuationSpectrum.instTopologicalSpace =
+      ValuationSpectrum.instTopologicalSpace.induced (comap (Ideal.Quotient.mk 𝔞))
+    simp only [instTopologicalSpace, induced_generateFrom_eq]
+    congr 1
+    ext U
+    simp only [Set.mem_setOf_eq, Set.mem_image]
+    constructor
+    · rintro ⟨f', s', rfl⟩
+      obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f'
+      obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective s'
+      exact ⟨basicOpen f s, ⟨f, s, rfl⟩, comap_preimage_basicOpen _ f s⟩
+    · rintro ⟨_, ⟨f, s, rfl⟩, rfl⟩
+      rw [comap_preimage_basicOpen]
+      exact ⟨_, _, rfl⟩
+  · exact comap_injective Ideal.Quotient.mk_surjective
+
+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 :=
+  letI : ValuativeRel A := v.toValuativeRel; ValuativeRel.not_vle_zero_of_isUnit hu
+
+/-! ### Localization -- Remark 4.4(1) of Wedhorn -/
+
+section Localization
+
+variable (S : Submonoid A) (B : Type*) [CommRing B] [Algebra A B] [IsLocalization S B]
+
+/-- Lift `v ∈ Spv A` with `S ≤ (supp v).primeCompl` to `Spv B` (localization at `S`). -/
+noncomputable def localizationLift (v : Spv A) (hS : S ≤ v.supp.primeCompl) :
+    Spv B :=
+  have hS' : S ≤ (@ValuativeRel.valuation A _ v.toValuativeRel).supp.primeCompl := by
+    intro s hs; change s ∉ _
+    rw [← @ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel]; exact hS hs
+  ofValuation ((@ValuativeRel.valuation A _ v.toValuativeRel).extendToLocalization hS' B)
+
+/-- `comap (algebraMap A B) (localizationLift S B v hS) = v`. -/
+lemma comap_localizationLift (v : Spv A) (hS : S ≤ v.supp.primeCompl) :
+    comap (algebraMap A B) (localizationLift S B v hS) = v := by
+  have hS' : S ≤ (@ValuativeRel.valuation A _ v.toValuativeRel).supp.primeCompl := by
+    intro s hs; change s ∉ _
+    rw [← @ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel]; exact hS hs
+  change comap (algebraMap A B)
+    (ofValuation ((@ValuativeRel.valuation A _ v.toValuativeRel).extendToLocalization hS' B)) = v
+  rw [comap_ofValuation,
+    show ((@ValuativeRel.valuation A _ v.toValuativeRel).extendToLocalization hS' B).comap
+      (algebraMap A B) = @ValuativeRel.valuation A _ v.toValuativeRel from
+      Valuation.ext fun a ↦ Valuation.extendToLocalization_apply_map_apply _ hS' B a]
+  exact ofValuation_valuation v
+
+/-- `S` is disjoint from `supp(comap(algebraMap, w))` for `w : Spv B`. -/
+lemma submonoid_le_supp_primeCompl_comap_algebraMap (w : Spv B) :
+    S ≤ (comap (algebraMap A B) w).supp.primeCompl := fun s hs ↦ by
+  change s ∉ (comap (algebraMap A B) w).supp
+  rw [mem_supp_iff, comap_vle, map_zero]
+  exact not_vle_zero_of_isUnit (IsLocalization.map_units B ⟨s, hs⟩) w
+
+/-- Range of `comap (algebraMap A B)` is `{ v | S ≤ supp(v).primeCompl }` (Remark 4.4(1)). -/
+lemma comap_localization_range :
+    Set.range (comap (algebraMap A B)) = { v : Spv A | S ≤ v.supp.primeCompl } := by
+  ext v
+  simp only [Set.mem_range, Set.mem_setOf_eq]
+  exact ⟨fun ⟨w, hw⟩ ↦ hw ▸ submonoid_le_supp_primeCompl_comap_algebraMap S B w,
+    fun h ↦ ⟨localizationLift S B v h, comap_localizationLift S B v h⟩⟩
+
+end Localization
+
+/-! ### Support map to PrimeSpectrum (Remark 4.6 / Corollary 4.8 of Wedhorn) -/
+
+/-- The support map `Spv A → Spec A` (Remark 4.6 of Wedhorn). -/
+def suppFun : Spv A → PrimeSpectrum A := fun v ↦ ⟨v.supp, inferInstance⟩
+
+@[simp]
+lemma suppFun_asIdeal (v : Spv A) : (suppFun v).asIdeal = v.supp := rfl
+
+/-- `suppFun ⁻¹' D(f) = Spv(A)(f/f)`. -/
+lemma suppFun_preimage_basicOpen (f : A) :
+    suppFun ⁻¹' (PrimeSpectrum.basicOpen f : Set (PrimeSpectrum A)) = basicOpen f f := by
+  ext v; simp [basicOpen_self, mem_supp_iff]
+
+/-- `suppFun` is continuous (Remark 4.6 of Wedhorn). -/
+theorem suppFun_continuous : Continuous (suppFun : Spv A → PrimeSpectrum A) :=
+  PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff.mpr fun _ ⟨f, hf⟩ ↦
+    hf ▸ suppFun_preimage_basicOpen f ▸
+      TopologicalSpace.isOpen_generateFrom_of_mem ⟨f, f, rfl⟩
+
+/-- `supp ∘ Spv(φ) = Spec(φ) ∘ supp` (Corollary 4.8 of Wedhorn). -/
+theorem suppFun_comap {B : Type*} [CommRing B] (φ : A →+* B) (v : Spv B) :
+    suppFun (comap φ v) = PrimeSpectrum.comap φ (suppFun v) := by
+  ext; simp [mem_supp_iff, comap_vle]
+
+end ValuationSpectrum
diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
new file mode 100644
index 00000000000000..2cd733d6623a48
--- /dev/null
+++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+import Mathlib.RingTheory.Valuation.ValuativeRel.Basic
+
+/-!
+# Comap for Valuative Relations
+
+We define the pullback (comap) of a `ValuativeRel` along a ring homomorphism.
+
+## Main definitions
+
+* `ValuativeRel.comap φ v` : Given `φ : A →+* B` and a valuative relation `v` on `B`,
+  the induced `ValuativeRel A` defined by `a₁ ≤ᵥ a₂ ↔ φ(a₁) ≤ᵥ φ(a₂)`.
+
+## Main results
+
+* `ValuativeRel.not_vle_zero_of_isUnit` : If `f` is a unit, then `¬ f ≤ᵥ 0`.
+-/
+
+namespace ValuativeRel
+
+variable {A B : Type*} [CommRing A] [CommRing B]
+
+/-- The pullback of a `ValuativeRel` along `φ : A →+* B`: `a₁ ≤ᵥ a₂ ↔ φ(a₁) ≤ᵥ φ(a₂)`. -/
+@[reducible]
+def comap (φ : A →+* B) (v : ValuativeRel B) : ValuativeRel A where
+  vle a₁ a₂ := v.vle (φ a₁) (φ a₂)
+  vle_total a₁ a₂ := v.vle_total (φ a₁) (φ a₂)
+  vle_trans h₁ h₂ := v.vle_trans h₁ h₂
+  vle_add h₁ h₂ := by simpa [map_add] using v.vle_add h₁ h₂
+  mul_vle_mul_left h z := by simpa [map_mul] using v.mul_vle_mul_left h (φ z)
+  vle_mul_cancel h₀ h := by
+    rw [map_zero] at h₀
+    simpa [map_mul] using v.vle_mul_cancel h₀ (by simpa [map_mul] using h)
+  not_vle_one_zero := by simp [map_one, map_zero, v.not_vle_one_zero]
+
+@[simp]
+theorem comap_vle (φ : A →+* B) (v : ValuativeRel B) (a₁ a₂ : A) :
+    (comap φ v).vle a₁ a₂ = v.vle (φ a₁) (φ a₂) := rfl
+
+/-- If `f` is a unit, then `¬ f ≤ᵥ 0`. -/
+theorem not_vle_zero_of_isUnit [ValuativeRel A] {f : A} (hu : IsUnit f) :
+    ¬ f ≤ᵥ (0 : A) := by
+  obtain ⟨u, rfl⟩ := hu
+  intro h
+  have := mul_vle_mul_right h (↑u⁻¹ : A)
+  rw [Units.inv_mul, mul_zero] at this
+  exact absurd this (not_vle.mpr zero_vlt_one)
+
+end ValuativeRel

From 7588fb10f76e225716f0ae01b0fcbadcb7835c1b Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 16:46:43 +0100
Subject: [PATCH 02/15] doc(ValuationSpectrum): explain the design choice to
 extend ValuativeRel

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 Mathlib/RingTheory/Valuation/ValuationSpectrum.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index 0d706220f0a0d5..7b0c880bcf14f2 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -29,7 +29,11 @@ We define the valuation spectrum `Spv A` following Definition 4.1 of Wedhorn.
   Proposition 4.7(2)
 -/
 
-/-- The *valuation spectrum* `Spv A` of a commutative ring `A` (Definition 4.1 of Wedhorn). -/
+/-- The *valuation spectrum* `Spv A` of a commutative ring `A` (Definition 4.1 of Wedhorn).
+
+This is defined as a structure extending `ValuativeRel A` rather than a type synonym, since we want
+to equip `Spv A` with a topology (generated by basic open sets) that we do not want to place on
+`ValuativeRel` itself, while still having direct access to the `ValuativeRel` API. -/
 @[ext]
 structure ValuationSpectrum (A : Type*) [CommRing A] extends ValuativeRel A
 

From 5ad9051e742d630f7532e618a74e5cda148509a4 Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 16:47:30 +0100
Subject: [PATCH 03/15] chore(ValuationSpectrum): remove redundant Wedhorn
 references from docstrings

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 Mathlib/RingTheory/Valuation/ValuationSpectrum.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index 7b0c880bcf14f2..a0c44d6fa7343b 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -59,7 +59,7 @@ lemma ofValuation_eq_of_isEquiv {Γ₀ : Type*} [LinearOrderedCommGroupWithZero
 def basicOpen (f s : A) : Set (Spv A) :=
   { v | v.vle f s ∧ ¬ v.vle s 0 }
 
-/-- `Spv(A)(tf/ts) ⊆ Spv(A)(f/s)` (note after Definition 4.1 in Wedhorn). -/
+/-- `Spv(A)(tf/ts) ⊆ Spv(A)(f/s)`. -/
 lemma basicOpen_mul_subset (t f s : A) :
     basicOpen (t * f) (t * s) ⊆ basicOpen f s := by
   intro v ⟨h1, h2⟩
@@ -69,11 +69,11 @@ lemma basicOpen_mul_subset (t f s : A) :
   exact ⟨v.vle_mul_cancel ht (by rwa [mul_comm t f, mul_comm t s] at h1),
     fun hs ↦ h2 (by have := v.mul_vle_mul_left hs t; rwa [zero_mul, mul_comm s t] at this)⟩
 
-/-- `Spv(A)(1/1) = Spv A`. Note after Definition 4.1 in Wedhorn. -/
+/-- `Spv(A)(1/1) = Spv A`. -/
 lemma basicOpen_one : basicOpen (1 : A) 1 = Set.univ :=
   Set.eq_univ_iff_forall.mpr fun v ↦ ⟨(v.vle_total 1 1).elim id id, v.not_vle_one_zero⟩
 
-/-- `Spv(A)(s/s) = { v ∈ Spv A | v(s) ≠ 0 }`. Note after Definition 4.1 in Wedhorn. -/
+/-- `Spv(A)(s/s) = { v ∈ Spv A | v(s) ≠ 0 }`. -/
 lemma basicOpen_self (s : A) :
     basicOpen s s = { v : Spv A | ¬ v.vle s 0 } :=
   Set.ext fun v ↦ ⟨fun ⟨_, h⟩ ↦ h, fun h ↦ ⟨(v.vle_total s s).elim id id, h⟩⟩

From 001627e25daed42b5da59c7d899f3b2e5e90722b Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 16:48:00 +0100
Subject: [PATCH 04/15] style(ValuationSpectrum): move design note from
 docstring to comment

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 Mathlib/RingTheory/Valuation/ValuationSpectrum.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index a0c44d6fa7343b..c8eb74379c3efd 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -29,11 +29,10 @@ We define the valuation spectrum `Spv A` following Definition 4.1 of Wedhorn.
   Proposition 4.7(2)
 -/
 
-/-- The *valuation spectrum* `Spv A` of a commutative ring `A` (Definition 4.1 of Wedhorn).
-
-This is defined as a structure extending `ValuativeRel A` rather than a type synonym, since we want
-to equip `Spv A` with a topology (generated by basic open sets) that we do not want to place on
-`ValuativeRel` itself, while still having direct access to the `ValuativeRel` API. -/
+-- This is defined as a structure extending `ValuativeRel A` rather than a type synonym, since we
+-- want to equip `Spv A` with a topology (generated by basic open sets) that we do not want to
+-- place on `ValuativeRel` itself, while still having direct access to the `ValuativeRel` API.
+/-- The *valuation spectrum* `Spv A` of a commutative ring `A` (Definition 4.1 of Wedhorn). -/
 @[ext]
 structure ValuationSpectrum (A : Type*) [CommRing A] extends ValuativeRel A
 

From 47bdca962dd19de8f592d44ac90c7da2448e7d66 Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 16:49:06 +0100
Subject: [PATCH 05/15] style(ValuationSpectrum): remove inline Wedhorn
 references from docstrings

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>
---
 .../Valuation/ValuationSpectrum.lean          | 20 +++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index c8eb74379c3efd..7c986299e6013d 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -32,7 +32,7 @@ We define the valuation spectrum `Spv A` following Definition 4.1 of Wedhorn.
 -- This is defined as a structure extending `ValuativeRel A` rather than a type synonym, since we
 -- want to equip `Spv A` with a topology (generated by basic open sets) that we do not want to
 -- place on `ValuativeRel` itself, while still having direct access to the `ValuativeRel` API.
-/-- The *valuation spectrum* `Spv A` of a commutative ring `A` (Definition 4.1 of Wedhorn). -/
+/-- The *valuation spectrum* `Spv A` of a commutative ring `A`. -/
 @[ext]
 structure ValuationSpectrum (A : Type*) [CommRing A] extends ValuativeRel A
 
@@ -88,7 +88,7 @@ section Functoriality
 
 variable {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
 
-/-- Contravariant map `Spv B → Spv A` induced by `φ : A →+* B` (Remark 4.3 of Wedhorn). -/
+/-- Contravariant map `Spv B → Spv A` induced by `φ : A →+* B`. -/
 def comap (φ : A →+* B) (v : Spv B) : Spv A :=
   ⟨ValuativeRel.comap φ v.toValuativeRel⟩
 
@@ -101,13 +101,13 @@ lemma comap_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
     (φ : A →+* B) (v : Valuation B Γ₀) :
     comap φ (ofValuation v) = ofValuation (v.comap φ) := rfl
 
-/-- `Spv(φ)⁻¹(Spv(A)(f/s)) = Spv(B)(φ(f)/φ(s))` (Equation (4.1.1) of Wedhorn). -/
+/-- `Spv(φ)⁻¹(Spv(A)(f/s)) = Spv(B)(φ(f)/φ(s))`. -/
 lemma comap_preimage_basicOpen (φ : A →+* B) (f s : A) :
     comap φ ⁻¹' basicOpen f s = basicOpen (φ f) (φ s) := by
   ext v
   simp only [Set.mem_preimage, basicOpen, Set.mem_setOf_eq, comap_vle, map_zero]
 
-/-- `Spv(φ)` is continuous (Remark 4.3 of Wedhorn). -/
+/-- `Spv(φ)` is continuous. -/
 lemma comap_continuous (φ : A →+* B) : Continuous (comap φ) :=
   continuous_generateFrom_iff.mpr fun _ ⟨f, s, hU⟩ ↦
     hU ▸ comap_preimage_basicOpen φ f s ▸
@@ -159,7 +159,7 @@ lemma ofValuation_valuation (v : Spv A) :
   letI : ValuativeRel A := v.toValuativeRel
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
-/-! ### Quotient -- Remark 4.4(2) of Wedhorn -/
+/-! ### Quotient -/
 
 section Quotient
 
@@ -228,7 +228,7 @@ end Quotient
 lemma not_vle_zero_of_isUnit {f : A} (hu : IsUnit f) (v : Spv A) : ¬ v.vle f 0 :=
   letI : ValuativeRel A := v.toValuativeRel; ValuativeRel.not_vle_zero_of_isUnit hu
 
-/-! ### Localization -- Remark 4.4(1) of Wedhorn -/
+/-! ### Localization -/
 
 section Localization
 
@@ -273,9 +273,9 @@ lemma comap_localization_range :
 
 end Localization
 
-/-! ### Support map to PrimeSpectrum (Remark 4.6 / Corollary 4.8 of Wedhorn) -/
+/-! ### Support map to PrimeSpectrum -/
 
-/-- The support map `Spv A → Spec A` (Remark 4.6 of Wedhorn). -/
+/-- The support map `Spv A → Spec A`. -/
 def suppFun : Spv A → PrimeSpectrum A := fun v ↦ ⟨v.supp, inferInstance⟩
 
 @[simp]
@@ -286,13 +286,13 @@ lemma suppFun_preimage_basicOpen (f : A) :
     suppFun ⁻¹' (PrimeSpectrum.basicOpen f : Set (PrimeSpectrum A)) = basicOpen f f := by
   ext v; simp [basicOpen_self, mem_supp_iff]
 
-/-- `suppFun` is continuous (Remark 4.6 of Wedhorn). -/
+/-- `suppFun` is continuous. -/
 theorem suppFun_continuous : Continuous (suppFun : Spv A → PrimeSpectrum A) :=
   PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff.mpr fun _ ⟨f, hf⟩ ↦
     hf ▸ suppFun_preimage_basicOpen f ▸
       TopologicalSpace.isOpen_generateFrom_of_mem ⟨f, f, rfl⟩
 
-/-- `supp ∘ Spv(φ) = Spec(φ) ∘ supp` (Corollary 4.8 of Wedhorn). -/
+/-- `supp ∘ Spv(φ) = Spec(φ) ∘ supp`. -/
 theorem suppFun_comap {B : Type*} [CommRing B] (φ : A →+* B) (v : Spv B) :
     suppFun (comap φ v) = PrimeSpectrum.comap φ (suppFun v) := by
   ext; simp [mem_supp_iff, comap_vle]

From e7df5bdb3ec083052c4434418164ad20e9bcbfa8 Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 16:58:06 +0100
Subject: [PATCH 06/15] some golfs

---
 .../Valuation/ValuationSpectrum.lean          | 30 +++++++++----------
 1 file changed, 14 insertions(+), 16 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index 7c986299e6013d..dc498712abf2bf 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -150,13 +150,14 @@ instance instIsPrimeSupp (v : Spv A) : v.supp.IsPrime := by
 lemma supp_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
     (v : Valuation A Γ₀) : (ofValuation v).supp = v.supp := by
   ext x; rw [mem_supp_iff, Valuation.mem_supp_iff]
-  change v x ≤ v 0 ↔ _; rw [map_zero]; exact le_zero_iff
+  change v x ≤ v 0 ↔ _
+  simp
 
 /-- The canonical valuation gives back the same point of `Spv`. -/
 lemma ofValuation_valuation (v : Spv A) :
     ofValuation (@ValuativeRel.valuation A _ v.toValuativeRel) = v := by
   apply ValuationSpectrum.ext; funext x y
-  letI : ValuativeRel A := v.toValuativeRel
+  let : ValuativeRel A := v.toValuativeRel
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
 /-! ### Quotient -/
@@ -167,11 +168,8 @@ variable (𝔞 : Ideal A)
 
 /-- `𝔞 ≤ supp(comap(mk 𝔞, w))` for all `w : Spv (A ⧸ 𝔞)`. -/
 lemma ideal_le_supp_comap_mk (w : Spv (A ⧸ 𝔞)) :
-    𝔞 ≤ (comap (Ideal.Quotient.mk 𝔞) w).supp := by
-  intro a ha
-  simp only [mem_supp_iff, comap_vle, map_zero]
-  rw [Ideal.Quotient.eq_zero_iff_mem.mpr ha]
-  exact (w.vle_total 0 0).elim id id
+    𝔞 ≤ (comap (Ideal.Quotient.mk 𝔞) w).supp :=
+  fun a ha => by simp [Ideal.Quotient.eq_zero_iff_mem.mpr ha]
 
 /-- Lift a point `v ∈ Spv A` with `𝔞 ≤ supp v` to `Spv (A ⧸ 𝔞)`. -/
 noncomputable def quotientLift (v : Spv A) (h : 𝔞 ≤ v.supp) : Spv (A ⧸ 𝔞) :=
@@ -181,8 +179,7 @@ noncomputable def quotientLift (v : Spv A) (h : 𝔞 ≤ v.supp) : Spv (A ⧸ 
 /-- `comap (mk 𝔞) (quotientLift 𝔞 v h) = v`. -/
 lemma comap_quotientLift (v : Spv A) (h : 𝔞 ≤ v.supp) :
     comap (Ideal.Quotient.mk 𝔞) (quotientLift 𝔞 v h) = v := by
-  simp only [quotientLift, comap_ofValuation, Valuation.onQuot_comap_eq]
-  exact ofValuation_valuation v
+  simpa using ofValuation_valuation v
 
 /-- `quotientLift 𝔞 (comap (mk 𝔞) w) _ = w`. -/
 lemma quotientLift_comap (w : Spv (A ⧸ 𝔞)) :
@@ -190,7 +187,7 @@ lemma quotientLift_comap (w : Spv (A ⧸ 𝔞)) :
   apply ValuationSpectrum.ext; funext x y
   obtain ⟨a₁, rfl⟩ := Ideal.Quotient.mk_surjective x
   obtain ⟨a₂, rfl⟩ := Ideal.Quotient.mk_surjective y
-  letI : ValuativeRel A := ValuativeRel.comap (Ideal.Quotient.mk 𝔞) w.toValuativeRel
+  let : ValuativeRel A := ValuativeRel.comap (Ideal.Quotient.mk 𝔞) w.toValuativeRel
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
 /-- The range of `comap (mk 𝔞)` is `{ v ∈ Spv A | 𝔞 ≤ supp v }`. -/
@@ -226,7 +223,7 @@ 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 :=
-  letI : ValuativeRel A := v.toValuativeRel; ValuativeRel.not_vle_zero_of_isUnit hu
+  let : ValuativeRel A := v.toValuativeRel; ValuativeRel.not_vle_zero_of_isUnit hu
 
 /-! ### Localization -/
 
@@ -247,7 +244,8 @@ lemma comap_localizationLift (v : Spv A) (hS : S ≤ v.supp.primeCompl) :
     comap (algebraMap A B) (localizationLift S B v hS) = v := by
   have hS' : S ≤ (@ValuativeRel.valuation A _ v.toValuativeRel).supp.primeCompl := by
     intro s hs; change s ∉ _
-    rw [← @ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel]; exact hS hs
+    rw [← @ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel]
+    exact hS hs
   change comap (algebraMap A B)
     (ofValuation ((@ValuativeRel.valuation A _ v.toValuativeRel).extendToLocalization hS' B)) = v
   rw [comap_ofValuation,
@@ -263,12 +261,11 @@ lemma submonoid_le_supp_primeCompl_comap_algebraMap (w : Spv B) :
   rw [mem_supp_iff, comap_vle, map_zero]
   exact not_vle_zero_of_isUnit (IsLocalization.map_units B ⟨s, hs⟩) w
 
-/-- Range of `comap (algebraMap A B)` is `{ v | S ≤ supp(v).primeCompl }` (Remark 4.4(1)). -/
+/-- Range of `comap (algebraMap A B)` is `{ v | S ≤ supp(v).primeCompl }`. -/
 lemma comap_localization_range :
     Set.range (comap (algebraMap A B)) = { v : Spv A | S ≤ v.supp.primeCompl } := by
   ext v
-  simp only [Set.mem_range, Set.mem_setOf_eq]
-  exact ⟨fun ⟨w, hw⟩ ↦ hw ▸ submonoid_le_supp_primeCompl_comap_algebraMap S B w,
+  simpa using ⟨fun ⟨w, hw⟩ ↦ hw ▸ submonoid_le_supp_primeCompl_comap_algebraMap S B w,
     fun h ↦ ⟨localizationLift S B v h, comap_localizationLift S B v h⟩⟩
 
 end Localization
@@ -284,7 +281,8 @@ lemma suppFun_asIdeal (v : Spv A) : (suppFun v).asIdeal = v.supp := rfl
 /-- `suppFun ⁻¹' D(f) = Spv(A)(f/f)`. -/
 lemma suppFun_preimage_basicOpen (f : A) :
     suppFun ⁻¹' (PrimeSpectrum.basicOpen f : Set (PrimeSpectrum A)) = basicOpen f f := by
-  ext v; simp [basicOpen_self, mem_supp_iff]
+  ext v
+  simp [basicOpen_self, mem_supp_iff]
 
 /-- `suppFun` is continuous. -/
 theorem suppFun_continuous : Continuous (suppFun : Spv A → PrimeSpectrum A) :=

From 42f18e90d270d9fbfc952322151c84dd992a852e Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 18:02:54 +0100
Subject: [PATCH 07/15] style(ValuationSpectrum): remove subsection headers

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 Mathlib/RingTheory/Valuation/ValuationSpectrum.lean | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index dc498712abf2bf..e6d6529212b0fc 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -82,8 +82,6 @@ for `f, s : A`. -/
 instance instTopologicalSpace : TopologicalSpace (Spv A) :=
   TopologicalSpace.generateFrom { U | ∃ f s : A, U = basicOpen f s }
 
-/-! ### Functoriality of Spv -/
-
 section Functoriality
 
 variable {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
@@ -130,8 +128,6 @@ lemma comap_injective {φ : A →+* B} (hφ : Function.Surjective φ) :
 
 end Functoriality
 
-/-! ### Support of a point of `Spv A` -/
-
 /-- The support prime ideal `{ a ∈ A | v(a) = 0 }` of a point `v ∈ Spv A`. -/
 def supp (v : Spv A) : Ideal A :=
   @ValuativeRel.supp A _ v.toValuativeRel
@@ -160,8 +156,6 @@ lemma ofValuation_valuation (v : Spv A) :
   let : ValuativeRel A := v.toValuativeRel
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
-/-! ### Quotient -/
-
 section Quotient
 
 variable (𝔞 : Ideal A)
@@ -225,8 +219,6 @@ end Quotient
 lemma not_vle_zero_of_isUnit {f : A} (hu : IsUnit f) (v : Spv A) : ¬ v.vle f 0 :=
   let : ValuativeRel A := v.toValuativeRel; ValuativeRel.not_vle_zero_of_isUnit hu
 
-/-! ### Localization -/
-
 section Localization
 
 variable (S : Submonoid A) (B : Type*) [CommRing B] [Algebra A B] [IsLocalization S B]
@@ -270,8 +262,6 @@ lemma comap_localization_range :
 
 end Localization
 
-/-! ### Support map to PrimeSpectrum -/
-
 /-- The support map `Spv A → Spec A`. -/
 def suppFun : Spv A → PrimeSpectrum A := fun v ↦ ⟨v.supp, inferInstance⟩
 

From f5ac855c33d546da29f611ab9c8635e9d43abf10 Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 18:31:20 +0100
Subject: [PATCH 08/15] style(ValuativeRel/Comap): fix line length in docstring

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
index 2cd733d6623a48..6fb3be5715478e 100644
--- a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
+++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
@@ -24,7 +24,8 @@ namespace ValuativeRel
 
 variable {A B : Type*} [CommRing A] [CommRing B]
 
-/-- The pullback of a `ValuativeRel` along `φ : A →+* B`: `a₁ ≤ᵥ a₂ ↔ φ(a₁) ≤ᵥ φ(a₂)`. -/
+/-- The pullback of a `ValuativeRel` along `φ : A →+* B`:
+`a₁ ≤ᵥ a₂ ↔ φ(a₁) ≤ᵥ φ(a₂)`. -/
 @[reducible]
 def comap (φ : A →+* B) (v : ValuativeRel B) : ValuativeRel A where
   vle a₁ a₂ := v.vle (φ a₁) (φ a₂)

From 2f5d0953895ce34cfad60db5408ba76a966ee956 Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 18:32:56 +0100
Subject: [PATCH 09/15] =?UTF-8?q?style(ValuationSpectrum):=20use=20?=
 =?UTF-8?q?=E2=86=A6=20instead=20of=20=3D>=20for=20consistency?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 Mathlib/RingTheory/Valuation/ValuationSpectrum.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index e6d6529212b0fc..25df5247955796 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -145,7 +145,8 @@ instance instIsPrimeSupp (v : Spv A) : v.supp.IsPrime := by
 /-- The support of `ofValuation v` equals `v.supp`. -/
 lemma supp_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
     (v : Valuation A Γ₀) : (ofValuation v).supp = v.supp := by
-  ext x; rw [mem_supp_iff, Valuation.mem_supp_iff]
+  ext x
+  rw [mem_supp_iff, Valuation.mem_supp_iff]
   change v x ≤ v 0 ↔ _
   simp
 
@@ -163,7 +164,7 @@ variable (𝔞 : Ideal A)
 /-- `𝔞 ≤ supp(comap(mk 𝔞, w))` for all `w : Spv (A ⧸ 𝔞)`. -/
 lemma ideal_le_supp_comap_mk (w : Spv (A ⧸ 𝔞)) :
     𝔞 ≤ (comap (Ideal.Quotient.mk 𝔞) w).supp :=
-  fun a ha => by simp [Ideal.Quotient.eq_zero_iff_mem.mpr ha]
+  fun a ha ↦ by simp [Ideal.Quotient.eq_zero_iff_mem.mpr ha]
 
 /-- Lift a point `v ∈ Spv A` with `𝔞 ≤ supp v` to `Spv (A ⧸ 𝔞)`. -/
 noncomputable def quotientLift (v : Spv A) (h : 𝔞 ≤ v.supp) : Spv (A ⧸ 𝔞) :=

From 31c5cfbd29a1c3cb30106c6ee95efc3c910bf0ef Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Mon, 13 Apr 2026 21:29:38 +0100
Subject: [PATCH 10/15] fix(ValuationSpectrum): add module declarations for
 Lean 4 module system

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>
---
 .../RingTheory/Valuation/ValuationSpectrum.lean  | 16 +++++++++++-----
 .../RingTheory/Valuation/ValuativeRel/Comap.lean |  8 +++++++-
 2 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index 25df5247955796..1b5d6dc5c54ae4 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -3,11 +3,13 @@ Copyright (c) 2026 Chris Birkbeck. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 -/
-import Mathlib.RingTheory.Valuation.ValuativeRel.Comap
-import Mathlib.RingTheory.Valuation.Quotient
-import Mathlib.RingTheory.Valuation.ExtendToLocalization
-import Mathlib.Topology.Order
-import Mathlib.RingTheory.Spectrum.Prime.Topology
+module
+
+public import Mathlib.RingTheory.Valuation.ValuativeRel.Comap
+public import Mathlib.RingTheory.Valuation.Quotient
+public import Mathlib.RingTheory.Valuation.ExtendToLocalization
+public import Mathlib.Topology.Order
+public import Mathlib.RingTheory.Spectrum.Prime.Topology
 
 /-!
 # The Valuation Spectrum of a Ring
@@ -29,6 +31,8 @@ We define the valuation spectrum `Spv A` following Definition 4.1 of Wedhorn.
   Proposition 4.7(2)
 -/
 
+@[expose] public section
+
 -- This is defined as a structure extending `ValuativeRel A` rather than a type synonym, since we
 -- want to equip `Spv A` with a topology (generated by basic open sets) that we do not want to
 -- place on `ValuativeRel` itself, while still having direct access to the `ValuativeRel` API.
@@ -287,3 +291,5 @@ theorem suppFun_comap {B : Type*} [CommRing B] (φ : A →+* B) (v : Spv B) :
   ext; simp [mem_supp_iff, comap_vle]
 
 end ValuationSpectrum
+
+end
diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
index 6fb3be5715478e..ea32e057dacb06 100644
--- a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
+++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
@@ -3,7 +3,9 @@ Copyright (c) 2026 Chris Birkbeck. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 -/
-import Mathlib.RingTheory.Valuation.ValuativeRel.Basic
+module
+
+public import Mathlib.RingTheory.Valuation.ValuativeRel.Basic
 
 /-!
 # Comap for Valuative Relations
@@ -20,6 +22,8 @@ We define the pullback (comap) of a `ValuativeRel` along a ring homomorphism.
 * `ValuativeRel.not_vle_zero_of_isUnit` : If `f` is a unit, then `¬ f ≤ᵥ 0`.
 -/
 
+@[expose] public section
+
 namespace ValuativeRel
 
 variable {A B : Type*} [CommRing A] [CommRing B]
@@ -52,3 +56,5 @@ theorem not_vle_zero_of_isUnit [ValuativeRel A] {f : A} (hu : IsUnit f) :
   exact absurd this (not_vle.mpr zero_vlt_one)
 
 end ValuativeRel
+
+end

From 4c379ca63d9f1e2bf0da178f765f8c62a01056f2 Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Tue, 14 Apr 2026 12:38:26 +0100
Subject: [PATCH 11/15] save

---
 .../Valuation/ValuationSpectrum.lean          | 62 +++++++++----------
 .../Valuation/ValuativeRel/Comap.lean         |  2 +-
 2 files changed, 29 insertions(+), 35 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index 1b5d6dc5c54ae4..6baef6d1ae90c1 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -134,16 +134,18 @@ end Functoriality
 
 /-- The support prime ideal `{ a ∈ A | v(a) = 0 }` of a point `v ∈ Spv A`. -/
 def supp (v : Spv A) : Ideal A :=
-  @ValuativeRel.supp A _ v.toValuativeRel
+  letI := v.toValuativeRel
+  ValuativeRel.supp A
 
 @[simp]
 lemma mem_supp_iff (v : Spv A) (x : A) : x ∈ v.supp ↔ v.vle x 0 :=
-  @ValuativeRel.supp_def A _ v.toValuativeRel x
+  letI := v.toValuativeRel
+  ValuativeRel.supp_def x
 
 /-- The support of a point `v ∈ Spv A` is a prime ideal. -/
 instance instIsPrimeSupp (v : Spv A) : v.supp.IsPrime := by
-  change (@ValuativeRel.supp A _ v.toValuativeRel).IsPrime
-  rw [@ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel]
+  letI := v.toValuativeRel
+  change (ValuativeRel.supp A).IsPrime
   infer_instance
 
 /-- The support of `ofValuation v` equals `v.supp`. -/
@@ -157,8 +159,8 @@ lemma supp_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
 /-- The canonical valuation gives back the same point of `Spv`. -/
 lemma ofValuation_valuation (v : Spv A) :
     ofValuation (@ValuativeRel.valuation A _ v.toValuativeRel) = v := by
+  letI := v.toValuativeRel
   apply ValuationSpectrum.ext; funext x y
-  let : ValuativeRel A := v.toValuativeRel
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
 section Quotient
@@ -186,37 +188,30 @@ lemma quotientLift_comap (w : Spv (A ⧸ 𝔞)) :
   apply ValuationSpectrum.ext; funext x y
   obtain ⟨a₁, rfl⟩ := Ideal.Quotient.mk_surjective x
   obtain ⟨a₂, rfl⟩ := Ideal.Quotient.mk_surjective y
-  let : ValuativeRel A := ValuativeRel.comap (Ideal.Quotient.mk 𝔞) w.toValuativeRel
+  letI : ValuativeRel A := ValuativeRel.comap (Ideal.Quotient.mk 𝔞) w.toValuativeRel
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
 /-- The range of `comap (mk 𝔞)` is `{ v ∈ Spv A | 𝔞 ≤ supp v }`. -/
 lemma comap_quotient_range :
-    Set.range (comap (Ideal.Quotient.mk 𝔞)) = { v : Spv A | 𝔞 ≤ v.supp } := by
-  ext v
-  simp only [Set.mem_range, Set.mem_setOf_eq]
-  exact ⟨fun ⟨w, hw⟩ ↦ hw ▸ ideal_le_supp_comap_mk 𝔞 w,
-    fun h ↦ ⟨quotientLift 𝔞 v h, comap_quotientLift 𝔞 v h⟩⟩
+    Set.range (comap (Ideal.Quotient.mk 𝔞)) = { v : Spv A | 𝔞 ≤ v.supp } :=
+  Set.ext fun _ ↦ ⟨fun ⟨w, hw⟩ ↦ hw ▸ ideal_le_supp_comap_mk 𝔞 w,
+    fun h ↦ ⟨quotientLift 𝔞 _ h, comap_quotientLift 𝔞 _ h⟩⟩
 
 /-- `comap (mk 𝔞) : Spv (A ⧸ 𝔞) → Spv A` is a topological embedding. -/
 lemma comap_quotient_isEmbedding :
-    Topology.IsEmbedding (comap (Ideal.Quotient.mk 𝔞)) := by
-  constructor
-  · constructor
-    change ValuationSpectrum.instTopologicalSpace =
-      ValuationSpectrum.instTopologicalSpace.induced (comap (Ideal.Quotient.mk 𝔞))
+    Topology.IsEmbedding (comap (Ideal.Quotient.mk 𝔞)) where
+  eq_induced := by
     simp only [instTopologicalSpace, induced_generateFrom_eq]
     congr 1
     ext U
-    simp only [Set.mem_setOf_eq, Set.mem_image]
     constructor
     · rintro ⟨f', s', rfl⟩
       obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f'
       obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective s'
-      exact ⟨basicOpen f s, ⟨f, s, rfl⟩, comap_preimage_basicOpen _ f s⟩
+      exact ⟨_, ⟨f, s, rfl⟩, comap_preimage_basicOpen _ f s⟩
     · rintro ⟨_, ⟨f, s, rfl⟩, rfl⟩
-      rw [comap_preimage_basicOpen]
-      exact ⟨_, _, rfl⟩
-  · exact comap_injective Ideal.Quotient.mk_surjective
+      exact ⟨_, _, comap_preimage_basicOpen _ f s⟩
+  injective := comap_injective Ideal.Quotient.mk_surjective
 
 end Quotient
 
@@ -231,32 +226,31 @@ variable (S : Submonoid A) (B : Type*) [CommRing B] [Algebra A B] [IsLocalizatio
 /-- Lift `v ∈ Spv A` with `S ≤ (supp v).primeCompl` to `Spv B` (localization at `S`). -/
 noncomputable def localizationLift (v : Spv A) (hS : S ≤ v.supp.primeCompl) :
     Spv B :=
-  have hS' : S ≤ (@ValuativeRel.valuation A _ v.toValuativeRel).supp.primeCompl := by
+  letI := v.toValuativeRel
+  have hS' : S ≤ (ValuativeRel.valuation A).supp.primeCompl := by
     intro s hs; change s ∉ _
-    rw [← @ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel]; exact hS hs
-  ofValuation ((@ValuativeRel.valuation A _ v.toValuativeRel).extendToLocalization hS' B)
+    rw [← ValuativeRel.supp_eq_valuation_supp]; exact hS hs
+  ofValuation ((ValuativeRel.valuation A).extendToLocalization hS' B)
 
 /-- `comap (algebraMap A B) (localizationLift S B v hS) = v`. -/
 lemma comap_localizationLift (v : Spv A) (hS : S ≤ v.supp.primeCompl) :
     comap (algebraMap A B) (localizationLift S B v hS) = v := by
-  have hS' : S ≤ (@ValuativeRel.valuation A _ v.toValuativeRel).supp.primeCompl := by
+  letI := v.toValuativeRel
+  have hS' : S ≤ (ValuativeRel.valuation A).supp.primeCompl := by
     intro s hs; change s ∉ _
-    rw [← @ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel]
-    exact hS hs
+    rw [← ValuativeRel.supp_eq_valuation_supp]; exact hS hs
   change comap (algebraMap A B)
-    (ofValuation ((@ValuativeRel.valuation A _ v.toValuativeRel).extendToLocalization hS' B)) = v
+    (ofValuation ((ValuativeRel.valuation A).extendToLocalization hS' B)) = v
   rw [comap_ofValuation,
-    show ((@ValuativeRel.valuation A _ v.toValuativeRel).extendToLocalization hS' B).comap
-      (algebraMap A B) = @ValuativeRel.valuation A _ v.toValuativeRel from
+    show ((ValuativeRel.valuation A).extendToLocalization hS' B).comap (algebraMap A B) =
+         ValuativeRel.valuation A from
       Valuation.ext fun a ↦ Valuation.extendToLocalization_apply_map_apply _ hS' B a]
   exact ofValuation_valuation v
 
 /-- `S` is disjoint from `supp(comap(algebraMap, w))` for `w : Spv B`. -/
 lemma submonoid_le_supp_primeCompl_comap_algebraMap (w : Spv B) :
-    S ≤ (comap (algebraMap A B) w).supp.primeCompl := fun s hs ↦ by
-  change s ∉ (comap (algebraMap A B) w).supp
-  rw [mem_supp_iff, comap_vle, map_zero]
-  exact not_vle_zero_of_isUnit (IsLocalization.map_units B ⟨s, hs⟩) w
+    S ≤ (comap (algebraMap A B) w).supp.primeCompl := fun s hs hmem ↦
+  not_vle_zero_of_isUnit (IsLocalization.map_units B ⟨s, hs⟩) w (by simpa using hmem)
 
 /-- Range of `comap (algebraMap A B)` is `{ v | S ≤ supp(v).primeCompl }`. -/
 lemma comap_localization_range :
diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
index ea32e057dacb06..2549a689b729f5 100644
--- a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
+++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
@@ -40,7 +40,7 @@ def comap (φ : A →+* B) (v : ValuativeRel B) : ValuativeRel A where
   vle_mul_cancel h₀ h := by
     rw [map_zero] at h₀
     simpa [map_mul] using v.vle_mul_cancel h₀ (by simpa [map_mul] using h)
-  not_vle_one_zero := by simp [map_one, map_zero, v.not_vle_one_zero]
+  not_vle_one_zero := by simp [v.not_vle_one_zero]
 
 @[simp]
 theorem comap_vle (φ : A →+* B) (v : ValuativeRel B) (a₁ a₂ : A) :

From 6f14d30549bf878f4d6ac29526f8009706b70b4e Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Tue, 14 Apr 2026 12:51:23 +0100
Subject: [PATCH 12/15] cleanup

---
 .../Valuation/ValuationSpectrum.lean          | 33 ++++++++++---------
 1 file changed, 18 insertions(+), 15 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index 6baef6d1ae90c1..9d591eeb67a836 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -156,9 +156,17 @@ lemma supp_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
   change v x ≤ v 0 ↔ _
   simp
 
+/-- The canonical valuation associated to a point `v ∈ Spv A`. -/
+noncomputable def valuation (v : Spv A) :
+    Valuation A (@ValuativeRel.ValueGroupWithZero A _ v.toValuativeRel) :=
+  @ValuativeRel.valuation A _ v.toValuativeRel
+
+/-- The support of `v : Spv A` equals the support of its canonical valuation. -/
+lemma supp_eq_valuation_supp (v : Spv A) : v.supp = v.valuation.supp :=
+  @ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel
+
 /-- The canonical valuation gives back the same point of `Spv`. -/
-lemma ofValuation_valuation (v : Spv A) :
-    ofValuation (@ValuativeRel.valuation A _ v.toValuativeRel) = v := by
+lemma ofValuation_valuation (v : Spv A) : ofValuation v.valuation = v := by
   letI := v.toValuativeRel
   apply ValuationSpectrum.ext; funext x y
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
@@ -174,8 +182,7 @@ lemma ideal_le_supp_comap_mk (w : Spv (A ⧸ 𝔞)) :
 
 /-- Lift a point `v ∈ Spv A` with `𝔞 ≤ supp v` to `Spv (A ⧸ 𝔞)`. -/
 noncomputable def quotientLift (v : Spv A) (h : 𝔞 ≤ v.supp) : Spv (A ⧸ 𝔞) :=
-  ofValuation ((@ValuativeRel.valuation A _ v.toValuativeRel).onQuot
-    (@ValuativeRel.supp_eq_valuation_supp A _ v.toValuativeRel ▸ h))
+  ofValuation (v.valuation.onQuot (v.supp_eq_valuation_supp ▸ h))
 
 /-- `comap (mk 𝔞) (quotientLift 𝔞 v h) = v`. -/
 lemma comap_quotientLift (v : Spv A) (h : 𝔞 ≤ v.supp) :
@@ -226,24 +233,20 @@ variable (S : Submonoid A) (B : Type*) [CommRing B] [Algebra A B] [IsLocalizatio
 /-- Lift `v ∈ Spv A` with `S ≤ (supp v).primeCompl` to `Spv B` (localization at `S`). -/
 noncomputable def localizationLift (v : Spv A) (hS : S ≤ v.supp.primeCompl) :
     Spv B :=
-  letI := v.toValuativeRel
-  have hS' : S ≤ (ValuativeRel.valuation A).supp.primeCompl := by
+  have hS' : S ≤ v.valuation.supp.primeCompl := by
     intro s hs; change s ∉ _
-    rw [← ValuativeRel.supp_eq_valuation_supp]; exact hS hs
-  ofValuation ((ValuativeRel.valuation A).extendToLocalization hS' B)
+    rw [← v.supp_eq_valuation_supp]; exact hS hs
+  ofValuation (v.valuation.extendToLocalization hS' B)
 
 /-- `comap (algebraMap A B) (localizationLift S B v hS) = v`. -/
 lemma comap_localizationLift (v : Spv A) (hS : S ≤ v.supp.primeCompl) :
     comap (algebraMap A B) (localizationLift S B v hS) = v := by
-  letI := v.toValuativeRel
-  have hS' : S ≤ (ValuativeRel.valuation A).supp.primeCompl := by
+  have hS' : S ≤ v.valuation.supp.primeCompl := by
     intro s hs; change s ∉ _
-    rw [← ValuativeRel.supp_eq_valuation_supp]; exact hS hs
-  change comap (algebraMap A B)
-    (ofValuation ((ValuativeRel.valuation A).extendToLocalization hS' B)) = v
+    rw [← v.supp_eq_valuation_supp]; exact hS hs
+  change comap (algebraMap A B) (ofValuation (v.valuation.extendToLocalization hS' B)) = v
   rw [comap_ofValuation,
-    show ((ValuativeRel.valuation A).extendToLocalization hS' B).comap (algebraMap A B) =
-         ValuativeRel.valuation A from
+    show (v.valuation.extendToLocalization hS' B).comap (algebraMap A B) = v.valuation from
       Valuation.ext fun a ↦ Valuation.extendToLocalization_apply_map_apply _ hS' B a]
   exact ofValuation_valuation v
 

From 7815f388a3d990c452b8478574a9a257363fe37d Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Tue, 14 Apr 2026 12:56:21 +0100
Subject: [PATCH 13/15] cleanup@

---
 .../Valuation/ValuationSpectrum.lean          | 22 ++++++++-----------
 1 file changed, 9 insertions(+), 13 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index 9d591eeb67a836..4abc00155de11f 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -47,8 +47,7 @@ namespace ValuationSpectrum
 variable {A : Type*} [CommRing A]
 
 /-- Construct a point of `Spv A` from a valuation `v : Valuation A Γ₀`. -/
-def ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
-    (v : Valuation A Γ₀) : Spv A :=
+def ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation A Γ₀) : Spv A :=
   ⟨ValuativeRel.ofValuation v⟩
 
 /-- Two equivalent valuations define the same point of `Spv A`. -/
@@ -59,12 +58,10 @@ lemma ofValuation_eq_of_isEquiv {Γ₀ : Type*} [LinearOrderedCommGroupWithZero
   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 }`. -/
-def basicOpen (f s : A) : Set (Spv A) :=
-  { v | v.vle f s ∧ ¬ v.vle s 0 }
+def basicOpen (f s : A) : Set (Spv A) := { v | v.vle f s ∧ ¬ v.vle s 0 }
 
 /-- `Spv(A)(tf/ts) ⊆ Spv(A)(f/s)`. -/
-lemma basicOpen_mul_subset (t f s : A) :
-    basicOpen (t * f) (t * s) ⊆ basicOpen f s := by
+lemma basicOpen_mul_subset (t f s : A) : basicOpen (t * f) (t * s) ⊆ basicOpen f s := by
   intro v ⟨h1, h2⟩
   have ht : ¬ v.vle t 0 := by
     intro ht
@@ -134,17 +131,17 @@ end Functoriality
 
 /-- The support prime ideal `{ a ∈ A | v(a) = 0 }` of a point `v ∈ Spv A`. -/
 def supp (v : Spv A) : Ideal A :=
-  letI := v.toValuativeRel
+  let := v.toValuativeRel
   ValuativeRel.supp A
 
 @[simp]
 lemma mem_supp_iff (v : Spv A) (x : A) : x ∈ v.supp ↔ v.vle x 0 :=
-  letI := v.toValuativeRel
+  let := v.toValuativeRel
   ValuativeRel.supp_def x
 
 /-- The support of a point `v ∈ Spv A` is a prime ideal. -/
 instance instIsPrimeSupp (v : Spv A) : v.supp.IsPrime := by
-  letI := v.toValuativeRel
+  let := v.toValuativeRel
   change (ValuativeRel.supp A).IsPrime
   infer_instance
 
@@ -167,7 +164,7 @@ lemma supp_eq_valuation_supp (v : Spv A) : v.supp = v.valuation.supp :=
 
 /-- The canonical valuation gives back the same point of `Spv`. -/
 lemma ofValuation_valuation (v : Spv A) : ofValuation v.valuation = v := by
-  letI := v.toValuativeRel
+  let := v.toValuativeRel
   apply ValuationSpectrum.ext; funext x y
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
@@ -195,7 +192,7 @@ lemma quotientLift_comap (w : Spv (A ⧸ 𝔞)) :
   apply ValuationSpectrum.ext; funext x y
   obtain ⟨a₁, rfl⟩ := Ideal.Quotient.mk_surjective x
   obtain ⟨a₂, rfl⟩ := Ideal.Quotient.mk_surjective y
-  letI : ValuativeRel A := ValuativeRel.comap (Ideal.Quotient.mk 𝔞) w.toValuativeRel
+  let : ValuativeRel A := ValuativeRel.comap (Ideal.Quotient.mk 𝔞) w.toValuativeRel
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
 /-- The range of `comap (mk 𝔞)` is `{ v ∈ Spv A | 𝔞 ≤ supp v }`. -/
@@ -231,8 +228,7 @@ section Localization
 variable (S : Submonoid A) (B : Type*) [CommRing B] [Algebra A B] [IsLocalization S B]
 
 /-- Lift `v ∈ Spv A` with `S ≤ (supp v).primeCompl` to `Spv B` (localization at `S`). -/
-noncomputable def localizationLift (v : Spv A) (hS : S ≤ v.supp.primeCompl) :
-    Spv B :=
+noncomputable def localizationLift (v : Spv A) (hS : S ≤ v.supp.primeCompl) : Spv B :=
   have hS' : S ≤ v.valuation.supp.primeCompl := by
     intro s hs; change s ∉ _
     rw [← v.supp_eq_valuation_supp]; exact hS hs

From fd2432a3bb535474263037cdf1939bfe4f048b9d Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Tue, 14 Apr 2026 15:11:43 +0100
Subject: [PATCH 14/15] review: address riccardobrasca feedback on valuation
 spectrum
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 .../Valuation/ValuationSpectrum.lean          | 59 ++++++++++---------
 .../Valuation/ValuativeRel/Comap.lean         | 19 +++---
 2 files changed, 39 insertions(+), 39 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index 4abc00155de11f..5fe5e2aabdc9f6 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -14,7 +14,7 @@ public import Mathlib.RingTheory.Spectrum.Prime.Topology
 /-!
 # The Valuation Spectrum of a Ring
 
-We define the valuation spectrum `Spv A` following Definition 4.1 of Wedhorn.
+We define the valuation spectrum `Spv A` following [Wedhorn][wedhorn_adic], Definition 4.1.
 
 ## Main definitions
 
@@ -27,7 +27,7 @@ We define the valuation spectrum `Spv A` following Definition 4.1 of Wedhorn.
 
 ## References
 
-* [T. Wedhorn, *Adic Spaces*][wedhorn2019adic], Definition 4.1, Remark 4.3, Remark 4.4,
+* [T. Wedhorn, *Adic Spaces*][wedhorn_adic], Definition 4.1, Remark 4.3, Remark 4.4,
   Proposition 4.7(2)
 -/
 
@@ -62,12 +62,11 @@ def basicOpen (f s : A) : Set (Spv A) := { v | v.vle f s ∧ ¬ v.vle s 0 }
 
 /-- `Spv(A)(tf/ts) ⊆ Spv(A)(f/s)`. -/
 lemma basicOpen_mul_subset (t f s : A) : basicOpen (t * f) (t * s) ⊆ basicOpen f s := by
-  intro v ⟨h1, h2⟩
-  have ht : ¬ v.vle t 0 := by
-    intro ht
-    exact h2 (by have := v.mul_vle_mul_left ht s; rwa [zero_mul] at this)
-  exact ⟨v.vle_mul_cancel ht (by rwa [mul_comm t f, mul_comm t s] at h1),
-    fun hs ↦ h2 (by have := v.mul_vle_mul_left hs t; rwa [zero_mul, mul_comm s t] at this)⟩
+  rintro v ⟨h1, h2⟩
+  have ht : ¬ v.vle t 0 := fun ht ↦ h2 (by simpa using v.mul_vle_mul_left ht s)
+  refine ⟨v.vle_mul_cancel ht ?_, fun hs ↦ h2 ?_⟩
+  · rwa [mul_comm t f, mul_comm t s] at h1
+  · simpa [mul_comm s t] using v.mul_vle_mul_left hs t
 
 /-- `Spv(A)(1/1) = Spv A`. -/
 lemma basicOpen_one : basicOpen (1 : A) 1 = Set.univ :=
@@ -100,25 +99,25 @@ lemma comap_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
     (φ : A →+* B) (v : Valuation B Γ₀) :
     comap φ (ofValuation v) = ofValuation (v.comap φ) := rfl
 
-/-- `Spv(φ)⁻¹(Spv(A)(f/s)) = Spv(B)(φ(f)/φ(s))`. -/
+/-- `comap φ ⁻¹' Spv(A)(f/s) = Spv(B)(φ(f)/φ(s))`. -/
 lemma comap_preimage_basicOpen (φ : A →+* B) (f s : A) :
     comap φ ⁻¹' basicOpen f s = basicOpen (φ f) (φ s) := by
   ext v
   simp only [Set.mem_preimage, basicOpen, Set.mem_setOf_eq, comap_vle, map_zero]
 
-/-- `Spv(φ)` is continuous. -/
+/-- `comap φ` is continuous. -/
 lemma comap_continuous (φ : A →+* B) : Continuous (comap φ) :=
   continuous_generateFrom_iff.mpr fun _ ⟨f, s, hU⟩ ↦
     hU ▸ comap_preimage_basicOpen φ f s ▸
       TopologicalSpace.isOpen_generateFrom_of_mem ⟨φ f, φ s, rfl⟩
 
-/-- `Spv(id) = id`. -/
+/-- `comap` of the identity is the identity. -/
 @[simp]
-lemma comap_id : comap (RingHom.id A) = id := by ext v : 1; ext; rfl
+lemma comap_id : comap (RingHom.id A) = id := by ext; rfl
 
-/-- `Spv(ψ ∘ φ) = Spv(φ) ∘ Spv(ψ)` (contravariant functoriality). -/
+/-- `comap` is contravariantly functorial: `comap (ψ ∘ φ) = comap φ ∘ comap ψ`. -/
 lemma comap_comp (φ : A →+* B) (ψ : B →+* C) :
-    comap (ψ.comp φ) = comap φ ∘ comap ψ := by ext v : 1; ext; rfl
+    comap (ψ.comp φ) = comap φ ∘ comap ψ := by ext; rfl
 
 /-- `comap φ` is injective when `φ` is surjective. -/
 lemma comap_injective {φ : A →+* B} (hφ : Function.Surjective φ) :
@@ -129,31 +128,33 @@ lemma comap_injective {φ : A →+* B} (hφ : Function.Surjective φ) :
 
 end Functoriality
 
-/-- The support prime ideal `{ a ∈ A | v(a) = 0 }` of a point `v ∈ Spv A`. -/
+/-- The support prime ideal `{ a ∈ A | v(a) = 0 }` of a point `v : Spv A`. -/
 def supp (v : Spv A) : Ideal A :=
-  let := v.toValuativeRel
+  letI := v.toValuativeRel
   ValuativeRel.supp A
 
 @[simp]
 lemma mem_supp_iff (v : Spv A) (x : A) : x ∈ v.supp ↔ v.vle x 0 :=
-  let := v.toValuativeRel
+  letI := v.toValuativeRel
   ValuativeRel.supp_def x
 
-/-- The support of a point `v ∈ Spv A` is a prime ideal. -/
-instance instIsPrimeSupp (v : Spv A) : v.supp.IsPrime := by
-  let := v.toValuativeRel
-  change (ValuativeRel.supp A).IsPrime
-  infer_instance
+/-- The support of a point `v : Spv A` is a prime ideal. -/
+instance instIsPrimeSupp (v : Spv A) : v.supp.IsPrime :=
+  letI := v.toValuativeRel
+  inferInstanceAs (ValuativeRel.supp A).IsPrime
+
+/-- `(ofValuation v).vle x y ↔ v x ≤ v y`. -/
+@[simp]
+lemma vle_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+    (v : Valuation A Γ₀) (x y : A) : (ofValuation v).vle x y ↔ v x ≤ v y := Iff.rfl
 
 /-- The support of `ofValuation v` equals `v.supp`. -/
 lemma supp_ofValuation {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
     (v : Valuation A Γ₀) : (ofValuation v).supp = v.supp := by
   ext x
-  rw [mem_supp_iff, Valuation.mem_supp_iff]
-  change v x ≤ v 0 ↔ _
-  simp
+  simp [mem_supp_iff, Valuation.mem_supp_iff]
 
-/-- The canonical valuation associated to a point `v ∈ Spv A`. -/
+/-- The canonical valuation associated to a point `v : Spv A`. -/
 noncomputable def valuation (v : Spv A) :
     Valuation A (@ValuativeRel.ValueGroupWithZero A _ v.toValuativeRel) :=
   @ValuativeRel.valuation A _ v.toValuativeRel
@@ -164,7 +165,7 @@ lemma supp_eq_valuation_supp (v : Spv A) : v.supp = v.valuation.supp :=
 
 /-- The canonical valuation gives back the same point of `Spv`. -/
 lemma ofValuation_valuation (v : Spv A) : ofValuation v.valuation = v := by
-  let := v.toValuativeRel
+  letI := v.toValuativeRel
   apply ValuationSpectrum.ext; funext x y
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
@@ -192,7 +193,7 @@ lemma quotientLift_comap (w : Spv (A ⧸ 𝔞)) :
   apply ValuationSpectrum.ext; funext x y
   obtain ⟨a₁, rfl⟩ := Ideal.Quotient.mk_surjective x
   obtain ⟨a₂, rfl⟩ := Ideal.Quotient.mk_surjective y
-  let : ValuativeRel A := ValuativeRel.comap (Ideal.Quotient.mk 𝔞) w.toValuativeRel
+  letI : ValuativeRel A := ValuativeRel.comap (Ideal.Quotient.mk 𝔞) w.toValuativeRel
   exact propext (ValuativeRel.valuation A).vle_iff_le.symm
 
 /-- The range of `comap (mk 𝔞)` is `{ v ∈ Spv A | 𝔞 ≤ supp v }`. -/
@@ -221,7 +222,7 @@ 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 :=
-  let : ValuativeRel A := v.toValuativeRel; ValuativeRel.not_vle_zero_of_isUnit hu
+  letI : ValuativeRel A := v.toValuativeRel; hu.not_vle_zero
 
 section Localization
 
diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
index 2549a689b729f5..804b5cf44c5b0c 100644
--- a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
+++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
@@ -19,7 +19,7 @@ We define the pullback (comap) of a `ValuativeRel` along a ring homomorphism.
 
 ## Main results
 
-* `ValuativeRel.not_vle_zero_of_isUnit` : If `f` is a unit, then `¬ f ≤ᵥ 0`.
+* `IsUnit.not_vle_zero` : If `f` is a unit, then `¬ f ≤ᵥ 0`.
 -/
 
 @[expose] public section
@@ -30,9 +30,9 @@ variable {A B : Type*} [CommRing A] [CommRing B]
 
 /-- The pullback of a `ValuativeRel` along `φ : A →+* B`:
 `a₁ ≤ᵥ a₂ ↔ φ(a₁) ≤ᵥ φ(a₂)`. -/
-@[reducible]
+@[implicit_reducible]
 def comap (φ : A →+* B) (v : ValuativeRel B) : ValuativeRel A where
-  vle a₁ a₂ := v.vle (φ a₁) (φ a₂)
+  vle a₁ a₂ := (φ a₁) ≤ᵥ (φ a₂)
   vle_total a₁ a₂ := v.vle_total (φ a₁) (φ a₂)
   vle_trans h₁ h₂ := v.vle_trans h₁ h₂
   vle_add h₁ h₂ := by simpa [map_add] using v.vle_add h₁ h₂
@@ -44,17 +44,16 @@ def comap (φ : A →+* B) (v : ValuativeRel B) : ValuativeRel A where
 
 @[simp]
 theorem comap_vle (φ : A →+* B) (v : ValuativeRel B) (a₁ a₂ : A) :
-    (comap φ v).vle a₁ a₂ = v.vle (φ a₁) (φ a₂) := rfl
+    (comap φ v).vle a₁ a₂ ↔ v.vle (φ a₁) (φ a₂) := Iff.rfl
+
+end ValuativeRel
 
 /-- If `f` is a unit, then `¬ f ≤ᵥ 0`. -/
-theorem not_vle_zero_of_isUnit [ValuativeRel A] {f : A} (hu : IsUnit f) :
+theorem IsUnit.not_vle_zero {A : Type*} [CommRing A] [ValuativeRel A] {f : A} (hu : IsUnit f) :
     ¬ f ≤ᵥ (0 : A) := by
   obtain ⟨u, rfl⟩ := hu
   intro h
-  have := mul_vle_mul_right h (↑u⁻¹ : A)
-  rw [Units.inv_mul, mul_zero] at this
-  exact absurd this (not_vle.mpr zero_vlt_one)
-
-end ValuativeRel
+  simpa [Units.inv_mul, ValuativeRel.not_vle.mpr ValuativeRel.zero_vlt_one]
+    using ValuativeRel.mul_vle_mul_right h ↑u⁻¹
 
 end

From a44161ae1b94104ecfc4cc6e013ca91b1612316b Mon Sep 17 00:00:00 2001
From: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Date: Tue, 14 Apr 2026 15:16:34 +0100
Subject: [PATCH 15/15] review: replace rfl with named comap_id/comap_comp
 lemmas
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 Mathlib/RingTheory/Valuation/ValuationSpectrum.lean  | 8 ++++++--
 Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean | 8 ++++++++
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
index 5fe5e2aabdc9f6..267c2d0dce1314 100644
--- a/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
+++ b/Mathlib/RingTheory/Valuation/ValuationSpectrum.lean
@@ -113,11 +113,15 @@ lemma comap_continuous (φ : A →+* B) : Continuous (comap φ) :=
 
 /-- `comap` of the identity is the identity. -/
 @[simp]
-lemma comap_id : comap (RingHom.id A) = id := by ext; rfl
+lemma comap_id : comap (RingHom.id A) = id := by
+  funext v
+  exact ValuationSpectrum.ext <| congr_arg (·.vle) (ValuativeRel.comap_id v.toValuativeRel)
 
 /-- `comap` is contravariantly functorial: `comap (ψ ∘ φ) = comap φ ∘ comap ψ`. -/
 lemma comap_comp (φ : A →+* B) (ψ : B →+* C) :
-    comap (ψ.comp φ) = comap φ ∘ comap ψ := by ext; rfl
+    comap (ψ.comp φ) = comap φ ∘ comap ψ := by
+  funext v
+  exact ValuationSpectrum.ext <| congr_arg (·.vle) (ValuativeRel.comap_comp φ ψ v.toValuativeRel)
 
 /-- `comap φ` is injective when `φ` is surjective. -/
 lemma comap_injective {φ : A →+* B} (hφ : Function.Surjective φ) :
diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
index 804b5cf44c5b0c..818056ba6bbc54 100644
--- a/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
+++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Comap.lean
@@ -46,6 +46,14 @@ def comap (φ : A →+* B) (v : ValuativeRel B) : ValuativeRel A where
 theorem comap_vle (φ : A →+* B) (v : ValuativeRel B) (a₁ a₂ : A) :
     (comap φ v).vle a₁ a₂ ↔ v.vle (φ a₁) (φ a₂) := Iff.rfl
 
+@[simp]
+theorem comap_id (v : ValuativeRel A) : comap (RingHom.id A) v = v := by
+  ext a₁ a₂; rfl
+
+theorem comap_comp {C : Type*} [CommRing C] (φ : A →+* B) (ψ : B →+* C) (v : ValuativeRel C) :
+    comap (ψ.comp φ) v = comap φ (comap ψ v) := by
+  ext a₁ a₂; rfl
+
 end ValuativeRel
 
 /-- If `f` is a unit, then `¬ f ≤ᵥ 0`. -/