ImperialCollegeLondon / M4P33

M4 algebraic geometry course in Lean
Apache License 2.0
58 stars 5 forks source link

Nullstellensatz roadmap #4

Open kbuzzard opened 4 years ago

kbuzzard commented 4 years ago

High-level idea:

1) Prove Zariski's Lemma following McCabe, Amer. Math Monthly, Vol 83 No 7 (1976), p560-561 2) Prove weak NSS in the usual way from Zariski's Lemma 3) Prove NSS using Rabinowitsch's trick (see e.g. Miles Reid's book).

kbuzzard commented 4 years ago

Zariski's Lemma: if k is a field (surely integral domain? Ed) and R=k[x_1,x_2,...,x_n] is an integral domain finitely generated as a k-algebra, which happens to be a field, then R/k is algebraic. Note that k[x_1,x_2,...,x_n] just means "the ring generated by k and the x_i", it's not necessarily a polynomial ring (it is a quotient of a polynomial ring).

[actually an integral domain won't do -- if k is the p-adic integers then R can be the p-adic numbers with x_1=1/p.]

kbuzzard commented 4 years ago

McCabe's proof: 1) re-arrange the x_i such that the map from the abstract poly ring k[X_1,X_2,...,X_t] -> R sending X_i to x_i is injective, and each x_j for j>t is algebraic over k(X_1,X_2,...,X_t). See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Algebraic.20geometry.20course/near/186047827

kbuzzard commented 4 years ago

Now set S=k[x_1,x_2,...,x_t], so S is a polynomial ring and each for each i>t, x_i satisfies an algebraic equation over the field of fractions of S. Hence there's some non-zero y in S such that each yx_i is integral over S; hence each x_i is integral over S[1/y], the abstract localisation (regarded as a subring of the field R).

kbuzzard commented 4 years ago

Hence R is integral over S[1/y], and because R is a field, S[1/y] must also be a field! This is Prop 5.7 in Atiyah--Macdonald.

kbuzzard commented 4 years ago

Now this looks fishy. Say the result is false and so t>0. Let m be a max ideal of S; then because S isn't s a field, m has a non-zero element f. In the field S[1/y], f is invertible and it's not hard to deduce from this that some power of y is in m, and hence y is in m. Hence y is in every maximal ideal of S.

kbuzzard commented 4 years ago

This means that 1+y is in no maximal ideal of S and is hence a unit. But the units of S are just k^*, so y is in k, and it's non-zero, so S[1/y]=S and S is a field, formally a contradiction.

kbuzzard commented 4 years ago

Here's a proof of prop 5.7 of AM: if R is a field and A is a subring such that R is integral over A, then A is also a field. It suffices to prove that if x,y are elements of R with xy=1 and x in A, then y must also be in A. For certainly y is in R, and thus satisfies some monic polynomial with coefficients in A, of degree n say; now multiply by x^{n-1} and re-arrange to see that y is a sum of elements of A.