Roadmap for sheaf cohomology

Stream: homology

[Adam Topaz]

@Kevin Buzzard suggested elsewhere that it would be worthwhile to have a roadmap for sheaf cohomology, and I agree, so I’ll get it started here. Others should feel free to weigh in!

As I see it, there are two main steps, each being fairly large:

1. Show that categories of sheaves we are interested in have enough injectives in a suitable level of generality to cover not just sheaf cohomology in the usual sense, but also (pro)étale cohomology, flat cohomology, etc. This could be done, for example, with Grothendieck abelian categories using the proof in his Tohoku paper.
2. Prove the equivalence with (hypercover) Cech cohomology as in https://stacks.math.columbia.edu/tag/01H0
   In general there is a map from the usual Cech cohomology to hypercover-Cech-cohomology to sheaf cohomology. The proof should at some point construct these maps. Even better: there is the so-called “Cech-to-derived” spectral sequence (I think this is also done in Tohoku?).

[Riccardo Brasca]

Is anyone thinking about spectral sequences? I remember @Amelia Livingston was interested in that

[Joël Riou]

Riccardo Brasca said:

Is anyone thinking about spectral sequences? I remember Amelia Livingston was interested in that

I have completely formalised the mechanism of spectral sequences! But these are thousands of lines of code. It is going to be very long to make this enter mathlib, and it is not my top priority. For many applications, we just do not really need spectral sequences...

[Adam Topaz]

Concerning this, another (better?) approach is to show that the colimit of the hypercover complexes computes $R\Gamma$ in the derived category. I didn’t mention it because I couldn’t find a good reference right now (but check out the comments on the stacks project link I mentioned above).

[Adam Topaz]

However I do hope we will be able to do concrete calculations using spectral sequences at some point. (For example the 5-term exact sequence for cohomology groups in low degree has been quite useful in my research)

[Notification Bot]

A message was moved here from #homology > Derived categories in mathlib by Adam Topaz.

[Joël Riou]

As I have already expressed this view, the simplicial homotopy theory in mathlib is not mature enough yet to consider general hypercovers seriously. Hypercovers are like morphisms of presheaves of simplicial sets (or simplicial presheaves) which are locally trivial fibrations for a Grothendieck topology, but we barely understand what is a trivial fibration of simplicial sets (for example, can we show that it induces a quasi-isomorphism in singular cohomology?).

[Joël Riou]

