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

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

Mathlib/RingTheory/Valuation/ValuationSpectrum.lean

@@ -0,0 +1,322 @@
+/-
+Copyright (c) 2026 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+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
+
+We define the valuation spectrum `Spv A` following [Wedhorn][wedhorn_adic], Definition 4.1.
+
+## 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*][wedhorn_adic], Definition 4.1, Remark 4.3, Remark 4.4,
+  Proposition 4.7(2)
+-/
+
+@[expose] public section
+
+/-- The *valuation spectrum* `Spv A` of a commutative ring `A`. A point of `Spv A` is a
+`ValuativeRel A`, but `Spv A` is kept as a distinct type so it can carry its own topology
+without affecting `ValuativeRel A`. -/
+@[ext]
+structure ValuationSpectrum (A : Type*) [CommRing A] where
+  ofValuativeRel ::
+  /-- The underlying `ValuativeRel A` of a point `v : Spv A`. -/
+  toValuativeRel : ValuativeRel A
+
+@[inherit_doc] notation "Spv" => ValuationSpectrum
+
+namespace ValuationSpectrum
+
+variable {A : Type*} [CommRing A]
+
+/-- The valuative relation `≤ᵥ` of a point `v : Spv A`. -/
+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 :=
+  v.toValuativeRel.vle_trans h₁ h₂
+
+lemma vle_add {v : Spv A} {x y z : A} (h₁ : v.vle x z) (h₂ : v.vle y z) : v.vle (x + y) z :=
+  v.toValuativeRel.vle_add h₁ h₂
+
+lemma mul_vle_mul_left {v : Spv A} {x y : A} (h : v.vle x y) (z : A) : v.vle (x * z) (y * z) :=
+  v.toValuativeRel.mul_vle_mul_left h z
+
+lemma vle_mul_cancel {v : Spv A} {x y z : A} (hz : ¬ v.vle z 0) (h : v.vle (x * z) (y * z)) :
+    v.vle x y :=
+  v.toValuativeRel.vle_mul_cancel hz h
+
+lemma not_vle_one_zero (v : Spv A) : ¬ v.vle 1 0 := v.toValuativeRel.not_vle_one_zero
+
+/-- 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 (ValuativeRel.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)`. -/
+lemma basicOpen_mul_subset (t f s : A) : basicOpen (t * f) (t * s) ⊆ basicOpen f s := by
+  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 :=
+  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 }`. -/
+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 }
+
+section Functoriality
+
+variable {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
+
+/-- Contravariant map `Spv B → Spv A` induced by `φ : A →+* B`. -/
+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
+
+/-- `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]
+
+/-- `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⟩
+
+/-- `comap` of the identity is the identity. -/
+@[simp]
+lemma comap_id : comap (RingHom.id A) = id := by
+  funext v
+  exact ValuationSpectrum.ext (ValuativeRel.comap_id v.toValuativeRel)
+
+/-- `comap` is contravariantly functorial: `comap (ψ ∘ φ) = comap φ ∘ comap ψ`. -/
+lemma comap_comp (φ : A →+* B) (ψ : B →+* C) :
+    comap (ψ.comp φ) = comap φ ∘ comap ψ := by
+  funext v
+  exact ValuationSpectrum.ext (ValuativeRel.comap_comp φ ψ v.toValuativeRel)
+
+/-- `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
+  apply ValuativeRel.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
+
+/-- 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
+  ValuativeRel.supp A
+
+@[simp]
+lemma mem_supp_iff (v : Spv A) (x : A) : x ∈ v.supp ↔ v.vle x 0 :=
+  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 :=
+  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
+  simp [mem_supp_iff, Valuation.mem_supp_iff]
+
+/-- 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 v.valuation = v := by
+  letI := v.toValuativeRel
+  apply ValuationSpectrum.ext
+  apply ValuativeRel.ext
+  funext x y
+  exact propext (ValuativeRel.valuation A).vle_iff_le.symm
+
+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 :=
+  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 ⧸ 𝔞) :=
+  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) :
+    comap (Ideal.Quotient.mk 𝔞) (quotientLift 𝔞 v h) = v := by
+  simpa using 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
+  apply ValuativeRel.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 } :=
+  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 𝔞)) where
+  eq_induced := by
+    simp only [instTopologicalSpace, induced_generateFrom_eq]
+    congr 1
+    ext U
+    constructor
+    · rintro ⟨f', s', rfl⟩
+      obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f'
+      obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective s'
+      exact ⟨_, ⟨f, s, rfl⟩, comap_preimage_basicOpen _ f s⟩
+    · rintro ⟨_, ⟨f, s, rfl⟩, rfl⟩
+      exact ⟨_, _, comap_preimage_basicOpen _ f s⟩
+  injective := 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; hu.not_vle_zero
+
+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 ≤ v.valuation.supp.primeCompl := by
+    intro s hs; change s ∉ _
+    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
+  have hS' : S ≤ v.valuation.supp.primeCompl := by
+    intro s hs; change s ∉ _
+    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 (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
+
+/-- `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 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 :
+    Set.range (comap (algebraMap A B)) = { v : Spv A | S ≤ v.supp.primeCompl } := by
+  ext v
+  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
+
+/-- The support map `Spv A → Spec A`. -/
+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. -/
+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`. -/
+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
+
+end