polynomials over R-modules

Stream: general

[Bolton Bailey]

I was trying to formalize a slide from a presentation and I came to the concept of "A (multivariable) polynomial over an R-module". Mathlib says that mv_polynomials are defined over rings. I guess you could define a polynomial over an R-module and evaluate it for values of R, though you just wouldn't be able to multiply such polynomials. Would it be reasonable to change the definition of mv_polynomial to allow this?

[Johan Commelin]

Yeah, I guess that's certainly possible.

[Adam Topaz]

You can also take polynomials over the tensor algebra of your module.

[Eric Wieser]

This is referring to polynomials that evaluate as u + x • v + x^2 • w + ...?

[Junyan Xu]

try using the tensor product of the mv_polynomial over the ring with the module?

[Antoine Chambert-Loir]

Adam Topaz said:

You can also take polynomials over the tensor algebra of your module.

But that would force you to view the “polynomial module” inside a big polynomial ring (the grade 1 part under the natural graduation), which is not really convenient.

[Antoine Chambert-Loir]

Junyan Xu said:

try using the tensor product of the mv_polynomial over the ring with the module?

As a module, this is exactly that, but it has a tensor product which hides its “free” nature
(\sigma \to_0 \nat) \to_0 M.

[Kevin Buzzard]

docs4#MvPolynomial

[Kevin Buzzard]

Oh we really do demand CommSemiring. One could imagine weakening this to AddCommMonoid initially, and then either going down the ring route or the module route.

[Eric Wieser]

I'm struggling to imagine that, because there wouldn't be any multiplication and so you just have finsupp

[Eric Wieser]

I guess the point is that there's no finsupp.eval

[Antoine Chambert-Loir]

You would have a multiplication from MvPolynomial of anything that has an action on your module.

[Eric Wieser]

Can you write the type of that out in pseudocode?

[Kevin Buzzard]

If M is an R-module then M[[X]] is an R[[X]]-module and M[[sigma]] is an R[[sigma]] module

[Eric Wieser]

Set M = R[X] and now you have that R[X][X] is an R[X] module in two incompatible ways...

[Kevin Buzzard]

Yes. That's a maths fact

[Kevin Buzzard]

That would be exactly why we wouldn't call both variables X

[Antoine Chambert-Loir]

I thought Bourbaki would have defined that, but they didn't go that far, except for a definition of M[X] (Algebra, chapter 4) using tensor product. I used that in Lean, when I formalized coefficients of a “polynomial map” between two modules, but that's awkward.