Additivity of the graded Ext-Euler characteristic

The graded Ext-Euler characteristic is additive on short exact sequences in either variable. The proof reads each Laurent coefficient as an ordinary Ext-Euler characteristic: the coefficient of q^j is the Euler characteristic against the target shifted by -j. Ordinary Ext-Euler additivity then applies, after mapping a short exact sequence through the grading shift when the sequence occurs in the second variable. The admissibility of the middle term is supplied by the extension-closure results of TauCeti.Algebra.Homology.EulerCharacteristic.ExtEuler.Graded.Basic.

Main results

• TauCeti.coeff_gradedExtEuler_eq_extEuler: a Laurent coefficient is an ordinary Ext-Euler characteristic against one shifted target.
• TauCeti.gradedExtEuler_shortExact₂ and TauCeti.gradedExtEuler_shortExact₁: additivity on short exact sequences in either variable.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Sections 2.4--2.7, for the long exact Ext sequences underlying ordinary Euler additivity.
• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Section 2.2, for the Laurent-polynomial-valued Ext-Euler form.
• TauCetiRoadmap/GrothendieckEulerForms/README.md, Layer 6, "q-Euler form".

Coefficients and additivity

@[simp]

theorem TauCeti.coeff_gradedExtEuler_eq_extEuler {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 : ℤ) : (gradedExtEuler k e h).coeff j = extEuler k ⋯

The coefficient of q^j in the graded Ext-Euler characteristic is the ordinary Ext-Euler characteristic against the target shifted by -j.

theorem TauCeti.gradedExtEuler_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₃) : gradedExtEuler k e ⋯ = gradedExtEuler k e h₁ + gradedExtEuler k e h₃

The graded Ext-Euler characteristic is additive on a short exact sequence in its second variable.

theorem TauCeti.gradedExtEuler_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) : gradedExtEuler k e ⋯ = gradedExtEuler k e h₁ + gradedExtEuler k e h₃

The graded Ext-Euler characteristic is additive on a short exact sequence in its first variable.