The q-Euler form at q = 1 on Grothendieck groups

Let C be a k-linear abelian category with a grading-shift autoequivalence e, and let D be an ungraded k-linear abelian category. Suppose conflation-exact functors forget the grading of two shift-stable extension-closed subcategories P and Q of C, landing in extension-closed subcategories P' and Q' of D, and identify the shift with the identity. By TauCeti.LaurentK0.forgetGrading they induce maps from graded K₀, specialized at q = 1, to ungraded K₀.

If, for every pair of objects, the bigraded Ext groups assemble into the ungraded Ext groups of the forgotten pair (TauCeti.IsGradedExtComparison), then the q-Euler form specialized at q = 1 is the ordinary Ext-Euler pairing pulled back along these maps. The object-level identity is TauCeti.IsGradedExtComparison.gradedExtEulerSpecialized_one_mk_of_mk_of; this file extends it to all classes. Shift compatibility alone does not give the identity: the comparison isomorphisms are a genuine hypothesis.

Over a left Noetherian graded algebra, TauCeti.GradedModuleCat.isGradedExtComparison_toModuleCat supplies the comparison isomorphisms for finitely generated graded modules, so the identity holds on G₀^gr(mod A) whenever both forms are defined. Euler-admissibility of all pairs of finitely generated ungraded modules is assumed separately: an ungraded module need not admit a grading, so it does not follow from the graded hypothesis.

Main results

• TauCeti.gradedExtEulerSpecialized_one_eq_extEulerPairing: under the Ext comparison hypothesis, the q-Euler form at q = 1 is the Ext-Euler pairing of the forgotten classes.
• TauCeti.gradedExtEulerSpecialized_one_eq_extEulerPairing_gradedFiniteModules: the same identity on the Grothendieck groups of finitely generated graded modules over a left Noetherian graded algebra.

References

• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Section 2.2, for graded Grothendieck groups, the q-Euler form and its specialization at q = 1.
• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Lecture Notes in Mathematics 1836, Springer (2004), Section 2.4, for the agreement of graded and ungraded Ext of a finitely generated module over a Noetherian graded ring.

theorem TauCeti.gradedExtEulerSpecialized_one_eq_extEulerPairing {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] {P' Q' : CategoryTheory.ObjectProperty D} [CategoryTheory.LocallySmall.{w', v', u'} D] [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) (hP' : (ExactStructure.abelian D).IsExtensionClosed P') (hQ' : (ExactStructure.abelian D).IsExtensionClosed Q') (h' : IsEulerAdmissibleOn k P' Q') {FP : CategoryTheory.Functor P.FullSubcategory P'.FullSubcategory} [FP.Additive] {FQ : CategoryTheory.Functor Q.FullSubcategory Q'.FullSubcategory} [FQ.Additive] (hFP : ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift).IsConflationExact (ExactStructure.fullSubcategory P' hP') FP) (hFQ : ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift).IsConflationExact (ExactStructure.fullSubcategory Q' hQ') FQ) (commP : ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift).shift.functor.comp FP ≅ FP) (commQ : ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift).shift.functor.comp FQ ≅ FQ) (hc : ∀ (X : P.FullSubcategory) (Y : Q.FullSubcategory), IsGradedExtComparison k e X.obj Y.obj (FP.obj X).obj (FQ.obj Y).obj) (x : LaurentSpecialization 1 (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift))) (y : LaurentSpecialization 1 (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift))) : ((gradedExtEulerSpecialized hP hQ hPshift hQshift h 1) x) y = ((extEulerPairing hP' hQ' h') ((LaurentK0.forgetGrading hFP commP) x)) ((LaurentK0.forgetGrading hFQ commQ) y)

The q-Euler form at q = 1 is the ordinary Ext-Euler pairing on Grothendieck groups. Let FP and FQ forget the grading of P and Q, conflation-exactly and compatibly with the grading shift. If for all objects X of P and Y of Q the bigraded Ext groups of (X, Y) assemble into the ungraded Ext groups of (FP X, FQ Y), then the q-Euler form specialized at q = 1 is the Ext-Euler pairing of the classes with their grading forgotten.

theorem TauCeti.gradedExtEulerSpecialized_one_eq_extEulerPairing_gradedFiniteModules {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [GradedAlgebra 𝒜] [IsNoetherianRing A] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] (h : IsGradedEulerAdmissibleOn (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜)) (h' : IsEulerAdmissibleOn k (ModuleCat.isFG A) (ModuleCat.isFG A)) (x y : LaurentSpecialization 1 (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) : ((gradedExtEulerSpecialized ⋯ ⋯ ⋯ ⋯ h 1) x) y = ((extEulerPairing ⋯ ⋯ h') ((finiteModulesExactK0Equiv A) ((gradedFiniteModulesForgetK0 𝒜) x))) ((finiteModulesExactK0Equiv A) ((gradedFiniteModulesForgetK0 𝒜) y))

The q-Euler form of finitely generated graded modules at q = 1 is the ordinary Ext-Euler pairing. Over a left Noetherian graded algebra, if every pair of finitely generated graded modules is graded Euler-admissible and every pair of finitely generated modules is Euler-admissible, then the q-Euler form on G₀^gr(mod A) specialized at q = 1 is the Ext-Euler pairing on G₀(mod A) of the classes with their grading forgotten.