an alternative formalization

Stream: mathlib4

[Bingyu Xia]

Hi all, I independently formalized that the power series ring over a noetherian ring is noetherian locally, and only afterwards I noticed that it already exists in the latest mathlib. My formalization uses a different approach that follows https://stacks.math.columbia.edu/tag/0306
I wanted to share it here in case anyone finds the approach useful
https://github.com/BryceT233/power-series-ring-is-noetherian-

If this is redundant and not worth upstreaming, that's fine — I mainly thought it might be helpful as an alternative explanation.

[Johan Commelin]

Congratulation! Nice work!

If you think there are some reusable components, then upstreaming those is welcome. I scrolled through your file, and it seems that most of it is private lemmas building up to the main result... So I couldn't identify reusable intermediate results quickly.

[Riccardo Brasca]

Hi! If you are interested in learning a little bit of Lean you can try to add that power series over finitely many variable is a noetherian ring. Beware that this is mostly a "formalization proof", in the sense that the math is trivial, but the formalization is probably a little annoying.

[Kevin Buzzard]

This would be literally immediate if we had the right induction. Do we?

[Bingyu Xia]

Riccardo Brasca 发言道：

Hi! If you are interested in learning a little bit of Lean you can try to add that power series over finitely many variable is a noetherian ring. Beware that this is mostly a "formalization proof", in the sense that the math is trivial, but the formalization is probably a little annoying.

Thanks for the suggestion, yes, this is something I’ve been thinking about as well. I’m aware that the mathematical content is fairly straightforward and that most of the work would be on the formalization side, but it still seems like a good exercise to understand the existing APIs better. I may give it a try when I have some time.

Kevin Buzzard 发言道：

This would be literally immediate if we had the right induction. Do we?

Good question — I’m actually not sure whether there is a cleaner induction / recursion principle available here. In my own formalizations I usually end up first proving an existence lemma and then defining things via recursion based on that, which works but is admittedly a bit cumbersome. If there is a more direct inductive setup that I’m missing, I’d be very interested to learn about it.

[Junyan Xu]

add that power series over finitely many variable is a noetherian ring.

Seems we're missing the analogue of MvPolynomial.optionEquivLeft for MvPowerSeries. Once we have that the proof should be similar to (half of) this mathlib3 PR (the other half deducing the infinite case from the finite case doesn't work here).

[Riccardo Brasca]

Yes, it's not trivial but it should be doable.

[Kevin Buzzard]

I'm saying that it should be trivial i.e. one line, because we should have some general lemma which can just be
applied. Unfortunately I ran into two issues when trying to make one (independent of the missing def Junyan has highlighted):

import Mathlib

universe u

theorem MvPowerSeries.semiring_finite_induction
    (P : (R : Type u) → Semiring R → Prop)
    (h : ∀ (R : Type u) {_ : Semiring R},
      P R inferInstance → P (PowerSeries R) inferInstance) :
    ∀ (ι : Type u) [Finite ι] (R : Type u) [Semiring R],
      P (MvPowerSeries ι R) inferInstance := by
  sorry

theorem MvPowerSeries.ring_finite_induction
    (P : (R : Type u) → Ring R → Prop)
    (h : ∀ (R : Type u) {_ : Ring R},
      P R inferInstance → P (PowerSeries R) inferInstance) :
    ∀ (ι : Type u) [Finite ι] (R : Type u) [Ring R],
      P (MvPowerSeries ι R) inferInstance := by
  sorry

theorem MvPowerSeries.commRing_finite_induction
    (P : (R : Type u) → CommRing R → Prop)
    (h : ∀ (R : Type u) {_ : CommRing R},
      P R inferInstance → P (PowerSeries R) inferInstance) :
    ∀ (ι : Type u) [Finite ι] (R : Type u) [CommRing R],
      P (MvPowerSeries ι R) inferInstance := by
  sorry

The first is that we seem to need one principle per typeclass. The second is that the index type is forced to be in Type u, the same type as the ring, unless we make a second one with an index type in Type which should also work, which would mean 6 theorems in all :-/

[Aaron Liu]

it's finite so it shouldn't matter

[Aaron Liu]

why does it have to be the same universe as the ring

[Aaron Liu]

oh I see now

[Aaron Liu]

then you should just state it for when the ring is Type (max u v) and the index is Type v

[Aaron Liu]

that should work right

[Aaron Liu]

and it specializes to both of the cases

[Aaron Liu]

so that takes care of the universe issue

[Kevin Buzzard]

Aaron Liu said:

that should work right

