The shift identities of the graded Ext-Euler characteristic

Let C be a k-linear abelian category with a grading shift e : C ≌ C, written {1}. The q-Euler characteristic χ_q(X, Y) = ∑ n,j (-1)^n q⁻ʲ dim_k Ext^n(X, Y{j}) of TauCeti.gradedExtEuler is q-linear in its second argument and q-antilinear in its first:

χ_q(X, Y{1}) = q · χ_q(X, Y),        χ_q(X{1}, Y) = q⁻¹ · χ_q(X, Y).

These are the generating identities behind the sesquilinearity of the q-Euler form, and they fix the handedness of the internal grading.

Both identities come from a reindexing of the internal degree. Shifting the target by one identifies Ext^{n,j}(X, Y{1}) with Ext^{n,j+1}(X, Y), which multiplies the target-shift graded dimension by q; shifting the source instead identifies Ext^{n,j}(X{1}, Y) with Ext^{n,j-1}(X, Y) and multiplies it by q⁻¹. The source identity uses that Ext is invariant under the equivalence e, so it needs e to be k-linear and not merely additive: an additive isomorphism of k-vector spaces need not preserve dimension. The comparison of e ^ (j + 1) with the composites e ^ j ∘ e and e ∘ e ^ j is CategoryTheory.Equivalence.powSuccIso and CategoryTheory.Equivalence.powSuccRightIso.

Every identity below takes a single admissibility witness, for the unshifted pair: the shifted witness it needs is the one this file constructs from it.

Main definitions

• TauCeti.shiftSourceObjIso: the comparison (Y{j-1}){1} ≅ Y{j} through which a source shift is moved into the internal degree.
• TauCeti.gradedExtShiftTargetEquiv: Ext^{n,j}(X, Y{1}) ≃ₗ[k] Ext^{n,j+1}(X, Y).
• TauCeti.gradedExtShiftTargetInverseEquiv: Ext^{n,j}(X, Y{-1}) ≃ₗ[k] Ext^{n,j-1}(X, Y).
• TauCeti.gradedExtShiftSourceEquiv: Ext^{n,j}(X{1}, Y) ≃ₗ[k] Ext^{n,j-1}(X, Y).
• TauCeti.gradedExtShiftSourceInverseEquiv: Ext^{n,j}(X{-1}, Y) ≃ₗ[k] Ext^{n,j+1}(X, Y).

Main results

