Graded Ext-Euler admissibility from finite resolutions

In a linear abelian category with an internal-shift autoequivalence, a finite resolution by projectives with finitely Laurent-supported graded Hom spaces makes the resolved pair graded Euler-admissible. Internal finiteness propagates through the long exact Ext sequence, while projectivity gives a cohomological bound uniform in every internal degree. These are separate conclusions: internal finiteness alone does not imply eventual Ext-vanishing.

The q-Euler characteristic is the alternating sum of the target-shift graded Hom dimensions of the resolving terms. This computes the Laurent polynomial without choosing cohomological or internal support bounds and shows that the result is independent of the resolution.

Main results

• TauCeti.ExactStructure.FiniteResolution.isGradedExtInternallyFinite: internal finiteness propagates along any finite resolution, without requiring projectivity.
• TauCeti.ExactStructure.FiniteResolution.isGradedExtBoundedBy: a projective resolution of length l gives vanishing from cohomological degree l + 1, in every internal degree.
• TauCeti.ExactStructure.FiniteResolution.isGradedEulerAdmissible: the resulting admissibility criterion using graded Hom-finiteness of the projectives.
• TauCeti.ExactStructure.FiniteResolution.gradedExtEuler_eq_foldAlternating: computation by the alternating graded Hom dimensions.
• TauCeti.ExactStructure.FiniteResolution.foldAlternating_gradedHom_eq: independence of the finite projective resolution and its graded Hom-support witnesses.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Sections 2.4--2.7, for dimension shifting and the long exact Ext sequence.
• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Section 2.2, for the q-Euler form and the target-shift grading convention.

The cohomological bound reuses TauCeti.ExactStructure.FiniteResolution.isExtBoundedBy.

theorem TauCeti.ExactStructure.FiniteResolution.isGradedExtInternallyFinite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {P : CategoryTheory.ObjectProperty C} {X Y : C} (r : (abelian C).FiniteResolution P X) (hfinite : ∀ (Z : C), P Z → IsGradedExtInternallyFinite k e Z Y) : IsGradedExtInternallyFinite k e X Y

Finite internal support of Ext propagates along a finite resolution. No projectivity of its terms is required.

theorem TauCeti.ExactStructure.FiniteResolution.isGradedExtBoundedBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {P : CategoryTheory.ObjectProperty C} {X Y : C} (r : (abelian C).FiniteResolution P X) (hproj : P ≤ (abelian C).isProjective) : IsGradedExtBoundedBy e X Y (r.length + 1)

A finite projective resolution of length l makes Ext vanish from degree l + 1 in all internal degrees. The same bound works against every shift of the target.

theorem TauCeti.ExactStructure.FiniteResolution.isGradedEulerAdmissible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {P : CategoryTheory.ObjectProperty C} {X Y : C} (r : (abelian C).FiniteResolution P X) (hproj : P ≤ (abelian C).isProjective) (hHom : ∀ (Z : C), P Z → HasFiniteLaurentSupport k fun (j : ℤ) => Z ⟶ (e ^ j).functor.obj Y) : IsGradedEulerAdmissible k e X Y

A finite resolution by projectives whose graded Hom spaces into Y have finite Laurent support makes (X,Y) graded Euler-admissible.

theorem TauCeti.ExactStructure.FiniteResolution.gradedExtEuler_eq_foldAlternating {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {P : CategoryTheory.ObjectProperty C} {X Y : C} (r : (abelian C).FiniteResolution P X) (hproj : P ≤ (abelian C).isProjective) (hHom : ∀ (Z : C), P Z → HasFiniteLaurentSupport k fun (j : ℤ) => Z ⟶ (e ^ j).functor.obj Y) : gradedExtEuler k e ⋯ = foldAlternating (fun (Z : C) (hZ : P Z) => targetShiftGradedDimension k (fun (j : ℤ) => Z ⟶ (e ^ j).functor.obj Y) ⋯) r

The q-Euler characteristic computed from a finite projective resolution is the alternating sum of the graded Hom dimensions of its terms, with exponent -j for target shift j.

theorem TauCeti.ExactStructure.FiniteResolution.foldAlternating_gradedHom_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {P : CategoryTheory.ObjectProperty C} {X Y : C} {P' : CategoryTheory.ObjectProperty C} (r : (abelian C).FiniteResolution P X) (s : (abelian C).FiniteResolution P' X) (hproj : P ≤ (abelian C).isProjective) (hHom : ∀ (Z : C), P Z → HasFiniteLaurentSupport k fun (j : ℤ) => Z ⟶ (e ^ j).functor.obj Y) (hproj' : P' ≤ (abelian C).isProjective) (hHom' : ∀ (Z : C), P' Z → HasFiniteLaurentSupport k fun (j : ℤ) => Z ⟶ (e ^ j).functor.obj Y) : foldAlternating (fun (Z : C) (hZ : P Z) => targetShiftGradedDimension k (fun (j : ℤ) => Z ⟶ (e ^ j).functor.obj Y) ⋯) r = foldAlternating (fun (Z : C) (hZ : P' Z) => targetShiftGradedDimension k (fun (j : ℤ) => Z ⟶ (e ^ j).functor.obj Y) ⋯) s

The alternating graded Hom dimension is independent of the finite projective resolution of X, allowing different object properties and finite Laurent-support witnesses.