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?
Kevin Buzzard (Aug 21 2019 at 09:58):
Not as far as I know. I would happily actively help you with this.
Kevin Buzzard (Aug 21 2019 at 10:00):
We have noetherian rings and we might well have the theorem that if is Noetherian then so is . I would recommend that you used bundled morphisms.
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?
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
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