• TauCeti.IsGradedEulerAdmissible.shiftTarget and TauCeti.IsGradedEulerAdmissible.shiftSource: graded Euler-admissibility is preserved by the grading shift in either variable; TauCeti.IsGradedEulerAdmissible.shiftTargetInverse and TauCeti.IsGradedEulerAdmissible.shiftSourceInverse are the same for the inverse shift.
• TauCeti.gradedExtEuler_shiftTarget: χ_q(X, Y{1}) = q · χ_q(X, Y).
• TauCeti.gradedExtEuler_shiftSource: χ_q(X{1}, Y) = q⁻¹ · χ_q(X, Y).
• TauCeti.gradedExtEuler_shiftTargetInverse and TauCeti.gradedExtEuler_shiftSourceInverse: the two identities for the inverse shift {-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 the q-antilinear/q-linear convention of the q-Euler form.

Shifting the target

Nothing in this section needs the shift to be additive or linear: the reindexing is induced by an isomorphism of objects. The two reindexing equivalences need only a commutative ring of scalars; k is a field only from the point where dimensions are taken.

noncomputable def TauCeti.gradedExtShiftTargetEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (k : Type t) (e : C ≌ C) [CommRing k] [CategoryTheory.Linear k C] (X Y : C) (n : ℕ) (j : ℤ) : GradedExt e X (e.functor.obj Y) n j ≃ₗ[k] GradedExt e X Y n (j + 1)

Shifting the target of a bigraded Ext group raises its internal degree by one: Ext^{n,j}(X, Y{1}) ≅ Ext^{n,j+1}(X, Y).

Equations

• TauCeti.gradedExtShiftTargetEquiv k e X Y n j = TauCeti.extLinearEquivOfIso k (CategoryTheory.Iso.refl X) ((e.powSuccIso j).app Y).symm n

@[simp]

theorem TauCeti.gradedExtShiftTargetEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (k : Type t) (e : C ≌ C) [CommRing k] [CategoryTheory.Linear k C] (X Y : C) (n : ℕ) (j : ℤ) (x : GradedExt e X (e.functor.obj Y) n j) : (gradedExtShiftTargetEquiv k e X Y n j) x = CategoryTheory.Abelian.Ext.comp x (CategoryTheory.Abelian.Ext.mk₀ ((e.powSuccIso j).app Y).inv) ⋯

TauCeti.gradedExtShiftTargetEquiv composes with the comparison isomorphism (Y{1}){j} ≅ Y{j+1}.

noncomputable def TauCeti.gradedExtShiftTargetInverseEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (k : Type t) (e : C ≌ C) [CommRing k] [CategoryTheory.Linear k C] (X Y : C) (n : ℕ) (j : ℤ) : GradedExt e X (e.inverse.obj Y) n j ≃ₗ[k] GradedExt e X Y n (j - 1)

Shifting the target by the inverse shift lowers the internal degree by one: Ext^{n,j}(X, Y{-1}) ≅ Ext^{n,j-1}(X, Y).

Equations

• TauCeti.gradedExtShiftTargetInverseEquiv k e X Y n j = TauCeti.extLinearEquivOfIso k (CategoryTheory.Iso.refl X) ((e.powPredIso j).app Y) n

@[simp]

theorem TauCeti.gradedExtShiftTargetInverseEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (k : Type t) (e : C ≌ C) [CommRing k] [CategoryTheory.Linear k C] (X Y : C) (n : ℕ) (j : ℤ) (x : GradedExt e X (e.inverse.obj Y) n j) : (gradedExtShiftTargetInverseEquiv k e X Y n j) x = CategoryTheory.Abelian.Ext.comp x (CategoryTheory.Abelian.Ext.mk₀ ((e.powPredIso j).app Y).hom) ⋯

TauCeti.gradedExtShiftTargetInverseEquiv composes with the comparison isomorphism (Y{-1}){j} ≅ Y{j-1}.

theorem TauCeti.HasFiniteLaurentSupport.gradedExtShiftTarget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] {X Y : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) : HasFiniteLaurentSupport k (GradedExt e X (e.functor.obj Y) n)

Finite Laurent support in one cohomological degree is preserved by shifting the target.

theorem TauCeti.HasFiniteLaurentSupport.gradedExtShiftTargetInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] {X Y : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) : HasFiniteLaurentSupport k (GradedExt e X (e.inverse.obj Y) n)

Finite Laurent support in one cohomological degree is preserved by the inverse shift of the target.

theorem TauCeti.IsGradedExtInternallyFinite.shiftTarget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) : IsGradedExtInternallyFinite k e X (e.functor.obj Y)

Finite internal support of bigraded Ext is preserved by shifting the target.

theorem TauCeti.IsGradedExtInternallyFinite.shiftTargetInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) : IsGradedExtInternallyFinite k e X (e.inverse.obj Y)

Finite internal support of bigraded Ext is preserved by the inverse shift of the target.

theorem TauCeti.IsGradedExtBoundedBy.shiftTarget {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) : IsGradedExtBoundedBy e X (e.functor.obj Y) N

A cohomological vanishing bound is preserved by shifting the target.

theorem TauCeti.IsGradedExtBoundedBy.shiftTargetInverse {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) : IsGradedExtBoundedBy e X (e.inverse.obj Y) N

A cohomological vanishing bound is preserved by the inverse shift of the target.

theorem TauCeti.IsGradedExtBounded.shiftTarget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {X Y : C} (h : IsGradedExtBounded e X Y) : IsGradedExtBounded e X (e.functor.obj Y)

Eventual cohomological vanishing of bigraded Ext is preserved by shifting the target.

theorem TauCeti.IsGradedExtBounded.shiftTargetInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {X Y : C} (h : IsGradedExtBounded e X Y) : IsGradedExtBounded e X (e.inverse.obj Y)

Eventual cohomological vanishing of bigraded Ext is preserved by the inverse shift of the target.

theorem TauCeti.IsGradedEulerAdmissible.shiftTarget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] {X Y : C} (h : IsGradedEulerAdmissible k e X Y) : IsGradedEulerAdmissible k e X (e.functor.obj Y)

