MvPowerSeries.rename

Stream: mathlib4

[Bingyu Xia]

Hi everyone, I am working on formalizing the proof that the ring of formal power series in finitely many variables over a Noetherian ring is itself Noetherian. To achieve this, the plan involves constructing MvPowerSeries.optionEquivLeft to support induction on the number of variables. However, while drafting the proof and referring to the polynomial library, I realized that I first need to implement MvPowerSeries.rename, analogous to what exists in MvPolynomial/rename.lean.

I have implemented a preliminary version of MvPowerSeries.rename, which is rename.lean in
https://github.com/BryceT233/power-series-ring-is-noetherian-

As this is my first time contribution to Mathlib, any advice or guidance would be greatly appreciated! thanks!

[Kim Morrison]

It's much easier to review as PR.

[Bingyu Xia]

this is PR #33188

[Kim Morrison]

Per the CI output, please run lake exe mk_all

[Antoine Chambert-Loir]

That's a legitimate proof but it will be superseded by a general result on graded rings.

[Riccardo Brasca]

@Antoine Chambert-Loir do you mean the rename operation? This seems pretty specific to power series (and polynomials of course).

[Antoine Chambert-Loir]

No, I meant the noetherian property of rings of multivariate power series.

[Bingyu Xia]

Thanks for the pointer, that makes sense.

My primary focus now is actually building rename and optionEquivLeft, which is missing for MvPowerSeries.

[Kevin Buzzard]

But power series rings are not graded, right?

[Antoine Chambert-Loir]

I should have written “filtered”. This is a general fact that a filtered ring is noetherian (with exhautive and separated filtration) if and only if its associated graded ring is.

[Bingyu Xia]

Just a quick update: I have completed a first draft of MvPowerSeries/Equiv.lean, modeled after MvPolynomial/Equiv.lean. It includes pUnitAlgEquiv, isEmptyAlgEquiv, mapEquiv, sumToIterAlgEquiv, commAlgEquiv and optionEquivLeft.

Since this file depends on Rename.lean, I plan to submit a PR for it once the Rename.lean PR has passed review. Thanks!

[Bingyu Xia]

update PR #33188: rearrange some of the results and refactored many old proofs

[Bingyu Xia]

update PR #33188: Based on the review feedback and PR #23499, I refactored the file and generalized the maps in the definition of rename from embeddings to maps with finite fibers

[Bingyu Xia]

just a quick bump on this: I noticed that another contributor recently opened a PR #35435 which implements a special case of rename, so it seems there is active interest/need for this result. To avoid duplicated effort or conflicting definitions, it might be good to move forward with this PR so the other user can build upon it (or use it directly). Thanks!