chore(RingTheory/Valuation): change definition of IsValuativeTopology (#27939)

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Author: kckennylau

Mathlib/RingTheory/Valuation/ValuativeRel.lean

@@ -680,8 +680,8 @@ open Topology ValuativeRel in
 /-- We say that a topology on `R` is valuative if the neighborhoods of `0` in `R`
 are determined by the relation `· ≤ᵥ ·`. -/
 class IsValuativeTopology (R : Type*) [CommRing R] [ValuativeRel R] [TopologicalSpace R] where
-  mem_nhds_iff : ∀ s : Set R, s ∈ 𝓝 (0 : R) ↔
-    ∃ γ : (ValueGroupWithZero R)ˣ, { x | valuation _ x < γ } ⊆ s
+  mem_nhds_iff {s : Set R} {x : R} : s ∈ 𝓝 (x : R) ↔
+    ∃ γ : (ValueGroupWithZero R)ˣ, (x + ·) '' { z | valuation _ z < γ } ⊆ s
 
 @[deprecated (since := "2025-08-01")] alias ValuativeTopology := IsValuativeTopology
 

Mathlib/Topology/Algebra/Valued/ValuativeRel.lean

@@ -17,50 +17,103 @@ to facilitate a refactor.
 
 -/
 
-namespace ValuativeRel
+namespace IsValuativeTopology
 
-variable {R : Type*} [CommRing R]
+section
 
-instance [UniformSpace R] [IsUniformAddGroup R] [ValuativeRel R] [IsValuativeTopology R] :
-    Valued R (ValueGroupWithZero R) :=
-  .mk (valuation R) IsValuativeTopology.mem_nhds_iff
+/-! # Alternate constructors -/
 
-end ValuativeRel
+variable {R : Type*} [CommRing R] [ValuativeRel R] [TopologicalSpace R]
 
-namespace IsValuativeTopology
+open ValuativeRel TopologicalSpace Filter Topology Set
+
+local notation "v" => valuation R
+
+/-- Assuming `ContinuousConstVAdd R R`, we only need to check the neighbourhood of `0` in order to
+prove `IsValuativeTopology R`. -/
+theorem of_zero [ContinuousConstVAdd R R]
+    (h₀ : ∀ s : Set R, s ∈ 𝓝 0 ↔ ∃ γ : (ValueGroupWithZero R)ˣ, { z | v z < γ } ⊆ s) :
+    IsValuativeTopology R where
+  mem_nhds_iff {s x} := by
+    simpa [← vadd_mem_nhds_vadd_iff (t := s) (-x), ← image_vadd, ← image_subset_iff] using
+      h₀ ((x + ·) ⁻¹' s)
+
+end
 
 variable {R : Type*} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R]
 
 open ValuativeRel TopologicalSpace Filter Topology Set
 
 local notation "v" => valuation R
 
+/-- A version mentioning subtraction. -/
+lemma mem_nhds_iff' {s : Set R} {x : R} :
+    s ∈ 𝓝 (x : R) ↔
+    ∃ γ : (ValueGroupWithZero R)ˣ, { z | v (z - x) < γ } ⊆ s := by
+  convert mem_nhds_iff (s := s) using 4
+  ext z
+  simp [neg_add_eq_sub]
+
+@[deprecated (since := "2025-08-01")]
+alias _root_.ValuativeTopology.mem_nhds := mem_nhds_iff'
+
+lemma mem_nhds_zero_iff (s : Set R) : s ∈ 𝓝 (0 : R) ↔
+    ∃ γ : (ValueGroupWithZero R)ˣ, { x | v x < γ } ⊆ s := by
+  convert IsValuativeTopology.mem_nhds_iff' (x := (0 : R))
+  rw [sub_zero]
+
+@[deprecated (since := "2025-08-04")]
+alias _root_.ValuativeTopology.mem_nhds_iff := mem_nhds_zero_iff
+
+/-- Helper `Valued` instance when `ValuativeTopology R` over a `UniformSpace R`,
+for use in porting files from `Valued` to `ValuativeRel`. -/
+instance (priority := low) {R : Type*} [CommRing R] [ValuativeRel R] [UniformSpace R]
+    [IsUniformAddGroup R] [IsValuativeTopology R] :
+    Valued R (ValueGroupWithZero R) where
+  «v» := valuation R
+  is_topological_valuation := mem_nhds_zero_iff
+
+theorem hasBasis_nhds (x : R) :
+    (𝓝 x).HasBasis (fun _ => True)
+      fun γ : (ValueGroupWithZero R)ˣ => { z | v (z - x) < γ } := by
+  simp [Filter.hasBasis_iff, mem_nhds_iff']
+
 variable (R) in
 theorem hasBasis_nhds_zero :
     (𝓝 (0 : R)).HasBasis (fun _ => True)
       fun γ : (ValueGroupWithZero R)ˣ => { x | v x < γ } := by
-  simp [Filter.hasBasis_iff, mem_nhds_iff]
+  convert hasBasis_nhds (0 : R); rw [sub_zero]
 
 @[deprecated (since := "2025-08-01")]
 alias _root_.ValuativeTopology.hasBasis_nhds_zero := hasBasis_nhds_zero
 
-variable [IsTopologicalAddGroup R]
-
-theorem mem_nhds {s : Set R} {x : R} :
-    s ∈ 𝓝 x ↔ ∃ γ : (ValueGroupWithZero R)ˣ, { y | v (y - x) < γ } ⊆ s := by
-  simp only [← nhds_translation_add_neg x, ← sub_eq_add_neg, preimage_setOf_eq, true_and,
-    ((hasBasis_nhds_zero R).comap fun y => y - x).mem_iff]
-
-@[deprecated (since := "2025-08-01")]
-alias _root_.ValuativeTopology.mem_nhds := mem_nhds
+variable (R) in
+instance (priority := low) isTopologicalAddGroup : IsTopologicalAddGroup R := by
+  have cts_add : ContinuousConstVAdd R R :=
+    ⟨fun x ↦ continuous_iff_continuousAt.2 fun z ↦
+      ((hasBasis_nhds z).tendsto_iff (hasBasis_nhds (x + z))).2 fun γ _ ↦
+        ⟨γ, trivial, fun y hy ↦ by simpa using hy⟩⟩
+  have basis := hasBasis_nhds_zero R
+  refine .of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm
+  · exact (basis.prod_self.tendsto_iff basis).2 fun γ _ ↦
+      ⟨γ, trivial, fun ⟨_, _⟩ hx ↦ (v).map_add_lt hx.left hx.right⟩
+  · exact (basis.tendsto_iff basis).2 fun γ _ ↦ ⟨γ, trivial, fun y hy ↦ by simpa using hy⟩
+  · ext; simp
+  · simpa [ContinuousAt] using (cts_add.1 x₀).continuousAt (x := (0 : R))
+  · simpa [ContinuousAt] using (cts_add.1 (-x₀)).continuousAt (x := x₀)
+
+instance (priority := low) : IsTopologicalRing R :=
+  letI := IsTopologicalAddGroup.toUniformSpace R
+  letI := isUniformAddGroup_of_addCommGroup (G := R)
+  inferInstance
 
 theorem isOpen_ball (r : ValueGroupWithZero R) :
     IsOpen {x | v x < r} := by
   rw [isOpen_iff_mem_nhds]
   rcases eq_or_ne r 0 with rfl | hr
   · simp
   · intro x hx
-    rw [mem_nhds]
+    rw [mem_nhds_iff']
     simp only [setOf_subset_setOf]
     exact ⟨Units.mk0 _ hr,
       fun y hy => (sub_add_cancel y x).symm ▸ ((v).map_add _ x).trans_lt (max_lt hy hx)⟩
@@ -89,7 +142,7 @@ lemma isOpen_closedBall {r : ValueGroupWithZero R} (hr : r ≠ 0) :
     IsOpen {x | v x ≤ r} := by
   rw [isOpen_iff_mem_nhds]
   intro x hx
-  rw [mem_nhds]
+  rw [mem_nhds_iff']
   simp only [setOf_subset_setOf]
   exact ⟨Units.mk0 _ hr, fun y hy => (sub_add_cancel y x).symm ▸
     le_trans ((v).map_add _ _) (max_le (le_of_lt hy) hx)⟩
@@ -102,7 +155,7 @@ theorem isClosed_closedBall (r : ValueGroupWithZero R) :
   rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
   intro x hx
   simp only [mem_compl_iff, mem_setOf_eq, not_le] at hx
-  rw [mem_nhds]
+  rw [mem_nhds_iff']
   have hx' : v x ≠ 0 := ne_of_gt <| lt_of_le_of_lt zero_le' <| hx
   exact ⟨Units.mk0 _ hx', fun y hy hy' => ne_of_lt hy <| Valuation.map_sub_swap v x y ▸
       (Valuation.map_sub_eq_of_lt_left _ <| lt_of_le_of_lt hy' hx)⟩
@@ -137,19 +190,6 @@ alias _root_.ValuativeTopology.isOpen_sphere := isOpen_sphere
 
 end IsValuativeTopology
 
-namespace Valued
-
-variable {R : Type*} [CommRing R] [ValuativeRel R] [UniformSpace R]
-  [IsUniformAddGroup R] [IsValuativeTopology R]
-
-/-- Helper `Valued` instance when `ValuativeTopology R` over a `UniformSpace R`,
-for use in porting files from `Valued` to `ValuativeRel`. -/
-scoped instance : Valued R (ValuativeRel.ValueGroupWithZero R) where
-  v := ValuativeRel.valuation R
-  is_topological_valuation := IsValuativeTopology.mem_nhds_iff
-
-end Valued
-
 namespace ValuativeRel
 
 @[inherit_doc]