## Stream: general

### Topic: Noether Normalization/Nullstellensatz

#### 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 $R$ is Noetherian then so is $R[X]$. 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