The graded Ext-Euler characteristic

Let C be a k-linear abelian category with a chosen grading-shift autoequivalence e. The bigraded Ext groups of two objects are

Ext^{n,j}(X,Y) = Ext^n(X,Y{j}).

Their q-Euler characteristic is the Laurent polynomial

χ_q(X,Y) = ∑ n, (-1)^n ∑ j, q⁻ʲ dim_k Ext^{n,j}(X,Y).

This construction uses two separate support conditions. For each cohomological degree, the internal-degree family must have finite Laurent support, and the Ext groups must vanish in every internal degree above a common cohomological bound. These conditions are recorded separately by TauCeti.IsGradedExtInternallyFinite and TauCeti.IsGradedExtBounded. Their conjunction TauCeti.IsGradedEulerAdmissible is consumed by TauCeti.gradedExtEuler; no infinite sum or totalized finsum occurs.

The internal-degree convention is inherited from TauCeti.targetShiftGradedDimension: shifting the target by j contributes q⁻ʲ. The characteristic coefficient theorem makes both signs visible and is the supported way to compute the polynomial.

Main definitions

• TauCeti.GradedExt: the bigraded family Ext^n(X,Y{j}).
• TauCeti.IsGradedExtInternallyFinite: finite-dimensionality and finite internal support in each cohomological degree.
• TauCeti.IsGradedExtBoundedBy and TauCeti.IsGradedExtBounded: a uniform cohomological vanishing bound across all internal degrees.
• TauCeti.IsGradedEulerAdmissible: the two support conditions together.
• TauCeti.IsGradedEulerAdmissibleOn: every pair in two object properties is graded Euler-admissible.
• TauCeti.gradedExtDimension: the target-shift graded dimension in one cohomological degree.
• TauCeti.gradedExtEuler: the q-Euler characteristic of an admissible pair.

Main results

• TauCeti.IsGradedEulerAdmissible.isEulerAdmissible: a graded Euler-admissible pair is ordinarily Euler-admissible against every fixed target shift.
• TauCeti.IsGradedEulerAdmissible.of_shortExact₂ and TauCeti.IsGradedEulerAdmissible.of_shortExact₂': graded Euler-admissibility is closed under extensions in the second and the first variable.
• TauCeti.gradedExtEuler_of_iso: the q-Euler characteristic depends only on the isomorphism classes of the two objects.
• TauCeti.isGradedEulerAdmissible_of_projective and TauCeti.gradedExtEuler_projective: graded projective evaluation, χ_q(P, Y) = ∑ j, q⁻ʲ dim_k Hom(P, Y{j}) for projective P.

References

• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Section 2.2, for the bigraded Ext-Euler form and its q-antilinear/q-linear shift convention.
• TauCetiRoadmap/GrothendieckEulerForms/README.md, Layers 5--6, "Graded Ext and graded descent" and "q-Euler form".

@[reducible, inline]

abbrev TauCeti.GradedExt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (e : C ≌ C) (X Y : C) (n : ℕ) (j : ℤ) : Type w

The bigraded Ext group Ext^{n,j}(X,Y) = Ext^n(X,Y{j}), where {j} is the j-fold power of the chosen grading-shift autoequivalence.

Equations

• TauCeti.GradedExt e X Y n j = CategoryTheory.Abelian.Ext X ((e ^ j).functor.obj Y) n

structure TauCeti.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) (X Y : C) : Prop

The internal grading of Ext is finite in each cohomological degree: every Ext^{n,j}(X,Y) is finite-dimensional and, for fixed n, only finitely many internal degrees are nonzero. This says nothing about how many cohomological degrees survive.

• finiteLaurentSupport (n : ℕ) : HasFiniteLaurentSupport k (GradedExt e X Y n)

  Each fixed cohomological degree has finite Laurent support in the internal grading.

structure TauCeti.IsGradedExtBoundedBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (e : C ≌ C) (X Y : C) (N : ℕ) : Prop

The bigraded Ext groups vanish in every internal degree from cohomological degree N on.

• subsingleton ⦃n : ℕ⦄ (hn : N ≤ n) (j : ℤ) : Subsingleton (GradedExt e X Y n j)

  Every internal-degree piece vanishes above the cohomological bound.

structure TauCeti.IsGradedExtBounded {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (e : C ≌ C) (X Y : C) : Prop

The bigraded Ext groups vanish in every internal degree for all sufficiently large cohomological degrees. The bound is uniform in the internal degree.

• exists_bound : ∃ (N : ℕ), IsGradedExtBoundedBy e X Y N

  Some natural number uniformly bounds the cohomological support.

structure TauCeti.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) (X Y : C) : Prop

