## Stream: maths

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

#### Mario Carneiro (Nov 19 2018 at 08:49):

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

#### Johan Commelin (Nov 19 2018 at 08:50):

But maybe UFD's are the right level of generality

#### Mario Carneiro (Nov 19 2018 at 08:50):

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

#### Mario Carneiro (Nov 19 2018 at 08:50):

for example you can use it to define a ufd

#### Mario Carneiro (Nov 19 2018 at 08:51):

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

#### 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 $\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 (Nov 19 2018 at 08:56):

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

#### Mario Carneiro (Nov 19 2018 at 08:56):

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

#### Mario Carneiro (Nov 19 2018 at 08:57):

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

#### Mario Carneiro (Nov 19 2018 at 08:57):

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

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

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

#### Mario Carneiro (Nov 19 2018 at 08:59):

I wish dvd was defined on monoids instead of semirings

#### Mario Carneiro (Nov 19 2018 at 09:00):

although you could argue about whether commutative matters

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

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

#### Mario Carneiro (Nov 19 2018 at 09:01):

It's like an archimedean property

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

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

#### Kevin Buzzard (Nov 19 2018 at 09:09):

Maybe it follows from Krull. @Kenny Lau ?

#### Kenny Lau (Nov 19 2018 at 09:10):

how should I know

#### Kevin Buzzard (Nov 19 2018 at 09:12):

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

#### Kevin Buzzard (Nov 19 2018 at 09:12):

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

#### Mario Carneiro (Nov 19 2018 at 09:13):

oh right, ignoring units

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

#### Mario Carneiro (Nov 19 2018 at 14:08):

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

#### Chris Hughes (Nov 19 2018 at 14:08):

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

#### Mario Carneiro (Nov 19 2018 at 14:10):

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

#### Mario Carneiro (Nov 19 2018 at 14:11):

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

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

#### Mario Carneiro (Nov 19 2018 at 14:12):

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

#### Mario Carneiro (Nov 19 2018 at 14:12):

is that a problem?

Sorry yeah.

#### Chris Hughes (Nov 19 2018 at 14:12):

Might be a problem

#### Chris Hughes (Nov 19 2018 at 14:12):

It just means p_adic_val_eq_zero_iff has an extra assumption

#### Mario Carneiro (Nov 19 2018 at 14:13):

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

#### Chris Hughes (Nov 19 2018 at 14:13):

Currently it defaults to zero.

Yes.

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

#### Mario Carneiro (Nov 19 2018 at 14:14):

or a proposition asserting finiteness

#### Mario Carneiro (Nov 19 2018 at 14:15):

perhaps the roption nat version works best here

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

#### Mario Carneiro (Nov 19 2018 at 14:16):

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

#### Chris Hughes (Nov 19 2018 at 14:17):

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

#### Mario Carneiro (Nov 19 2018 at 14:18):

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

#### Mario Carneiro (Nov 19 2018 at 14:18):

because of pfun.fix

#### Mario Carneiro (Nov 19 2018 at 14:20):

maybe nat.rfind is easier to use

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

#### Mario Carneiro (Nov 19 2018 at 14:21):

my point is that here the mathematics and computability aspects coincide

#### Mario Carneiro (Nov 19 2018 at 14:21):

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

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

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

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

#### Mario Carneiro (Nov 21 2018 at 15:00):

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

#### Chris Hughes (Nov 21 2018 at 15:10):

You're right. I'm being stupid.

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

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

#### Johan Commelin (Nov 21 2018 at 18:48):

@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 (Nov 21 2018 at 18:50):

But I think it satisfies your other requirement.

#### Chris Hughes (Nov 21 2018 at 22:34):

Situation like that happening didn't occur to me.

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


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

#### Mario Carneiro (Nov 22 2018 at 07:38):

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

#### Mario Carneiro (Nov 22 2018 at 07:38):

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

#### Mario Carneiro (Nov 22 2018 at 07:39):

how about divisibility?

#### 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 $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 (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⟩


#### Chris Hughes (Nov 22 2018 at 12:35):

I'll probably change the name at some point.

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

#### Mario Carneiro (Nov 23 2018 at 12:19):

maybe specialized to enat?

#### Mario Carneiro (Nov 23 2018 at 12:20):

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

Okay sure.

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