(Mv)Polynomial vs (Mv)PowerSeries

Stream: mathlib4

[Antoine Chambert-Loir]

Polynomial R is defined as AddMonoidAlgebra R ℕ while PowerSeries R is defined as MvPowerSeries Unit R.
Isn't there a reasonable reason to make these two definitions parallel, and either defining Polynomial R as MvPolynomial Unit R, or defining PowerSeries R as (Unit →₀ ℕ) → R.
And if yes, which one to choose?

[Eric Wieser]

Antoine Chambert-Loir said:

either defining Polynomial R as MvPolynomial Unit R

I think we used to do this, but it was annoying

, or defining PowerSeries R as (Unit →₀ ℕ) → R.

Wish granted:

import Mathlib.RingTheory.PowerSeries.Basic

variable {R} [CommRing R]
example : PowerSeries R = ((Unit →₀ ℕ) → R) := rfl

[Johan Commelin]

It think it's reasonable to align them. The question is, which definition makes it easiest to set up the API?
And of course aligning them might be a sizable refactor...

[Eric Wieser]

Maybe you meant

or defining PowerSeries R as ℕ → R.

[Yaël Dillies]

Antoine Chambert-Loir said:

Polynomial R is defined as AddMonoidAlgebra R ℕ

Wait, no it's not. It's a one field structure wrapper around it.

[Yaël Dillies]

We really should make AddMonoidAlgebra the one field structure and Polynomial an abbrev.

[Alex J. Best]

Some more general API would really be good for polynomials, so that we dont have to keep reproving things, can we just make coeff an abbreviation for taking the component in the nth graded piece or something? So many arguments would be a lot cleaner if we were allowed to talk about the -1 coefficient of a polynomial but setting up a parallel zcoeff seems really annoying

[Eric Wieser]

Yaël Dillies said:

We really should make AddMonoidAlgebra the one field structure and Polynomial an abbrev.

@Damiano Testa and I were discussing the same thing at LftCM 2023 (and agree with you)

[Antoine Chambert-Loir]

I take this opportunity to make one further remark.
docs#MvPowerSeries makes no assumption on the type of coefficients which is just a type, while docs#AddMonoidAlgebra assumes that it is a semiring. The first choice is better, because it paves the way to having MvPowerSeries M with coefficients in a M : Module R, which would be a module over MvPowerSeries R.
In Bourbaki, Algebra, they play with M[X], with M a module, but it is defined there using tensor product, and this gives rise to useless complications (for us only, for @María Inés de Frutos Fernández and I in particular; of course, they don't let any such identification bother them more than 2 seconds).
My feeling is that would be nice to have this, but I have no idea of how it should be set up.
I don't expect we should have AddMonoidAddMonoid, AddMonoidModule, etc.

[Eric Wieser]

Morally AddMonoidModule is just Finsupp; but I guess it's nice to allow AddMonoidAlgebra to be used in the general case

[Eric Wieser]

Note also we have docs#PolynomialModule already, defined in terms of Finsupp

[Adam Topaz]

Can we introduce IsPowerSeries and IsPolynomial classes (also for mv variants) similar to IsLocalization? We shouldn't care about the actual definition of the types themselves at the end of the day.

[Eric Wieser]

Presumably M[X] would not satisfy IsPolynomial?

[Adam Topaz]

What is M[X]?

[Eric Wieser]

docs#PolynomialModule (admittedly M[X] isn't actually notation)

[Adam Topaz]

Oh so it's ${R}[X] \otimes_R M$?

[Eric Wieser]

I guess that's what was meant by

Antoine Chambert-Loir said:

In Bourbaki, Algebra, they play with M[X], with M a module, but it is defined there using tensor product

[Adam Topaz]

Right. In that case I would suggest we also introduce a IsBaseChange class for modules.

[Eric Wieser]

We already have docs#IsTensorProduct

[Eric Wieser]

But it's not clear to me how IsPolynomial would be useful; what instances do you envisage?

[Adam Topaz]

That's a good start, but thinking of a module as a base-change would include some additional API

[Adam Topaz]

(I have to teach in 5 mins, so I need to run!)

[Eric Wieser]

I think making IsTensorProduct heterobasic would suffice; but maybe an easier approach would be to define IsBaseChange in terms of a module isomorphism with the appropriate tensor product

[Eric Wieser]

Then things like docs#CliffordAlgebra.equivBaseChange would directly populate the instance

[Antoine Chambert-Loir]

I presume that Is(Mv)Polynomial would contain the universal property? What about Is(Mv)PowerSeries?

[Eric Wieser]

Unless we can think of more than one instance for each of these typeclasses, I claim they are pointless

[Antoine Chambert-Loir]

For IsPolynomial, I see two of them, one using Nat, and the other using Unit to Nat.

[Eric Wieser]

Ah, so you'd have IsPolynomial R (MvPolynomial Unit R)?

[Antoine Chambert-Loir]

yes

[Damiano Testa]

This may also simplify working with polynomials in several variables as polynomials in one variable over the rest, using locally the instance inside a proof.

[Eric Wieser]

I'm worried that this would end up more confusing than just applying the isomorphisms we already have (docs#MvPolynomial.pUnitAlgEquiv and docs#MvPolynomial.optionEquivLeft)

[Damiano Testa]

Right now it is possible, but somewhat inconvenient to prove results on MvPolynomials by induction on the number of variables...

[Damiano Testa]

Eric Wieser said:

I'm worried that this would end up more confusing than just applying the isomorphism we already have

That's possible, and I trust your judgement on what is easier to get a computer to understand!

However, I find the current setup a little clunky.

[Damiano Testa]

Is there an isGradedBy typeclass? That might generalise (Mv)Polynomial(Module).

[Damiano Testa]

For the series version, I do not currently see a way around completions.

[Eric Wieser]

Damiano Testa said:

Is there an isGradedBy typeclass? That might generalise (Mv)Polynomial(Module).

docs#DirectSum.Decomposition, but you have to specify what you're decomposing into as subobjects of the original type

[Damiano Testa]

I guess then it is just a matter of trying it out and seeing if using it for (Mv)Polynomials is helpful or not...

[Eric Wieser]

Yaël Dillies said:

We really should make AddMonoidAlgebra the one field structure and Polynomial an abbrev.

I'd be inclined to prioritize this refactor, but maybe others have different opinions

[Junyan Xu]

Eric Wieser said:

Yaël Dillies said:

We really should make AddMonoidAlgebra the one field structure and Polynomial an abbrev.

Damiano Testa and I were discussing the same thing at LftCM 2023 (and agree with you)

I'm about to do something that would make the refactor harder, since the defeq is really convenient:

variable {σ}
/-- The submodule of polynomials that are sum of monomials in the set `s`. -/
def restrictSupport (s : Set (σ →₀ ℕ)) : Submodule R (MvPolynomial σ R) :=
  Finsupp.supported _ _ s

/-- `restrictSupport R s` has a canonical `R`-basis indexed by `s`. -/
def basisRestrictSupport (s : Set (σ →₀ ℕ)) : Basis s R (restrictSupport R s) where
  repr := Finsupp.supportedEquivFinsupp s

The first def is extracted from both docs#MvPolynomial.restrictTotalDegree and restrictDegree. If we make AddMonoidAlgebra a one field structure, this would need to be defined using Submodule.comap with the (algebra or linear) Equiv between AddMonoidAlgebra and MvPolynomial. (comap is definitionally better but we have docs#LinearEquiv.submoduleMap with map. docs#Polynomial.degreeLE and degreeLT are currently defined in a different way, but we already have docs#Polynomial.degreeLTEquiv.)

[Eric Wieser]

We already have to pay this price for polynomial, the refactor being proposed just moves where this toll lies to be finsupp/addmonoidalgebra rather than addmonoidalgebra/polynomial