p-adic Valuation of negative numbers

Stream: Is there code for X?

[Gareth Ma]

Is there code for (-r).valuation = r.valuation for either r : \Z_[2]or r : \Q_[2]?

[Johan Commelin]

Should be called valuation_neg

[Johan Commelin]

I would be very surprised if that isn't there

[Adam Topaz]

we have docs#valuation.map_neg but this is the docs#padic.valuation if I understand correctly, and it seems that we don't have docs#padic.valuation_neg

[Adam Topaz]

we should have padic.valuation as a genuine docs#valuation but I can't seem to find it right now

[Adam Topaz]

oh it's docs#padic.add_valuation so you should be able to use docs#add_valuation.map_neg

[Gareth Ma]

Thank you! Transfering to add_valuation works. I will add to mathlib when I get more lemmas going(?)

[David Loeffler]

It's slightly unfortunate that mathlib's development of valuations doesn't really match the usual mathematical usage of the term "valuation". When number theorists talk about p-adics (outside of the very particular context of Huber's adic-space theory), what they call "valuation" is what mathlib calls "add_valuation" -- a map that converts multiplication into addition (and satisfies the triangle inequality, etc).

I think it wouldn't hurt to add some text to the file docstring for p-adics explaining this

[Kevin Buzzard]

I agree that this is not great, but of course half the problem is the inconsistencies in the human literature. I think Maria Ines tried to stick to Bosch-Guentzer-Remmert's notation when she was doing extensions of norms (I convinced her it was canonical). But Huber is also canonical :-/

[David Loeffler]

Huber's work, and Wedhorn's exposition of it, are canonical for the theory of adic spaces, but I would certainly not consider them canonical texts for p-adic arithmetic! Gouvea's textbook, for instance, is pretty unambiguous that the "p-adic valuation" on $\mathbb{Q}$ or $\mathbb{Q}_p$ is a map into $\mathbb{Z}$. Anyway, I'm not trying to advocate for a change of conventions, just saying that we should perhaps add a bit more documentation to explain what we presently have.

[Gareth Ma]

Anyway, I'm not trying to advocate for a change of conventions

Actually I think it's not a bad idea to migrate and correct the notations, since the padic files are not that big right now

[Gareth Ma]

Also I think apart from valuation and add_valuations etc, there's also padic_val_nat and padic_val_rat which seems to be duplicates

[Adam Topaz]

I generally agree (at least from my experience with the literature on valuation theory) that valuations are usually written in the additive form. But this is awkward to formalize for a few reasons. First, in books we usually write
$v : K^\times \to \Gamma$
where $K$ is a field and $\Gamma$ is a totally ordered additive abelian group. To extend it to $K$, we usually add $\infty$, and to get an absolute value in the rank 1 case we take some exponential. All of these additional (mathematically superficial) steps make it annoying to work with in lean. And because of this, I actually quite prefer the current definition we have for docs#valuation taking values in a multiplicative object with 0. Of course, if some API is missing to go back and forth between docs#valuation and docs#add_valuation then it should be added, but I personally think that docs#valuation should be the preferred definition in mathlib.

[David Loeffler]

First, in books we usually write $v : K^\times \to \Gamma$ where K is a field and $\Gamma$ is a totally ordered additive abelian group.

Indeed; and that's exactly what end-users will expect to see in mathlib, and be confused when they don't.

One change that wouldn't break anything, and might render the p-adic code less confusing, would be to rename the current valuation as mul_valuation, and the current add_valuation as valuation.

[David Loeffler]

An aside: is it worth introducing some kind of classes monoid_hom_mul_to_add and monoid_hom_add_to_mul for maps which convert addition into multiplication and vice versa? Clearly the p-adic valuation would naturally be a mul_to_add_monoid_hom; but the opposite problem comes up in developing Fourier theory, where one needs to consider homomorphisms $(R, +) \to \mathbb{C}^\times$, for R a ring; the canonical example is $x \mapsto e^{2\pi i x}$ on $\mathbb{R}$, but the case $R = \mathbb{Q}_p$ is interesting too.

[Yaël Dillies]

See docs#add_char

[David Loeffler]

That's good to have (but clearly shouldn't be hidden away in number_theory.legendre_symbol). I guess we don't have the mirror image, multiplicative-to-additive definition, though?

[Yaël Dillies]

No indeed. So far we've decided to make-do with docs#multiplicative or docs#additive to reduce code duplication.

[Michael Stoll]

You'll actually get code multiplication by 4 or 8 or ... when there are several homomorphisms in play...