Noether Normalization/Nullstellensatz

Stream: general

[Lennard Henze]

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]

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

[Kevin Buzzard]

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

[Lennard Henze]

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]

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]

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.