Documentation

TauCeti.Algebra.Homology.EulerCharacteristic.ExtEuler.Graded.Numerical

Numerical quotients of the graded Ext-Euler pairing #

The graded Ext-Euler characteristic gives a Laurent-polynomial-valued sesquilinear pairing on the Laurent-module Grothendieck groups of two extension-closed, shift-stable subcategories. This file quotients the first group by the left radical and the second group by the right radical, and descends the q-Euler form to the resulting numerical Grothendieck groups.

The two quotients are kept separate because the q-Euler form need not be symmetric or Hermitian. The left radical is a Laurent submodule even though scalar multiplication in the first variable is twisted by LaurentPolynomial.invert; this closure is built into the kernel of the semilinear map. The generic numerical-quotient construction supplies the quotient modules and descended pairings, while the results here expose their values in terms of graded Ext.

Main definitions #

Main results #

References #

The separate left and right numerical quotients for nonsymmetric q-pairings follow Zsuzsanna Dancso and Anthony Licata, Koszul algebras and flow lattices, Section 3.1.

source
@[reducible, inline]
abbrev TauCeti.GradedExtEulerLeftNumericalQuotient {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) :
Type w

The left numerical quotient of the first Laurent-module Grothendieck group for the graded Ext-Euler pairing.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.GradedExtEulerRightNumericalQuotient {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) :
    Type w

    The right numerical quotient of the second Laurent-module Grothendieck group for the graded Ext-Euler pairing.

    Equations
    Instances For
      source
      noncomputable def TauCeti.gradedExtEulerLeftNumericalQuotientMk {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 ℤ] GradedExtEulerLeftNumericalQuotient hP hQ hPshift hQshift h

      The quotient map from the first Laurent-module Grothendieck group to its left graded Ext-Euler numerical quotient.

      Equations
      Instances For
        source
        noncomputable def TauCeti.gradedExtEulerRightNumericalQuotientMk {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 Q hQ hQshift) →ₗ[LaurentPolynomial ℤ] GradedExtEulerRightNumericalQuotient hP hQ hPshift hQshift h

        The quotient map from the second Laurent-module Grothendieck group to its right graded Ext-Euler numerical quotient.

        Equations
        Instances For
          source
          theorem TauCeti.mem_gradedExtEulerLeftRadical_iff {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 : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)) :
          x ∈ leftRadical (gradedExtEulerSesquilinear hP hQ hPshift hQshift h) ↔ ∀ (y : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)), ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) x) y = 0

          The left radical of the graded Ext-Euler pairing consists exactly of the classes pairing to zero with every class on the right.

          source
          theorem TauCeti.mem_gradedExtEulerRightRadical_iff {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) (y : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)) :
          y ∈ rightRadical (gradedExtEulerSesquilinear hP hQ hPshift hQshift h) ↔ ∀ (x : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)), ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) x) y = 0

          The right radical of the graded Ext-Euler pairing consists exactly of the classes pairing to zero with every class on the left.

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

          The one-sided q-Euler pairing after quotienting the left Laurent-module Grothendieck group.

          Equations
          Instances For
            source
            noncomputable def TauCeti.gradedExtEulerRightNumericalPairing {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] GradedExtEulerRightNumericalQuotient hP hQ hPshift hQshift h →ₗ[LaurentPolynomial ℤ] LaurentPolynomial ℤ

            The one-sided q-Euler pairing after quotienting the right Laurent-module Grothendieck group.

            Equations
            Instances For
              source
              noncomputable def TauCeti.gradedExtEulerNumericalPairing {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) :
              GradedExtEulerLeftNumericalQuotient hP hQ hPshift hQshift h →ₛₗ[LaurentPolynomial.invert.toRingEquiv.toRingHom] GradedExtEulerRightNumericalQuotient hP hQ hPshift hQshift h →ₗ[LaurentPolynomial ℤ] LaurentPolynomial ℤ

              The graded Ext-Euler pairing between the left and right numerical Grothendieck groups.

              Equations
              Instances For
                source
                @[simp]
                theorem TauCeti.gradedExtEulerLeftNumericalPairing_mk {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 : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)) (y : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)) :
                ((gradedExtEulerLeftNumericalPairing hP hQ hPshift hQshift h) ((gradedExtEulerLeftNumericalQuotientMk hP hQ hPshift hQshift h) x)) y = ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) x) y

                The left numerical q-Euler pairing evaluates on a quotient representative as the original graded Ext-Euler pairing.

                source
                @[simp]
                theorem TauCeti.gradedExtEulerRightNumericalPairing_mk {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 : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)) (y : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)) :
                ((gradedExtEulerRightNumericalPairing hP hQ hPshift hQshift h) x) ((gradedExtEulerRightNumericalQuotientMk hP hQ hPshift hQshift h) y) = ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) x) y

                The right numerical q-Euler pairing evaluates on a quotient representative as the original graded Ext-Euler pairing.

                source
                @[simp]
                theorem TauCeti.gradedExtEulerNumericalPairing_mk {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 : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)) (y : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)) :
                ((gradedExtEulerNumericalPairing hP hQ hPshift hQshift h) ((gradedExtEulerLeftNumericalQuotientMk hP hQ hPshift hQshift h) x)) ((gradedExtEulerRightNumericalQuotientMk hP hQ hPshift hQshift h) y) = ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) x) y

                The numerical q-Euler pairing evaluates on quotient representatives as the original graded Ext-Euler pairing.

                source
                theorem TauCeti.gradedExtEulerNumericalPairing_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) :
                ((gradedExtEulerNumericalPairing hP hQ hPshift hQshift h) ((gradedExtEulerLeftNumericalQuotientMk hP hQ hPshift hQshift h) (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift) X))) ((gradedExtEulerRightNumericalQuotientMk hP hQ hPshift hQshift h) (LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift) Y)) = gradedExtEuler k e ⋯

                The numerical q-Euler pairing evaluates on object classes as their graded Ext-Euler characteristic.

                source
                theorem TauCeti.gradedExtEulerLeftNumericalPairing_separatingLeft {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) :
                (gradedExtEulerLeftNumericalPairing hP hQ hPshift hQshift h).SeparatingLeft

                The left numerical graded Ext-Euler pairing separates its left argument.

                source
                theorem TauCeti.gradedExtEulerRightNumericalPairing_separatingRight {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) :
                (gradedExtEulerRightNumericalPairing hP hQ hPshift hQshift h).SeparatingRight

                The right numerical graded Ext-Euler pairing separates its right argument.

                source
                theorem TauCeti.gradedExtEulerNumericalPairing_nondegenerate {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) :
                (gradedExtEulerNumericalPairing hP hQ hPshift hQshift h).Nondegenerate

                Quotienting by both graded Ext-Euler radicals makes the q-Euler pairing nondegenerate.

                source
                theorem TauCeti.gradedExtEulerNumericalPairing_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 : GradedExtEulerLeftNumericalQuotient hP hQ hPshift hQshift h →ₛₗ[LaurentPolynomial.invert.toRingEquiv.toRingHom] GradedExtEulerRightNumericalQuotient hP hQ hPshift hQshift h →ₗ[LaurentPolynomial ℤ] LaurentPolynomial ℤ) (hb : ∀ (x : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)) (y : LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)), (b ((gradedExtEulerLeftNumericalQuotientMk hP hQ hPshift hQshift h) x)) ((gradedExtEulerRightNumericalQuotientMk hP hQ hPshift hQshift h) y) = ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) x) y) :
                b = gradedExtEulerNumericalPairing hP hQ hPshift hQshift h

                The numerical q-Euler pairing is the unique sesquilinear pairing whose representative values are the original graded Ext-Euler values.