## Stream: Is there code for X?

### Topic: P-adic valuation on polynomials

#### Julien Marquet (Feb 05 2021 at 15:01):

Hi,
I'm trying to implement p-adic valuations on principal rings.
I copied the definition of p-adic valuations for int, which gets me here :

import data.real.basic
import data.real.cau_seq
import ring_theory.principal_ideal_domain

open_locale classical
noncomputable theory

def padic_val {α} [comm_ring α] [is_principal_ideal_ring α] (p: α) [prime p] (a: α): ℝ :=
if a ≠ 0 then (multiplicity p a).get (multiplicity.finite_def.2 (by { sorry /-  -/}))
else 0


The question is :

• Is this the right way to implement it or did I miss something more adequate ?
• Are there lemmas on well-founded orders that can help me with this ?
(what I'm looking for here is "if I have an infinite decreasing sequence, then my order is not well-founded")

#### Johan Commelin (Feb 05 2021 at 15:20):

I don't think this should take values in real. That will make your life more difficult down the road.

#### Johan Commelin (Feb 05 2021 at 15:20):

There are some subtleties here. You'll have to choose whether you want an additive or multiplicative valuation. Both have pros and cons.

#### Kevin Buzzard (Feb 05 2021 at 15:24):

My thoughts on this are that there should be a totally ordered monoid with zero which is {0} union naturals, with notation "rho^n" corresponding to natural n, where 0<rho<1 is thought of as a real number, so it's ordered like this: 0 < ...<rho^100<rho^99<...<rho^2<rho^1<rho^0. Talking to people, some say I should make a new structure and some say I should use with_zero (order_dual (multiplicative nat)). I don't want to use the latter, but I've never thought of a good name for it so I stopped there.

#### Kevin Buzzard (Feb 05 2021 at 15:25):

If someone could only give me a name for this structure, I can make the API and then I would recommend to Julien that they define their valuation to take values in this totally ordered commutative monoid with 0. I don't think I quite got around to changing the definition of valuation so that it would allow a target of a monoid with 0 rather than a group, but I am now absolutely convinced that it should.

#### Ryan Lahfa (Feb 05 2021 at 15:26):

Kevin Buzzard said:

If someone could only give me a name for this structure, I can make the API and then I would recommend to Julien that they define their valuation to take values in this totally ordered commutative monoid with 0. I don't think I quite got around to changing the definition of valuation so that it would allow a target of a monoid with 0 rather than a group, but I am now absolutely convinced that it should.

The Buzzard monoid? :p

#### Kevin Buzzard (Feb 05 2021 at 15:26):

Let's really not call it that.

#### Kevin Buzzard (Feb 05 2021 at 15:26):

We also need a version for integers, because this is the correct target for the p-adic valuation on the rationals, or more generally the valuation on the field of fractions of a Dedekind domain.

#### Johan Commelin (Feb 05 2021 at 15:27):

menat for multiplicative (enat).

#### Johan Commelin (Feb 05 2021 at 15:28):

@Kevin Buzzard Do you have notation for it? If so, we don't have to care about the name.

#### Julien Marquet (Feb 05 2021 at 15:29):

Actually in this case I will need absolute values with values in ℝ
The function I wrote before should have its value in ℕ

#### Kevin Buzzard (Feb 05 2021 at 15:29):

No -- you know what we do in practice, we just call it the reals like Julien suggested, because in real life there is no DTT hell.

#### Johan Commelin (Feb 05 2021 at 15:29):

you could call it exp_nat_with_zero and hide it behind good notation

#### Kevin Buzzard (Feb 05 2021 at 15:30):

And when we apply it to $\mathbb{C}[T]$ with the $T$-adic valuation, we just send $T$ to some random real between 0 and 1 because there is no canonical choice. Or we just use the additive version to $\mathbb{Z}\cup\{\infty\}$.

#### Kevin Buzzard (Feb 05 2021 at 15:31):

@Julien Marquet you can look at what I did in discrete_valuation_ring.lean -- there I wrote the additive valuation and I just let it take values in the naturals and I sent 0 to a random value.

#### Julien Marquet (Feb 05 2021 at 15:34):

What caught my attention is that mathlib apparently lacks lemmas on well-founded orders : no infinite decreasing chain; existence of a min; ...

#### Julien Marquet (Feb 05 2021 at 15:34):

(I am currently writing proofs for these)

#### Johan Commelin (Feb 05 2021 at 15:35):

I think there is quite some stuff, but I'm not an expert.

#### Johan Commelin (Feb 05 2021 at 15:35):

@Aaron Anderson :up:

#### Julien Marquet (Feb 05 2021 at 15:41):

Actually I found the theorems in order.well_founded

Last updated: May 16 2021 at 05:21 UTC