I love your optimism :-) I fear that this is a recipe for big weird slowdowns and obscure universe unification errors. Also I'm not convinced that it solves the problem: I want to be able to prove that if (R : Type u) and P R -> P (PowerSeries R) then P R -> P (MvPowerSeries \sigma R) for (\sigma : Type v) and I don't think your suggestion will do this but this is the natural statement.

[Riccardo Brasca]

I mean that we are missing the isomorphism, after that it is of course a one liner.
In my opinion we should not rush to the result about option, we should make sure we have all the results in Mathlib.Algebra.MvPolynomial.Equiv, including the case of infinitely many variables (when it holds of course).

[Aaron Liu]

Kevin Buzzard said:

I want to be able to prove that if (R : Type u) and P R -> P (PowerSeries R) then P R -> P (MvPowerSeries \sigma R) for (\sigma : Type v) and I don't think your suggestion will do this but this is the natural statement.

That doesn't typecheck so I'm not worried about it

[Kevin Buzzard]

But IsNoetherianRing R -> IsNoetherianRing (MvPowerSeries \sigma R) typechecks!

[Aaron Liu]

That's because you have two different Ps

[Aaron Liu]

IsNoetherianRing.{u} and IsNoetherianRing.{max u v}

[Aaron Liu]

if you want to make an induction principle with them then you have to add in the hypothesis that said they're related

[Kevin Buzzard]

Youch. So here's the concrete question:

import Mathlib

-- assume this
theorem PowerSeries.isNoetherianRing' (R : Type*) [CommRing R] (hR : IsNoetherianRing R) :
    IsNoetherianRing (PowerSeries R) := sorry

-- Is there now a general induction principle which can be applied to prove this:

universe u v

theorem MvPowerSeries.isNoetherianRing (R : Type u) [CommRing R] (hR : IsNoetherianRing R)
  (σ : Type v) : IsNoetherianRing (MvPowerSeries σ R) := sorry

[Kevin Buzzard]

And the relation is probably just this, right?

-- assume this too
theorem IsNoetherianRing.equiv (R : Type u) (S : Type v) [CommRing R] [CommRing S] (e : R ≃+* S) :
    IsNoetherianRing R ↔ IsNoetherianRing S := sorry

[Aaron Liu]

yeah that would suffice

[Kevin Buzzard]

You say that and I believe you mathematically but what's the general induction principle which can be made to apply?

[Aaron Liu]

I'll think about it

[Aaron Liu]

right now it still feels like you're gonna have one per typeclass :(

[Violeta Hernández]

Can we not sidestep the universe issue by using IsNoetherianRing R ↔ IsNoetherianRing (ULift R)?

[Aaron Liu]

Then your induction principle only works for IsNoetherianRing

[Aaron Liu]

and we still need a way of going from PowerSeries (PowerSeries (...)) to MvPowerSeries

[Aaron Liu]

so you'll need some sort of transfer across equiv anyway

[Kevin Buzzard]

Yeah that's the missing MvPowerSeries.optionEquivLeft which Junyan highlighted

[Kevin Buzzard]

and then you use the appropriate induction hypothesis for finite types which IIRC we do have.

[Aaron Liu]

I mean we need the hypothesis that the P respects equivalence

[Aaron Liu]

even without the universe issue

[Christian Merten]

You can look at docs#Module.pi_induction for a similar case. The trick is having two motives and relating them by an equiv relation.

[Bingyu Xia]

I just finished a first draft of formalization of the finitely many variable case, which is noetherian_mv.lean in
https://github.com/BryceT233/power-series-ring-is-noetherian-
I will add more documentation, keep revising everything and finish the empty case soon.

I also noticed the corresponding, more general setup in MvPolynomial/Equiv.lean; compared to that, the argument here is limited and does not reach the same level of generality.

[Riccardo Brasca]

Nice work! On the other hand I think that for mathlib we should really follow what we did for MvPolynomial. Did you try that? It is of course a longer route, but it should be doable.

[Bingyu Xia]

Riccardo Brasca 发言道：

Nice work! On the other hand I think that for mathlib we should really follow what we did for MvPolynomial. Did you try that? It is of course a longer route, but it should be doable.

There might be some chance to generalize my Fin n case argument to option case, I will try!

[Bingyu Xia]

Indeed, the arguments in Fin n case generalizes to option case with no difficulty. I updated the first draft of the generalized arguments in a new file optionEquivLeft.lean. A minor issue is that I used subtraction, which will not work for semirings.

[Bingyu Xia]

I improved the argument and it no longer uses subtraction! maybe I should open a PR for this?