Rank one valuations

Stream: mathlib4

[Antoine Chambert-Loir]

There is a slight ambiguity in the mathematical literature about what a rank one valuation is.
In most cases, this is used to say that the value group of the valuation embeds into the reals, as an ordered abelian group., that is, that the rank is at most one.
Mathlib's docs#Valuation.RankOne seems to have taken the terminology seriously and further insists that the valuation is nontrivial (so the rank is exactly one).

This is highly legitimate but might lead to unfortunate discrepancies when translating math literature into Lean.

For example, this makes the correspondence between valued nonarchimedean fields and fields endowed with a rank one valuation a bit awkward, since the trivial absolute value is allowed in one case and not in the other one. This is more or less visible in docs#Valued.norm, but not too much yet, because of the inaccurracy in Mathlib's definition of the topology of a ring endowed with a valuation.

I wonder whether it is more natural to reorganize as

• some RankLeOne type class that corresponds to the embedding into the real
• combined with a Nontrivial condition.

[Antoine Chambert-Loir]

Cc @Filippo A. E. Nuccio and @María Inés de Frutos Fernández and @Patrick Massot

[María Inés de Frutos Fernández]

I think this sounds like a good change; we can create the class RankLeOne and then redefine RankOne as the class extending RankLeOne and Nontrivial (I discussed this with @Filippo A. E. Nuccio and he agrees).