Restriction of module sheaves preserves limits

Restriction along an open immersion has a left adjoint, given by sheafifying the corresponding presheaf pullback along the functor taking an open to its image. It therefore preserves limits, in addition to preserving colimits by Mathlib's restriction--pushforward adjunction. In particular, ambient kernels can be computed after restriction to an open subscheme.

The adjunction is Mathlib's SheafOfModules.PullbackConstruction.adjunction; the underlying presheaf right adjoint is PresheafOfModules.instIsRightAdjointPushforward.

instance AlgebraicGeometry.Scheme.Modules.restrictFunctorIsRightAdjoint {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (restrictFunctor f).IsRightAdjoint

Restriction of module sheaves along an open immersion is a right adjoint, so it preserves limits. Its left adjoint is the sheafified presheaf pullback along the open-image functor.

instance AlgebraicGeometry.Scheme.Modules.restrictFunctorAdditive {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (restrictFunctor f).Additive

Restriction along an open immersion is additive. In particular it preserves the zero morphisms used in kernel diagrams.