Does Schwartz-Zippel hold for Integral Domains?

Stream: maths

[Bolton Bailey]

This is blowing my mind right now. I replaced my Field F instance with CommRing F in my Schwartz-Zippel proof just to see what would break, and it came back complaining about IsDomain F. I added that and the proof just ... worked. Does S-Z not require a field as the Wikipedia article, implies?

[Bolton Bailey]

I guess not, the original paper confirms in the intro.

[Flo (Florent Schaffhauser)]

It’s cool that you found out about that by formalizing the result 😊

[Flo (Florent Schaffhauser)]

(to be clear, I had no idea about any of this myself: I just find it interesting that we can advance our own understanding of math by explaining stuff to a computer)

[Bolton Bailey]

I should edit Wikipedia to clarify this.

[Bolton Bailey]

Now I want to go further. Can we weaken to semirings?

[Bolton Bailey]

Does the Finset version of docs#Polynomial.card_roots' hold for CommSemiring?

[Flo (Florent Schaffhauser)]

Hmm, I actually don’t know.

[Flo (Florent Schaffhauser)]

I just find it funny because of the whole discussion we had yesterday and the days before on linearly ordered semirings :smiling_face:️

[Eric Rodriguez]

No, you need domains. x(x-2) has 0,2,4 as roots in z/8z for an example. I think cancellative semirings aren't enough either, but I can't remember

[Kevin Buzzard]

and 6

[Antoine Chambert-Loir]

From a math point of view, the case of a field and the case of a domain are equivalent because you can embed any domain into a field, its field of fractions, and knowing the result there suffices.

[Bolton Bailey]

Eric Rodriguez said:

No, you need domains. x(x-2) has 0,2,4 as roots in z/8z for an example. I think cancellative semirings aren't enough either, but I can't remember

Well yes, but what about comm semirings that are domains, like Nat?

[Eric Rodriguez]

I don't see why it would be true, as there's no euclidean algorithm, which usually means it's false, but I've been shocked before. I tried to make counterexamplea for a bit but it's actually quite hard to make a polynomial that has roots in a strict semiring

[Eric Rodriguez]

(domain isn't the right condition, you need cancellative - no zero divisors does not imply cancellative in semirings)

[Yong Kiam]

jumping in very late here: indeed, we found the same thing out in our formalization of Schwartz-Zippel for the AFP (changed field -> idom in Isabelle and it just worked)

[Antoine Chambert-Loir]

Bolton Bailey said:

reak, and it came back complaining about IsDomain F. I added that and the proof just ... worked. Does S-Z not r

The Schwartz-Zippel theorem says something about the probability that a $n$-tuple $(x_1,\dots,x_n)$ randomly sampled from a set $S$ is a root of a given multivariate polynomial $f \in F[x_1,\dots,x_n]$. Your question is about whether $F$ has to be a field $F$ or whether the assumption can be relaxed to integral domain. Lean told you the latter was enough, because it is the hypothesis needed by the standard proof. Actually, if you happen to know the case for fields and ask about what happens for an integral domain $R$, you can always embed $R$ into its field of fractions $F$. It is plain that the statement for a subset $S$ in $R$ is the same as the statement for $S$ viewed in $F$, hence it holds.

[Yaël Dillies]

FYI, #5297 (the PR proving Schwartz-Zippel) is now ready for review!

[Yaël Dillies]

... and #5297 is ready for review again, hopefully for the last time