Cech Cohomology

Stream: Is there code for X?

[Nicolas Alexander Weiss]

Is there anyone working on Cech cohomology so far? Or though about this?

We were thinking of starting on sites first and constructing the Cech complex for sheaves of abelian groups there.

Is this a good level of generality? (or construct H^0, H^1 in the non-abelian case ...)

[Patrick Massot]

@Oliver Nash

[Ruben Van de Velde]

Junyan Xu said:

Jujian did some Cech cohomology last year so he surely also knows how to deal with open covers :)

[Adam Topaz]

We have all the building blocks for this

[Matthew Ballard]

I thought you Zuliped a definition once upon a time

[Adam Topaz]

We have the Cech nerve as a simplicial thing, whiskering for such objects, and the alternating face complex

[Adam Topaz]

What we don’t have is a convenient way to take a colimit over all covers, but that should be quite easy

[Adam Topaz]

I did give some thought about this, but I have to run now so I’ll plan to write more later

[Oliver Nash]

I note we have things like docs#CategoryTheory.SimplicialObject.cechNerve

[Oliver Nash]

And docs#AlgebraicTopology.alternatingFaceMapComplex

[Adam Topaz]

Here is the theorem from the stacks project which I think we should aim for: https://stacks.math.columbia.edu/tag/01H0
See in particular the top comment by Kestutis Cesnavicius.

[Adam Topaz]

Here $H_{HC}$ is hypercover cohomology, which is like Cech cohomology except involves arbitrary hypercovers as opposed to Cech hypercovers. I think once the above is proved, we could then write down the conditions that are required for the canonical map from Cech cohomology to hypercover cohomology to be an isomorphism.

[Nicolas Alexander Weiss]

@Adam Topaz thanks a lot!

[Joël Riou]

I think that an interesting result we should be able to prove soon is that if X is a sheaf of sets on a site S such that the map from X to the final object is epi, then for any abelian group A, there is a quasi-isomorphism A[Cech(X)] ⟶ A in the category of sheaves of A-modules on S.

[Joël Riou]

When we have the derived category in mathlib, this is basically what is needed in order to define a map from the Cech-cohomology on a given covering to the cohomology defined as morphisms in the derived category. I would think it is more important to develop a good API for Cech-cohomology on a fixed cover rather than attempting to take the colimit.

[Joël Riou]

(Here is a sketch of proof of the fact above: arguing locally on S, we may assume that there is a section of the map X ⟶ (final object), and then Cech(X) has an extradegeneracy, which implies that the map A[Cech(X)] ⟶ A is a homotopy equivalence.

[Joël Riou]

Note : In the particular case of the classifying topos of a group, this principle was already applied to group cohomology: Representation.GroupCohomology.Resolution by @Amelia Livingston