Preliminary exact-K₀ descent of the graded Ext-Euler characteristic

For extension-closed object properties P and Q, pointwise graded Euler-admissibility makes the Laurent-polynomial-valued Ext-Euler characteristic additive on every conflation in either subcategory. The universal property of exact K₀ therefore gives a biadditive pairing between their Grothendieck groups.

The two groups remain distinct because the pairing need not be symmetric. This file records only biadditivity on ordinary exact K₀. Descent to graded K₀ additionally requires shift identities and shift-closed subcategories; those belong to the later sesquilinear packaging of this preliminary pairing.

Main definitions

• TauCeti.gradedExtEulerRight: the graded Ext-Euler characteristic with its first argument fixed, descended to exact K₀ in the second variable.
• TauCeti.gradedExtEulerPairing: the graded Ext-Euler characteristic descended to exact K₀ in both variables.

Main results

• TauCeti.gradedExtEulerPairing_of_of: evaluation on two object classes.
• TauCeti.gradedExtEulerPairing_unique: the universal characterization of the pairing.

References

• TauCetiRoadmap/GrothendieckEulerForms/README.md, Layer 6, "q-Euler form".

noncomputable def TauCeti.gradedExtEulerRight {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} {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsGradedEulerAdmissibleOn P Q) (X : P.FullSubcategory) : ExactK0 (ExactStructure.fullSubcategory Q hQ) →+ LaurentPolynomial ℤ

For a fixed object in P, the graded Ext-Euler characteristic descends in the second variable to the exact K₀ of the extension-closed subcategory on Q.

Equations

• TauCeti.gradedExtEulerRight hQ h X = (TauCeti.gradedExtEulerRightAdditiveInvariant✝ hQ h).rightLift X

@[simp]

theorem TauCeti.gradedExtEulerRight_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} {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsGradedEulerAdmissibleOn P Q) (X : P.FullSubcategory) (Y : Q.FullSubcategory) : (gradedExtEulerRight hQ h X) (ExactK0.of Y) = gradedExtEuler k e ⋯

gradedExtEulerRight evaluates on an object class as the object-level graded Ext-Euler characteristic.

noncomputable def TauCeti.gradedExtEulerPairing {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} {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 : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsGradedEulerAdmissibleOn P Q) : ExactK0 (ExactStructure.fullSubcategory P hP) →+ ExactK0 (ExactStructure.fullSubcategory Q hQ) →+ LaurentPolynomial ℤ

The Laurent-polynomial-valued Ext-Euler pairing on the exact Grothendieck groups of two extension-closed subcategories. It is additive in both variables and is not asserted to be symmetric.

Equations

• TauCeti.gradedExtEulerPairing hP hQ h = (TauCeti.gradedExtEulerBiadditiveInvariant✝ hP hQ h).bilift

@[simp]

theorem TauCeti.gradedExtEulerPairing_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} {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 : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsGradedEulerAdmissibleOn P Q) (X : P.FullSubcategory) (Y : Q.FullSubcategory) : ((gradedExtEulerPairing hP hQ h) (ExactK0.of X)) (ExactK0.of Y) = gradedExtEuler k e ⋯

The descended graded Ext-Euler pairing evaluates on object classes as the original object-level characteristic.

theorem TauCeti.gradedExtEulerPairing_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} {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 : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsGradedEulerAdmissibleOn P Q) (b : ExactK0 (ExactStructure.fullSubcategory P hP) →+ ExactK0 (ExactStructure.fullSubcategory Q hQ) →+ LaurentPolynomial ℤ) (hb : ∀ (X : P.FullSubcategory) (Y : Q.FullSubcategory), (b (ExactK0.of X)) (ExactK0.of Y) = gradedExtEuler k e ⋯) : b = gradedExtEulerPairing hP hQ h

The descended pairing is the unique biadditive map with the prescribed values on pairs of object classes.