Zulip Chat Archive

Stream: maths

Topic: lemma for noether normalization


view this post on Zulip Lennard Henze (Oct 28 2019 at 14:20):

I want to formalize the following lemma for noether normalization:

lemma2.png

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 28 2019 at 14:44):

I'm actually pretty confused by the original statement

view this post on Zulip 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)

view this post on Zulip Reid Barton (Oct 28 2019 at 14:47):

Other than zero. That was my first thought too

view this post on Zulip 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]

view this post on Zulip Reid Barton (Oct 28 2019 at 14:47):

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

view this post on Zulip Kenny Lau (Oct 28 2019 at 14:48):

yeah

view this post on Zulip Reid Barton (Oct 28 2019 at 14:48):

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

view this post on Zulip Kenny Lau (Oct 28 2019 at 14:48):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 28 2019 at 14:57):

which my API readily provides :P

view this post on Zulip Kevin Buzzard (Oct 28 2019 at 15:14):

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

view this post on Zulip Kevin Buzzard (Oct 28 2019 at 15:19):

Looking at the proof (this is from Bosch) Reid is right, it's the KK-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 )

view this post on Zulip 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"?)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 28 2019 at 16:40):

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

view this post on Zulip Johan Commelin (Oct 28 2019 at 16:40):

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

view this post on Zulip Johan Commelin (Oct 28 2019 at 16:40):

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

view this post on Zulip 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"

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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 ..."

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 15:03):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Oct 30 2019 at 15:43):

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

view this post on Zulip Kenny Lau (Oct 30 2019 at 15:43):

it isn't equivalent to saying that y0y \ne 0

view this post on Zulip Reid Barton (Oct 30 2019 at 15:45):

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

view this post on Zulip Reid Barton (Oct 30 2019 at 15:46):

The condition is long enough I worry I am missing something

view this post on Zulip Reid Barton (Oct 30 2019 at 15:46):

(Polynomial over K, of course)

view this post on Zulip Kenny Lau (Oct 30 2019 at 15:46):

I think it is

view this post on Zulip 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