Ext-finiteness from quotient generators

This file isolates the degreewise homological-algebra reduction used by coherent-sheaf applications. Suppose every object in a class is the quotient of an object whose Ext groups against the class are finite-dimensional, with kernel still in the class. The contravariant long exact Ext sequence then proves finite-dimensionality for every pair in the class, by induction on the Ext degree.

The conclusion is deliberately only degreewise finiteness. It does not manufacture a uniform Ext-amplitude or finite support in the degree variable; those require a separate geometric input before DerivedCategory.ExtFiniteBounded.of_ext can be applied.

Main results

• Abelian.Ext.biproductLinearEquiv refines the additive finite-biproduct comparison to a linear equivalence;
• Abelian.Ext.module_finite_coproduct_left propagates Ext-finiteness from finitely many summands to their coproduct;
• Abelian.Ext.module_finite_of_quotient_generators performs the degreewise dévissage.

noncomputable def CategoryTheory.Abelian.Ext.biproductLinearEquiv {k : Type t} [Field k] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear k C] [HasExt C] {J : Type u_1} [Fintype J] {X : J → C} {c : Limits.Bicone X} (hc : c.IsBilimit) (Y : C) (n : ℕ) : Ext c.pt Y n ≃ₗ[k] (j : J) → Ext (X j) Y n

The standard comparison from Ext out of a finite biproduct is linear.

Equations

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

theorem CategoryTheory.Abelian.Ext.module_finite_coproduct_left {k : Type t} [Field k] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear k C] [HasExt C] {J : Type u_1} [Fintype J] (X : J → C) (Y : C) (n : ℕ) [∀ (j : J), Module.Finite k (Ext (X j) Y n)] : Module.Finite k (Ext (∐ X) Y n)

Ext out of a finite coproduct is finite-dimensional when Ext out of every summand is.

theorem CategoryTheory.Abelian.Ext.module_finite_of_quotient_generators {k : Type t} [Field k] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear k C] [HasExt C] (Q : ObjectProperty C) (hpresentation : ∀ (X : C), Q X → ∃ (S : ShortComplex C) (_ : S.ShortExact) (x : S.X₃ ≅ X), Q S.X₁ ∧ ∀ (Y : C), Q Y → ∀ (n : ℕ), Module.Finite k (Ext S.X₂ Y n)) (X Y : C) (hX : Q X) (hY : Q Y) (n : ℕ) : Module.Finite k (Ext X Y n)

Degreewise Ext-finiteness from quotient generators.

For each object satisfying Q, the hypothesis supplies a short exact sequence K ⟶ G ⟶ X with Q K, and asks that Ext out of G against every object satisfying Q be finite-dimensional in every degree. Exactness gives the induction step

Extⁿ(K,Y) ⟶ Extⁿ⁺¹(X,Y) ⟶ Extⁿ⁺¹(G,Y).

In degree zero, the epimorphism G ⟶ X makes Hom(X,Y) ⟶ Hom(G,Y) injective. No projectivity, resolution, boundedness, or finite-support claim is used.