State of etale cohomology

Stream: Is there code for X?

[Felix Sefzig]

My name is Felix and I'm a PhD Student at the University of Zurich . I've been interested in formal proof verification for some time now and since I currently have some free time, I am planning to (or at least try to) formalise some results in etale cohomology. I'm reaching out because I was hoping you could point me in the right direction regarding what is already formalised and where to start.

[Kevin Buzzard]

I think one interesting question is whether we are already at the state where we can give some mathematically correct but completely impractical definition of etale cohomology ("derive this functor on this site"), at least for torsion coefficients (unless we want to go proetale from day 1, which is also a question worth talking about). What is the most useful definition if one wants to e.g. compute cohomology of a curve?

[Kevin Buzzard]

Definitions are a very delicate part of formalization. Currently one proposal for the definition of elliptic curve over a scheme is "base can be covered by affines over which the curve is Proj(y^2z+a1xyz+...+a6z^3=0)", which is mathematically correct and will make representability theorems (modular curves) much easier, and also avoids having to prove Riemann-Roch! Ultimately the definition "doesn't matter" because you prove all definitions give the same answer, but when making basic API (i.e. on the journey to prove the equivalence) the definition matters a lot.

[Christian Merten]

Hello! Good to see more people interested in this topic! This has been asked multiple times before on this Zulip. One thread is here, with a demo on what is currently possible: #homology > Étale cohomology @ 💬. The short answer is: yes we have all the definitions to write down a group that is the étale cohomology of an étale sheaf.

A nice next step would be to write down any (interesting) short exact sequence of étale sheafs. The blocker for this is that we don't have any étale sheafs yet. A few possible sources of étale sheafs:

• fpqc is subcanonical: this is done if you piece together things from the proetale repository and work by @Yong-Gyu Choi. This is on the PR queue, but things just take time to get in.
• quasi coherent sheafs induce étale sheafs: This is very far from done, because we still have no good API for quasi-coherent sheafs (details in the thread I linked to above). This will eventually need faithfully flat descent, of which a reasonable chunk is in #24434.
• locally constant sheafs: this needs sheafification on the small étale site, which is in #19462.

For the proétale site of things, @Jiang Jiedong and I are working on proétale cohomology at the moment (https://github.com/chrisflav/proetale). We are working (literally right now) on expanding the blueprint quite a bit, so there are many easy commutative algebra tasks I could point you to if you are interested in that.

[Christian Merten]

Generally, we are still missing many important ingredients on étale morphisms. Some that come to my mind right now are:

• étale is locally standard étale (we have étale is locally standard smooth of rel. dim 0)
• flat + unramified implies étale (this should go via "smooth = flat + smooth on fibres")
• smooth over a field implies regular
• (strictly) Henselian rings, Henselisation

If you are interested in any of these, please let me know. There is material on all of these topics spread over the review queue, blocked PRs, the Pi1 repository and the proetale repository, so I can give more detailed instructions if you tell me what you are interested in.

I can also suggest something more "sheafy" if you are more interested in that.

[Felix Sefzig]

Dear Christian,
thanks for the quick reply, sounds really exciting! I would definitely be interested in working on a sheafy project, and then work out the commutative algebra as needed. What did you have in mind?

[Christian Merten]

If you are willing to assume for now that the étale site is subcanonical (as I said above, this should be available in mathlib in the not-so distant future), you could do Kummer theory, i.e., define the Kummer sequence and show it is an exact sequence of étale sheafs if $n$ is invertible.
I believe this would be quite doable and fun.

Some other doable and sheafy topics that come to my mind are:

• Show the small étale site of a scheme has enough points: You could start by defining étale neighbourhoods and the stalk functor associated to a geometric point of the base scheme. Then you would have to show that an étale sheaf is zero if and only if all stalks are zero.
• Show the category of abelian sheafs on the classifying site of a pro-finite group $G$ is equivalent to discrete $G$-modules. This would eventually lead to showing a comparison between Galois cohomology and étale cohomology.