mathlib

mathlib copied to clipboard

Schemes are ticking along nicely, as is commutative algebra. Currently we still don't have schemes in mathlib, or etale maps of rings, but it is not hard to imagine them being there at some point in the future. Once they're there, it's easy to imagine trying some cohomology theories. This will also need some homological algebra so it's a fair way into the future, but I thought it would be good to isolate it as a long term goal. I am not specifically working on it right now because there is still plenty of work to be done with both schemes and perfectoid spaces and I think I would be foolish to take on another project, but etale cohomology will raise universe issues and there might be foundational problems to solve. I guess the basic examples in Deligne's SGA 4.5, i.e. basic computations of etale cohomology groups e.g. cohomology of curves, would be something to aim for.