Exact extension by zero for presheaves of modules

For a presheaf of rings on a preorder, the left adjoint to restriction to a lower interval preserves finite limits. It is extension by zero outside that interval. After sheafification this gives exact extension by zero for sheaves of modules, which makes restriction preserve injectives.

The construction adapts the lower-interval extension in TauCeti.CategoryTheory.PresheafExtensionByZero to the varying scalar rings.

instance PresheafOfModules.isRightAdjoint_pushforward_over {P : Type u} [Preorder P] (R : CategoryTheory.Functor Pᵒᵖ RingCat) (U : P) : (pushforward (CategoryTheory.CategoryStruct.id ((CategoryTheory.Over.forget U).op.comp R))).IsRightAdjoint

Restriction of module presheaves to a lower interval has a left adjoint in arbitrary module universes, given by extension by zero.

instance PresheafOfModules.preservesFiniteLimits_pullback_over {P : Type u} [Preorder P] (R : CategoryTheory.Functor Pᵒᵖ RingCat) (U : P) : CategoryTheory.Limits.PreservesFiniteLimits (pullback (CategoryTheory.CategoryStruct.id ((CategoryTheory.Over.forget U).op.comp R)))

Extension by zero from a lower interval of a preorder preserves finite limits. Together with its left adjoint structure, this makes extension by zero exact.