Pushforward along an affine morphism preserves epimorphisms of quasi-coherent sheaves

Pushforward of module sheaves is a right adjoint, so it is left exact on every sheaf; along an affine morphism it is also right exact on quasi-coherent sheaves. This file proves the epimorphism half of that statement, which is what makes the pushforward of coherent sheaves along a finite morphism exact (Modules/Coherent/Pushforward/Finite.lean).

Main results

• Scheme.Modules.isQuasicoherent_pushforward_SpecMap: pushforward along a morphism of affine spectra preserves quasi-coherent module sheaves.
• gammaPushforwardNatIso: global sections identify affine pushforward with restriction of scalars, naturally in the module sheaf.
• Scheme.Modules.pushforward_map_epi_of_isAffineHom: for an affine morphism f and an epimorphism u of quasi-coherent sheaves, f_* u is an epimorphism.

Implementation notes

The statement is about one morphism, not (pushforward f).PreservesEpimorphisms: pushforward along an affine morphism does not preserve epimorphisms of arbitrary module sheaves, so the class would be false; the closed-embedding case where it does hold on every sheaf is pushforward_preservesFiniteColimits_of_isClosedImmersion.

The proof is the pointwise-preimage criterion epi_of_pointwise_preimages: a section of f_* N near a point of Y lives on an affine open W, the preimage f ⁻¹ᵁ W is affine because f is, and surjective_app_of_epi_of_isAffineOpen lifts the section there. The sections of f_* N over W are the sections of N over f ⁻¹ᵁ W by definition, so no comparison isomorphism appears.

References

• Hartshorne, Algebraic Geometry, Exercise II.5.17(b) and (e): an affine morphism identifies quasi-coherent sheaves on the source with quasi-coherent modules over f_* 𝒪_X, of which this is the right-exactness half; the affine-sections input is referenced in Modules/Affine/Epi.lean.

noncomputable def AlgebraicGeometry.gammaPushforwardIso {R S : CommRingCat} (f : R ⟶ S) (M : (Spec S).Modules) : moduleSpecΓFunctor.obj ((Scheme.Modules.pushforward (Spec.map f)).obj M) ≅ (ModuleCat.restrictScalars (CommRingCat.Hom.hom f)).obj (moduleSpecΓFunctor.obj M)

The global sections of a pushforward along Spec.map f, as an R-module, are the global sections of the original with R acting through f.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.gammaPushforwardNatIso {R S : CommRingCat} (f : R ⟶ S) : (Scheme.Modules.pushforward (Spec.map f)).comp moduleSpecΓFunctor ≅ moduleSpecΓFunctor.comp (ModuleCat.restrictScalars (CommRingCat.Hom.hom f))

Global sections identify affine pushforward with restriction of scalars, naturally in the module sheaf.

Equations

• AlgebraicGeometry.gammaPushforwardNatIso f = CategoryTheory.NatIso.ofComponents (AlgebraicGeometry.gammaPushforwardIso f) ⋯

theorem AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pushforward_SpecMap {R S : CommRingCat} (f : R ⟶ S) (M : (Spec S).Modules) [SheafOfModules.IsQuasicoherent M] : SheafOfModules.IsQuasicoherent ((pushforward (Spec.map f)).obj M)

Pushforward along a morphism of affine spectra preserves quasi-coherence. The affine counit remains invertible after pushforward, and on an affine spectrum invertibility of that counit characterizes quasi-coherent module sheaves.

theorem AlgebraicGeometry.Scheme.Modules.pushforward_map_epi_of_isAffineHom {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] {M N : X.Modules} (u : M ⟶ N) [CategoryTheory.Epi u] [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : CategoryTheory.Epi ((pushforward f).map u)

Pushforward along an affine morphism sends an epimorphism of quasi-coherent module sheaves to an epimorphism. Locally on the target, a section over an affine open W is a section of N over the affine open f ⁻¹ᵁ W, where surjective_app_of_epi_of_isAffineOpen lifts it.