Documentation

DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Pushforward.Finite

Coherent pushforward along a finite morphism #

For a finite morphism f : X ⟶ Y into a locally Noetherian scheme, f_* sends coherent sheaves to coherent sheaves and is exact on them. This file proves both and packages the result as the functor Coh.pushforward f : Coh X ⥤ Coh Y, the f_* on coherent sheaves that the derived direct image on Dᵇ(Coh) is built from. A closed immersion is finite (Mathlib's instance in Mathlib/AlgebraicGeometry/Morphisms/Finite.lean), so #572 step 2, coherence of ι_* F along a closed immersion, is the theorem isCoherent_pushforward here.

Main definitions #

Main results #

The three inputs to coherence, and what each was missing #

Every ingredient existed before the closed-immersion version of this argument; none of them fitted the next one without a bridge, and the same three bridges serve the finite case.

The affine case is a factorisation, not an induction: Scheme.isoSpec_inv_naturality gives f = X.isoSpec.hom ≫ Spec.map f.appTop ≫ Y.isoSpec.inv, and Modules.pushforward of a composite is the composite of pushforwards by rfl, so the affine case is three steps with no glue: transport to Spec Γ(X, ⊤) along an isomorphism, apply the affine theorem, transport back. isAffine_of_isAffineHom supplies affineness of X and Scheme.Hom.finite_appTop finiteness of the coordinate-ring map, the two facts a closed immersion used to supply as affineness and surjectivity.

The globalisation is by opens, not by an AffineOpenCover: Modules.isCoherent_iff_restrict_affineOpenCover is the obvious criterion and is not what this file uses. Its members are affine schemes mapping in, and the base-change square is stated for an open U and its U.ι; going straight to IsFinitePresentation.of_coversTop over Y.affineOpens avoids carrying an isomorphism 𝒰.X i ≅ U.toScheme through every step, with Scheme.Opens.opensRange_ι as the slice-versus-restriction bridge and iSup_affineOpens_eq_top as the covering hypothesis.

IsLocallyNoetherian Y is used once per chart, to see that Γ(U.toScheme, ⊤) is Noetherian; X is not assumed Noetherian for coherence and does not need to be. The two spellings _of_finite (a ring map, RingHom.Finite) and IsFinite f (a morphism of schemes) both occur in this directory and follow Mathlib's naming of the two notions.

Exactness #

Exactness is where finite morphisms differ from closed immersions. Pushforward along a closed immersion is exact on every module sheaf; along a finite morphism it is exact only on quasi-coherent sheaves, so Coh.pushforward_preservesFiniteColimits cannot be reflected from the ambient functor. Instead, left exactness is reflected through Coh.ι from pushforward being a right adjoint, and right exactness comes from preservation of epimorphisms, which is pushforward_map_epi_of_isAffineHom on the underlying quasi-coherent sheaves, reflected through Coh.ι; preservesHomology_of_preservesEpis_and_kernels then gives finite colimits.

References #

source
theorem AlgebraicGeometry.Scheme.isCoherent_pushforward_affine {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] [IsFinite f] [IsNoetherianRing ↑(Y.presheaf.obj (Opposite.op ⊤))] (M : X.Modules) (hM : Modules.IsCoherent X M) :
Modules.IsCoherent Y ((Modules.pushforward f).obj M)

The affine case. A finite morphism into an affine scheme with Noetherian coordinate ring pushes coherent sheaves to coherent sheaves. f is factored through Spec.map f.appTop by isoSpec_inv_naturality; the source is affine because f is an affine morphism, and f.appTop is a finite ring map because f is finite (Scheme.Hom.finite_appTop).

source
theorem AlgebraicGeometry.Scheme.isCoherent_restrict_chart {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] [IsFinite f] (M : X.Modules) (hM : Modules.IsCoherent X M) (U : Y.Opens) (hU : IsAffineOpen U) :
SheafOfModules.IsFinitePresentation (((Modules.pushforward f).obj M).restrict U.ι)

One chart. Over an affine open U of Y, the restriction of f_* M is finitely presented: pushforwardRestrictIso turns the restriction of a pushforward into the pushforward of a restriction along f ∣_ U, which is again finite, and the affine case applies.

source
theorem AlgebraicGeometry.Scheme.isCoherent_pushforward {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] [IsFinite f] (M : X.Modules) (hM : Modules.IsCoherent X M) :
Modules.IsCoherent Y ((Modules.pushforward f).obj M)

Coherence is preserved by pushforward along a finite morphism into a locally Noetherian scheme; for a closed immersion this is #572 step 2. The affine opens cover Y, and finite presentation descends along a covering family; each chart is isCoherent_restrict_chart.

source
noncomputable def AlgebraicGeometry.Coh.pushforward {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] [IsFinite f] :
CategoryTheory.Functor (Coh X) (Coh Y)

Pushforward of coherent sheaves along a finite morphism, f_* : Coh X ⥤ Coh Y.

It is module-sheaf pushforward restricted to coherent sheaves, which lands in coherent sheaves by Scheme.isCoherent_pushforward. Finiteness of f buys both coherence of the image and, through affineness, exactness on quasi-coherent sheaves. A proper morphism that is not finite still preserves coherence (Grothendieck's finiteness theorem, Hartshorne III.8.8), but its f_* is not exact, so the functor the paper wants on Dᵇ(Coh) is the derived Rf_*, which the repository does not own.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.Coh.pushforwardCompι {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] [IsFinite f] :
    (pushforward f).comp (ι Y) ≅ (ι X).comp (Scheme.Modules.pushforward f)

    Forgetting coherence after coherent pushforward is module-sheaf pushforward after forgetting coherence. Definitional, since ObjectProperty.liftCompιIso is Iso.refl; recorded because a contract consuming Coh.pushforward asks for the comparison as data.

    Equations
    Instances For
      source
      instance AlgebraicGeometry.Coh.pushforward_preservesFiniteLimits {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] [IsFinite f] [IsLocallyNoetherian X] :
      CategoryTheory.Limits.PreservesFiniteLimits (pushforward f)

      Coherent pushforward along a finite morphism preserves finite limits. Reflected through the fully faithful Coh.ι Y from the composite Coh.ι X ⋙ Modules.pushforward f, where pushforward is a right adjoint; X must be locally Noetherian for Coh.ι X to be left exact. The composite instance is comp_preservesFiniteLimits, a lemma rather than an instance, hence supplied by name.

      source
      instance AlgebraicGeometry.Coh.pushforward_additive {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] [IsFinite f] :
      (pushforward f).Additive

      Coherent pushforward along a finite morphism is additive, reflected through the faithful additive inclusion Coh.ι Y. Needed by Functor.mapDerivedCategory, which asks for additivity separately from exactness.

      source
      instance AlgebraicGeometry.Coh.pushforward_preservesEpimorphisms {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] [IsFinite f] [IsLocallyNoetherian X] :
      (pushforward f).PreservesEpimorphisms

      Coherent pushforward along a finite morphism preserves epimorphisms. This is where finiteness, through affineness, is spent on exactness: an epimorphism of coherent sheaves is an epimorphism of the underlying quasi-coherent sheaves, pushforward_map_epi_of_isAffineHom pushes it forward, and Coh.ι Y reflects it. The finite-presentation instances are stated on (ι X).obj M, the spelling the goal carries, because Coh.ι is a def that instance search does not unfold.

      source
      instance AlgebraicGeometry.Coh.pushforward_preservesFiniteColimits {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] [IsFinite f] [IsLocallyNoetherian X] :
      CategoryTheory.Limits.PreservesFiniteColimits (pushforward f)

      Coherent pushforward along a finite morphism preserves finite colimits: it preserves kernels and epimorphisms, hence homology, hence finite colimits.