Graded Euler-admissibility is preserved by shifting the target.

theorem TauCeti.IsGradedEulerAdmissible.shiftTargetInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] {X Y : C} (h : IsGradedEulerAdmissible k e X Y) : IsGradedEulerAdmissible k e X (e.inverse.obj Y)

Graded Euler-admissibility is preserved by the inverse shift of the target.

theorem TauCeti.gradedExtDimension_shiftTarget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] {X Y : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) : gradedExtDimension k e ⋯ = LaurentPolynomial.T 1 * gradedExtDimension k e h

Shifting the target multiplies the graded Ext dimension in one cohomological degree by q.

theorem TauCeti.gradedExtEuler_shiftTarget {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] {X Y : C} (h : IsGradedEulerAdmissible k e X Y) : gradedExtEuler k e ⋯ = LaurentPolynomial.T 1 * gradedExtEuler k e h

χ_q(X, Y{1}) = q · χ_q(X, Y): the q-Euler characteristic is q-linear in its second argument.

theorem TauCeti.gradedExtEuler_shiftTargetInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] {X Y : C} (h : IsGradedEulerAdmissible k e X Y) : gradedExtEuler k e ⋯ = LaurentPolynomial.T (-1) * gradedExtEuler k e h

χ_q(X, Y{-1}) = q⁻¹ · χ_q(X, Y): the inverse shift of the second argument.

Shifting the source

The source identity uses that Ext is invariant under e, so e must be k-linear and not merely additive. As for the target, the two reindexing equivalences need only a commutative ring of scalars.

noncomputable def TauCeti.shiftSourceObjIso {C : Type u} [CategoryTheory.Category.{v, u} C] (e : C ≌ C) (Y : C) (j : ℤ) : e.functor.obj ((e ^ (j - 1)).functor.obj Y) ≅ (e ^ j).functor.obj Y

The comparison (Y{j-1}){1} ≅ Y{j}, which moves a source shift into the internal degree.

Equations

• TauCeti.shiftSourceObjIso e Y j = ((e.powSuccRightIso (j - 1)).app Y).symm ≪≫ CategoryTheory.eqToIso ⋯

