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 !

[Kenny Lau]

@Joël Riou Thanks for pointing me here. This discussion was 1 year ago. Has there been any new developments? Where can I start and contribute?

[Johan Commelin]

cc @Raphael Douglas Giles

[Kenny Lau]

I'm not very familiar with sites, are they supposed to have a terminal object representing the "whole space"?

[Adam Topaz]

@Kenny Lau no, they dont, but you can still have a "global sections" functor by taking the appropriate limit. See #maths > global sections functor

[Kenny Lau]

Also, I'm now stuck on another point: if I have a cover (corresponding to an element of J X), how do I view it as one morphism?

[Adam Topaz]

wme?

[Kenny Lau]

i.e. I think if {U_i -> X}_i is a cover then I need one object U := coproduct of U_i so that I can view that cover as one morphism U -> X?

[Adam Topaz]

Are you using a Grothendieck topology or something else?

[Adam Topaz]

E.g. a pretopology or a coverage...

[Kenny Lau]

Adam Topaz said:

wme?

import Mathlib

universe w' w v u

namespace CategoryTheory

open Abelian

namespace Sheaf

variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}

def Cech.complex (F : Sheaf J AddCommGrp.{v}) (X : C) (𝒰 : J X) : CochainComplex AddCommGrp ℕ :=
  (AlgebraicTopology.alternatingCofaceMapComplex _).obj <|
    Functor.rightOp (Arrow.cechNerve _) ⋙ -- I need one arrow here
      F.val -- this is wrong too

end Sheaf

end CategoryTheory

[Kenny Lau]

a Grothendieck topology

[Kenny Lau]

I'm not very well versed in Category Theory, so some parts are just my guess

[Kenny Lau]

to be more specific, I've never been explicitly told to convert a covering into one arrow

[Adam Topaz]

I think you want to take the colimit of the functor associated to the sieve U, that should be the analogue of the "union of the objects in the cover", and use the universal property of the colimit to obtain a morphism to X.

[Adam Topaz]

I don't remember whether we have a developed API for this... @Dagur Asgeirsson or @Joël Riou might know.

[Kenny Lau]

@Adam Topaz That sounds like Sieve.sup?

CategoryTheory.Sieve.sup.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (𝒮 : Set (Sieve X)) : Sieve X

The supremum of a collection of sieves: the union of them all.

but also, I also need to extend the sheaf F as a functor in a larger category...

[Adam Topaz]

import Mathlib

universe w' w v u

namespace CategoryTheory

open Limits

open Abelian


variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}

noncomputable
def Presieve.asMorphism (X : C) (S : Presieve X) [HasColimit S.diagram]: colimit S.diagram ⟶ X :=
  colimit.desc S.diagram ⟨_, fun f => f.obj.hom, by aesop_cat⟩

namespace Sheaf

noncomputable
def Cech.complex (F : Sheaf J AddCommGrp.{v}) (X : C) (𝒰 : J X)
    [HasColimit 𝒰.val.arrows.diagram]
    [HasWidePullbacks C] :
    CochainComplex AddCommGrp ℕ :=
  (AlgebraicTopology.alternatingCofaceMapComplex _).obj <|
    Functor.rightOp (Arrow.cechNerve <| 𝒰.val.arrows.asMorphism) ⋙ -- I need one arrow here
      F.val -- this is wrong too

end Sheaf

end CategoryTheory

[Kenny Lau]

@Adam Topaz do you think maybe we're missing some ingredients to make everything work smoothly?

[Adam Topaz]

Isnt’t that always true? ;)

[Kenny Lau]

@Adam Topaz ok, but do you happen to know how this is done in the literature? Specifically, if I just have a topological space X and a cover {Ui -> X}_i, how do I convert this into one morphism, so that I can then do the Cech nerve construction?

[Adam Topaz]

If you have such a cover, you just take the coproduct of the U_i. The issue is that given such a cover, {U_i}_i, the sieve associated to it is the collection of all morphisms Y -> X which factor through one of the U_i. The sheaf library has been set up primarily around Grothendieck topologies which are collections of sieves satisfying some properties, but we also have two other constructions, pretopologies and coverages, which let you construct a Grothendieck topology and prove the sheaf condition associated to that Grothendieck topology in a more direct way.

[Adam Topaz]

See Presieve.ofArrows and Sieve.generate

[Adam Topaz]

The closest we have to what's done in the literature is going via a pretopology or a coverage, depending on whether your category happens to have pullbacks or not.

[Adam Topaz]

(Here "literature" means "the stacks project")

[Kenny Lau]

