Module-sheaf pushforward along a closed immersion #
An inducing map has faithful module-sheaf pushforward: every source open is the preimage of its canonical target open, so equality after pushforward detects every component of a module-sheaf morphism. For a closed immersion this makes the pullback/pushforward adjunction counit epic.
The underlying abelian-sheaf pushforward along a closed embedding is also exact. This file
transports that theorem through the faithful, exact, and epi-reflecting forgetful functor at the
neutral Scheme.Modules layer. The results are registered on Mathlib's existing functors, so
every generic exact or adjunction construction uses the common API directly.
Module-sheaf pushforward is faithful when the underlying continuous map is inducing.
For a source open U, hf.functorObj U is a target open whose preimage is exactly U.
Evaluating equality of pushed-forward morphisms there recovers equality of their components on
U.
Module-sheaf pushforward along a closed immersion is faithful.
Every component of the module-sheaf pullback/pushforward counit along a closed immersion is epic. This uses only faithfulness of the right adjoint, not the stronger standard assertion that the counit is an isomorphism.
Module-sheaf pushforward along a closed immersion preserves epimorphisms.
Module-sheaf pushforward along a closed immersion preserves homology.
Module-sheaf pushforward along a closed immersion preserves finite colimits.
Pushing a short exact sequence through a closed immersion remains short exact.
The generic filtration adapter now applies without a geometric wrapper.