feat: WithVal v and WithVal w are isomorphic as uniform spaces when v and w are equivalent valuations (leanprover-community#30133)

Author: smmercuri

Mathlib/Algebra/Order/Hom/Ring.lean

@@ -388,6 +388,14 @@ theorem symm_symm (e : α ≃+*o β) : e.symm.symm = e := rfl
 theorem symm_bijective : Bijective (OrderRingIso.symm : (α ≃+*o β) → β ≃+*o α) :=
   Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
 
+@[simp]
+theorem symm_apply_apply (e : α ≃+*o β) (a : α) : e.symm (e a) = a :=
+  e.toRingEquiv.symm_apply_apply a
+
+@[simp]
+theorem apply_symm_apply (e : α ≃+*o β) (b : β) : e (e.symm b) = b :=
+  e.toRingEquiv.apply_symm_apply b
+
 /-- Composition of `OrderRingIso`s as an `OrderRingIso`. -/
 @[trans]
 protected def trans (f : α ≃+*o β) (g : β ≃+*o γ) : α ≃+*o γ :=
@@ -420,6 +428,18 @@ theorem symm_trans_self (e : α ≃+*o β) : e.symm.trans e = OrderRingIso.refl
 
 end LE
 
+section Preorder
+
+variable {R S : Type*} [Mul R] [Add R] [Mul S] [Add S] [Preorder R] [Preorder S]
+
+theorem lt_symm_apply (e : R ≃+*o S) {x : R} {y : S} : x < e.symm y ↔ e x < y := by
+  simpa using e.toOrderIso.lt_symm_apply
+
+theorem symm_apply_lt (e : R ≃+*o S) {x : R} {y : S} : e.symm y < x ↔ y < e x := by
+  simpa using e.toOrderIso.symm_apply_lt
+
+end Preorder
+
 section NonAssocSemiring
 
 variable [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β]

Mathlib/RingTheory/Valuation/Basic.lean

@@ -594,6 +594,10 @@ lemma lt_one_iff_lt_one (h : v₁.IsEquiv v₂) {x : R} :
     v₁ x < 1 ↔ v₂ x < 1 := by
   rw [← v₁.map_one, h.lt_iff_lt, map_one]
 
+lemma pos_iff (h : v₁.IsEquiv v₂) {x : R} :
+    0 < v₁ x ↔ 0 < v₂ x := by
+  rw [zero_lt_iff, zero_lt_iff, h.ne_zero]
+
 end IsEquiv
 
 -- end of namespace

Mathlib/Topology/Algebra/Valued/WithVal.lean

@@ -80,6 +80,9 @@ instance {P S : Type*} [Ring S] [Semiring P] [Module P R] [Module P S]
     [Algebra R S] [IsScalarTower P R S] :
     IsScalarTower P (WithVal v) S := inferInstanceAs (IsScalarTower P R S)
 
+instance [Ring R] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+    {v : Valuation R Γ₀} : Preorder (WithVal v) := v.toPreorder
+
 end Instances
 
 section Ring
@@ -94,13 +97,37 @@ def valuation : Valuation (WithVal v) Γ₀ := v.comap (equiv v)
 
 @[simp] lemma valuation_equiv_symm (x : R) : valuation v ((equiv v).symm x) = v x := rfl
 
+variable {Γ'₀ : Type*} [LinearOrderedCommGroupWithZero Γ'₀]
+
+/-- Canonical ring equivalence between `WithVal v` and `WithVal w`. -/
+def equivWithVal (v : Valuation R Γ₀) (w : Valuation R Γ'₀) :
+    WithVal v ≃+* WithVal w :=
+  (equiv v).trans (equiv w).symm
+
+theorem equivWithVal_symm (v : Valuation R Γ₀) (w : Valuation R Γ'₀) :
+    (equivWithVal v w).symm = equivWithVal w v := rfl
+
+@[simp]
+theorem equivWithVal_apply (v : Valuation R Γ₀) (w : Valuation R Γ'₀) {x : WithVal v} :
+    equivWithVal v w x = (equiv w).symm (equiv v x) := rfl
+
+@[simp]
+theorem equivWithVal_symm_apply (v : Valuation R Γ₀) (w : Valuation R Γ'₀) {x : WithVal w} :
+    (equivWithVal v w).symm x = (equiv v).symm (equiv w x) := rfl
+
 instance {R} [Ring R] (v : Valuation R Γ₀) : Valued (WithVal v) Γ₀ :=
   Valued.mk' (valuation v)
 
 theorem apply_equiv (r : WithVal v) : v (equiv v r) = Valued.v r := rfl
 
 @[simp] theorem apply_symm_equiv (r : R) : Valued.v ((equiv v).symm r) = v r := rfl
 
+theorem le_def {v : Valuation R Γ₀} {a b : WithVal v} :
+    a ≤ b ↔ v (equiv v a) ≤ v (equiv v b) := .rfl
+
+theorem lt_def {v : Valuation R Γ₀} {a b : WithVal v} :
+    a < b ↔ v (equiv v a) < v (equiv v b) := .rfl
+
 end Ring
 
 section CommRing
@@ -128,6 +155,56 @@ abbrev Completion := UniformSpace.Completion (WithVal v)
 instance : Coe R v.Completion :=
   inferInstanceAs <| Coe (WithVal v) (UniformSpace.Completion (WithVal v))
 
+section Equivalence
+
+/-! The uniform isomorphism between `WithVal v` and `WithVal w` when `v` and `w` are
+equivalent. -/
+
+variable {R Γ₀ Γ₀' : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ₀]
+  [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'}
+
+/-- If two valuations `v` and `w` are equivalent then `WithVal v` is order-isomorphic
+to `WithVal w`. -/
+def IsEquiv.orderRingIso (h : v.IsEquiv w) :
+    WithVal v ≃+*o WithVal w where
+  __ := equivWithVal v w
+  map_le_map_iff' := h.symm ..
+
+@[simp]
+theorem IsEquiv.orderRingIso_apply (h : v.IsEquiv w) (x : WithVal v) :
+    h.orderRingIso x = (equivWithVal v w) x := rfl
+
+@[simp]
+theorem IsEquiv.orderRingIso_symm_apply (h : v.IsEquiv w) (x : WithVal w) :
+    h.orderRingIso.symm x = (equivWithVal v w).symm x := rfl
+
+-- TODO: remove hw when we have range bases for Valued's ValuativeRel #27314
+theorem IsEquiv.uniformContinuous_equivWithVal
+    (hw : ∀ γ : Γ₀'ˣ, ∃ r s, 0 < w r ∧ 0 < w s ∧ w r / w s = γ) (h : v.IsEquiv w) :
+    UniformContinuous (equivWithVal v w) := by
+  refine uniformContinuous_of_continuousAt_zero _ ?_
+  rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
+    (Valued.hasBasis_nhds_zero _ _)]
+  intro γ _
+  obtain ⟨r, s, hr₀, hs₀, hr⟩ := hw γ
+  use .mk0 (v r / v s) (by simp [h.ne_zero, hr₀.ne.symm, hs₀.ne.symm]), trivial, fun x hx ↦ ?_
+  rw [← hr, Set.mem_setOf_eq, ← WithVal.apply_equiv, ← (equiv w).apply_symm_apply r,
+    lt_div_iff₀ hs₀, ← (equiv w).apply_symm_apply s, ← map_mul, ← map_mul, ← lt_def,
+    ← h.orderRingIso_apply, ← h.orderRingIso.apply_symm_apply ((equiv w).symm s), ← map_mul,
+    ← h.orderRingIso.lt_symm_apply]
+  simpa [lt_def, lt_div_iff₀ (h.pos_iff.2 hs₀)] using hx
+
+/-- If two valuations `v` and `w` are equivalent then `WithVal v` and `WithVal w` are
+isomorphic as uniform spaces. -/
+def IsEquiv.uniformEquiv (hv : ∀ γ : Γ₀ˣ, ∃ r s, 0 < v r ∧ 0 < v s ∧ v r / v s = γ)
+    (hw : ∀ γ : Γ₀'ˣ, ∃ r s, 0 < w r ∧ 0 < w s ∧ w r / w s = γ)
+    (h : v.IsEquiv w) : WithVal v ≃ᵤ WithVal w where
+  __ := equivWithVal v w
+  uniformContinuous_toFun := h.uniformContinuous_equivWithVal hw
+  uniformContinuous_invFun := h.symm.uniformContinuous_equivWithVal hv
+
+end Equivalence
+
 end Valuation
 
 namespace NumberField.RingOfIntegers