Zulip Chat Archive

Stream: Is there code for X?

Topic: P-adic valuation on polynomials


view this post on Zulip 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")

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:20):

@Kevin Buzzard thought a lot about this.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 15:26):

Let's really not call it that.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:27):

menat for multiplicative (enat).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:29):

you could call it exp_nat_with_zero and hide it behind good notation

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 15:30):

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

view this post on Zulip 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.

view this post on Zulip 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; ...

view this post on Zulip Julien Marquet (Feb 05 2021 at 15:34):

(I am currently writing proofs for these)

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:35):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 15:35):

@Aaron Anderson :up:

view this post on Zulip 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