Truncation of (multivariate) power series

Stream: PR reviews

[Antoine Chambert-Loir]

docs#MvPowerSeries.trunc truncates a multivariate power series by keeping exactly those coefficients which are strictly below some monomial. It is rarely (if ever) used in mathlib except in the one variable case, via docs#PowerSeries.trunc.

#20958 adds a variant MvPowerSeries.trunc' of this truncation process by keeping the coefficients which are below some monomial, possibly equal to it. It is genuinely distinct from the previous one, except in the one variable case since f.trunc n.succ = f.trunc' n.
We need that variant for defining linear topologies on multivariate topologies.

The question raised by @Anatole Dedecker is whether the new variant couldn't simply replace the former one. @Filippo A. E. Nuccio, what do you think?

(Of course, a further step could be done, by defining a general truncation API with respect to any subset of σ →₀ ℕ that is “lower-closed”, aka the complement of a filter, but I urge you not to suggest this.)

[Filippo A. E. Nuccio]

Well, the only things that comes to mind is when we want to find representatives in the MvPowerSeries for a basis of a quotient by an ideal. If you're looking at $R[\![X,Y]\!]/X^2\cdot Y$ it seems to me that being able to truncate every mv power series to something which is $<X^2\cdot Y$ instead of $\leq$ could be useful.

[Anatole Dedecker]

Aha, indeed this perspective makes a ton of sense.

[Filippo A. E. Nuccio]

IMHO "getting rid" of trunc is not really needed (whereas adding trunc' is certainly a great plus!)

[Filippo A. E. Nuccio]

Worst case scenario: it will linger unused for a while...

[Antoine Chambert-Loir]

Filippo A. E. Nuccio said:

Well, the only things that comes to mind is when we want to find representatives in the MvPowerSeries for a basis of a quotient by an ideal. If you're looking at $R[\![X,Y]\!]/X^2\cdot Y$ it seems to me that being able to truncate every mv power series to something which is $<X^2\cdot Y$ instead of $\leq$ could be useful.

Not quite, you're abused by the 1-variable case. Remainders are much more complicated in the multivariate case. (For example $X\cdot Y^2$ can't be reduced modulo $X^2\cdot Y$, you're forced to keep this monomial.)

[Filippo A. E. Nuccio]

Oh, good point.