Zulip Chat Archive

Stream: maths

Topic: generalizing padic_val


view this post on Zulip Chris Hughes (Nov 19 2018 at 08:48):

In my proof of FTA, I need the highest power of a polynomial that divides another polynomial. Should padic_val be generalized to do this. What's the correct generality for this function?

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:49):

You should be able to say this in any comm semiring (where dvd is defined)

view this post on Zulip Johan Commelin (Nov 19 2018 at 08:50):

But maybe UFD's are the right level of generality

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:50):

no, some of this you want to be able to state even without ufd

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:50):

for example you can use it to define a ufd

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:51):

plus that's a hell of a proof obligation for using the notation

view this post on Zulip Kevin Buzzard (Nov 19 2018 at 08:55):

The theory really takes off in a ring where the notions of prime and irreducible elements coincide; then for r an irreducible element of a comm ring with this property, the "r-adic valuation" is very well-behaved (e.g. it's additive). Even for a ring like Z[(5)1/2]:={a+b(5)1/2a,bZ}\mathbb{Z}[(-5)^{1/2}]:=\{\,a+b(-5)^{1/2}\,\mid\,a,b\in\mathbb{Z}\,\} the 2-adic valuation of both 1±(5)1/21\pm (-5)^{1/2} is 0 but the 2-adic valuation of $(1+(-5)^{1/2})(1-(-5)^{1/2})$ is 1, and 2 is irreducible.

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:56):

I don't think it necessarily has to be a valuation like in the padics

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:56):

you can say 2 is the highest power of 4 that divides 48

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:57):

and you have to worry about infinity being a possible answer regardless, because of 0

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:57):

so at that point it's really valid as long as dvd and power are defined

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:58):

We do rely on the property a^m | b -> a^n | b when m >= n, but that is true in any monoid

view this post on Zulip Kevin Buzzard (Nov 19 2018 at 08:59):

Right. I don't know the answer to Chris' question of the generality it should be defined in Lean, I was just explaining the boundaries of where it started to be useful in commutative algebra.

view this post on Zulip Mario Carneiro (Nov 19 2018 at 08:59):

I wish dvd was defined on monoids instead of semirings

view this post on Zulip Mario Carneiro (Nov 19 2018 at 09:00):

although you could argue about whether commutative matters

view this post on Zulip Kevin Buzzard (Nov 19 2018 at 09:00):

I can't imagine ever needing this function for a non prime element and it won't have any nice properties, but over a UFD this function is used all the time by mathematicians

view this post on Zulip Mario Carneiro (Nov 19 2018 at 09:01):

One interesting thing you can do with this function is define the class of rings where it is always finite for nonzeros

view this post on Zulip Mario Carneiro (Nov 19 2018 at 09:01):

It's like an archimedean property

view this post on Zulip Mario Carneiro (Nov 19 2018 at 09:04):

Here is a silly example using a non-prime: the count of 10 inside a number n is its number of trailing zeros

view this post on Zulip Kevin Buzzard (Nov 19 2018 at 09:08):

Maybe Noetherian rings with no nilpotents have this property. Nilpotents will always screw you up, and Noetherian is a finiteness hypothesis which typically makes intuitive things like this true

view this post on Zulip Kevin Buzzard (Nov 19 2018 at 09:09):

Maybe it follows from Krull. @Kenny Lau ?

view this post on Zulip Kenny Lau (Nov 19 2018 at 09:10):

how should I know

view this post on Zulip Kevin Buzzard (Nov 19 2018 at 09:12):

Krull needs proper ideals. Aah. So for a unit it's always infinite

view this post on Zulip Kevin Buzzard (Nov 19 2018 at 09:12):

You didn't do krull yet Kenny? It's in AM. .

view this post on Zulip Mario Carneiro (Nov 19 2018 at 09:13):

oh right, ignoring units

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:03):

If I define it over a comm_semiring it's going to be noncomputable. Is that the right approach?

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:08):

ah, that's true. How about a decidable_rel dvd assumption?

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:08):

Still not computable. I have to decide whether it's finite or not.

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:10):

right, this puts it in the same class as order-finding

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:11):

how is it being represented in the first place? are you using with_top nat?

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:11):

I haven't decided. Probably default to zero since zero's not being used for anything else.

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:12):

well, zero has a meaning here (no powers of p in the number)

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:12):

is that a problem?

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:12):

Sorry yeah.

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:12):

Might be a problem

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:12):

It just means p_adic_val_eq_zero_iff has an extra assumption

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:13):

although for general comm semirings that assumption is kind of complicated, right?

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:13):

Currently it defaults to zero.

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:13):

Yes.

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:14):

But maybe in a UFD or something it's simpler, so there'll have to be a UFD version of the lemma.

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:14):

or a proposition asserting finiteness

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:15):

perhaps the roption nat version works best here

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:15):

since that way you get the proposition for free, encoded in the roption, and it's computable

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:16):

but we will want to specialize the function to rings where we can prove finiteness

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:16):

like padics

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:17):

You still have to decide if somethings a unit or not.

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:18):

With the roption version, you can just do the naive search and it's computable

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:18):

because of pfun.fix

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:20):

maybe nat.rfind is easier to use

view this post on Zulip Chris Hughes (Nov 19 2018 at 14:21):

It's "computable" but you still have to give a proof to actually compute it. I'm not a fan of worsening ease of proof for the sake of computability.

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:21):

my point is that here the mathematics and computability aspects coincide

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:21):

we need an extra "infinity" value, and roption gives us that

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:22):

and as far as giving a proof, that is exactly what we can do in nice rings like int

view this post on Zulip Mario Carneiro (Nov 19 2018 at 14:24):

(actually, in the VM you can cheat and evaluate any roption, even if it is an infinite search)

view this post on Zulip Chris Hughes (Nov 21 2018 at 14:59):

@Mario Carneiro One downside of generalizing padic val, is that now for integers it will return an int rather than a nat, which I know can be very annoying. Is this a good reason to have two definitions?

view this post on Zulip Mario Carneiro (Nov 21 2018 at 15:00):

How so? If it's defined based on monoid.pow then it should give a nat

view this post on Zulip Chris Hughes (Nov 21 2018 at 15:10):

You're right. I'm being stupid.

view this post on Zulip Kevin Buzzard (Nov 21 2018 at 18:06):

In maths you would have valuations taking on natural values on the "integers" and valuations taking integer values on the "rationals", and both would be used (in some generality).

view this post on Zulip Chris Hughes (Nov 21 2018 at 18:46):

@Kevin Buzzard Is the statement that every non-zero non unit has a finite padic val equivalent to UFD. It seems to be provided there aren't any elements which can be divided by infinitely many distinct primes, and I'm not sure if that's possible or not.

view this post on Zulip Johan Commelin (Nov 21 2018 at 18:48):

@Chris Hughes In Z[5]\mathbb{Z}[\surd{-5}] you have (15)(1+5)=6=23(1 - \surd{-5})(1 + \surd{-5}) = 6 = 2 \cdot 3. So that is not a UFD.

view this post on Zulip Johan Commelin (Nov 21 2018 at 18:50):

But I think it satisfies your other requirement.

view this post on Zulip Chris Hughes (Nov 21 2018 at 22:34):

Situation like that happening didn't occur to me.

view this post on Zulip Chris Hughes (Nov 22 2018 at 04:57):

Some of the statements become a bit ugly with roption. Is there a good way around this?

protected lemma mul {a b : α} (ha0 : a  0) (hb0 : b  0) :
  get (padic_val p a) (finite_of_prime hp ha0) +
  get (padic_val p b) (finite_of_prime hp hb0) =
  get (padic_val p (a * b)) (finite_of_prime hp (mul_ne_zero ha0 hb0))

view this post on Zulip Johan Commelin (Nov 22 2018 at 07:29):

@Chris Hughes What is your current definition of padic_val? Is there someplace we can read your latest code?
I think the idea was that you don't even assume that p is prime... (I didn't even know that we had prime elements in arbitrary rings already). If you want to make an assumption on the element, it is probably most natural to assume that it is irreducible. Also, maybe the name should now also be generalised to adic_val?

view this post on Zulip Mario Carneiro (Nov 22 2018 at 07:38):

I called it "prime count" in metamath, although it wasn't defined only on primes

view this post on Zulip Mario Carneiro (Nov 22 2018 at 07:38):

it's not really the padic valuation since usually that involves a reciprocal

view this post on Zulip Mario Carneiro (Nov 22 2018 at 07:39):

how about divisibility?

view this post on Zulip Kevin Buzzard (Nov 22 2018 at 08:26):

Re the gets -- can you just define addition on roption? I don't quite know what I'm talking about here. Re

it's not really the padic valuation since usually that involves a reciprocal

even though the term is used for both the multiplicative and additive versions of this idea, I think "the pp-adic valuation" usually refers to the map vpv_p with vp(p)=1v_p(p)=1, where as "the pp-adic norm" is the one with pp=1/p|p|_{p}=1/p. Sadly, in perfectoid land, the norm is referred to as a "valuation" :-(

view this post on Zulip Chris Hughes (Nov 22 2018 at 12:12):

The current definition is

def padic_val [comm_semiring α] [decidable_rel (() : α  α  Prop)] (a b : α) : roption  :=
⟨∃ n : , ¬a ^ (n + 1)  b, λ h, nat.find h

view this post on Zulip Chris Hughes (Nov 22 2018 at 12:35):

I'll probably change the name at some point.

view this post on Zulip Chris Hughes (Nov 23 2018 at 12:19):

@Mario Carneiro Are you in favour of making a version of with_top with roption instead of option, with all the order and algebra on it? It would make sense for padic_val, but also order of elements of infinite groups.

view this post on Zulip Mario Carneiro (Nov 23 2018 at 12:19):

maybe specialized to enat?

view this post on Zulip Mario Carneiro (Nov 23 2018 at 12:20):

that particular structure seems useful, not so sure about generally with-topping a set

view this post on Zulip Chris Hughes (Nov 23 2018 at 12:21):

Okay sure.

view this post on Zulip Chris Hughes (Nov 23 2018 at 14:03):

I can't do inf computably for the lattice on enat. Should I leave it out?


Last updated: May 18 2021 at 07:19 UTC