Coherent Ext-finiteness from restricted-twist presentations

This file connects the projective presentation lane to the generic quotient-generator dévissage for Ext. It gives two honest reductions:

1. coherent presentations whose middle terms have finite ambient Ext imply degreewise finite ambient Ext between arbitrary coherent sheaves;
2. the restricted-twist presentations constructed by a ProjectivePresentation, together with restricted-twist Ext-finiteness, reduce that hypothesis to the closed-immersion pullback/pushforward counit being epi.

That counit premise is discharged in RestrictedTwistPresentation through faithfulness of closed-immersion pushforward. The reductions here remain useful independently, while module_finite_ambientExt gives their unconditional projective-variety specialization.

Remaining geometric boundary

The restricted-twist premise is discharged by module_finite_restrictedTwistExt, and the counit epimorphism follows without the unavailable stronger comparison ι^* ι_* F ≅ F. Two later geometric obligations remain:

• these theorems concern Ext in X.Modules. Passing to Ext internal to Coh X still requires the non-affine CoherentExtComparison X;
• degreewise finiteness alone does not give the finite degree support required by DerivedCategory.ExtFiniteBounded.of_ext. A geometric regularity/global-dimension bound remains necessary.

Thus the result advances the Serre/Dqc lane as far as the present APIs justify, without assuming Grothendieck boundedness, postulating a class map, or installing a MuHNInput instance.

theorem AlgebraicGeometry.ProjectivePresentation.module_finite_ambientExt_of_coherent_presentations {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (hpresentation : ∀ (F : Coh X), ∃ (S : CategoryTheory.ShortComplex (Coh X)) (_ : S.ShortExact) (x : S.X₃ ≅ F), ∀ (G : Coh X) (n : ℕ), Module.Finite k (CategoryTheory.Abelian.Ext ((Coh.ι X).obj S.X₂) ((Coh.ι X).obj G) n)) (F G : Coh X) (n : ℕ) : Module.Finite k (CategoryTheory.Abelian.Ext ((Coh.ι X).obj F) ((Coh.ι X).obj G) n)

Degreewise ambient Ext-finiteness follows from coherent quotient presentations whose middle terms have finite ambient Ext against every coherent target.

The kernel stays coherent because the presentation lives in Coh X; exactness is transported to X.Modules by the exact inclusion.

theorem AlgebraicGeometry.ProjectivePresentation.module_finite_ambientExt_of_restrictedTwists {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (hcounit : ∀ (F : Coh X), CategoryTheory.Epi ((Scheme.Modules.pullbackPushforwardAdjunction P.embedding).counit.app ((Coh.ι X).obj F))) (htwist : ∀ (N : ℕ), 1 ≤ N → ∀ (G : Coh X) (n : ℕ), Module.Finite k (CategoryTheory.Abelian.Ext ((Coh.ι X).obj (P.restrictedTwist (-↑N))) ((Coh.ι X).obj G) n)) (F G : Coh X) (n : ℕ) : Module.Finite k (CategoryTheory.Abelian.Ext ((Coh.ι X).obj F) ((Coh.ι X).obj G) n)

Projective coherent Ext-finiteness reduced to the two missing restricted-twist inputs.

The counit premise turns Serre's ambient projective-space quotient into a quotient on X. The second premise asks only for degreewise ambient Ext-finiteness from the negative restricted twists that occur in that quotient. Finite coproduct compatibility and the long exact Ext sequence then give the conclusion for all coherent source and target sheaves.

theorem AlgebraicGeometry.ProjectivePresentation.module_finite_ambientExt_of_counit_epi {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (hcounit : ∀ (F : Coh X), CategoryTheory.Epi ((Scheme.Modules.pullbackPushforwardAdjunction P.embedding).counit.app ((Coh.ι X).obj F))) (F G : Coh X) (n : ℕ) : Module.Finite k (CategoryTheory.Abelian.Ext ((Coh.ι X).obj F) ((Coh.ι X).obj G) n)

Projective coherent ambient Ext-finiteness assembled from the closed-immersion counit.

Restricted twists have finite ambient Ext by module_finite_restrictedTwistExt, so the only explicit premise of this reduction is that the pullback/pushforward counit of the chosen projective closed immersion is epi on coherent sheaves. That premise is discharged by Scheme.Modules.pullbackPushforwardAdjunction_counit_epi_of_isClosedImmersion; the theorem below packages the unconditional specialization.

theorem AlgebraicGeometry.ProjectivePresentation.module_finite_ambientExt {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (F G : Coh X) (n : ℕ) : Module.Finite k (CategoryTheory.Abelian.Ext ((Coh.ι X).obj F) ((Coh.ι X).obj G) n)

Ambient Ext between coherent sheaves on a projective variety is finite-dimensional in every degree.

The restricted-twist generator calculation supplies finite Ext for each presentation term, and faithfulness of pushforward along the chosen projective closed immersion makes the adjunction counit epic. This is degreewise finiteness only: no finite cohomological-amplitude claim is made.