Affine pushforward of quasicoherent modules #
Pushforward between affine schemes and along an affine morphism preserves quasicoherence,
without finiteness, flatness, or separation assumptions. In particular, the pushforward of
the structure sheaf along an affine morphism is quasicoherent. The spectrum case is supplied by
AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pushforward_specMap in
Pushforward/Basic.lean, based on Mathlib's isIso_fromTildeΓ_pushforward.
References #
- The Stacks Project, Tag 01LC (quasicoherence of pushforward).
instance
TauCeti.AlgebraicGeometry.isQuasicoherent_pushforward_of_isAffineHom
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.IsAffineHom f]
(M : X.Modules)
[SheafOfModules.IsQuasicoherent M]
:
Pushforward along an affine scheme morphism preserves quasicoherence.
No finiteness, flatness, or separation hypothesis is needed.