the "augmentation ideal" of a multivariable polynomial ring

Stream: Is there code for X?

[Kevin Buzzard]

If $R$ is a commutative ring and $S$ is a type, then the multivariable polynomial ring $R[S]:=$ mv_polynomial S R of polynomials in variables indexed by $S$ has an ideal generated by all the variables. This ideal is the kernel of the ring homomorphism sending a multivariable polynomial to its constant coefficient, and the latter morphism is a surjective ring morphism from $R[S]$ to $R$. Do we have this ideal, and a name for this ideal? This came up as a possible route to removing this sorry.

[Adam Topaz]

We do have docs#mv_polynomial.eval so you could evaluate at zero and take a kernel.

[Kevin Buzzard]

Yeah. I put a couple of sorries up on branch xena-augmentation and I'll see if I can get an undergrad to fill them in :-)

[Eric Wieser]

I would expect to have a coeff_zero_ring_hom that's defeq to coeff 0 as well

[Andrew Yang]

There is docs#mv_polynomial.constant_coeff.