noncomputable def TauCeti.gradedExtShiftSourceEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (k : Type t) (e : C ≌ C) [CommRing k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (X Y : C) (n : ℕ) (j : ℤ) : GradedExt e (e.functor.obj X) Y n j ≃ₗ[k] GradedExt e X Y n (j - 1)

Shifting the source of a bigraded Ext group lowers its internal degree by one: Ext^{n,j}(X{1}, Y) ≅ Ext^{n,j-1}(X, Y).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.gradedExtShiftSourceEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (k : Type t) (e : C ≌ C) [CommRing k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (X Y : C) (n : ℕ) (j : ℤ) (x : GradedExt e X Y n (j - 1)) : (gradedExtShiftSourceEquiv k e X Y n j).symm x = (CategoryTheory.Abelian.Ext.mapExactFunctor e.functor x).comp (CategoryTheory.Abelian.Ext.mk₀ (shiftSourceObjIso e Y j).hom) ⋯

The inverse of TauCeti.gradedExtShiftSourceEquiv transports along e and then composes with the comparison isomorphism (Y{j-1}){1} ≅ Y{j}; this is the direction in which the equivalence is built.

noncomputable def TauCeti.gradedExtShiftSourceInverseEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (k : Type t) (e : C ≌ C) [CommRing k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (X Y : C) (n : ℕ) (j : ℤ) : GradedExt e (e.inverse.obj X) Y n j ≃ₗ[k] GradedExt e X Y n (j + 1)

Shifting the source by the inverse shift raises the internal degree by one: Ext^{n,j}(X{-1}, Y) ≅ Ext^{n,j+1}(X, Y).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.gradedExtShiftSourceInverseEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (k : Type t) (e : C ≌ C) [CommRing k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] (X Y : C) (n : ℕ) (j : ℤ) (x : GradedExt e (e.inverse.obj X) Y n j) : (gradedExtShiftSourceInverseEquiv k e X Y n j) x = (CategoryTheory.Abelian.Ext.mk₀ (e.counitIso.app X).inv).comp ((CategoryTheory.Abelian.Ext.mapExactFunctor e.functor x).comp (CategoryTheory.Abelian.Ext.mk₀ ((e.powSuccRightIso j).app Y).inv) ⋯) ⋯

TauCeti.gradedExtShiftSourceInverseEquiv transports along e and then composes with the counit and the comparison isomorphism (Y{j}){1} ≅ Y{j+1}.

theorem TauCeti.HasFiniteLaurentSupport.gradedExtShiftSource {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {X Y : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) : HasFiniteLaurentSupport k (GradedExt e (e.functor.obj X) Y n)

Finite Laurent support in one cohomological degree is preserved by shifting the source.

theorem TauCeti.HasFiniteLaurentSupport.gradedExtShiftSourceInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {X Y : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) : HasFiniteLaurentSupport k (GradedExt e (e.inverse.obj X) Y n)

Finite Laurent support in one cohomological degree is preserved by the inverse shift of the source.

theorem TauCeti.IsGradedExtInternallyFinite.shiftSource {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) : IsGradedExtInternallyFinite k e (e.functor.obj X) Y

Finite internal support of bigraded Ext is preserved by shifting the source.

theorem TauCeti.IsGradedExtInternallyFinite.shiftSourceInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {X Y : C} (h : IsGradedExtInternallyFinite k e X Y) : IsGradedExtInternallyFinite k e (e.inverse.obj X) Y

Finite internal support of bigraded Ext is preserved by the inverse shift of the source.

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

A cohomological vanishing bound is preserved by shifting the source.

theorem TauCeti.IsGradedExtBoundedBy.shiftSourceInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} [e.functor.Additive] {X Y : C} {N : ℕ} (h : IsGradedExtBoundedBy e X Y N) : IsGradedExtBoundedBy e (e.inverse.obj X) Y N

A cohomological vanishing bound is preserved by the inverse shift of the source.

theorem TauCeti.IsGradedExtBounded.shiftSource {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} [e.functor.Additive] {X Y : C} (h : IsGradedExtBounded e X Y) : IsGradedExtBounded e (e.functor.obj X) Y

Eventual cohomological vanishing of bigraded Ext is preserved by shifting the source.

theorem TauCeti.IsGradedExtBounded.shiftSourceInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} [e.functor.Additive] {X Y : C} (h : IsGradedExtBounded e X Y) : IsGradedExtBounded e (e.inverse.obj X) Y

Eventual cohomological vanishing of bigraded Ext is preserved by the inverse shift of the source.

theorem TauCeti.IsGradedEulerAdmissible.shiftSource {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {X Y : C} (h : IsGradedEulerAdmissible k e X Y) : IsGradedEulerAdmissible k e (e.functor.obj X) Y

Graded Euler-admissibility is preserved by shifting the source.

theorem TauCeti.IsGradedEulerAdmissible.shiftSourceInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {X Y : C} (h : IsGradedEulerAdmissible k e X Y) : IsGradedEulerAdmissible k e (e.inverse.obj X) Y

Graded Euler-admissibility is preserved by the inverse shift of the source.

theorem TauCeti.gradedExtDimension_shiftSource {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {X Y : C} {n : ℕ} (h : HasFiniteLaurentSupport k (GradedExt e X Y n)) : gradedExtDimension k e ⋯ = LaurentPolynomial.T (-1) * gradedExtDimension k e h

Shifting the source multiplies the graded Ext dimension in one cohomological degree by q⁻¹.

theorem TauCeti.gradedExtEuler_shiftSource {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {X Y : C} (h : IsGradedEulerAdmissible k e X Y) : gradedExtEuler k e ⋯ = LaurentPolynomial.T (-1) * gradedExtEuler k e h

χ_q(X{1}, Y) = q⁻¹ · χ_q(X, Y): the q-Euler characteristic is q-antilinear in its first argument.

theorem TauCeti.gradedExtEuler_shiftSourceInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {k : Type t} {e : C ≌ C} [Field k] [CategoryTheory.Linear k C] [e.functor.Additive] [CategoryTheory.Functor.Linear k e.functor] {X Y : C} (h : IsGradedEulerAdmissible k e X Y) : gradedExtEuler k e ⋯ = LaurentPolynomial.T 1 * gradedExtEuler k e h

χ_q(X{-1}, Y) = q · χ_q(X, Y): the inverse shift of the first argument.