Coherence is preserved by pushforward along a finite map of affine schemes

A finite morphism of schemes pushes coherent sheaves to coherent sheaves; #572 step 2 asked for this along a closed immersion. This file proves the affine case, for a finite ring map φ : R ⟶ S, which is where the mathematical content is: everything else is the descent already in Coherent/Descent/Locality.lean and the chart argument in Pushforward/Finite.lean.

Main results

• moduleFinite_gammaPushforward_of_finite, isCoherent_pushforward_of_finite — the finite-ring-map statements.
• moduleFinite_gammaPushforward, isCoherent_pushforward_of_surjective — their surjective corollaries, the closed-immersion case.

The route

Three facts do the work, and all three are at the pin:

• a coherent sheaf on an affine scheme is the tilde of its global sections (Scheme.Modules.isIso_fromTildeΓ_of_isQuasicoherent);
• being a tilde is preserved by pushforward along Spec.map (AlgebraicGeometry.isIso_fromTildeΓ_pushforward);
• the global sections of the pushforward are the global sections of the original, with the base ring acting through φ (AlgebraicGeometry.gammaPushforwardIso).

So the pushforward is the tilde of an R-module, and coherence reduces to that module being finitely generated over R. That is the only place the hypothesis on φ is used, and it is used through Module.Finite R S, so the natural hypothesis is φ.hom.Finite, which is what a finite morphism of schemes supplies chart by chart (Scheme.Hom.finite_appTop). Surjectivity, what a closed immersion supplies, is the corollary isCoherent_pushforward_of_surjective.

Noetherian hypotheses

R must be noetherian: finite generation of the pushed-forward module gives finite presentation only there, and coherence in this repository is finite presentation. S needs no hypothesis — moduleFinite_globalSections reads finiteness straight off the presentation.

theorem AlgebraicGeometry.moduleFinite_gammaPushforward_of_finite {R S : CommRingCat} (φ : R ⟶ S) (hφ : (CommRingCat.Hom.hom φ).Finite) (M : (Spec S).Modules) (hM : Scheme.Modules.IsCoherent (Spec S) M) : Module.Finite ↑R ↑(moduleSpecΓFunctor.obj ((Scheme.Modules.pushforward (Spec.map φ)).obj M))

Global sections of a coherent sheaf stay finitely generated after restriction of scalars along a finite ring map: S is a finite R-module, and finiteness composes down the tower. This is the hypothesis a finite morphism of schemes supplies chart by chart (IsFinite.finite_app); the surjective case below is the closed-immersion special case.

theorem AlgebraicGeometry.moduleFinite_gammaPushforward {R S : CommRingCat} (φ : R ⟶ S) (hφ : Function.Surjective ⇑(CommRingCat.Hom.hom φ)) (M : (Spec S).Modules) (hM : Scheme.Modules.IsCoherent (Spec S) M) : Module.Finite ↑R ↑(moduleSpecΓFunctor.obj ((Scheme.Modules.pushforward (Spec.map φ)).obj M))

The surjective case of moduleFinite_gammaPushforward_of_finite, which is what a closed immersion supplies.

theorem AlgebraicGeometry.isCoherent_pushforward_of_finite {R S : CommRingCat} (φ : R ⟶ S) [IsNoetherianRing ↑R] (hφ : (CommRingCat.Hom.hom φ).Finite) (M : (Spec S).Modules) (hM : Scheme.Modules.IsCoherent (Spec S) M) : Scheme.Modules.IsCoherent (Spec R) ((Scheme.Modules.pushforward (Spec.map φ)).obj M)

Coherence is preserved by pushforward along a finite map of affine schemes.

The tilde identification is what makes this true rather than merely plausible: the pushforward is not coherent because coherence is somehow local along φ, it is coherent because it is the tilde of a finitely generated module over a noetherian ring.

theorem AlgebraicGeometry.isCoherent_pushforward_of_surjective {R S : CommRingCat} (φ : R ⟶ S) [IsNoetherianRing ↑R] (hφ : Function.Surjective ⇑(CommRingCat.Hom.hom φ)) (M : (Spec S).Modules) (hM : Scheme.Modules.IsCoherent (Spec S) M) : Scheme.Modules.IsCoherent (Spec R) ((Scheme.Modules.pushforward (Spec.map φ)).obj M)

Coherence is preserved by pushforward along an affine closed immersion, the surjective case of isCoherent_pushforward_of_finite.