Schemes

Stream: mathlib4

[Kevin Buzzard]

@Mario Carneiro update from Thursday: I ported some core Lean 3 set stuff and also div_inv_monoid although I'm yet to attach it to group_with_zero (I'll do this this weekend). Are you happy with me pushing to master on my fork of mathlib4 and then making another PR from there?

I would like to formalise the definition of schemes as an experiment in Lean 4. Leo wants people to do small experiments and we have the perfect blueprint, namely the lean 3 definition of a scheme. Because it's only a definition we shouldn't need too many high powered tactics. My proposal was to work from the top down, so there will be sorrys at all times eg we can start with def Scheme := sorry and then work back from there, replacing the sorry with the definition of scheme in lean 3 and then sorrying a bunch more definitions. Would you be happy to have this going on in a non-master branch which you'd be happy to have others pushing to, or would you rather I did this in a fork? I am envisaging undergraduates helping