The q-Euler form at q = 1 against the ungraded Ext-Euler characteristic

Let C be a k-linear abelian category with a grading-shift autoequivalence e, and let D be a k-linear abelian category thought of as C with its grading forgotten along a functor U. Setting q = 1 collapses the internal degrees of

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

into the single alternating sum ∑ n, (-1)ⁿ ∑ j, dim_k Ext^n(X, Y{j}). That is the ordinary Ext-Euler characteristic of the ungraded pair only when the ungraded Ext groups assemble the graded ones, so the identification is not a formal consequence of having a shift: it needs the comparison isomorphisms

⨁ j, Ext^n(X, Y{j}) ≅ Ext^n(X', Y')

as an extra hypothesis, recorded here as TauCeti.IsGradedExtComparison. A pair (X', Y') of objects of D is the intended value (U X, U Y) of such a functor, but nothing below uses U itself, so the predicate is stated for two objects of D directly. Only the isomorphisms themselves are asked for: comparing the two Ext long exact sequences would need them to be compatible with the connecting maps as well, which the numerical identity below does not use.

Under that hypothesis the ungraded pair inherits both halves of Euler-admissibility from the graded one, and TauCeti.IsGradedExtComparison.laurentEval_one_gradedExtEuler identifies the specialization of the q-Euler characteristic at q = 1 with the ordinary Ext-Euler characteristic. The same identity for the packaged sesquilinear form is TauCeti.IsGradedExtComparison.gradedExtEulerSpecialized_one_mk_of_mk_of.

Main definitions

• TauCeti.IsGradedExtComparison: the bigraded Ext groups of a pair in C assemble, degree by cohomological degree, into the ungraded Ext groups of a pair in D.

Main results

• TauCeti.isGradedExtComparison_of_subsingleton_ne: a grading concentrated in a single internal degree admits the shifted pair (X, Y{d}) as a comparison inside the same category.
• TauCeti.IsGradedExtComparison.isEulerAdmissible: a graded Euler-admissible pair has an Euler-admissible comparison pair.
• TauCeti.IsGradedExtComparison.laurentEval_one_gradedExtEuler: χ_q(X, Y) evaluated at q = 1 is χ(X', Y').
• TauCeti.IsGradedExtComparison.gradedExtEulerSpecialized_one_mk_of_mk_of: the same identity for the q-Euler form specialized at q = 1.

References

• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Sections 1.2 and 2.2, for graded Grothendieck groups, the q-Euler form and its specializations.

structure TauCeti.IsGradedExtComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (e : C ≌ C) (X Y : C) (X' Y' : D) : Prop

The bigraded Ext groups of (X, Y) assemble into the ungraded Ext groups of a pair (X', Y'): in every cohomological degree the direct sum over the internal degrees of Ext^n(X, Y{j}) is Ext^n(X', Y').

This is the hypothesis under which a q-Euler form specializes at q = 1 to an ordinary Ext-Euler characteristic. A functor forgetting the grading supplies the intended pairs (U X, U Y); the existence of such a functor, or even of a shift-compatible one, does not by itself supply these isomorphisms.

• nonempty_linearEquiv (n : ℕ) : Nonempty ((DirectSum ℤ fun (j : ℤ) => GradedExt e X Y n j) ≃ₗ[k] CategoryTheory.Abelian.Ext X' Y' n)

  In each cohomological degree the internal degrees add up to the ungraded Ext group.

theorem TauCeti.isGradedExtComparison_of_subsingleton_ne {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} (d : ℤ) (hd : ∀ (n : ℕ) (j : ℤ), j ≠ d → Subsingleton (GradedExt e X Y n j)) : IsGradedExtComparison k e X Y X ((e ^ d).functor.obj Y)

A grading concentrated in a single internal degree admits a shifted comparison pair. If the bigraded Ext groups of (X, Y) vanish in every internal degree other than d, then the surviving degree is the whole direct sum, so (X, Y{d}) is a comparison pair for (X, Y) inside the same category.

theorem TauCeti.IsGradedExtComparison.isExtFinite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {e : C ≌ C} {X Y : C} {X' Y' : D} (hc : IsGradedExtComparison k e X Y X' Y') (h : IsGradedExtInternallyFinite k e X Y) : IsExtFinite k X' Y'

Ext-finiteness of the ungraded pair follows from finiteness of the internal grading: a direct sum of finitely many finite-dimensional spaces is finite-dimensional.

theorem TauCeti.IsGradedExtComparison.isExtBoundedBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {e : C ≌ C} {X Y : C} {X' Y' : D} (hc : IsGradedExtComparison k e X Y X' Y') {N : ℕ} (h : IsGradedExtBoundedBy e X Y N) : IsExtBoundedBy X' Y' N

A uniform cohomological vanishing bound for the bigraded Ext groups bounds the ungraded ones.

theorem TauCeti.IsGradedExtComparison.isEulerAdmissible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {e : C ≌ C} {X Y : C} {X' Y' : D} (hc : IsGradedExtComparison k e X Y X' Y') (h : IsGradedEulerAdmissible k e X Y) : IsEulerAdmissible k X' Y'

Euler-admissibility descends to the comparison pair. Both halves transfer separately: finite internal support gives Ext-finiteness and the uniform cohomological bound gives eventual vanishing.

theorem TauCeti.IsGradedExtComparison.laurentEval_one_truncatedGradedExtEuler {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {e : C ≌ C} {X Y : C} {X' Y' : D} (hc : IsGradedExtComparison k e X Y X' Y') (h : IsGradedExtInternallyFinite k e X Y) (N : ℕ) : (laurentEval 1) (truncatedGradedExtEuler k e h N) = truncatedExtEuler k X' Y' N

Every truncation of the q-Euler sum evaluates at q = 1 to the corresponding truncation of the ungraded alternating sum.

theorem TauCeti.IsGradedExtComparison.laurentEval_one_gradedExtEuler {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {e : C ≌ C} {X Y : C} {X' Y' : D} (hc : IsGradedExtComparison k e X Y X' Y') (h : IsGradedEulerAdmissible k e X Y) : (laurentEval 1) (gradedExtEuler k e h) = extEuler k ⋯

The q-Euler characteristic at q = 1 is the ordinary Ext-Euler characteristic of the comparison pair. The comparison isomorphisms are what make this true: a grading shift alone identifies no graded sum of Ext groups with an ungraded one.

The specialized q-Euler form

theorem TauCeti.IsGradedExtComparison.gradedExtEulerSpecialized_one_mk_of_mk_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (e : C ≌ C) [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (GradedExactStructure.abelian C e).IsExtensionClosed P) (hQ : (GradedExactStructure.abelian C e).IsExtensionClosed Q) (hPshift : P.inverseImage (GradedExactStructure.abelian C e).shift.functor = P) (hQshift : Q.inverseImage (GradedExactStructure.abelian C e).shift.functor = Q) (h : IsGradedEulerAdmissibleOn P Q) (X : P.FullSubcategory) (Y : Q.FullSubcategory) {X' Y' : D} (hc : IsGradedExtComparison k e X.obj Y.obj X' Y') : ((gradedExtEulerSpecialized hP hQ hPshift hQshift h 1) ((LaurentSpecialization.mk 1) (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift) X))) ((LaurentSpecialization.mk 1) (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift) Y)) = extEuler k ⋯

The q-Euler form specialized at q = 1, evaluated on two object classes, is the ordinary Ext-Euler characteristic of any comparison pair for those two objects.