Nilpotent/zero divisors in polynomial/power series ring

Stream: Is there code for X?

[Riccardo Brasca]

Am I right in saying that we don't have the description of nilpotent/zero divisors polynomial? We know of course that R[X] is a domain if R is, but I don't find the precise description of the zero divisors. And similarly for power series. If those are really missing I have students who want to work on them, so I hope they're not in mathlib :sweat_smile:

[Junyan Xu]

Yeah those are missing AFAIK; I found these nice notes by Conrad for the polynomial case and this paper for the power series case, which states the simple description when R is Noetherian, and tries to extend the result to more general comm_rings, so a simple description probably doesn't exist in general (I've came across this paper before).
The proof for multivariate polynomials uses induction w.r.t. lexicographic order, and is reminiscent of the second proof of the fundamental theorem of symmetric polynomials in Wikipedia, which was part of my motivation for introducing docs#finsupp.lex.well_founded_lt.

[Riccardo Brasca]

Yes zero divisors for in the power series case are complicated. There is a rather simple example of a ring R and an element r : R such that r+x is a zero divisor.

[Eric Rodriguez]

What's that example Riccardo?

[Riccardo Brasca]

Start with a field K and let S be the polynomial ring with coefficients in K and variables y, z_0, z_1, \ldots (infinitely many z). Let I be the ideal of S generated by (y*z_0, z_0+y*z_1, z_1+y*z_2, z_2+y*z_3, ...). Let R = S/I. and let consider the power series f = y + x.

Letting g = z_0 + z_1*x + z_2*x^2 + ... it's easy to check that f*g = 0.

[Riccardo Brasca]

Please don't formalize this! :stuck_out_tongue:

[Ruben Van de Velde]

Easy to check or easy to formalize? :)

[Riccardo Brasca]

Well it seems easy even to formalize, the only not trivial part is to define the ideal

[Kevin Buzzard]

it's ideal.span (y * z 0) + ideal.span (set.image ...) right? Doesn't look too bad.

[Riccardo Brasca]

Yes, it's not that hard. But I am sure that this is the point where my beginners students will struggle a little bit.

[Kevin Buzzard]

actually using span is really pleasant

[Kevin Buzzard]

If you want to give them practice, roll your own span s as the intersection of all the ideals containing s and then tell them to prove it's a closure operator in the sense of Wikipedia

[Jireh Loreaux]

how about in the sense of mathlib? docs#closure_operator :smile: