Extension by zero and injective module sheaves

On a preorder site, extension by zero from a lower interval is exact: it is presheaf extension by zero followed by sheafification. Consequently restriction to a lower interval preserves injective sheaves of modules. For open subsets this is the injectivity property needed to restrict injective resolutions.

The proof uses Mathlib's sheaf-module pullback construction and uniqueness of left adjoints to identify its canonical pullback with exact extension by zero.

instance SheafOfModules.isRightAdjoint_pushforward_over {P : Type u} [Preorder P] {J : CategoryTheory.GrothendieckTopology P} (R : CategoryTheory.Sheaf J RingCat) (U : P) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : (pushforward (CategoryTheory.CategoryStruct.id (R.over U))).IsRightAdjoint

Restriction to a lower interval is a right adjoint on sheaves of modules. Its left adjoint is extension by zero.

instance SheafOfModules.isRightAdjoint_overFunctor {P : Type u} [Preorder P] {J : CategoryTheory.GrothendieckTopology P} (R : CategoryTheory.Sheaf J RingCat) (U : P) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : (overFunctor R U).IsRightAdjoint

The public restriction-functor presentation is also a right adjoint. Its semireducible wrapper needs a separate instance for instance search to match.

instance SheafOfModules.preservesFiniteLimits_pullback_over {P : Type u} [Preorder P] {J : CategoryTheory.GrothendieckTopology P} (R : CategoryTheory.Sheaf J RingCat) (U : P) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.Limits.PreservesFiniteLimits (pullback (CategoryTheory.CategoryStruct.id (R.over U)))

Extension by zero from a lower interval of a preorder site preserves finite limits and is therefore exact.

instance SheafOfModules.preservesInjectiveObjects_overFunctor {P : Type u} [Preorder P] {J : CategoryTheory.GrothendieckTopology P} (R : CategoryTheory.Sheaf J RingCat) (U : P) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : (overFunctor R U).PreservesInjectiveObjects

Restricting an injective sheaf of modules to a lower interval of a preorder site gives an injective sheaf of modules.