formalisation of Hilbert basis theorem for power series ring

Stream: new members

[Chen Ling]

Hi, I tried proving Hilbert basis theorem for power series ring.
The statement is as follows :

import Mathlib

theorem PowerSeries.isNoetherianRing' {R : Type*} [Ring R] [inst : IsNoetherianRing R] : IsNoetherianRing (PowerSeries R) := sorry

The ring R can be non-commutative here.

And if we work in a commutative ring, use the theorem IsLocalization.IsNoetherianRing, as a direct corollary of the above, we have Hilbert Basis theorem for Laurent series ring.

It might be like this :

example {R : Type*} [CommRing R] [inst : IsNoetherianRing R] :
  IsNoetherianRing (LaurentSeries R) := by
  have h1 := @LaurentSeries.of_powerSeries_localization R
  have h2 : IsNoetherianRing (PowerSeries R) := PowerSeries.isNoetherianRing'
  apply IsLocalization.isNoetherianRing (Submonoid.powers PowerSeries.X)
    (LaurentSeries R) h2

The whole proof is available at
https://github.com/chenlingccll/a-lean4-formalisation-of-Hilbert-basis-theorem-for-power-series-ring/blob/main/hilbert_basis.lean

It's a lean4 code file, and you may paste it to local VSCode or lean4 web or somewhere. It complies under this month's mathlib with lean toolchain v4.22.0-rc2, I guess it also works for earlier version.

I'd like to add the result to Mathlib, seems like we do not have Hilbert basis theorem for power series ring? The proof I post is more than 1000 lines, and I'll try to refine the codes before making pull request to mathlib.

Anyway, I want to add some lemmas to PowerSeries.Order and PowerSeries.Trunc file first. I have not contributed to Mathlib before, and do not know how to do it. Make the codes obey naming conventions of Mathlib, make a pull request, and start a topic here?

[Michael Rothgang]

Thanks for your contribution; it's great to grow mathlib together. It seems mathlib already knows that power series are Noetherian in some special case (see docs#PowerSeries.isNoetherianRing) --- but it assumes a field. So, it would be great to compare your approach with the existing mathlib proof and get the stronger version in.
@Filippo A. E. Nuccio @María Inés de Frutos Fernández you wrote the current mathlib version. Would you like to chime in; does your proof also work more generally than for fields?

[Ruben Van de Velde]

And yes, it's a good idea to submit some of the more general lemmas first - maybe no more than 50 lines for your first pr. Ideally we'd get to it anyway, but feel free to post the pr number here to get eyes on it sooner (the maintainers are quite overloaded)

[Kenny Lau]

I feel like there has to be a higher proof of this? More precisely:

1. Assume R is Noetherian.
2. Then R[X] is Noetherian (Polynomial.isNoetherianRing).
3. Then R[[X]] is Noetherian (Stacks 05GH) because it is the completion of R[X] under the ideal (X).

[Kenny Lau]

maybe it's the same amount of work to prove Stacks 05GH than to prove directly that R[[X]] is Noetherian, but I feel like 05GH is the right generalisation that one should prove instead.

[Chen Ling]

I guess to say two power series p,q have same first n terms, is equivalent to say they mod ideal formed by X^n are same. Maybe we can try to get a more general proof. Thanks for the reference.

[Riccardo Brasca]

Concerning the commutative case, I have some students with a proof of this (to be precise of a more precise version of this), see here

[Riccardo Brasca]

cc @Anthony Fernandes maybe it works also for semirings? I don't remember

[Anthony Fernandes]

Unfortunately no, we tried to rework the proof a few times but we can't get around without subtracting.

[Riccardo Brasca]

Anyway what we have (the fact that it is enough to consider prime ideals) it is surely worth to have in mathlib.

[Anthony Fernandes]

Riccardo Brasca said:

Anyway what we have (the fact that it is enough to consider prime ideals) it is surely worth to have in mathlib.

And our proof of this fact may be valid for a CommSemiring, I'll check when I get to my computer.

Edit: it isn't

[Chen Ling]

Riccardo Brasca 发言道：

Concerning the commutative case, I have some students with a proof of this (to be precise of a more precise version of this), see here

Elegant proof and formalization, looks great!