Matrices of the graded Ext--Euler pairing #
The graded Ext--Euler pairing is Laurent-sesquilinear: the involution
LaurentPolynomial.invert acts on its first argument and the second argument is linear. This file
records its matrix in independently chosen bases and proves the corresponding change-of-basis
formula. The first coordinate matrix is transposed after applying q ↦ q⁻¹ entrywise, while the
second coordinate matrix is unchanged.
No symmetry is assumed. In particular, the source and target properties and their bases may be different. This distinction is essential for the projective/simple matrices of nonsymmetric Euler forms.
Main definitions #
TauCeti.gradedExtEulerMatrix: the matrix of the graded Ext--Euler pairing in two bases.
Main results #
TauCeti.gradedExtEulerMatrix_apply: a matrix entry is the pairing of the corresponding basis vectors.TauCeti.gradedExtEulerMatrix_of_of: when two basis vectors are object classes, their entry is the object-level graded Ext--Euler characteristic.TauCeti.gradedExtEulerMatrix_basis_change: changing the two bases transforms the matrix by an involution-transpose on the left and an ordinary coordinate matrix on the right.
The convention follows Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Sections 1.2 and 3.1--3.2: a q-antilinear first argument forces conjugate transpose on the left change-of-basis matrix.
theorem
TauCeti.instIsClosedUnderIsomorphisms_tauCeti_2
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(P : CategoryTheory.ObjectProperty C)
[P.ContainsZero]
[P.IsClosedUnderBinaryProducts]
:
theorem
TauCeti.instIsClosedUnderIsomorphisms_tauCeti_3
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(Q : CategoryTheory.ObjectProperty C)
[Q.ContainsZero]
[Q.IsClosedUnderBinaryProducts]
:
noncomputable def
TauCeti.gradedExtEulerMatrix
{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)
{I : Type u_1}
{J : Type u_2}
(bP :
Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)))
(bQ :
Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)))
:
Matrix I J (LaurentPolynomial ℤ)
The matrix of the graded Ext--Euler pairing in independently chosen bases of the Laurent
Grothendieck groups selected by P and Q. Neither symmetry nor equal source and target modules
is required.
Equations
- TauCeti.gradedExtEulerMatrix e P Q hP hQ hPshift hQshift h bP bQ = (LinearMap.toMatrix₂Aux (LaurentPolynomial ℤ) ⇑bP ⇑bQ) (TauCeti.gradedExtEulerSesquilinear hP hQ hPshift hQshift h)
Instances For
@[simp]
theorem
TauCeti.gradedExtEulerMatrix_apply
{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)
{I : Type u_1}
{J : Type u_2}
(bP :
Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)))
(bQ :
Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)))
(i : I)
(j : J)
:
gradedExtEulerMatrix e P Q hP hQ hPshift hQshift h bP bQ i j = ((gradedExtEulerSesquilinear hP hQ hPshift hQshift h) (bP i)) (bQ j)
An entry of the graded Ext--Euler matrix is the pairing of the corresponding basis vectors.
theorem
TauCeti.gradedExtEulerMatrix_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)
{I : Type u_1}
{J : Type u_2}
(bP :
Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)))
(bQ :
Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)))
(i : I)
(j : J)
(X : P.FullSubcategory)
(Y : Q.FullSubcategory)
(hi : bP i = LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift) X)
(hj : bQ j = LaurentK0.of ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift) Y)
:
If two basis vectors are classes of objects, their graded Ext--Euler matrix entry is the object-level graded Ext--Euler characteristic.
theorem
TauCeti.gradedExtEulerMatrix_basis_change
{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)
{I : Type u_1}
{J : Type u_2}
{I' : Type u_3}
{J' : Type u_4}
[Fintype I]
[Fintype J]
(bP :
Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)))
(bQ :
Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)))
(cP :
Module.Basis I' (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory P hP hPshift)))
(cQ :
Module.Basis J' (LaurentPolynomial ℤ) (LaurentK0 ((GradedExactStructure.abelian C e).fullSubcategory Q hQ hQshift)))
:
((bP.toMatrix ⇑cP).map ⇑LaurentPolynomial.invert).transpose * gradedExtEulerMatrix e P Q hP hQ hPshift hQshift h bP bQ * bQ.toMatrix ⇑cQ = gradedExtEulerMatrix e P Q hP hQ hPshift hQshift h cP cQ
Involution-transpose change of basis for the graded Ext--Euler matrix. The first basis
matrix is transformed entrywise by LaurentPolynomial.invert and transposed, while the second
basis matrix acts without the involution. This is the matrix law forced by q-antilinearity in the
first argument and q-linearity in the second.