@Adam Topaz the issue is that the "coproduct" goes outside of the category. Going back to my example of open subsets of a topological space, the coproduct is just union. You need to first extend the notion to "open immersion from a different topological space", and that already causes problems, because sheaves are usually defined only on open subsets of a space.

[Kenny Lau]

The thing I worry is that this "extending the functor" construction has not been done

[Adam Topaz]

No, the coproduct is the disjoint union in the category of topological spaces.

[Kenny Lau]

you're using a different category here. note that i started with the category of "open subsets of a topological space"

[Adam Topaz]

Okay, I see the issue now. You want to work in Opens X for some topological space X, right?

[Kenny Lau]

Yes.

[Kenny Lau]

The extension of the functor should just be global section of pullback sheaf

[Adam Topaz]

So I would take a look at https://github.com/leanprover-community/mathlib4/blob/f0f62b727da0394080ccfad6a667cfc0ee62488e/Mathlib/CategoryTheory/Sites/Spaces.lean#L43-L54

[Kenny Lau]

@Adam Topaz That's very well, but I still don't think we've extended the sheaf yet... If you look at the definition of a sheaf:

https://github.com/leanprover-community/mathlib4/blob/f0f62b727da0394080ccfad6a667cfc0ee62488e/Mathlib/CategoryTheory/Sites/Sheaf.lean#L297-L302

variable {C : Type u₁} [Category.{v₁} C]
variable (J : GrothendieckTopology C)
variable (A : Type u₂) [Category.{v₂} A]

/-- The category of sheaves taking values in `A` on a grothendieck topology. -/
structure Sheaf where
  /-- the underlying presheaf -/
  val : Cᵒᵖ ⥤ A
  /-- the condition that the presheaf is a sheaf -/
  cond : Presheaf.IsSheaf J val

You'll see that the sheaf is defined as a functor with domain being the original category, regardless of what the Grothendieck topology says

[Kenny Lau]

and you still need to extend the functor

[Kenny Lau]

so the sheaf on Opens X, as a functor, is still of type (Opens X)ᵒᵖ ⥤ A.

[Joël Riou]

In https://github.com/leanprover-community/mathlib4/compare/master...cech-experiment I considered the category of "formal coproducts" of objects. This is the right generality (in some form or another, it was already in SGA 4). (In the construction I am linking here, I am working in a category C, but I am "thinking" of this category C as the category Over X for some object X in a category D, i.e. we consider families of objects U i ⟶ X, and doing products in this category correspond to taking (wide) pullbacks over X. It may be easier to work directly in a category Over X.)

[Kenny Lau]

That sounds like the correct category!

[Kenny Lau]

But the correct question is now, what am I doing here if you @Joël Riou already has a Cech experiment made?

[Adam Topaz]

That's the correct category if you work with a coverage (or a pretopology) but if you want to work with a Grothendieck topology then you probably need to look at the free cocompletion (i.e. the category of presheaves of types)

[Kenny Lau]

@Adam Topaz could you point me somewhere?

[Adam Topaz]

I'm not sure mathlib knows that the category of presheaves is the free cocompletion...

[Adam Topaz]

https://ncatlab.org/nlab/show/free+completion

[Joël Riou]

Kenny Lau said:

But the correct question is now, what am I doing here if you Joël Riou already has a Cech experiment made?

My code was only a draft posted here. I did not work more on this.

[Kenny Lau]

@Adam Topaz ok, so that means I first need to extend the sheaf to Set^(Opens X)ᵒᵖ, presumably by the Yoneda embedding?

[Kenny Lau]

presumably I don't want a second Grothendieck topology on that cocompletion?

[Kenny Lau]

and then I want to show that a Sieve on Opens X become one element in that new category

[Adam Topaz]

I don't think you would even have to extend it. I think you can combine the "evaluate at F" and the "extend" into one step.

[Adam Topaz]

For example, if you take a "formal disjoint union" $U \coprod V$, you can view it as the formal colimit of the diagrams of opens which are contained in either $U$ or $V$. Now given a sheaf $F$, when you evaluate at this formal colimit, you would get the limit of the values of those opens.

[Adam Topaz]

wait, I'm suspicious.

[Adam Topaz]

yeah, that's not quite right because you can have some $W$ mapping to both $U$ and $V$ (and the code above with the presieve is probably wrong too)

[Joël Riou]

An important remark I would like to make is that we want a definition of the Cech cohomology (with respect to a family U i ⟶ X) not just for sheaves, but more generally for presheaves. (A significant part of the formalization should not involve Grothendieck topologies at all!)

