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)