Polynomial and PolynomialModule

Stream: mathlib4

[Luna]

Why are Polynomial and PolynomialModule two different definitions?

In mathlib, they are respectively defined like:

structure Polynomial (R : Type*) [Semiring R] where ofFinsupp ::
  toFinsupp : AddMonoidAlgebra R ℕ

def PolynomialModule (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] := ℕ →₀ M

If you unfold AddMonoidAlgebra R ℕ it is just ℕ →₀ R. These two definition look like they contain the same type of data but with different instances. Should these definitions be merged? And would a PR be welcomed?

For context of why this came up, I'm working on Chapter 10 of MIL and want to show:

import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Eigenspace.Minpoly
import Mathlib.LinearAlgebra.Charpoly.Basic

open Polynomial Module LinearMap End

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) :
    ker (aeval φ P) ⊔ ker (aeval φ Q) = ker (aeval φ (P*Q)) := by sorry

Ideally I'd like to show that these are equivalent using the theorem Polynomial.roots_mul (i.e. the kernel of these expressions occur when the image of φ equals the roots of the polynomial when evaluated on the elements of the module; so showing the kernels are equal is equivalent to showing the roots of $P*Q$ are equal to the roots $P$ unioned with the roots of $Q$). But the regular Polynomial K definition cannot be evaluated on the elements of a module.

[Eric Wieser]

There's some ongoing work refactoring AddMonoidAlgebra by @Yaël Dillies , which I think aims to replace the first one with Polynomial := AddMonoidAlgebra R ℕ (which is also what it used to be defined as!)

[Yaël Dillies]

Indeed. The current blocker is #29207, where I would like some help to debug an obscure error

[Yaël Dillies]

Update here: Progress is steady, but the current refactor (#25273, making MonoidAlgebra a one-field structure) has got a long way to go, and the refactor you actually want (making Polynomial an abbrev for AddMonoidAlgebra) must wait on that.

[Junyan Xu]

What happens if you make Polynomial an abbrev without making AddMonoidAlgebra a one-field structure?

[Scott Carnahan]

To answer one of the original questions, Polynomial and PolynomialModule should not be merged - If R acts on M, we don't want an instance of Polynomial R acting on Polynomial M, because we would get two inequivalent actions when M = Polynomial R. We use the type synonym PolynomialModule M to get around that problem. The docstring on PolynomialModule gives some more details about the possible actions.