Pullback of abelian sheaves #
Mathlib's CategoryTheory.Functor.sheafPullback is the left adjoint of the pushforward of sheaves
along a continuous functor. For sheaves of abelian groups, this file records that it is additive
and right exact, as a left adjoint between preadditive categories.
Main declarations #
CategoryTheory.Functor.sheafPullback_additive: the pullback of abelian sheaves is additive.CategoryTheory.Functor.preservesFiniteColimits_sheafPullback: the pullback of abelian sheaves preserves finite colimits.
instance
CategoryTheory.Functor.sheafPullback_additive
{C : Type u_1}
[Category.{v_1, u_1} C]
{J : GrothendieckTopology C}
{D : Type u_2}
[Category.{v_2, u_2} D]
{K : GrothendieckTopology D}
(u : Functor C D)
[u.IsContinuous J K]
[(u.sheafPushforwardContinuous AddCommGrpCat J K).IsRightAdjoint]
:
(u.sheafPullback AddCommGrpCat J K).Additive
The pullback of abelian sheaves along a continuous functor is additive, as a left adjoint.
instance
CategoryTheory.Functor.preservesFiniteColimits_sheafPullback
{C : Type u_1}
[Category.{v_1, u_1} C]
{J : GrothendieckTopology C}
{D : Type u_2}
[Category.{v_2, u_2} D]
{K : GrothendieckTopology D}
(u : Functor C D)
[u.IsContinuous J K]
[(u.sheafPushforwardContinuous AddCommGrpCat J K).IsRightAdjoint]
:
The pullback of abelian sheaves along a continuous functor preserves finite colimits, as a left adjoint.