A pair is graded Euler-admissible when its internal support is finite in each cohomological degree and its cohomological support has a uniform finite bound. The construction of its Laurent-polynomial-valued Ext-Euler characteristic uses these two conditions.

• internallyFinite : IsGradedExtInternallyFinite k e X Y

  Finite-dimensionality and finite internal support in every cohomological degree.

• bounded : IsGradedExtBounded e X Y

  Uniform eventual vanishing in the cohomological degree.

theorem TauCeti.IsGradedExtBoundedBy.mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {X Y : C} {N M : ℕ} (h : IsGradedExtBoundedBy e X Y N) (hNM : N ≤ M) : IsGradedExtBoundedBy e X Y M

A cohomological vanishing bound may always be raised.

theorem TauCeti.IsGradedExtBoundedBy.isGradedExtBounded {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {X Y : C} {N : ℕ} (h : IsGradedExtBoundedBy e X Y N) : IsGradedExtBounded e X Y

An explicit cohomological bound witnesses eventual graded Ext-vanishing.

Admissibility on object properties

structure TauCeti.IsGradedEulerAdmissibleOn {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 Q : CategoryTheory.ObjectProperty C) : Prop

Every pair of objects in P × Q is graded Euler-admissible. The internal-support and cohomological bounds may depend on the pair.

• isGradedEulerAdmissible ⦃X Y : C⦄ (hX : P X) (hY : Q Y) : IsGradedEulerAdmissible k e X Y

  Each pair drawn from P and Q is graded Euler-admissible.

theorem TauCeti.IsGradedEulerAdmissibleOn.mono {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 P' Q Q' : CategoryTheory.ObjectProperty C} (h : IsGradedEulerAdmissibleOn P Q) (hP : P' ≤ P) (hQ : Q' ≤ Q) : IsGradedEulerAdmissibleOn P' Q'

Graded Euler-admissibility on two object properties restricts to smaller properties.

Passage to one internal degree

theorem TauCeti.IsGradedExtInternallyFinite.isExtFinite {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} {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) (j : ℤ) : IsExtFinite k X ((e ^ j).functor.obj Y)

Finite internal support gives ordinary Ext-finiteness against every fixed target shift.

theorem TauCeti.IsGradedExtBoundedBy.isExtBoundedBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {X Y : C} {N : ℕ} (h : IsGradedExtBoundedBy e X Y N) (j : ℤ) : IsExtBoundedBy X ((e ^ j).functor.obj Y) N

A uniform graded Ext bound gives the same ordinary Ext bound against every fixed target shift.

theorem TauCeti.IsGradedEulerAdmissible.isEulerAdmissible {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} {X Y : C} (h : IsGradedEulerAdmissible k e X Y) (j : ℤ) : IsEulerAdmissible k X ((e ^ j).functor.obj Y)

A graded Euler-admissible pair is ordinarily Euler-admissible against each fixed target shift.

Closure under extensions

theorem TauCeti.IsGradedExtInternallyFinite.of_shortExact₂ {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} {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {X : C} (h₁ : IsGradedExtInternallyFinite k e X S.X₁) (h₃ : IsGradedExtInternallyFinite k e X S.X₃) : IsGradedExtInternallyFinite k e X S.X₂

Finite internal support is closed under extensions in the second variable.

theorem TauCeti.IsGradedExtInternallyFinite.of_shortExact₂' {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} {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y : C} (h₁ : IsGradedExtInternallyFinite k e S.X₁ Y) (h₃ : IsGradedExtInternallyFinite k e S.X₃ Y) : IsGradedExtInternallyFinite k e S.X₂ Y

Finite internal support is closed under extensions in the first variable.

theorem TauCeti.IsGradedExtBoundedBy.of_shortExact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {X : C} {N₁ N₃ : ℕ} (h₁ : IsGradedExtBoundedBy e X S.X₁ N₁) (h₃ : IsGradedExtBoundedBy e X S.X₃ N₃) : IsGradedExtBoundedBy e X S.X₂ (max N₁ N₃)

A uniform graded Ext bound is closed under extensions in the second variable.

theorem TauCeti.IsGradedExtBoundedBy.of_shortExact₂' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y : C} {N₁ N₃ : ℕ} (h₁ : IsGradedExtBoundedBy e S.X₁ Y N₁) (h₃ : IsGradedExtBoundedBy e S.X₃ Y N₃) : IsGradedExtBoundedBy e S.X₂ Y (max N₁ N₃)

A uniform graded Ext bound is closed under extensions in the first variable.

theorem TauCeti.IsGradedEulerAdmissible.of_shortExact₂ {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} {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {X : C} (h₁ : IsGradedEulerAdmissible k e X S.X₁) (h₃ : IsGradedEulerAdmissible k e X S.X₃) : IsGradedEulerAdmissible k e X S.X₂

Graded Euler-admissibility is closed under extensions in the second variable.

theorem TauCeti.IsGradedEulerAdmissible.of_shortExact₂' {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} {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y : C} (h₁ : IsGradedEulerAdmissible k e S.X₁ Y) (h₃ : IsGradedEulerAdmissible k e S.X₃ Y) : IsGradedEulerAdmissible k e S.X₂ Y

Graded Euler-admissibility is closed under extensions in the first variable.

The q-Euler value

noncomputable def TauCeti.gradedExtDimension {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) {X Y : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) : LaurentPolynomial ℤ

The Laurent polynomial ∑ j, q⁻ʲ dim_k Ext^{n,j}(X,Y) in one cohomological degree.

Equations

• TauCeti.gradedExtDimension k e h = TauCeti.targetShiftGradedDimension k (TauCeti.GradedExt e X Y n) h

theorem TauCeti.gradedExtDimension_eq_targetShiftGradedDimension {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) {X Y : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) : gradedExtDimension k e h = targetShiftGradedDimension k (GradedExt e X Y n) h

The graded Ext dimension is the target-shift graded dimension of the bigraded family, so the generic reindexing lemmas for TauCeti.targetShiftGradedDimension apply to it.

@[simp]

theorem TauCeti.coeff_gradedExtDimension {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) {X Y : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) (j : ℤ) : (gradedExtDimension k e h).coeff j = ↑(Module.finrank k (GradedExt e X Y n (-j)))

The coefficient of q^j in the graded Ext dimension is dim_k Ext^{n,-j}(X,Y).

noncomputable def TauCeti.truncatedGradedExtEuler {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) {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) (N : ℕ) : LaurentPolynomial ℤ

The q-Euler sum truncated to cohomological degrees below N. The internal sum in every term is genuine because h supplies finite Laurent support.

Equations

• TauCeti.truncatedGradedExtEuler k e h N = ∑ n ∈ Finset.range N, (-1) ^ n • TauCeti.gradedExtDimension k e ⋯

@[simp]

theorem TauCeti.truncatedGradedExtEuler_zero {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) {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) : truncatedGradedExtEuler k e h 0 = 0

The empty truncation of the graded Ext-Euler sum is zero.

@[simp]

theorem TauCeti.truncatedGradedExtEuler_succ {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) {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) (N : ℕ) : truncatedGradedExtEuler k e h (N + 1) = truncatedGradedExtEuler k e h N + (-1) ^ N • gradedExtDimension k e ⋯

Raising the truncation bound by one adds the signed graded dimension in the new degree.

theorem TauCeti.coeff_truncatedGradedExtEuler {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) {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) (N : ℕ) (j : ℤ) : (truncatedGradedExtEuler k e h N).coeff j = ∑ n ∈ Finset.range N, (-1) ^ n * ↑(Module.finrank k (GradedExt e X Y n (-j)))

The coefficient of a truncation is the finite alternating sum of the dimensions in the corresponding internal degree.

theorem TauCeti.truncatedGradedExtEuler_eq_of_le {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) {X Y : C} {N M : ℕ} (hfinite : IsGradedExtInternallyFinite k e X Y) (hbounded : IsGradedExtBoundedBy e X Y N) (hNM : N ≤ M) : truncatedGradedExtEuler k e hfinite M = truncatedGradedExtEuler k e hfinite N

Raising a truncation past a cohomological vanishing bound does not change it.

noncomputable def TauCeti.gradedExtEuler {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) {X Y : C} (h : IsGradedEulerAdmissible k e X Y) : LaurentPolynomial ℤ

The graded Ext-Euler characteristic χ_q(X,Y) = ∑ n,j (-1)^n q⁻ʲ dim_k Ext^{n,j}(X,Y) of a graded Euler-admissible pair.

Equations

• TauCeti.gradedExtEuler k e h = TauCeti.truncatedGradedExtEuler k e ⋯ ⋯.choose

theorem TauCeti.gradedExtEuler_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) {X Y : C} (h : IsGradedEulerAdmissible k e X Y) {N : ℕ} (hN : IsGradedExtBoundedBy e X Y N) : gradedExtEuler k e h = truncatedGradedExtEuler k e ⋯ N

Every valid cohomological vanishing bound computes the graded Ext-Euler characteristic.

theorem TauCeti.coeff_gradedExtEuler {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) {X Y : C} (h : IsGradedEulerAdmissible k e X Y) {N : ℕ} (hN : IsGradedExtBoundedBy e X Y N) (j : ℤ) : (gradedExtEuler k e h).coeff j = ∑ n ∈ Finset.range N, (-1) ^ n * ↑(Module.finrank k (GradedExt e X Y n (-j)))

The coefficient of the q-Euler characteristic is the alternating sum of the dimensions in the opposite internal degree, truncated at any valid cohomological bound.

theorem TauCeti.gradedExtEuler_eq_zero_of_isGradedExtBoundedBy_zero {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) {X Y : C} (h : IsGradedEulerAdmissible k e X Y) (hzero : IsGradedExtBoundedBy e X Y 0) : gradedExtEuler k e h = 0

A pair whose graded Ext groups vanish in every cohomological degree has q-Euler characteristic zero.

Isomorphism invariance

theorem TauCeti.IsGradedExtInternallyFinite.of_iso {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} {X X' Y Y' : C} (h : IsGradedExtInternallyFinite k e X Y) (i : X ≅ X') (j : Y ≅ Y') : IsGradedExtInternallyFinite k e X' Y'

Finite internal support of bigraded Ext depends only on the isomorphism classes of the two objects.

theorem TauCeti.IsGradedExtBoundedBy.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {X X' Y Y' : C} {N : ℕ} (h : IsGradedExtBoundedBy e X Y N) (i : X ≅ X') (j : Y ≅ Y') : IsGradedExtBoundedBy e X' Y' N

A cohomological vanishing bound for bigraded Ext depends only on the isomorphism classes of the two objects.

theorem TauCeti.IsGradedExtBounded.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {X X' Y Y' : C} (h : IsGradedExtBounded e X Y) (i : X ≅ X') (j : Y ≅ Y') : IsGradedExtBounded e X' Y'

Eventual cohomological vanishing of bigraded Ext depends only on the isomorphism classes of the two objects.

theorem TauCeti.IsGradedEulerAdmissible.of_iso {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} {X X' Y Y' : C} (h : IsGradedEulerAdmissible k e X Y) (i : X ≅ X') (j : Y ≅ Y') : IsGradedEulerAdmissible k e X' Y'

Graded Euler-admissibility depends only on the isomorphism classes of the two objects.

theorem TauCeti.gradedExtDimension_of_iso {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} {X X' Y Y' : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) (h' : HasFiniteLaurentSupport k (GradedExt e X' Y' n)) (i : X ≅ X') (j : Y ≅ Y') : gradedExtDimension k e h = gradedExtDimension k e h'

The graded Ext dimension in one cohomological degree is invariant under isomorphisms of the two objects.

theorem TauCeti.truncatedGradedExtEuler_of_iso {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} {X X' Y Y' : C} (h : IsGradedExtInternallyFinite k e X Y) (h' : IsGradedExtInternallyFinite k e X' Y') (i : X ≅ X') (j : Y ≅ Y') (N : ℕ) : truncatedGradedExtEuler k e h N = truncatedGradedExtEuler k e h' N

Every finite truncation of the graded Ext-Euler sum is invariant under isomorphisms of the two objects.

theorem TauCeti.gradedExtEuler_of_iso {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} {X X' Y Y' : C} (h : IsGradedEulerAdmissible k e X Y) (h' : IsGradedEulerAdmissible k e X' Y') (i : X ≅ X') (j : Y ≅ Y') : gradedExtEuler k e h = gradedExtEuler k e h'

The graded Ext-Euler characteristic depends only on the isomorphism classes of the two objects.

Projective evaluation

theorem TauCeti.isGradedEulerAdmissible_of_projective {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 Y : C) [CategoryTheory.Projective P] (h : HasFiniteLaurentSupport k fun (j : ℤ) => P ⟶ (e ^ j).functor.obj Y) : IsGradedEulerAdmissible k e P Y

A projective first entry whose graded Hom spaces Hom(P, Y{j}) have finite Laurent support is graded Euler-admissible: the bigraded Ext groups of positive cohomological degree vanish, and in degree zero they are those Hom spaces.

theorem TauCeti.gradedExtEuler_projective {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 Y : C} [CategoryTheory.Projective P] (h : IsGradedEulerAdmissible k e P Y) : gradedExtEuler k e h = targetShiftGradedDimension k (fun (j : ℤ) => P ⟶ (e ^ j).functor.obj Y) ⋯

Graded projective evaluation: the q-Euler characteristic of a pair with projective first entry is the target-shift graded dimension of its graded Hom spaces, χ_q(P, Y) = ∑ j, q⁻ʲ dim_k Hom(P, Y{j}). The finite Laurent support of these Hom spaces is read off from the degree-zero part of the admissibility witness.