[Kenny Lau]

@Adam Topaz @Joël Riou I did some more experimentations, and came up with this:

import Mathlib

universe w' w v u

namespace CategoryTheory

open Abelian Limits

variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}

namespace Sheaf

def toCocompletion (F : Cᵒᵖ ⥤ AddCommGrp.{u}) : (Cᵒᵖ ⥤ Type v)ᵒᵖ ⥤ AddCommGrp.{v} where
  obj X := limit sorry /- I tried to come up with something like, take limit of a diagram where
    every map `V ⟶ U` corresponds to a new map `F(U) ⟶ F(V)`, and something like, take
    `X(U)` copies of `U`, but couldn't really make it work. -/
  map f := sorry

noncomputable def sieveToCocompletion (X : C) (𝒰 : J X) : Cᵒᵖ ⥤ Type v where
  obj y := 𝒰.val.arrows (Y := y.unop)
  map f g := ⟨f.unop ≫ g.1, 𝒰.val.downward_closed _ f.unop⟩

noncomputable def sieveToCocompletionArrow (X : C) (𝒰 : J X) : Arrow (Cᵒᵖ ⥤ Type v) where
  left := sieveToCocompletion X 𝒰
  right := yoneda.obj X
  hom := { app y f := f.1 }

def Cech.complex (F : Sheaf J AddCommGrp.{v}) (X : C) (𝒰 : J X) : CochainComplex AddCommGrp ℕ :=
  (AlgebraicTopology.alternatingCofaceMapComplex _).obj <|
    Functor.rightOp (Arrow.cechNerve <| sieveToCocompletionArrow X 𝒰) ⋙
      (toCocompletion F.val) -- I should use one universe?


end Sheaf

end CategoryTheory

[Kenny Lau]

perhaps you'll be able to fill in the sorrys?

[Adam Topaz]

Sure, but even if you don't apply the construction to a sheaf but just to a presheaf, you still need to decide what it means to be a "cover". If we have a Grothedieck topology $J$, we can say that a morphism $f : X \to Y$ is a cover if the sieve it generates is a covering sieve, and once you have the notion of a morphism being a cover, you get the notion of a hypercover. What I don't know is under what assumptions there are "enough" such hypercovers so that (hyper)Cech-cohomology agrees with sheaf cohomology for the given topology.

[Kenny Lau]

my desired application is to schemes

[Adam Topaz]

but even in schemes there are many Grothendieck topologies (etale, crystalline, flat, v, ...)

[Kenny Lau]

true

[Kenny Lau]

So am I on the right track with the code above?

[Joël Riou]

For Cech-cohomology, "covers" means any family of maps U i ⟶ X (see for example, SGA 4 V 2.3.5). What is remarkable with Cech-cohomology is that it has an interpretation as Ext-group in the category of abelian presheaves (SGA 4 V 2.3.4) (in particular, it only depends on the sieve generated by the U i ⟶ X), but we certainly want to formalize more details...

[Joël Riou]

Kenny Lau said:

So am I on the right track with the code above?

I am not exactly sure what this is, but there should not be J : GrothendieckTopology C anywhere in the first definitions.

[Kenny Lau]

Joël Riou said:

Kenny Lau said:

So am I on the right track with the code above?

I am not exactly sure what this is, but there should not be J : GrothendieckTopology C anywhere in the first definitions.

I'm trying to extend a sheaf to the co-completion, so that I can turn a cover into one arrow, and then apply Cech nerve

[Kenny Lau]

a cover {U_i -> X}_i becomes one arrow in the co-completion, using either the formal coproducts in your Cech experiment, or Adam's provided cocompletion as C^op => Set

[Kenny Lau]

is this correct?

[Joël Riou]

This seems unnecessarily complicated to me, and it is probably wrong because your definition depends on a sieve, even though in the Cech-complex, the summands are indexed by types which are related to index type of a family of maps. (These index types appear quite clearly in my code...)

[Kenny Lau]

Joël Riou said:

This seems unnecessarily complicated to me, and it is probably wrong because your definition depends on a sieve, even though in the Cech-complex, the summands are summands are indexed by types which are related to index type of a family of maps. (These index types appear quite clearly in my code...)

If an open subset Ui -> X is part of the sieve, then the sieve necessarily also contains all those V -> Ui, which are useless information; I dealt with this useless information by considering the limit of those F(Ui) -> F(V), which should be just F(Ui) itself.

[Kenny Lau]

I see that your code in the Cech experiment does not care about these other useless information

[Kenny Lau]

