The q-Euler form on graded Grothendieck groups

Let P and Q be extension-closed, shift-stable full subcategories of a graded abelian category. The preliminary exact-K₀ descent TauCeti.gradedExtEulerPairing makes the graded Ext-Euler characteristic biadditive on their induced exact Grothendieck groups. The shift identities say that the shift acts on this pairing by q⁻¹ in the first variable and by q in the second. Consequently the pairing upgrades to a map on Laurent-module Grothendieck groups which is semilinear for the involution q ↦ q⁻¹ in the first variable and linear in the second.

The two subcategories are allowed to differ: neither symmetry nor Hermitian symmetry is assumed. The coefficient involution is Mathlib's LaurentPolynomial.invert, and the handedness is fixed by the convention [M{1}] = q[M] on TauCeti.LaurentK0.

Main definitions

• TauCeti.gradedExtEulerSesquilinear: the q-Euler form on the Laurent-module Grothendieck groups of P and Q.
• TauCeti.gradedExtEulerSpecialized: its specialization at q = ε for a unit ε : ℤˣ, that is at q = 1 or q = -1, a ℤ-bilinear form on specialized graded Grothendieck groups.

Main results

• TauCeti.gradedExtEulerSesquilinear_of_of: evaluation on two object classes.
• TauCeti.gradedExtEulerSesquilinear_T_smul_left and TauCeti.gradedExtEulerSesquilinear_T_smul_right: the shift normalizations in both variables.
• TauCeti.gradedExtEulerSesquilinear_unique: the form is determined by its values on object classes.
• TauCeti.gradedExtEulerSpecialized_mk_of_mk_of: the specialized form on two object classes is the graded Ext-Euler characteristic evaluated at q = ε.

References

• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Sections 1.2, 2.2 and 3.1.

theorem TauCeti.instIsClosedUnderIsomorphisms_tauCeti {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] : P.IsClosedUnderIsomorphisms

theorem TauCeti.instIsClosedUnderIsomorphisms_tauCeti_1 {C : Type u} [CategoryTheory.Category.{v, u} C] {Q : CategoryTheory.ObjectProperty C} [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] : Q.IsClosedUnderIsomorphisms

noncomputable def TauCeti.gradedExtEulerSesquilinear {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} [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) : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift) →ₛₗ[LaurentPolynomial.invert.toRingEquiv.toRingHom] LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift) →ₗ[LaurentPolynomial ℤ] LaurentPolynomial ℤ

The q-Euler form on graded Grothendieck groups. It is semilinear in the first variable for the Laurent involution q ↦ q⁻¹ and linear in the second variable. Its value on object classes is the graded Ext-Euler characteristic.

The source and target properties may differ; no symmetry hypothesis is imposed.

Equations

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

@[simp]

theorem TauCeti.gradedExtEulerSesquilinear_of_of {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} [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) : ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift) X)) (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift) Y) = gradedExtEuler k e ⋯

The q-Euler form evaluates on two object classes as the object-level graded Ext-Euler characteristic.

@[simp]

theorem TauCeti.gradedExtEulerSesquilinear_T_smul_left {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} [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) (n : ℤ) (x : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)) (y : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)) : ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) (LaurentPolynomial.T n • x)) y = LaurentPolynomial.T (-n) * ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) x) y

Shifting the first graded Grothendieck class by n multiplies the q-Euler form by q⁻ⁿ.

theorem TauCeti.gradedExtEulerSesquilinear_T_smul_right {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} [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) (n : ℤ) (x : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)) (y : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)) : ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) x) (LaurentPolynomial.T n • y) = LaurentPolynomial.T n * ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) x) y

Shifting the second graded Grothendieck class by n multiplies the q-Euler form by qⁿ.

theorem TauCeti.gradedExtEulerSesquilinear_unique {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} [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) (B : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift) →ₛₗ[LaurentPolynomial.invert.toRingEquiv.toRingHom] LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift) →ₗ[LaurentPolynomial ℤ] LaurentPolynomial ℤ) (hB : ∀ (X : P.FullSubcategory) (Y : Q.FullSubcategory), (B (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift) X)) (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift) Y) = gradedExtEuler k e ⋯) : B = gradedExtEulerSesquilinear hP hQ hPshift hQshift h

The q-Euler form is the unique Laurent-sesquilinear map with the prescribed values on pairs of object classes.

noncomputable def TauCeti.gradedExtEulerSpecialized {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} [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) (ε : ℤˣ) : LaurentSpecialization ε (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)) →ₗ[ℤ] LaurentSpecialization ε (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)) →ₗ[ℤ] ℤ

The q-Euler form specialized at q = ε, for a unit ε : ℤˣ, that is at q = 1 or q = -1. It is the ℤ-bilinear form on the specializations of the Laurent-module Grothendieck groups of P and Q obtained from TauCeti.gradedExtEulerSesquilinear by evaluating at ε; since ε⁻¹ = ε over ℤ, both arguments are specialized at the same unit.

Equations

• TauCeti.gradedExtEulerSpecialized hP hQ hPshift hQshift h ε = (TauCeti.gradedExtEulerSesquilinear hP hQ hPshift hQshift h).laurentSpecialize ⋯

@[simp]

theorem TauCeti.gradedExtEulerSpecialized_mk_of_mk_of {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} [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) : ((gradedExtEulerSpecialized hP hQ hPshift hQshift h ε) ((LaurentSpecialization.mk ε) (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift) X))) ((LaurentSpecialization.mk ε) (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift) Y)) = (laurentEval ε) (gradedExtEuler k e ⋯)

The specialized q-Euler form on two specialized object classes is the graded Ext-Euler characteristic evaluated at q = ε.