Shouldn't this (and possibly a bunch of other things) be done for any compatible valuation? In fact, would it be interesting to change the definition of the topology to not refer to the canonical valuation, by replacing the balls {x | v x < r} with {x | u * x ≤ᵥ y} where y is in R and u in posSubmonoid r? This way it's clear that the topology is still determined by any compatible valuation.

@adamtopaz what do you think of such a redefinition of the class? I can show an iff in the meantime.

Hmm, it's not an iff, because u * x ≤ᵥ y means v u * v x ≤ v y, while the topology has a strict inequality.

Ah right, I meant the strict inequality (so the negation of the converse). That should work right?

This way it's clear that the topology is still determined by any compatible valuation.

I think that "compatibility" here has to be very powerful. Because on its own, I could have a valuation that maps to Zm0, and another that maps into Zm0 x Zm0 where the first component is always 1. Then something like (-1, 1) is a unit, but everything in the nonzero range of my valuation is greater than that. So this new valuation induces a discrete topology, because there the ideal less than the unit is the {0}.

Here it is formalized:

import Mathlib

open WithZero LinearOrderedCommGroupWithZero

variable {R : Type*} [CommRing R] (v : Valuation R ℤᵐ⁰)

def other : Valuation R (WithZero (ℤᵐ⁰ˣ ×ₗ ℤᵐ⁰ˣ)) where
  toMonoidWithZeroHom := (inr _ _).toMonoidWithZeroHom.comp v.toMonoidWithZeroHom
  map_add_le_max' := by
    intro x y
    simpa using ((inr ℤᵐ⁰ _).monotone' (v.map_add_le_max' x y))

lemma other_apply {x : R} (hx : v x ≠ 0) :
    other v x = WithZero.coe (toLex (1, Units.mk0 (v x) hx)) := by
  -- simp lemmas get in the way
  change (inr _ _) (v x) = _
  simp [inr_eq_coe_inrₗ hx]

lemma isEquiv : v.IsEquiv (other v) := by
  intro r s
  by_cases hr : v r = 0
  · simp [hr, other]
  by_cases hs : v s = 0
  · simp [hs, other]
  simp [other_apply v hr, other_apply v hs, Prod.Lex.toLex_le_toLex, ← Units.val_le_val]

lemma problem :
    ∃ (r : (WithZero (ℤᵐ⁰ˣ ×ₗ ℤᵐ⁰ˣ))ˣ), ∀ x : R, other v x < r → v x = 0 := by
  let r := OrderMonoidHom.inlₗ ℤᵐ⁰ˣ ℤᵐ⁰ˣ
    (OrderMonoidIso.unitsWithZero.symm (Multiplicative.ofAdd (-1)))
  use OrderMonoidIso.unitsWithZero.symm r
  intro x
  contrapose!
  intro hx
  rw [other_apply v hx]
  simp [r, Prod.Lex.toLex_le_toLex, ← Units.val_lt_val, ← Multiplicative.toAdd_lt]

This is just the usual codomain issue right? By "the topology is determined by any compatible valuation", I indeed meant that you would only take radii in the nonzero range of the valuation.

My reasoning behind this proposal is that, I assumed, there will be cases where there's one convenient valuation at hand to study the topology (e.g the one coming from the Haar measure for local fields, or the p-adic one on p-adics, etc...), and it would be a pain to always have to translate back to the "canonical" valuation associated to the ValuativeRel. But I'm no number theorist, so I may well be completely wrong about the way you think about this.

The whole point of ValuativeRel is to avoid having to keep around another type for the codomain of the valuation. IMO, ValuativeTopology should only involve the underlying type of the ring itself, so I don't think we should define it in terms of some arbitrary compatible valuation. If you want to define a $$<_v$$ in terms of $$\le_v$$ and use that to define ValuativeTopology, then that's something I would support.

I understand that in practice there would be rings which obtain a topology from some seminorm, but I think in such cases ValuativeRel would also be defined in terms of the seminorm.

Sure, nothing should be defined in terms of an arbitrary valuation. My point is that we should be able to study the topology by means of any preferred valuation which is compatible.

I think these should be separate definitions (and not abbrev, very importantly)

@kckennylau what do you mean? These are lemmas not data.

I meant that { p : R × R | v (p.2 - p.1) < r } etc. should be definitions

@kckennylau what do you mean? These are lemmas not data.

But it's about a normed commring R? Should this be in the NormedField namespace? Confused.

Unfortunately, this is NormedCommRing + NormOneClass + NormMulClass, which gives the multiplicative normed structure, as opposed to the submultiplicative norm (‖x * y‖ ≤ ‖x‖ ‖y‖) property. I'll change the docstring. However, I think it still makes sense to keep the NormedField namespace because of this. And this file uses Normed.Field.Lemmas.

This lemma looks quite weird to me. I think we shouldn't work with bundled ValuativeRel.posSubmonoid R in the first place?

We get such bundled terms from ValuativeRel.exists_valuation_div_valuation_eq and friends.