which is of course equivalent, but I just thought that people might complain if we don't prove stuff in the highest generality and always use the higher generalities to derive the lower generalities

[Kenny Lau]

in particular, this means that people might complain if we don't build the Cech cohomology out of the Cech nerve

[Kenny Lau]

Kenny Lau said:

Hello, I have come from 2 years in the future to resurrect this thread. So, as noted above, we have all the building blocks for Cech cohomology (?)

1. We have the Čech nerve CategoryTheory.Arrow.cechNerve

$$\cdots ~\begin{smallmatrix}\rightrightarrows \\ \rightrightarrows\end{smallmatrix}~ U \times_X U \times_X U \Rrightarrow U \times_X U \rightrightarrows U$$

2. Then just by the sheaf $\mathcal{F}$ (on the site? extended to the site?) being a functor, we get a cochain complex:

$$\mathcal{F}(U) \rightrightarrows \mathcal{F}(U \times_X U) \Rrightarrow \mathcal{F}(U \times_X U \times_X U) ~\begin{smallmatrix}\rightrightarrows \\ \rightrightarrows\end{smallmatrix}~ \cdots$$

, which finally brings us to an abelian category (assuming $\mathcal{F}$ takes value in an abelian category).

3. Then by AlgebraicTopology.alternatingCofaceMapComplex we bring it to a cochain complex:

$$\mathcal{F}(U) \to \mathcal{F}(U \times_X U) \to \mathcal{F}(U \times_X U \times_X U) \to \cdots$$

4. This is the Čech (cochain) complex associated to a cover $U \to X$ and sheaf $\mathcal{F}$. Its cohomology is the Čech cohomology.

Is this correct? Then my next step would be to make it finite, by considering the alternating Čech cohomology as well as the ordered Čech cohomology. Before that I would also translate it back to the site of open subsets (rather than open covers).

[Kenny Lau]

What do you think?

[Joël Riou]

Kenny Lau said:

in particular, this means that people might complain if we don't build the Cech cohomology out of the Cech nerve

The definition in SGA 4 does not use "the Cech nerve". It is a linearized version, which is very close to the definition I made. I would argue that it is easier to manipulate objects in FormalCoproduct rather than presheaves of sets which happen to be isomorphic to a coproduct of representables; this is one of the reasons for this choice in my code.

[Joël Riou]

With your notations,

$$\cdots ~\begin{smallmatrix}\rightrightarrows \\ \rightrightarrows\end{smallmatrix}~ U \times_X U \times_X U \Rrightarrow U \times_X U \rightrightarrows U$$

my understanding is that U is the presheaf of types that is the coproduct of the presheaves represented by the U i ⟶ X in a family of morphisms. Then, U \times_X U identifies to a coproduct of the presheaves represented by the fiber products of U i and U j over X, etc. We want to evaluate this on a presheaf with values in a category A. With my approach, these U, U \times_X U, etc correspond directly to objects in FormalCoproduct corresponding to the family of the U i, or the family of the fiber products of the U i and U j, etc, which makes it easy to evaluate on any presheaf (provided the target category has suitable products).

[Kenny Lau]

I do prefer your approach, in general I like concrete definitions; but I'm just saying, there might be people who insist that Mathlib4 has to derive the most general stuff etc.

[Kenny Lau]

And @Adam Topaz above seems to believe that it's possible to do it abstractly via the cocompletion?

[Joël Riou]

Can you explain how my definition is not general enough?

[Kenny Lau]

People might say that there might be some way to use Cech nerve, and also we have an existing notion of covering called "Grothendieck topology" which you abandonned (which I agree with!), tho as I said I much prefer your approach without the unnecessary extra sets in the covering required by the downwards closure axiom

[Kenny Lau]

@Joël Riou anyway, shall I take your code and make it into a PR?

[Joël Riou]

I am not "abandonning" Grothendieck topology: I am only saying it is irrelevant when one wants to define the Cech cohomology of a presheaf with respect to a family of morphisms U i ⟶ X, but of course it shall have interesting properties basically only when it generates a covering sieve with respect to a Grothendieck topology. Requiring that the family "is" a sieve is not at all a good idea. Also, the notion of "presieve" is not great here because in the case of an open covering of a topological space X by two open subsets U and V, we may still want to use an index type with two elements even if U=V!

[Joël Riou]

Kenny Lau said:

Joël Riou anyway, shall I take your code and make it into a PR?

Of course, you may freely reuse this code. It may have to be reorganised in several files though.

[Kenny Lau]

By the way, what's a use case where there is no terminal object?

[Adam Topaz]

the prismatic site

[Calle Sönne]

