Extension by zero Sheaf

Stream: Is there code for X?

[Brian Nugent]

I would like to use extension by zero for sheaves of abelian groups on a topological space: https://stacks.math.columbia.edu/tag/00A4. Is there a general version of this for sites in mathlib? Maybe defined as a left adjoint to the restriction functor or something?

[Christian Merten]

I don't think we have a definition, but this would be the abstract nonsense version:

import Mathlib

open CategoryTheory

variable {C : Type*} [Category* C] (J : GrothendieckTopology C)
  {A : Type*} [Category* A]

noncomputable def extensionByZero (U : C)
    -- this assumption will be automatic if `A` has sufficiently large colimits
    [((Over.forget U).sheafPushforwardContinuous A (J.over U) J).IsRightAdjoint] :
    Sheaf (J.over U) A ⥤ Sheaf J A :=
  (Over.forget U).sheafPullback A (J.over U) J

[Christian Merten]

That being said, this won't be particularly useful for your use case.
However, It should not be hard to show that this extensionByZero can be more explicitly described (under suitable assumptions) as the sheafification of the presheaf $V \mapsto \coprod_{\mathrm{Hom}(V, U)} F(V)$.
From this, it follows that this indeed agrees with the extension by zero for sheaves of abelian groups on a topological space.

[Brian Nugent]

I think the abstract nonsense definition is actually exactly what I need, thank you!