Epimorphisms of sheaves

Stream: Is there code for X?

[Dagur Asgeirsson]

Has anyone formalised this result?

import Mathlib.CategoryTheory.Sites.Surjective

namespace CategoryTheory

open GrothendieckTopology

variable {C : Type*} [Category C]
variable {J : GrothendieckTopology C}
variable {A : Type*} [Category A] [ConcreteCategory A]
variable {F G : Sheaf J A} (f : F ⟶ G)

theorem epi_iff_locallySurjective : Epi f ↔ IsLocallySurjective J f.val := by
  sorry

(probably with some more assumptions on A). It doesn't seem to be in mathlib, but maybe something similar was done in LTE @Johan Commelin @Adam Topaz? For (light) condensed sets it means that a map is an epi iff for every (light) profinite set S mapping into the target, there is another (light) profinite set S' with a surjection to S and a map to the source, making the square commute.

[Joël Riou]

I have done this very recently for sheaves of sets https://github.com/leanprover-community/mathlib4/pull/9965
(see the file CategoryTheory.Sites.EpiMono). The argument is based on the fact that the category of sheaves is balanced (for sheaves of sets, I have followed the argument in SGA 4 II 4.2; for sheaves of abelian groups, it follows from the fact it is an abelian category) and the existence of an epi-mono factorization of a morphism for which we would know the epi is locally surjective.

[Dagur Asgeirsson]

Great! I’ll take a look at your PR this evening

[Joël Riou]

Thanks to your message, I notice that part of my code duplicates the file Sites.Surjective by @Andrew Yang

[Adam Topaz]

Yeah IIRC Andrew did this in a reasonable level of generality (we did it for condensed abelian groups in LTE)

[Dagur Asgeirsson]

#13478 characterises epimorphisms in condensed sets and condensed modules over any ring R (this now includes condensed abelian groups by definition), as objectwise surjections on Stonean (and hence generalises this result in LTE).

Thanks @Joël Riou for providing the general API for locally surjective maps of sheaves!

[Adam Topaz]

Is there a reason this is done only for CondensedSet and CondensedMod, and not for more general condensed objects (maybe satisfying some further assumptions)?

[Dagur Asgeirsson]

The target category has to be concrete, and satisfy the assumptions in docs#CategoryTheory.Sheaf.isLocallySurjective_iff_epi'. But indeed the theorem in the condensed file should be stated for this type of category, it should then apply directly to condensed sets and condensed modules

[Joël Riou]

Dagur Asgeirsson said:

Thanks Joël Riou for providing the general API for locally surjective maps of sheaves!

Half of the credit should go to @Andrew Yang!

[Dagur Asgeirsson]

Of course! Sorry Andrew

[Dagur Asgeirsson]

I'm running into some universe issues when trying to apply this to light condensed sets. I wonder if some of the universes in the concrete sheafification file could be generalised so it applies to essentially small sites

[Joël Riou]

In a very draft branch https://github.com/leanprover-community/mathlib4/blob/dense-subsite-refactor/Mathlib/CategoryTheory/Sites/DenseSubsiteNew.lean based of my 1-hypercovers PRs I have a plan for a refactor of DenseSubsite which would eventually allow to get properties of categories of sheaves by transporting properties of a "smaller" site with equivalent categories of sheaves (in particular, we could get sheafification if the category of the site is essentially small, but this shall more general).

Also, I would think that an alternative (or replacement?) construction of the "concrete sheafification" should be done using 1-hypercovers of a certain size w. (The difference is that the current sheafification using the ordered set of covering sieves involves limits and colimits indexed by types in a universe max u v.). The extra difficulty is that we would have to consider the homotopy category of 1-hypercovers instead of an ordered set... (Using such constructions, I think it will be possible to sheafify presheaves Scheme.{u}ᵒᵖ ⥤ Type u (and not just `Scheme.{u}ᵒᵖ ⥤ Type (u + 1)) for the Zariski, étale or fppf topologies.)

(Doing all of this may take some time though...)

[Dagur Asgeirsson]

I think this is a good approach, but indeed sounds like it might take some time!

For my application, my site is already equivalent to a small category, so I should be able to prove directly things like the fact that PreservesSheafification is preserved by the equivalence of sites, and use that (similar to what we did for HasSheafify and HasSheafCompose in this file).

[Joël Riou]

Yes, this is the short term solution...

[Andrew Yang]

Sounds like someone is volunteering to review #13004 :)

[Adam Topaz]

I agree it would be great to refactor sheafification to use 1-hypercovers. I think the construction works in a single step with such an approach, as opposed to two steps like this "plus-plus" construction!

[Adam Topaz]

Does docs#CategoryTheory.GrothendieckTopology.OneHypercover have a category structure yet?

[Joël Riou]

No, it does not.

[Adam Topaz]

Ok. Why do you need the homotopy category BTW? Is it not the case that you just take the colimit over the category of hypercovers of the limit of the presheaf applied to the objects in the hypercover?

[Joël Riou]

For the colimit, it does not change whether we take the homotopy category or not, but this is (co?)filtering only after passing to the homotopy category. Eventually, we would probably want to apply cofinality results to this category (introducing suitable small cofinal subcategories), and as we have more cofinality results for filtering categories, it is probably better to use the homotopy category.

[Adam Topaz]

I see, yes, you would need that it's filtered to prove left exactness and things of that sort.

[Dagur Asgeirsson]

It all works now for light condensed sets and modules as well: #13495.

[Dagur Asgeirsson]

Using the short term solution, of course. If we refactor sheafification using 1-hypercovers, I guess almost everything in the file Sites/Equivalence becomes obsolete

[Joël Riou]

I now have very draft PR #19444 and #19462. The first #19444 shows that if we have a functor F : C₀ ⥤ C which is a dense subsite (for topologies J₀ and J), then if moreover F is "1-hypercover dense" (any object in C has a 1-hypercover consisting of objects from C₀, with index types in a certain universe w), then assuming the target category A has limits of size w, I obtain an equivalence Sheaf J A ≌ Sheaf J₀ A, and show that a HasSheafify J₀ A instance transports to a HasSheafify J A instance.
In the second #19462 (still a few sorries), I outline a construction of such a C₀ in case C is the small étale site of a scheme S : Scheme.{u}. Indeed, the issue is that the small étale site of S is a large category! By using a certain packaging of schemes X ⟶ S that are finitely presented (and étale) over an affine open subset of S, I obtain a small category C₀ (which is not equivalent to C) but such that all objects in C have a "small" 1-hypercover consisting of objects in C₀.

As a result, we shall get HasSheafify (smallEtaleTopology S) (Type u). (The second part obviously depends on the work by @Christian Merten, @Andrew Yang et al. on notions of smooth and étale morphisms, and part of the code will have to be adapted after Christian's PR #19096 and #18945 are merged.) Eventually, the étale cohomology of a scheme in Scheme.{0} shall be in Type 0...

A similar method would work for the fppf site, for the site of smooth schemes over a base, etc. However, it would not work for the big étale site of all S-schemes (but do we need to sheafify presheaves over such categories?). A different method would have to be followed: if someone is interested, they may implement a construction of the associated sheaf directly in one step using 1-hypercovers (as an alternative to the "plus-plus" construction).

[Johan Commelin]

Wow, very nice!

[Johan Commelin]

It's cool that these technical pieces of the puzzle are falling into place