There is also the infinitesimal site

[Antoine Chambert-Loir]

Or the crystalline one.

[Calle Sönne]

For a simple example, can one make sense of an affine site on a separated non-affine scheme? Then a disjoint union of affines covering the scheme should give you a weakly final object so you can compute cohomology using the cech nerve?

[Bhavik Mehta]

Adam Topaz said:

I'm not sure mathlib knows that the category of presheaves is the free cocompletion...

https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Presheaf.html#CategoryTheory.Presheaf.uniqueExtensionAlongYoneda this, or something nearby, should be that statement

[Adam Topaz]

Yeah, that sounds right! Thanks!

[Kenny Lau]

so i realised that formal products and formal coproducts are exactly the same lol

[Joël Riou]

Adam suggested naming it Indexed C instead.

[Kenny Lau]

@Joël Riou I'll do that, thanks; I can't quite figure out what eval should look like for formal products, would you have any idea?

[Kenny Lau]

i think i would actually have to flip the direction? so it's like coeval : (A => C) => (A => FormalProduct C)?

[Kenny Lau]

no that doesn't sound right either

[Kenny Lau]

also i know that your file didn't make it into a functor and that's probably because it's not possible unless there's some finite fibre assumption

[Kenny Lau]

what if I put that assumption into the Hom?

[Joël Riou]

I defined (FormalCoproduct.{w} C)ᵒᵖ ⥤ (Cᵒᵖ ⥤ A) ⥤ A (which, flipped, would be (Cᵒᵖ ⥤ A) ⥤ ((FormalCoproduct.{w} C)ᵒᵖ ⥤ A)), and I also defined (Jᵒᵖ ⥤ FormalCoproduct.{w} C)ᵒᵖ ⥤ (Cᵒᵖ ⥤ A) ⥤ (J ⥤ A) .

[Kenny Lau]

I'm still not sure I actually understand the difference between formal products and formal coproducts lol

[Kenny Lau]

oh, should the Hom be reversed?

[Kenny Lau]

structure Hom (X Y : FormalProduct.{w} C) where
  f : Y.I → X.I
  φ (i : Y.I) : X.obj (f i) ⟶ Y.obj i

structure Hom' (X Y : FormalCoproduct.{w} C) where
  f : X.I → Y.I
  φ (i : X.I) : X.obj i ⟶ Y.obj (f i)

[Kenny Lau]

something like this?

[Kenny Lau]

yeah, that looks right!

[Joël Riou]

"Formal products" seem to be irrelevant for the formalization of Cech cohomology.

[Kenny Lau]

yes, but i'll define it nevertheless

[Kenny Lau]

so now I won't use Indexed because they actually have different category structure

[Joël Riou]

If you just throw random definitions which are not supported by the mathematical literature and have no known applications, the reviewers/maintainers may rightfully complain.

The reason for the definition of morphisms in FormalCoproduct C is that if X is thought as the formal coproduct of the X i and Y the same for the Y j, we are interested in understanding what are the morphisms in the category of presheaves from the coproduct of the Yoneda presheaves of X i to the coproduct of the Yoneda presheaves of the Y j. We see that it is the data, for each i, of the "section" over X i of the coproduct presheaf of the Yoneda presheaves of the Y j, and this is the choice of an index j and a map from X i to Y j. (In other words, when the universes satisfy certain conditions, there is a "coproduct" functor from FormalCoproduct C to presheaves that is fully faithful. Part of the reason for using FormalCoproduct instead of the cocompletion approach is that the universes are not always perfectly aligned...)

The other category you suggest defining may be the opposite category of FormalCoproduct of the opposite category. If there is no specific application for it, we do not need this in mathlib.

[Kenny Lau]

and the maintainers won't complain if I make one definition without the dual? like sometimes i get confused by mathlib culture

[Joël Riou]

I do not know what is co-Cech homology ;-)

[Kenny Lau]

no, I just mean formal product

[Kenny Lau]

https://ncatlab.org/nlab/show/free+cartesian+category

[Kenny Lau]

#26402 created

[Kevin Buzzard]

Kenny Lau said:

and the maintainers won't complain if I make one definition without the dual? like sometimes i get confused by mathlib culture

