You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
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.
The text was updated successfully, but these errors were encountered:
Etale morphisms of rings (should be straightforward)
Etale morphisms of schemes (straightforward modulo the fact that schemes have very little API)
Etale sheaves (there will be design decisions here)
enough homological algebra to do some cohomology (there will be design decisions here).
The design decisions in (3) will be trying to work out a way of doing sheaves which is sufficiently general to work in the etale site. The design decisions in (4) will depend on how cohomology is defined. There are concrete ways involving cocycles and very abstract ways involving derived functors.
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.
The text was updated successfully, but these errors were encountered: