EPSRC TCC algebraic geometry course

Stream: maths

[Kevin Buzzard]

I'm teaching a Lean algebraic geometry course. The repo is here. The course is really following a basic principle which I've always been driven by, which is that when the community is unsure which route to take, just have a go. It's kind of like the anti-Gouëzel principle: Sébastien likes to think hard about the right way to do it, and then do it correctly the first time. We have been thinking about sheaves of modules for ages at Imperial, and during one recent meeting we concluded that there had been about six proposals for formalising the definition of a sheaf of modules for a scheme, and various threads scattered around #maths explaining various pros and cons of the competing definitions, but nobody doing much. So I just chose one randomly and thought I'd have a go. @Jujian Zhang , who knows a lot more about this stuff than I do, and is actually implementing another of the definitions right now, reckons that whatever definition we end up going in mathlib4 for we're probably going to have to do what I'm doing anyway, which seemed as good a reason as any to do it. Lectures aren't live, but anyone at Imperial, Oxford, Warwick, Bristol, Bath or Swansea can attend as long as they register beforehand. Last two lectures on Monday and a week Monday, 4-6, see the TCC web pages for more information. I'm currently trying to figure out pushforwards.

PRs welcome.