I think that this is a very interesting question. When I first learnt about formalization I was very keen on the idea of making every single definition in small steps and creating a full API of everything. But later on I understood that definitions which don't have a point can actually obscure things, slow the system down, create an unnecessary maintenance burden and so on. I think that right at the bottom it is important that we have semigroups and nonassociative non-unital rings or what have you (and as you know we had these things years ago) -- but these things are being used by people. When we're talking about Grassmannians etc, and general more abstract objects, I think there's an art in defining just the right amount of stuff. Every new def and structure gives us a chance to hide a bunch of data behind something which Lean will not unfold by default, and I think there's an art to deciding where these defs go in order to make lean's life easier. In particular I think that at this kind of level the answer is definitely not "make as many new defs as you can think of" (which is is contrast to what's going on at the very bottom, where this seems to be a profitable approach).

[Joël Riou]

Another thing is that we do not always get the right design and the best phrasing of lemmas/definitions immediately. If we need 1000 lines of code or so to make a good API for a certain notion (e.g. left Kan extension and right derived functors), it may be appropriate to first test extensively the development of the notion on one side, and only when we are happy with it, dualize the results. Doing both API immediately can be very painful if we have to roll back any change. (Also, in terms of review process, if we have a good API for "left stuff", we can create a PR saying "In this PR, we dualize the results from the file *.*.... about left stuff to right stuff", e.g. https://github.com/leanprover-community/mathlib4/pull/14238 which makes the review process very easy...)

[Adam Topaz]

Joël Riou said:

I do not know what is co-Cech homology ;-)

I don't know either, but "cosheaves" is a thing that people seriously think about.

[Kenny Lau]

robin-carlier 3 hours ago

Please do not state this in terms of opposites. Rather, you should assume [∀ (I : Type w), HasCoproductsOfShape I A], and use ∐, and have the functor be out of C.

@Robin Carlier I'm intentionally using opposites because we're extending presheaves to the formal coproduct (also note that I'm mentally translating your 5 points to formal coproducts because I've removed formal products)

[Kenny Lau]

I have done half of 1 and all of 2 in my local copy

[Robin Carlier]

Maintainer’s word seems to be that we don’t want to dualize definitions and get the dual version right away, I’m not a fan of this but this is not my call to make and so be it.

I would still really prefer if you'd provide a statement not in terms of opposite, this does not prevent also providing one in terms of opposite if needed.

This category is the free category on C with coproducts, its universal property is that restriction along the inclusion induces an equivalence with coproduct-preserving functors when the target category has coproducts. It feels just plain wrong to have to go through the gymnastic of opposite categories (which are, in general, a pain) to state and use that universal property.
I understand the need of the use case of extending presheaves, but to me this does not warrant not stating the universal property in its most natural way.

[Robin Carlier]

Regarding the use of "formal products", the case of formal finite products (which is yet an other definition than what we have here) is more interesting, , if I recall correctly they are used by Lurie as an object within the proof that simplicial objects with values in an "algebraic category" (e. g rings) have a model structure that presents the "free homotopy-(sifted cocompletion)" of the algebraic theory underlying everything. This is for instance how you prove that the model structure on simplicial rings really presents the infinity-category of what people call "derived rings". So related notion do have some use cases, but I would understand the call that in this case we can just wait until we get there to add them.

[Kenny Lau]

Robin Carlier said:

in terms of opposite if needed

well we do need it, so I guess I'll just have both statements?

[Kenny Lau]

I haven't pushed this change yet, but there's one proof where I proved that it has pullback if C has pullback, and i got into DTT hell so my proof was rather long, just as a heads up

[Kenny Lau]

(advice on how to do this more efficiently is certainly welcome)

[Kenny Lau]

@Joël Riou I've finished proving all the statements in #26402 . There are some proofs that are a bit long, and there might be some spacing problems, but I'll fix them later, so don't worry about them for the moment.

If you have the time to review it, could you just focus on the statements for now, until I polish the file at a later time, thanks a lot.

[Kenny Lau]

cc @Robin Carlier if you would also like to review.

[Kenny Lau]

@Robin Carlier I've updated the file to complete the tasks.

[Kenny Lau]

@Joël Riou I have a question about implementation. I proved that if C has terminal then FormalCoproduct F has terminal, and the same for pullback, so now I’m conjecturing that it’s probably true for all limits of all shapes? But should I prove that as well if I don’t think I would use it for the specific use case of cech cohomology?

[Kenny Lau]

After further thought I think this might be doable but might require 200 more lines, so I think it’s better to delay it to a (non-existent) future PR.

[Joël Riou]

My approach would be to focus on what it is necessary for Cech cohomology. Anything else that is nontrivial could be done in future PRs.

[Kenny Lau]

@Robin Carlier Thanks for the review. I've removed the non-terminal simps as well as added more @[simps!].

[Kenny Lau]

I've kept the two newlines because I think it's more readable.

[Robin Carlier]

