Schemes

Stream: maths

[Andre Knispel]

I'm interested in playing around with schemes a bit, trying to see how close I can come to working with moduli problems. I heard that there are schemes in the Mathlib, but I couldn't really find anything other than spectra of rings. Where do I need to look?

[Andre Knispel]

Ah, I've discovered lean-scheme, I assume that's where I should go

[Alex J. Best]

@Kevin Buzzard must know!

[Kevin Buzzard]

Schemes are not in mathlib, but they exist in a different repo. They are slowly being ported to mathlib. The issue is that we used a "low-level" definition of a sheaf on a topological space, e.g. a presheaf of types (the analogue of a presheaf of sets in type theory) was literally a function from open sets to types (such that blah), and a sheaf of types was a presheaf of types such that (blah), and a sheaf of rings was a sheaf of types and a ring structure on each type (such that blah). But in mathlib they have already got presheaves and it's defined as a functor from the category of opens to some other category, and whilst this definition sounds more general, it is apparently infinitely more complicated to even say stuff like "this presheaf is a sheaf" or "sheafify this presheaf". So if you want schemes with old-fashioned sheaves of rings on them, then lean-scheme is the place to be, but this repo will slowly bitrot and until I can talk about sheaves in mathlib I'm very limited in what I can do with regards to porting stuff over (I can just about use the category theory library right now but I'm not confident enough to write new definitions such as sheaves).

[Andre Knispel]

I see, so the question is whether to try and improve the situation in Mathlib or build on something that will eventually be replaced... I might be interested in playing around with the presheaves from Mathlib and see if I can do something to improve the situation

[Aaron Anderson]

If you hadn't seen it already, they're discussing new progress on sheaves here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/topos