1. My suggestion is to first use Ext groups (see draft PRs #13883, #13879, #13963, this shall soon be in mathlib). From this, we may get Mayer-Vietoris exact sequences, etc.

[Joël Riou]

2. When we know that at least some categories of sheaves have enough injectives (this is Adam's 1.), we may introduce the derived functor approach D^+(abelian sheaves) ⥤ D^+(CommGrp). The notion of abstract derived functor is already in mathlib #12788. With the formalism of derivability structures from Bruno Kahn/Georges Maltsiniotis that I am implementing, the main remaining step is to show that bounded above complexes have resolutions by complexes of injective objects. I have introduced definitions in #12624, and will have to PR the rest of it. (I have already shown that these Functor.mapDerivedCategoryPlus compose well, and obtained the associated Grothendieck spectral sequence.)

[Joël Riou]

3. (Mostly independant of 2). Develop Cech cohomology on a given covering. Show that it maps to the actual cohomology (either from 1. or 2.). This is based on a simplicial object (the "Cech nerve"), which would fit in the general setting of hypercovers, but there is a special trick which allows to circumvent the strong technical issues with general hypercovers, which is the notion of extra-degeneracy that I introduced in mathlib. This can be used to show that the after "abelianization" the Cech nerve gives a resolution of the constant sheaf (this method was already used successfully by @Amelia Livingston in the context of group cohomology). A student of Patrick @yannis monbru in Orsay is currently making some progress on this part.

[Joël Riou]

4. In the context of topological spaces, pass though the colimit over open coverings to get a map from the Cech cohomology to the actual cohomology. Then get the technical lemma by Henri Cartan (Théorème II.5.9.2 in Godement's book, in French) which says that the morphisms from the Cech cohomology to the actual cohomology is an isomorphism under certain circumstances. Then, deduce the vanishing of the cohomology of quasi-coherent sheaves on affine schemes. The proof in Godement's book uses a spectral sequence (probably the one Adam is referring to), but a careful analysis of filtrations on the single complex of a double complex may be enough.

[Joël Riou]

(deleted)

[Adam Topaz]

I agree that the hypercover approach would require that we further develop the homotopy theory of simplicial sets. But the nice thing about mathlib is that work can be distributed, and there are already a few people in the community interested in simplicial methods. My opinion is that the hypercover approach is the “right” abstraction, which is why I suggested it (of course, this is just an opinion). Further developing simplicial homotopy theory and the theory of hypercovers would be useful elsewhere as well (e.g. I’m interested in étale homotopy).

[Adam Topaz]

Maybe @Jack McKoen would be interested in working on the statement that a trivial fibration induces a quasi-iso?

[Joël Riou]

I agree that eventually we would like to have the hypercovering theorem for the computation of cohomology, but strong foundations in simplicial homotopy theory are a prerequisite (see for example the proofs of SGA 4 V 7.2.1/7.3.2 which use a fair share of simplicial homotopy/homology theory).

[Ravi Vakil]

Joël Riou said:

As I have already expressed this view, the simplicial homotopy theory in mathlib is not mature enough yet to consider general hypercovers seriously. Hypercovers are like morphisms of presheaves of simplicial sets (or simplicial presheaves) which are locally trivial fibrations for a Grothendieck topology, but we barely understand what is a trivial fibration of simplicial sets (for example, can we show that it induces a quasi-isomorphism in singular cohomology?).

This sounds good to me. And this programme that Joel proposes is not one that needs to be followed in linear order, as he notes (and indeed he is moving forward on several of these fronts at once).

[Adam Topaz]

I wanted to check how many things we are missing from pinning down a definition of the Cech complex (and thus Cech cohomology), and this is what I came up with:

import Mathlib

open AlgebraicGeometry CategoryTheory Limits

universe u
variable {A : Type*} [Category A] {X : Scheme.{u}}

instance : HasFiniteLimits (Scheme.OpenCover.{u} X) := sorry

structure OpenOver (X : Scheme) where
  dom : Scheme
  f : dom ⟶ X
  isOpen : IsOpenImmersion f := by infer_instance

instance (f : OpenOver X) : IsOpenImmersion f.f := f.isOpen

instance : Category (OpenOver X) :=
  InducedCategory.category fun f => Over.mk f.f

def OpenOver.toOpens (X : Scheme) : OpenOver X ⥤ TopologicalSpace.Opens X where
  obj f := f.f.opensRange
  map e := LE.le.hom <| sorry

def TopCat.Presheaf.openImmersionFunctor (F : TopCat.Presheaf A X) :
    (OpenOver X)ᵒᵖ ⥤ A :=
  (OpenOver.toOpens X).op ⋙ F

def AlgebraicGeometry.Scheme.OpenCover.toOpenOver (U : Scheme.OpenCover.{u} X) (j : U.J) :
    OpenOver X where
  f := U.map j

def Scheme.OpenCover.mapToOpenOver {U V : Scheme.OpenCover.{u} X} (e : U ⟶ V) (j : U.J) :
    U.toOpenOver j ⟶ V.toOpenOver (e.idx j) where
  left := e.app _
  right := 𝟙 _
  w := e.w _

noncomputable
def Scheme.OpenCover.inducedFunctor [HasProducts A] (F : TopCat.Presheaf A X) :
    (Scheme.OpenCover.{u} X)ᵒᵖ ⥤ A where
  obj U := piObj fun j : U.unop.J => F.obj <| .op <|
    (OpenOver.toOpens X).obj <| U.unop.toOpenOver j
  map := fun {U V} f => Pi.lift fun j =>
    Pi.π _ (f.unop.idx j) ≫ F.map (Quiver.Hom.op <| (OpenOver.toOpens X).map <|
      Scheme.OpenCover.mapToOpenOver f.unop _)
  map_id := sorry
  map_comp := sorry

noncomputable
def Scheme.OpenCover.cechComplex [HasProducts A] [Preadditive A]
    (U : Scheme.OpenCover.{u} X) (F : TopCat.Presheaf A X) : CochainComplex A ℕ :=
  let e : U ⟶ ⊤_ _ := terminal.from U
  let e := Arrow.mk e
  let e := e.cechNerve
  let e : CosimplicialObject _ := e.rightOp ⋙ Scheme.OpenCover.inducedFunctor F
  (AlgebraicTopology.alternatingCofaceMapComplex _).obj e

For some reason, I'm still not completely happy with this definition. I would much rather be able to take $U_j$ an open cover of $X$, consider the map $\coprod_j U_j \to X$, take the Cech nerve of that, take global sections, and take the associated complex. But it seems that for such an approach we will need the pullback functors that some people were working on at the AIM-AG workshop last week. How far are we from having such pullbacks?

[Joël Riou]

My suggestion would be to introduce a category FormalCoproduct C (which for certain universes could be identified to the full subcategory of presheaves of sets which identify to coproducts of representable presheaves). My definition of the Cech complex would then be https://github.com/leanprover-community/mathlib4/compare/master...cech-experiment
(This API would be immediately usable when it becomes reasonable to study general hypercovers.)

[Adam Topaz]

yes, I agree. BTW I think FormalCoproduct C should rather be called Indexed C (and possibly should even be defined for plain types independently of category theory)

[Adam Topaz]

Unfortunately Indexed C is a little "evil"... ext for its Homs would involve HEq or eqToHoms

[Adam Topaz]

The stacks project calls this the category of "Semi-representable" objects BTW. I'm not a huge fan of that name.

[Adam Topaz]

I remember when constructing the Cech Nerve that I thought about using products in Over X as opposed to wide pullbacks, and realized that it was painful (I don't remember exactly why though). It may be worthwhile to make a definition for families of arrows over a fixed base X as well, say IndexedOver X (or some other name). This has a terminal object which is the singleton 1 : X -> X, and if X : C and C has finite wide-pullbacks over X, then IndexedOver X has finite wide-pullbacks over the terminal object. You could then use the preexisting cechNerve instead of the variant cechSimplicial.

[Sophie Morel]

Joël Riou said:

4. In the context of topological spaces, pass though the colimit over open coverings to get a map from the Cech cohomology to the actual cohomology. Then get the technical lemma by Henri Cartan (Théorème II.5.9.2 in Godement's book, in French) which says that the morphisms from the Cech cohomology to the actual cohomology is an isomorphism under certain circumstances. Then, deduce the vanishing of the cohomology of quasi-coherent sheaves on affine schemes. The proof in Godement's book uses a spectral sequence (probably the one Adam is referring to), but a careful analysis of filtrations on the single complex of a double complex may be enough.

I am not saying that things in this list are not useful and should not be done, but proving the vanishing of the cohomology of quasi-coherent sheaves on affine schemes is much easier and does not require Cech cohomology (or spectral sequences for that matter), if you know that the functor $M \mapsto \widetilde{M}$ is an equivalence from $A$-modules to quasi-coherent sheaves on $Spec(A)$. As far as I remember, you only need to know that flabby sheaves have trivial cohomology.

[Sophie Morel]

But maybe you meant a more general version of the result?

[Joël Riou]

As far as I know, to make this argument work, we also need to know that if M is an injective module, then $\widetilde{M}$ is flasque, which may be true only in the Noetherian case (this is the proof in Hartshorne's book).

[Sophie Morel]

I was thinking of the proof in this paper of Kempf (in section 1, proposition 1 and theorem 2). I don't think that you need to know that $\widetilde{M}$ is flasque for $M$ injective. Also, @Antoine Chambert-Loir mentioned to me that the proof is unnecessarily complicated at one point but I forgot the details, so it's probably better to ask him.

[Antoine Chambert-Loir]

Indeed, the first lemma of that paper can be replaced by the simpler fact that cohomology classes (of degree alas 1) vanish locally.

[Sophie Morel]

Then you would also have to modify the proof of Theorem 2 of the paper, I think? I'm sorry, I'm probably missing something but I don't see how to do that.

[Joël Riou]

It seems to me that the proof of theorem 2 would not need much change. Then, for the variant of proposition 1 that Antoine suggests, it seems we do not even need to know anything about flasque sheaves. If $I^\bullet$ is an injective resolution of an abelian sheaf F, then a cohomology class of F shall be the class of a cocycle of the complex $I^{n-1}(X) \to I^n(X) \to I^{n+1}(X)$. By the exactness of $I^\bullet$, locally this cocycle has to be a coboundary.

[Sophie Morel]

I don't have a problem with the fact that cohomology classes are locally zero, but I don't understand how to relate $H^i(X,{}_V F)$ and $H^i(V,F)$, and it seems that you need that to prove theorem 2.

[Sophie Morel]

(Notation as in Kempf's paper: $V$ is an open subset of $X$, and if we call $j$ the inclusion of $V$ in $X$, then ${}_VF$ is by definition $j_*j^*F$.)

[Sophie Morel]

The proof of theorem 2 is that you take a cohomology class $\alpha$ in $H^n(X,F)$ (here $X$ is an affine scheme, $F$ is quasi-coherent sheaf on $X$, and $n>0$) and you want to embed $F$ into a quasi-coherent sheaf $G$ on $X$ such that the image of $\alpha$ in $H^n(X,G)$ is $0$. Kempf takes $G$ to be equal to a direct sum ${}_{V_i}F$ for $(V_i)$ a finite open cover of $X$ by small enough basic open subschemes. How, from the local triviality of $\alpha$, do you deduce that you can choose $(V_i)$ such that the image of $\alpha$ in each $H^n(X,{}_{V_i}F)$ is zero? It is not true for a general sheaf $F$ that $H^n(X,{}_{V_i}F)=H^n(V_i,F)$, so it cannot be an abstract nonsense argument. Am I missing something?

[Sophie Morel]

(Of course the isomorphism $H^n(X,{}_{V}F)=H^n(V,F)$ holds for $F$ quasi-coherent and $V$ affine, but that is usually deduced from the vanishing of the cohomology of quasi-coherent sheaves on affine schemes.)

[Joël Riou]

Thanks! Yes, I was confused with the notatoins. The proof of proposition 1 is more subtle than I initially thought.

[Antoine Chambert-Loir]

I had written down the proof for my course in algebraic geometry. There are certainly mistakes that remain but that may be useful. See §6.1, page 267 of my notes on
Algebraic Geometry of Schemes

[Joël Riou]

I am afraid that the issue Sophie pointed out seems to apply to the statement "the cohomology group $H^n(X,F_x)$ identifies with $H^n(U_x,F_x)$" in your text :-(

[Antoine Chambert-Loir]

(In some sense, that's reassuring that Kempf has not missed an easy proof.)

[Sophie Morel]

I have also taught this proof in an algebraic geometry course, and I remember finding it more subtle than it looked at first.

[Sophie Morel]

But it does allow one to prove that the cohomology of quasi-coherent sheaves on affine schemes vanishes with minimal information about cohomology. If I remember well, what you need is the fact that $H^0$ identifies to global sections, the existence of the long exact sequence, and the fact that cohomology of flasque sheaves vanish. That last fact can be replaced with the fact that the restriction to an open subset of an injective abelian sheaf stays injective, which follows from the existence of an exact left adjoint of $j^*$ (i.e. $j_!$).

[Sophie Morel]

You do need to know some stuff about the $\widetilde{M}$, for example you have to be able to calculate the restriction of $$\wildetilde{M}$$ to an affine open subscheme $U$ of $X$ (it's $\widetilde{M\otimes_{O(X)}O(U)}$). Actually you only need the case where $U$ is basic, but the fact is true for any affine $U$.

[Antoine Chambert-Loir]

Sophie Morel said:

I have also taught this proof in an algebraic geometry course, and I remember finding it more subtle than it looked at first.

Lemma 1 is a bit intricate, indeed, and I was happy to avoid it… Alas…

[Sophie Morel]

Once you have proved that cohomology of quasi-coherent sheaves on affine schemes vanishes, it is possible to deduce the isomorphism between the cohomology of a quasi-coherent sheaf (on a quasi-compact separated scheme) and its Cech cohomology for a finite affine open cover, by showing that the Cech complex of the quasi-coherent sheaf is an acyclic resolution of it. This is Theorem 13 in the same paper of Kempf. Here we take the non-alternating Cech complex, but where you choose an ordering on the opens in the cover and you don't repeat indices, so it is finite. You can also use the cohomology of this complex as a "cheap" definition of Cech cohomology in that case, and use this to do calculations like the cohomology of line bundles on projective space. I also did that in an algebraic geometry class, though the calculations were exercises!

[Joël Riou]

I have just PRed the definition of the sheaf cohomology of abelian sheaves on categories equipped with a Grothendieck topoplogy #14800.

[Riccardo Brasca]

Do we know that sheaves have enough injectives? Or did you avoid that?

[Joël Riou]

Riccardo Brasca said:

Do we know that sheaves have enough injectives? Or did you avoid that?

The Ext groups are defined using the derived category, which does not require the existence of enough injectives.
(The existence of enough injectives (for sheaves of modules over a topological space) was formalised during the AIM workshop using skyscraper sheaves.)

[Joël Riou]

Using the long exact sequences of Ext, I have just formalized the Mayer-Vietoris long exact sequences in sheaf cohomology #15099. For this, I have formalized certain types of "Mayer-Vietoris squares" so that it applies not only to the case of topological spaces (see https://github.com/leanprover-community/mathlib4/pull/15099/files#diff-28ed9f5f546a4424154cd41eed47f1bf7e4300ada781f26de22c6abf2d65ad3eR55-R69), but also to "Nisnevich distinguished squares" when more algebraic geometry is formalized.

[Riccardo Brasca]

Magnifique travail !