Hom-finiteness of a bounded derived category from Ext-finiteness

This file isolates the exact heart-level input needed to prove HomFiniteBounded k (DerivedCategory.Bounded A). The input says that the derived Ext spaces between degree-zero single objects are finite-dimensional and have finite support. A two-variable bounded induction then propagates those facts across distinguished triangles.

For an abelian category, ExtFiniteBounded.of_ext reduces this input to the usual nonnegative groups Abelian.Ext X Y n: negative shifted Homs vanish by the canonical t-structure, while Abelian.Ext.homLinearEquiv handles nonnegative degrees.

Geometric boundary

For A = Coh X, neither Serre finiteness of coherent cohomology nor CoherentExtComparison X alone proves the hypotheses of of_ext. A smooth projective application still has to prove that every coherent-sheaf Ext group is finite-dimensional and that these groups vanish in sufficiently high degree (for a K3 surface, regularity should give the sharp amplitude). This file makes that remaining obligation explicit; it does not install a geometric instance or assume a bounded resolution.

theorem Module.Finite.of_exact_middle {k : Type t} [DivisionRing k] {U : Type u} {V : Type v} {W : Type w} [AddCommGroup U] [AddCommGroup V] [AddCommGroup W] [Module k U] [Module k V] [Module k W] (f : U →ₗ[k] V) (g : V →ₗ[k] W) (h : Function.Exact ⇑f ⇑g) [Module.Finite k U] [Module.Finite k W] : Module.Finite k V

If U ⟶ V ⟶ W is exact and the outer vector spaces are finite-dimensional, then so is the middle vector space.

class DerivedCategory.ExtFiniteBounded {k : Type t} [DivisionRing k] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] [HasDerivedCategory A] : Prop

Heart-level properness: derived Ext spaces between degree-zero single objects are finite-dimensional and only finitely many shifts contribute.

The uniform ℤ-grading is the form consumed by triangulated dévissage. Use ExtFiniteBounded.of_ext to construct it from the usual nonnegative Abelian.Ext groups.

• finite (X Y : A) (i : ℤ) : Module.Finite k (CategoryTheory.ShiftedHom ((singleFunctor A 0).obj X) ((singleFunctor A 0).obj Y) i)

  Every shifted Ext space between heart objects is finite-dimensional.

• support_finite (X Y : A) : (Function.support fun (i : ℤ) => ↑(Module.finrank k (CategoryTheory.ShiftedHom ((singleFunctor A 0).obj X) ((singleFunctor A 0).obj Y) i))).Finite

  Only finitely many shifted Ext spaces between a fixed pair contribute.

theorem DerivedCategory.ExtFiniteBounded.of_ext {k : Type t} [DivisionRing k] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] [HasDerivedCategory A] (hfinite : ∀ (X Y : A) (n : ℕ), Module.Finite k (CategoryTheory.Abelian.Ext X Y n)) (hsupport : ∀ (X Y : A), (Function.support fun (n : ℕ) => ↑(Module.finrank k (CategoryTheory.Abelian.Ext X Y n))).Finite) : ExtFiniteBounded

Construct heart-level properness from finite-dimensional ordinary Ext groups with finite support. Negative shifted Homs vanish formally from the canonical t-structure.

structure DerivedCategory.HomFiniteBoundedPair {k : Type t} [DivisionRing k] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] [HasDerivedCategory A] (X Y : DerivedCategory A) : Prop

The pairwise version of HomFiniteBounded, used while dévissing one variable at a time.

• finite (i : ℤ) : Module.Finite k (X ⟶ (CategoryTheory.shiftFunctor (DerivedCategory A) i).obj Y)
• support_finite : (Function.support fun (i : ℤ) => ↑(Module.finrank k (X ⟶ (CategoryTheory.shiftFunctor (DerivedCategory A) i).obj Y))).Finite

theorem DerivedCategory.HomFiniteBoundedPair.of_iso {k : Type t} [DivisionRing k] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] [HasDerivedCategory A] {X Y X' Y' : DerivedCategory A} (h : X.HomFiniteBoundedPair Y) (eX : X ≅ X') (eY : Y ≅ Y') : X'.HomFiniteBoundedPair Y'

HomFiniteBoundedPair is invariant under isomorphism in both variables.

theorem DerivedCategory.HomFiniteBoundedPair.shift {k : Type t} [DivisionRing k] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] [HasDerivedCategory A] {X Y : DerivedCategory A} (h : X.HomFiniteBoundedPair Y) (s t : ℤ) : ((CategoryTheory.shiftFunctor (DerivedCategory A) s).obj X).HomFiniteBoundedPair ((CategoryTheory.shiftFunctor (DerivedCategory A) t).obj Y)

HomFiniteBoundedPair is invariant under independent shifts of its two objects.

theorem DerivedCategory.HomFiniteBoundedPair.obj₂_right {k : Type t} [DivisionRing k] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] [HasDerivedCategory A] {X : DerivedCategory A} (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory A)) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : X.HomFiniteBoundedPair T.obj₁) (h₃ : X.HomFiniteBoundedPair T.obj₃) : X.HomFiniteBoundedPair T.obj₂

Pairwise Hom-finiteness is closed under the middle object of a distinguished triangle in the second variable.

theorem DerivedCategory.HomFiniteBoundedPair.obj₂_left {k : Type t} [DivisionRing k] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] [HasDerivedCategory A] {Y : DerivedCategory A} (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory A)) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : T.obj₁.HomFiniteBoundedPair Y) (h₃ : T.obj₃.HomFiniteBoundedPair Y) : T.obj₂.HomFiniteBoundedPair Y

Pairwise Hom-finiteness is closed under the middle object of a distinguished triangle in the first variable.

theorem DerivedCategory.homFiniteBoundedPair_of_bounded {k : Type t} [DivisionRing k] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] [HasDerivedCategory A] [ExtFiniteBounded] {E E' : DerivedCategory A} (hE : TStructure.t.bounded E) (hE' : TStructure.t.bounded E') : E.HomFiniteBoundedPair E'

Heart-level Ext-finiteness propagates to every pair of bounded derived objects.

theorem DerivedCategory.homFiniteBounded_boundedDerived {k : Type t} [DivisionRing k] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear k A] [HasDerivedCategory A] [ExtFiniteBounded] : CategoryTheory.Triangulated.HomFiniteBounded k (Bounded A)

Bounded derived Hom-finiteness from heart Ext-finiteness.

This is a named theorem rather than a global instance so geometric callers must choose and expose the heart-level input explicitly.