P-adic valuation on polynomials

Stream: Is there code for X?

[Julien Marquet]

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]

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

[Johan Commelin]

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

[Johan Commelin]

@Kevin Buzzard thought a lot about this.

[Kevin Buzzard]

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]

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]

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]

Let's really not call it that.

[Kevin Buzzard]

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]

menat for multiplicative (enat).

[Johan Commelin]

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

[Julien Marquet]

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

[Kevin Buzzard]

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]

you could call it exp_nat_with_zero and hide it behind good notation

[Kevin Buzzard]

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]

@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]

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

[Julien Marquet]

(I am currently writing proofs for these)

[Johan Commelin]

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

[Johan Commelin]

@Aaron Anderson :up:

[Julien Marquet]

Actually I found the theorems in order.well_founded