Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Etale cohomology #1142

Open
kbuzzard opened this issue Jun 21, 2019 · 2 comments
Open

Etale cohomology #1142

kbuzzard opened this issue Jun 21, 2019 · 2 comments
Labels
feature-request This issue is a feature request, either for mathematics, tactics, or CI long term

Comments

@kbuzzard
Copy link
Member

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.

@kbuzzard
Copy link
Member Author

An overview of what we would need:

  1. Etale morphisms of rings (should be straightforward)
  2. Etale morphisms of schemes (straightforward modulo the fact that schemes have very little API)
  3. Etale sheaves (there will be design decisions here)
  4. 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.

@jcommelin
Copy link
Member

Minor addition: (4) requires sheaves of abelian groups (or modules over some commutative ring), not just sheaves of types.

@bryangingechen bryangingechen added the feature-request This issue is a feature request, either for mathematics, tactics, or CI label Mar 30, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature-request This issue is a feature request, either for mathematics, tactics, or CI long term
Projects
None yet
Development

No branches or pull requests

4 participants