generalizing padic_val

Stream: maths

[Chris Hughes]

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?

[Mario Carneiro]

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

[Johan Commelin]

But maybe UFD's are the right level of generality

[Mario Carneiro]

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

[Mario Carneiro]

for example you can use it to define a ufd

[Mario Carneiro]

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

[Kevin Buzzard]

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 $\mathbb{Z}[(-5)^{1/2}]:=\{\,a+b(-5)^{1/2}\,\mid\,a,b\in\mathbb{Z}\,\}$ the 2-adic valuation of both $1\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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

I wish dvd was defined on monoids instead of semirings

[Mario Carneiro]

although you could argue about whether commutative matters

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

It's like an archimedean property

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Maybe it follows from Krull. @Kenny Lau ?

[Kenny Lau]

how should I know

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

oh right, ignoring units

[Chris Hughes]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

is that a problem?

[Chris Hughes]

Sorry yeah.

[Chris Hughes]

Might be a problem

[Chris Hughes]

It just means p_adic_val_eq_zero_iff has an extra assumption

[Mario Carneiro]

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

[Chris Hughes]

Currently it defaults to zero.

[Chris Hughes]

Yes.

[Chris Hughes]

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

[Mario Carneiro]

or a proposition asserting finiteness

[Mario Carneiro]

perhaps the roption nat version works best here

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

like padics

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

because of pfun.fix

[Mario Carneiro]

maybe nat.rfind is easier to use

[Chris Hughes]

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.

[Mario Carneiro]

my point is that here the mathematics and computability aspects coincide

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Chris Hughes]

You're right. I'm being stupid.

[Kevin Buzzard]

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).

[Chris Hughes]

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

[Johan Commelin]

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

[Johan Commelin]

But I think it satisfies your other requirement.

[Chris Hughes]

Situation like that happening didn't occur to me.

[Chris Hughes]

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))

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

how about divisibility?

[Kevin Buzzard]

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 $p$-adic valuation" usually refers to the map $v_p$ with $v_p(p)=1$, where as "the $p$-adic norm" is the one with $|p|_{p}=1/p$. Sadly, in perfectoid land, the norm is referred to as a "valuation" :-(

[Chris Hughes]

The current definition is

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

[Chris Hughes]

I'll probably change the name at some point.

[Chris Hughes]

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

[Mario Carneiro]

maybe specialized to enat?

[Mario Carneiro]

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

[Chris Hughes]

Okay sure.

[Chris Hughes]

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