Great! will re-review tomorrow but except for name nitpicking I think we’re getting close.

[Kenny Lau]

Thanks!

[Andrew Yang]

Is FormalCoproduct C (at least in the PR) just StructuredArrow typeToCat C?

[Kenny Lau]

@Andrew Yang It is similar to CategoryTheory.CostructuredArrow instead, but I think they are still different.

A term X : CostructuredArrow typeToCat C encodes X.I : Type and then X.obj : X.I → C (in the notation of my PR), but a morphism f : X ⟶ Y in the category CostructuredArrow typeToCat C encodes a function f.f : X.I → Y.I such that Y.obj (f.f i) = X.obj i.

[Kenny Lau]

image.png

[Kenny Lau]

The category of S-costructured arrows with target T : D (here S : C ⥤ D), has as its objects D-morphisms of the form S Y ⟶ T, for some Y : C, and morphisms C-morphisms Y ⟶ Y' making the obvious triangle commute.

[Andrew Yang]

You're right. Then it's probably

import Mathlib

namespace CategoryTheory

universe u v w

@[simps]
def Category.Pi : Type uᵒᵖ ⥤ Cat.{v, w} ⥤ Cat where
  obj I := { obj C := .of (I.unop → C), map f := Functor.pi fun _ ↦ f }
  map f := { app C := Pi.comap _ f.unop }

abbrev FormalCoproduct {C : Type v} [Category.{w} C] : Type _ :=
  (Grothendieck (Category.Pi.flip.obj (.of C)))ᵒᵖ

[Kenny Lau]

@Andrew Yang ok, what properties do you get for free if this is the case?

[Andrew Yang]

I'm guessing you can get the limits and colimit statments for free.

[Kenny Lau]

@Andrew Yang I think something is still flipped:

import Mathlib

universe w w₁ w₂ w₃ v v₁ v₂ v₃ u u₁ u₂ u₃

open Opposite

namespace CategoryTheory

namespace Limits

variable {C : Type u} [Category.{v} C] (A : Type u₁) [Category.{v₁} A]

variable (C) in
@[simps]
def Category.Pi : Type wᵒᵖ ⥤ Cat.{v, u} ⥤ Cat where
  obj I := { obj C := .of (I.unop → C), map f := Functor.pi fun _ ↦ f }
  map f := { app C := Pi.comap _ f.unop }

variable (C) in
abbrev FormalCoproduct' : Type _ :=
  (Grothendieck (Category.Pi.{w}.flip.obj (.of C)))ᵒᵖ


variable (C) in
structure FormalCoproduct where
  /-- The indexing type. -/
  I : Type w
  /-- The object in the original category indexed by `x : I`. -/
  obj (i : I) : C

structure Hom (X Y : FormalCoproduct.{w} C) where
  /-- The function on the indexing sets. -/
  f : X.I → Y.I
  /-- The map on each component. -/
  φ (i : X.I) : X.obj i ⟶ Y.obj (f i)

def foo : FormalCoproduct'.{w} C ≃ FormalCoproduct.{w} C where
  toFun X := ⟨X.unop.base.unop, X.unop.fiber⟩
  invFun X := ⟨op X.I, X.obj⟩

def bar (X Y : FormalCoproduct'.{w} C) : Hom (foo X) (foo Y) ≃ (X ⟶ Y) where
  toFun f := ⟨op f.f, fun i ↦ by simp⟩ -- unop Y).fiber (f.f i) ⟶ (unop X).fiber i

[Kenny Lau]

maybe you need to take the dual of C too...

[Andrew Yang]

Yeah you're right its (Grothendieck (Category.Pi.{w}.flip.obj (.of Cᵒᵖ)))ᵒᵖ

[Kenny Lau]

import Mathlib

universe w w₁ w₂ w₃ v v₁ v₂ v₃ u u₁ u₂ u₃

open Opposite

namespace CategoryTheory

namespace Limits

variable {C : Type u} [Category.{v} C] (A : Type u₁) [Category.{v₁} A]

variable (C) in
@[simps]
def Category.Pi : Type wᵒᵖ ⥤ Cat.{v, u} ⥤ Cat where
  obj I := { obj C := .of (I.unop → C), map f := Functor.pi fun _ ↦ f }
  map f := { app C := Pi.comap _ f.unop }

variable (C) in
abbrev FormalCoproduct' : Type _ :=
  (Grothendieck (Category.Pi.{w}.flip.obj (.of Cᵒᵖ)))ᵒᵖ


