Zulip Chat Archive

Stream: general

Topic: Noether Normalization/Nullstellensatz


view this post on Zulip Lennard Henze (Aug 21 2019 at 09:44):

I want to start working on Noether Normalization and Hilberts Nullstellensatz as part of my bachelor thesis. Is anyone else currently working on that?

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 09:58):

Not as far as I know. I would happily actively help you with this.

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 10:00):

We have noetherian rings and we might well have the theorem that if RR is Noetherian then so is R[X]R[X]. I would recommend that you used bundled morphisms.

view this post on Zulip Lennard Henze (Aug 21 2019 at 10:17):

Since I am new to lean some help would be gladly appreciated :)
I will have a look into bundled morphisms. Any reason you prefer that, or a proof you would recommend?

view this post on Zulip Alex J. Best (Aug 21 2019 at 10:59):

There is some discussion at https://leanprover-community.github.io/archive/116395maths/71000TerenceTaosproofofHilbertsNullstellensatz.html about one proof.
And we do have hilbert basis as kevin says, https://github.com/leanprover-community/mathlib/blob/3e77fec25f69f759ab91b752445b01b467149c72/src/ring_theory/polynomial.lean#L226

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 11:57):

I'd definitely not recommend Tao's proof! It's very long and I am not sure that constructiveness buys you anything that anyone wants. Reading the article it seems that he thought he'd found a short cute argument but then there was a problem and he didn't want to delete the post, so it ended up being a long non-cute argument. I would suggest formalising a high-powered argument because high-powered commutative algebra should be fine to do in Lean and we would like to see more of it.


Last updated: May 11 2021 at 00:31 UTC