global sections functor

Stream: maths

[Ben Eltschig]

When working with sheaves / toposes, one really important functor is the global sections functor $\Gamma$, i.e. the forwards part of the unique (up to isomorphism) geometric morphism to $\text{Set}$. There are two ways of constructing it that I know of, that generalise in two different directions:

• As the functor $\Gamma(*,-)$ that evaluates sheaves on a terminal object. This works for sheaves valued in any category, but requires the site to have a terminal object. On topological spaces these are literally sections on the whole space, so they are nice to work with concretely and give reason to the name.
• As the functor $\text{Hom}(*,-)$ of morphisms out of the terminal sheaf/object. This works on any site, but only for sheaves valued in a category with a terminal object (since that's what's needed for there to be a terminal sheaf); it is also always a functor to $\text{Set}$, not to the category the sheaves are valued in. While more abstract, this does have the advantage of clearly only depending on the category of sheaves, not the site.

For sheaves of types on any local site, in particular on any topological space, the two functors are naturally isomorphic. This is the case I am most interested in, but of course to formalise anything I still need to pick one (or both) of the definitions and state it, preferably in the right generality. I am thus wondering:

• Do we want to have one or both of these under some name like Sheaf.Γ or globalSectionsFunctor in mathlib? I have looked around and seen that we already have Scheme.Γ, LocallyRingedSpace.Γ, SheafedSpace.Γ and PresheafedSpace.Γ as special cases of the first definition, but (as far as I can see) nothing in full generality and also nothing on the second definition yet.
• If we do want both, how do we name them? Something short like Sheaf.Γ seems ideal, but then what is the second name? Or do we simply construct the second functor as coyoneda.obj (op (⊤_ (Sheaf J A))) on the fly whenever it comes up?

If you want to see some code for how this could look, I do have a version of both functors and an isomorphism between them here already, albeit not in full generality because I only focused on concrete sites back then.

[Joël Riou]

Let us consider Sheaf J A where J is a Grothendieck topology on C, and A the "coefficient" category of the sheaves.

• When we want the sections of F to be a type, the best candidate I see is F.1.sections (which may be in a larger universe). It was not made a functor though. This is defined for A := Type u (and we could have a AddCommGrp variant easily), and for a general category A, we may apply this construction to the sheaf of types obtained by composing F with some coyoneda functor.
• When we want the sections of F to be an object in A, we should probably apply the right adjoint to the constant sheaf functor. This corresponds also to taking the projective limit of the underlying presheaf F.1. A suggestion of design could be through the introduction of a type class HasGlobalSectionsFunctor J A (abbrev for (constantSheaf J A).IsLeftAdjoint). Then, Sheaf.Γ and Sheaf.globalSectionsFunctor could be defined. (Taking Hom from the terminal object of A to Sheaf.Γ should give an equivalent type to the above construction.)

[Ben Eltschig]

Joël Riou said:

• When we want the sections of F to be an object in A, we should probably apply the right adjoint to the constant sheaf functor. This corresponds also to taking the projective limit of the underlying presheaf F.1. A suggestion of design could be through the introduction of a type class HasGlobalSectionsFunctor J A (abbrev for (constantSheaf J A).IsLeftAdjoint). Then, Sheaf.Γ and Sheaf.globalSectionsFunctor could be defined.

That's a good suggestion - I knew that getting a right-adjoint to the constant sheaf functor is what we were trying to accomplish, but it didn't occur to me that we could also use that as the definition. I'm slightly worried that not having this functor be definitionally equal to anything useful will be troublesome, but then again, CategoryTheory.presheafToSheaf is defined in the same way and didn't lead to any problems that I am aware of.

[Ben Eltschig]

Do you happen to know conditions on A and J under which this adjoint exists, and when it is isomorphic to evaluation on the terminal object? I'll try to think about it a bit on my own too , but I don't usually work with sheaves valued in things other than sets and groups much, so it might take a while

[Adam Topaz]

The global sections is a suitable limit of the sections over all objects in the site. This is often a large indexing category, so one must take some care is determining whether it exists. If the site has a terminal object, then this limit will be (canonically) isomorphic to the sections over the terminal object via the projection out of the limit

[Adam Topaz]

So if C is the category underlying the site, and A is the category where your sheaves take their values, you will have a global sections functor whenever A has limits of shape C

[Adam Topaz]

(or rather C^op)

[Ben Eltschig]

I see - that makes sense. Thanks for your input, I'll see what I can do with that.

[Adam Topaz]

I haven't formalized anything in a while, and I had a few minutes before my class today to play around with Lean, so I came up with the following (under a spoiler, if you want to do the above as an exercise):

import Mathlib

open CategoryTheory Limits
variable {C : Type*} [Category C] (J : GrothendieckTopology C) (D : Type*) [Category D]

noncomputable
def globalSectionsFunctor [HasLimitsOfShape Cᵒᵖ D] : Sheaf J D ⥤ D :=
  sheafToPresheaf _ _ ⋙  lim

noncomputable
def globalSectionsFunctorIsoOfIsTerminal [HasLimitsOfShape Cᵒᵖ D] (t : C) (h : IsTerminal t) :
    globalSectionsFunctor J D ≅ sheafToPresheaf _ _ ⋙  (evaluation _ _).obj (.op t) :=
  have h' : IsInitial (Opposite.op t) := by exact initialOpOfTerminal h
  let e : Limits.lim ⟶ (evaluation Cᵒᵖ D).obj (.op t) := { app := fun F => limit.π _ _ }
  have he : IsIso e := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro F
    exact isIso_π_of_isInitial h' F
  asIso <| whiskerLeft _ e

[Ben Eltschig]

I have opened a PR for this now: #22816. I've gone with Adam's suggestion of defining the global sections as a limit there since it seemed sufficient to me, but if there actually are examples of situations we care about where an adjoint exists despite D not having limits of shape Cᵒᵖ I suppose it might still make sense to switch to the HasGlobalSectionsFunctor solution instead.

[Ben Eltschig]

I've also opened another PR #22817 that builds on top of this to define the right-adjoint of Γ on local sites; I'm just mentioning this so you have some more context for what I'm actually using this Sheaf.Γ for.

[Ben Eltschig]

Ben Eltschig said:

[...] but if there actually are examples of situations we care about where an adjoint exists despite D not having limits of shape Cᵒᵖ [...]

To be clear, the reason I'm unsure about this is that asking for a right-adjoint to the constant sheaf functor only makes sense when the constant sheaf functor exists, which requires sheafification, which as far as I know already requires A to have certain limits too. So while I know that the definition of Sheaf.Γ via limits won't work on large sites, it's not clear to me whether constant sheaves might make sense on them anyways.

[Joël Riou]

It seems to me that the sites which appear in the definition of crystalline cohomology will fit into the situation I am describing.
Assuming HasSheafify is not a very strong assumption: we already have situations where we can show it holds even though the underlying category of the site is large. (It may sound strange, but the "small" étale site of a scheme is a large category, not even essentially small, and yet it shall have suitable HasSheafify instances as I will show in the WIP PR #19462.)
I very much prefer we do a small effort now, rather than having to refactor the definitions in the future (there is an active formalization of divided powers going on...).