MvPolynomial module

Stream: mathlib4

[Brendan Seamas Murphy]

There's a type PolynomialModule R M, defined as a type synonym for finitely supported functions instead of a newtype like Polynomial M. I'm not sure why we have separate versions of this but I guess it makes inference better? Anyways, is there a multivariate version of this? If there isn't I would like to add it, and I think I need a better understanding of why there's two types here in the first place

[Johan Commelin]

cc @Eric Wieser I think you've thought about design (issues) of this part of the library a lot...

[Scott Carnahan]

If M = R[X] you get two non-defeq actions of R[X] on Polynomial M. This is briefly explained in docs#PolynomialModule .

[Brendan Seamas Murphy]

Ah sure this makes sense. But it still seems strange to use a type synonym for finsupp instead of the existing type of polynomials, imo

[Brendan Seamas Murphy]

I would assume this causes some code duplication

[Eric Wieser]

Polynomial M isn't legal when M isn't a ring

[Brendan Seamas Murphy]

I mean, that also seems a little questionable? Eg for ordinal notation you might want to talk about polynomials with ordinal coefficients, which don't form a ring

[Brendan Seamas Murphy]

For right now I'm just going to define MvPolynomialModule mimicking PolynomialModule as closely as possible

[Eric Wieser]

I think the mental model is that Polynomial is Finsupp with pointwise * replaced by convolutional *, and if you don't have a ring then you don't have that *.

[Antoine Chambert-Loir]

No but you have a convolution from the sale Finsupp of anything that acts on M.

[Eric Wieser]

The problem is that SMul only works for SMul X Y -> SMul X (F Y), but what you're asking for needs SMul X Y -> Smul (F X) (F Y), and you can't have both without diamonds

[Brendan Seamas Murphy]

I created a PR #13573 to add MvPolynomialModule

[Johan Commelin]

@Scott Carnahan did you also have something like :up: , or was it @Antoine Chambert-Loir ?

[Scott Carnahan]

I contributed docs#HahnModule given as a type alias for HahnSeries (with a lot of help from Eric). Instead of convolutional *, we have convolutional SMul.

[Antoine Chambert-Loir]

What #13573 does is not the analogue of docs#HahnModule, nor the type of finsupp function from index type Ito a given module M (which would be a Module (MvPolynomial I A) under Module A M, but the structure of module over a docs#MvPolynomial ring that a module possesses when the variables are mapped to elements of the ring that acts on the module.

[Brendan Seamas Murphy]

Should it have a more descriptive name? I didn't think there would be any confusion over the module structure. To me this is what $M[x_1, \ldots, x_n]$ means

[Antoine Chambert-Loir]

I don't want to be prescriptive, but the ambiguity with the existing docs#HahnModule or docs#PolynomialModule would suggest finding another name.
In your case, I know that there is a similar definition for polynomial in one indeterminate (but I can't find it, surely @Oliver Nash will tell us which one it is), and their names and API should be aligned.

By the way, docs#MvPolynomial is an instance of docs#MonoidAlgebra and I believe that everything that is done for #MvPolynomial should be inherited from similar constructions at the level of docs#MonoidAlgebra.

[Brendan Seamas Murphy]

The similar definition in one indeterminate is docs#PolynomialModule, no? I mean I wrote the file largely by copy and pasting from PolynomialModule and then changing as appropriate

[Brendan Seamas Murphy]

As is we can't use MonoidAlgebra because it has a typeclass parameter [Semiring k]. I'm not sure how much we can inherit from this in principle (even if we change the parameter) vs inheriting from Finsupp, because of the instance clashing nevermind, you were talking about MvPolynomial not MvPolynomialModule