sheaves on a site

Stream: maths

[Johan Commelin]

I've just kicked #4608 on the merge queue. Major kudos to @Bhavik Mehta
You might know that at Lean Together 2019, I gave a talk titled "Sheaves in Lean". I gave a report on how I was trying to do the stuff that Bhavik has now accomplished. The talk was nice, but the project failed miserably. I am really happy that the problem was me, and not the sheaves!

[Johan Commelin]

/me tips his :top_hat:

[Kevin Buzzard]

This was a really nice PR. There is still work to do though. We still cannot state the first exercise in chapter 2 of Hartshorne because it involves sheafification of a presheaf of abelian groups. But we're getting there.

[Bhavik Mehta]

Thanks to you both for the helpful and speedy reviews!