## Stream: maths

### Topic: lemma for noether normalization

#### Lennard Henze (Oct 28 2019 at 14:20):

I want to formalize the following lemma for noether normalization:

My idea was like this:

lemma lemma22 (t : finset A) :
∀ a : A,
∃ s : finset A,
∃ m : module (adjoin k (finset.to_set s)) ((adjoin k (finset.to_set t)),
a ∈ s ∧ t.card = s.card ∧ module.is_of_finite_type m


So the lemma is invoked with the generating set and the finite monomorphism property is translated to the equivalent formulation for modules. Does it make sense to define it this way?
Also I am still missing, that the morphism is the canonical one sending y_1 to x_1 .... y to x_n

#### Reid Barton (Oct 28 2019 at 14:41):

∃ m : module ... ... means "there exists a ...-module structure on .... I don't think that's what you want to say. Maybe that is what you mean by your last sentence.

#### Reid Barton (Oct 28 2019 at 14:44):

I'm actually pretty confused by the original statement

#### Kenny Lau (Oct 28 2019 at 14:46):

my first thought is that the expression is redundant (i.e. every element of K[x1 ... xn] is of that form)

#### Reid Barton (Oct 28 2019 at 14:47):

Other than zero. That was my first thought too

#### Kenny Lau (Oct 28 2019 at 14:47):

and I think the lemma means that for any y in K[x1 ... xn] there are y1 ... y_(n-1) in K[x1 ... xn] such that K[x1 ... xn] is module-finite over the subring K[y1 ... y_(n-1) y]

#### Reid Barton (Oct 28 2019 at 14:47):

I think $K[x_1, \dots, x_n]$ doesn't mean the polynomial ring, just some $K$-algebra generated by $x_1$, ..., $x_n$.
Like how people will write $K[x, 1/x]$, etc.

yeah

#### Reid Barton (Oct 28 2019 at 14:48):

And then is $K[y_1, \dots, y_{n-1}, y]$ the analogous thing?

#### Kenny Lau (Oct 28 2019 at 14:48):

the K-algebra generated by y1 ... yn-1 y

#### Reid Barton (Oct 28 2019 at 14:57):

So in this setup we have one subalgebra contained in another one and we need the module structure of the second over the first

#### Kenny Lau (Oct 28 2019 at 14:57):

which my API readily provides :P

#### Kevin Buzzard (Oct 28 2019 at 15:14):

$\mathbb{N}^0$ is non-empty, so contrary to the claim it doesn't seem to me to implicitly imply $n\geq1$.

#### Kevin Buzzard (Oct 28 2019 at 15:19):

Looking at the proof (this is from Bosch) Reid is right, it's the $K$-algebra generated by some bunch of elements, and Kenny is right, it's the subalgebra. The proof will be quite interesting to do in Lean, but will be tough for a beginner (that's not a bad thing, it just means that @Lennard Henze will learn a lot :D )

#### Reid Barton (Oct 28 2019 at 15:24):

Will it matter for practical implementation purposes whether K[x1, ..., xn] is a K-algebra which is generated by some elements, or the K-subalgebra of some other algebra generated by those elements? (Do we need to do Gonthier-style "commutative subalgebra"?)

#### Johan Commelin (Oct 28 2019 at 16:40):

I think it would make sense to introduce an is_free predicate on (sub)algebras. Polynomial algebras satisfy this predicate. For any algebra satisfying this predicate, one can choose an algebra isom with a polynomial algebra.

#### Johan Commelin (Oct 28 2019 at 16:40):

I haven't thought through the details of the api needed in this case

#### Johan Commelin (Oct 28 2019 at 16:40):

But somehow, it feels like it would be useful to have a characteristic predicate for polynomials

#### Johan Commelin (Oct 28 2019 at 16:40):

Maybe it shouldn't be a Prop. Maybe it should save data about the generators

#### Johan Commelin (Oct 28 2019 at 16:41):

If so... we'll probably have to move 80% of (mv_)polynomial to this new data-carrying "predicate"

#### Lennard Henze (Oct 30 2019 at 10:43):

my first thought is that the expression is redundant (i.e. every element of K[x1 ... xn] is of that form)

I think he is just giving this explicit form, bc he references the coefficients in the proof. Thats why I wanted to get rid of the explicit form in the formulation of the statement and just use it in the proof ( although I have no idea how I can get these coefficients for arbitrary elements of a k-algebra in lean)

#### Lennard Henze (Oct 30 2019 at 10:47):

∃ m : module ... ... means "there exists a ...-module structure on .... I don't think that's what you want to say. Maybe that is what you mean by your last sentence.

no i actually want to say: "there exists a module structure, that has certain properties ..." ie being of finite type (finitely generated) and being the module corresponding to the homomoprhism that sends y1 to x1 ... y to xn.

#### Reid Barton (Oct 30 2019 at 14:01):

Rather than "there exists a module structure such that ... and is the module structure corresponding to ..." it's presumably better to say "the module structure corresponding to ... has property ..."

#### Kevin Buzzard (Oct 30 2019 at 15:02):

@Kenny Lau you're really good at this stuff. Can you just review Lennard's set-up so he can get on with the proofs? Newcomers can find level-setting hard if they're working at high level.

#### Kevin Buzzard (Oct 30 2019 at 15:03):

https://github.com/Forsetes/mathlib/blob/hilberts_nullstellensatz/src/ring_theory/noether_normalization.lean

#### Kevin Buzzard (Oct 30 2019 at 15:04):

You're much better than me. I still don't know whether X should extend Y or just have Y in as an axiom. I need someone to write a basic "mathematicians' guide to making definitions" for me.

#### Kenny Lau (Oct 30 2019 at 15:43):

that "nonempty index set" seems non-trivial to state

#### Kenny Lau (Oct 30 2019 at 15:43):

it isn't equivalent to saying that $y \ne 0$

#### Reid Barton (Oct 30 2019 at 15:45):

is it "y = P(x_1, ..., x_n) for some nonzero polynomial P"?

#### Reid Barton (Oct 30 2019 at 15:46):

The condition is long enough I worry I am missing something

#### Reid Barton (Oct 30 2019 at 15:46):

(Polynomial over K, of course)

I think it is

#### Lennard Henze (Oct 30 2019 at 18:57):

y = P(x_1,...,x_n) for some nonzero polynomial P looks good to me, but is there an api to use this?
Also in the proof of noether normalization I want to use this to say: If my x_1,...,x_n generating the algebra are not algebraically independent, than I can use the above lemma for y=0 to get new elements y_1,...,y_{n-1}. And than do this over and over until I arrive at alge. independent elements. What would be a good api for lemma2, to make this possible to achieve?

Last updated: May 12 2021 at 08:14 UTC