Sheafification on big sites with small pretopologies

Stream: mathlib4

[Christian Merten]

The main construction for sheafification in mathlib right now is via docs#CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover (the plus-plus construction). In practice, as far as I can tell, this has only ever been applied in (essentially) small categories, where all the necessary limits and colimits always exist.

If we have a big category though, sheafification will in general not exist, but I think we can do slightly better than what we currently have. The main conditions of the above lemma are (here J is a Grothendieck topology on the category C : Type (u + 1) (with say [Category.{u} C]):

1. for every X, various colimits of shape (J.Cover X)ᵒᵖ must exist and be preserved by suitable functors.
2. ∀ (P : Functor Cᵒᵖ (Type u)) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)

Now let's suppose J is generated by a pretopology K. Then one can define similar categories K.Cover X (with a suitable preorder that is not the one coming from inclusion of presieves!) and there is an obvious initial functor K.Cover X ⥤ J.Cover X.

Let's now suppose the categories K.Cover X are all (essentially) small and for every X and R a covering presieve of X wrt. to K, R isu-small. Then condition

1. is satisfied, because via the initial functor K.Cover X ⥤ J.Cover X we can check things on K.Cover X which is (essentially) small.

2. is harder: If S : Sieve X and R : Presieve X with S = Sieve.generate R, then HasMultiequalizer (R.index P) implies HasMultiequalizer (S.index P). But the sieves of J = K.toGrothendieck are all sieves that contain a covering presieve of K. This means that even if all covering presieves are small, we won't be able to deduce HasMultiequalizer (S.index P) for every J-sieve S. But since K.Cover X ⥤ J.Cover X is initial, I think it should be sufficient, in the plus-plus construction, to only consider sieves in the image of this functor. Those are precisely the ones that satisfy S = Sieve.generate R for some K-presieve and hence the multiequalizers exist with our smallness assumptions.

One way to use this last point, is to change the plus-plus construction and start with a setup like:

variable {T : C → Type*} [∀ X, Category (T X)] (L : ∀ X, T X ⥤ J.Cover X)
  [∀ X, (L X).Initial]
  [∀ (X : C) (P : Cᵒᵖ ⥤ D) (S : T X), HasMultiequalizer (((L X).obj S).index P)]

(where later T X = K.Cover X) and replace all occurences of J.Cover X with T X. I have not checked yet if everything goes through.

Do you think it worth to do this refactor? Is there a better approach?
(Probably at least @Joël Riou is interested.)

[Joël Riou]

For sites like the "small" étale site, I have a WIP PR handling such cases because there is a small dense subsite with an equivalent category of sheaves. (This is based on the notion of 1-hypercover.) This approach would not work for the Zariski sheafification of presheaves over a large category though.
If we refactor the sheafification, I would rather see a "direct" construction of the sheafification by using colimits over a (homotopy) category of 1-hypercovers. (Contrary to the "plus-plus" construction, we would have to apply the construction only once.)

[Christian Merten]

Yes, I am aware of your approach for the étale site, but I was indeed thinking how to get sheafification for the big zariski site.

[Christian Merten]

Do you have a reference explaining this 1-hypercover sheafification process?

[Joël Riou]

I do not know a reference, but it would be safe to start looking at SGA 4 V or the stacks project.

[Joël Riou]

(Note that there are minor subtle differences between docs#CategoryTheory.GrothendieckTopology.OneHypercover and general n-hypercovers in the particular case n = 1. Here, the first steps would be to understand what is "map" between two OneHypercover and what is a homotopy.)

[Christian Merten]

I made an attempt here: #26326.