lemma for noether normalization

Stream: maths

[Lennard Henze]

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

[Reid Barton]

∃ 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]

I'm actually pretty confused by the original statement

[Kenny Lau]

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

[Reid Barton]

Other than zero. That was my first thought too

[Kenny Lau]

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]

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.

[Kenny Lau]

yeah

[Reid Barton]

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

[Kenny Lau]

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

[Reid Barton]

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]

which my API readily provides :P

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Lennard Henze]

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]

∃ 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]

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]

@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]

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

[Kevin Buzzard]

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]

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

[Kenny Lau]

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

[Reid Barton]

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

[Reid Barton]

The condition is long enough I worry I am missing something

[Reid Barton]

(Polynomial over K, of course)

[Kenny Lau]

I think it is

[Lennard Henze]

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?