Zulip Chat Archive

Stream: maths

Topic: sheaves on a site


Johan Commelin (Nov 18 2020 at 07:48):

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 (Nov 18 2020 at 07:48):

/me tips his :top_hat:

Kevin Buzzard (Nov 18 2020 at 08:06):

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 (Nov 18 2020 at 14:29):

Thanks to you both for the helpful and speedy reviews!


Last updated: Dec 20 2023 at 11:08 UTC