variable (C) in
structure FormalCoproduct where
  /-- The indexing type. -/
  I : Type w
  /-- The object in the original category indexed by `x : I`. -/
  obj (i : I) : C

structure Hom (X Y : FormalCoproduct.{w} C) where
  /-- The function on the indexing sets. -/
  f : X.I → Y.I
  /-- The map on each component. -/
  φ (i : X.I) : X.obj i ⟶ Y.obj (f i)

def foo : FormalCoproduct'.{w} C ≃ FormalCoproduct.{w} C where
  toFun X := ⟨X.unop.base.unop, fun i ↦ (X.unop.fiber i).unop⟩
  invFun X := ⟨op X.I, fun i ↦ op (X.obj i)⟩

def bar (X Y : FormalCoproduct'.{w} C) : Hom (foo X) (foo Y) ≃ (X ⟶ Y) where
  toFun f := ⟨op f.f, fun i ↦ op (f.φ i)⟩
  invFun f := ⟨f.unop.base.unop, fun i ↦ (f.unop.fiber i).unop⟩

[Kenny Lau]

there you go

[Kenny Lau]

@Joël Riou So in light of this new result I see three ways forward:

1. Keep the current definition in the PR, and construct an equivalence of categories to Grothendieck, and try to transport all the limit stuff from there.
2. Replace the definition in the PR with abbrev, and then define custom constructors and projections, and also define custom constructors and projections for the various cones. (can we please make @[simps] support custom projections)
3. Keep the current definition in the PR, make the equivalence a TODO, and change nothing.

[Joël Riou]

I would suggest doing 3. The whole point of FormalCoproduct in my original code was to make it easy to work with formal coproducts of objects.

[Andrew Yang]

I don't think 2 would make it harder to work with? And it would allow us to get abstract nonsense results more easily.

[Joël Riou]

As it was pointed out, the @[simps] lemmas generated for objects/morphisms in the Grothendieck construction would not match the ones obtained via the more direct approach: this is only making things more complicated IMO. (If some properties are much easier to obtain using the Grothendieck construction, we could do 1.)

[Robin Carlier]

I'd also prefer 3.
Do we even have that many results for existence of co/limits in Grothendieck constructions? What results currently in Mathlib would be used to get the "abstract nonsense" results with this redefinition?

[Kenny Lau]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.html

Grothendieck has colimits (assuming conditions on base category), so we should be able to get limits (we took dual).

[Robin Carlier]

From what I'm reading, this file is about colimits of functors out of Grothendieck F, not about colimits inside Grothendieck F. I'm note sure these would help.

[Andrew Yang]

I think ideally the metric we should be is not “what is the easiest way to prove it given current mathib” but rather “what is the easiest way to prove it if mathlib contained everything it should have contained” (this is still the same question that was raised in the reviewer chat). And the proof that Grothendieck construction has limits is basically in mathlib as “presheafed spaces has limits”. (the proof should be generalizable)
Of course practically this might be too big of a detour and it might be fine if this is done manually for now and left as a TODO.

But note that you might also need formal finite (co)products so this duplication might need to appear four times. (Or we should just do formal completion for a set of diagrams instead)

[Andrew Yang]

And for the simps issue, I totally agree that simps should add support to custom projections and I might eventually try to do this in some distant future if nobody else does.

But I think it already supports custom projection if it is a chain of projections, which seems to be the case here.

[Robin Carlier]

For formal finite coproducts, we can maybe "cheat" and use a full subcategory of the full formal coproducts?

As to the "right generality" of the result, if we want to go that way, then we should probably prove general results about (co)limits in (co)fibered categories, these would be part of "things mathlib should contain" IMO, but they probably need to wait on more stuff on (co)fibered categories I think. (I also can’t find the reference, but I recall these results being proven in Lurie’s HTT as an application of "relative colimits" in cofibered categories (related), but I don’t know if Mathlib wants relative colimits...)

[Andrew Yang]

I might be hallucinating but is it not true that a fibered category is equivalent to the grothendieck construction of its fibers so this generalization is just a syntactic one not a mathematical one? (Though we probably want both anyways even if the answer is yes)

[Robin Carlier]

Yes, it's true, but as you say there's the "syntax" thing going on so this is why I stated things that way: it's speculative since I have no code for any of this yet but I feel that stating things with general fibered categories would avoid constantly going back to the (equivalent) Grothendieck construction and carrying the equivalence everywhere.

[Paul Lezeau]

cc @Calle Sönne

[Kenny Lau]

@Robin Carlier I've updated my PR (#26402).

[Robin Carlier]

Will try to have a look today or tomorrow

[Kenny Lau]

Thanks!