Structure presheaf on an affine scheme is a sheaf

[kbuzzard]

What is left:

1. Sheaf axiom for finite cover of Spec(R) by opens of the form D(f).

2. Sheaf axiom for finite cover by opens D(f) implies sheaf axiom for arbitrary cover by opens D(f) [this is because Spec(R) is compact]

3. Sheaf axiom for covers by opens of the form D(f) implies sheaf axiom for arbitrary cover by arbitrary opens

[kbuzzard]

More information about 1: The result we need is tag 00EJ . The proof uses a version of the multinomial theorem, which Chris proved. I also prove span = generate in here (two definitions of "ideal generated by" are equal) -- this should perhaps be moved at some point.

[kbuzzard]

More information about 2: The result we need is tag 009L whose proof should be a lot of fun to do in Lean. Note that a harder theorem is proved in tag 009K but we only need the simpler 009L. The cofinal set is the set of finite covers.

[kbuzzard]

More information about 3: The main result we need is tag 009N although strictly speaking we are going to have to confirm that it's a sheaf of rings, not just a sheaf of sets.

[kbuzzard]

OK so most of this is done now. At the time of writing here is what I think is left.

1. tag00EJ.lean proofs have been broken by the changes in ^ and I don't know if Chris finished the proof. I didn't check to see if Kenny's refactoring of the localisation maps was enough for Chris.

2. is done.

3. I proved that we had a sheaf of sets. Proving it's a sheaf of rings should just be one of those trivial proofs where you go "oh look, this map is a map between rings and it's a ring homomorphism because every proof is rfl". I didn't do it in tag009N.lean because it belongs in another tag.

So now we need to think about the glue.

We need to define the sheaf on a basis, and this involves some nonconstructive maths which I've not yet managed to make a decision on. If we want to define the basis-sheaf on $$D(f)$$ as $$R[1/f]$$ then we need to deal with the fact that $$f$$ is not well-defined -- we can have $$D(f)=D(g)$$ but $$f \not= g$$ and in that case we need to invoke the fact that $$R[1/f]$$ is uniquely (as $$R$$-algebra) isomorphic to $$R[1/g]$$ -- Kenny, is this proved somewhere?

Then to apply the ring lemma (1) we need to say things like "if this a sheaf but if I change one of the spaces of sections to something isomorphic, it's still a sheaf". Mathematicians find this obvious and I am a bit confused about whether this will be easy in Lean.

To apply (2) we now need that any cover of $$D(f)$$ by sets of the form $$D(g)$$ has a finite subcover. The "correct" proof of this is to replace $$D(f)$$ with $$Spec(R[1/f])$$ and to argue that the analogous fact is true for spectrum of a ring.

Then I think it's all over.

I will try to figure out how much of this is non-trivial, later on today.

Any comments @kckennylau @dorhinj ?

[jcommelin]

I am not sure if this idea is useful, but maybe this would help: if U is a basis open, say U = D(f), then we can define S = {f \in R | \forall P \in U : f \notin P}
-- So we take the union T of all prime ideals that make up the open set U and then S = R - T
Then we assign to the open U the ring S^{-1}R. This definition only depends on U, but of course the fact that U is a basis open D(f) still refers to a specific element of R.

Ok, I just realised that this is exactly what Reid Barton also suggested, and what @kbuzzard already recorded in notes.txt.

[kbuzzard]

So this is the approach I'm going to take. The reason it hasn't happened yet is just that recent changes and re-organisation in mathlib (changes to ^ in core lean, gsmul, is_submonoid etc) broke a lot of the code. When it's up and running again we will need some lemmas proving that the ring you describe above is uniquely R-isomorphic to R[1/f] and then everything should be straightforward. The end is in sight!

[kbuzzard]

OK so I've just finished the proof that Spec(R) is compact, and in particular the proof that any cover by opens of the form D(f) has a finite subcover. I am now in a position to start putting things together.

[kbuzzard]

Update: I have spent some time getting the universal properties of localization straight. There are some "obvious in maths" results which we need, such as R[1/f][1/g] = R[1/fg], but I think that these should drop out very quickly now from the universal properties. It is stuff like this which has to be straightened out before we can prove that the structure presheaf on an affine scheme satisfies the sheaf property for finite covers by basic opens, and then general nonsense (all of which I believe is done) extends the sheaf to the whole space.

The comments currently at https://github.com/kbuzzard/lean-stacks-project/blob/master/src/tag01HR.lean give some indication of the state of play.