Matrices of the Ext-Euler pairing

This file records the matrix of the Ext-Euler pairing in independently chosen bases of two exact Grothendieck groups. No symmetry is assumed, so the source and target properties and their bases may be different.

Main definitions

• TauCeti.extEulerMatrix: the matrix of the Ext-Euler pairing in two bases.

Main results

• TauCeti.extEulerMatrix_apply: a matrix entry is the pairing of the corresponding basis vectors.
• TauCeti.extEulerMatrix_of_of: when two basis vectors are object classes, their entry is the object-level Ext-Euler characteristic.
• TauCeti.extEulerMatrix_basis_change: changing the two bases transforms the matrix by the transposed first and the untransposed second change-of-basis matrix.

noncomputable def TauCeti.extEulerMatrix {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt 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 : IsEulerAdmissibleOn k P Q) {I : Type u_1} {J : Type u_2} (bP : Module.Basis I ℤ (ExactK0 (ExactStructure.fullSubcategory P hP))) (bQ : Module.Basis J ℤ (ExactK0 (ExactStructure.fullSubcategory Q hQ))) : Matrix I J ℤ

The matrix of the Ext-Euler pairing in independently chosen bases of two exact Grothendieck groups. Neither symmetry nor equal source and target groups is required.

Equations

• TauCeti.extEulerMatrix P Q hP hQ h bP bQ = (LinearMap.toMatrix₂Aux ℤ ⇑bP ⇑bQ) (TauCeti.extEulerBilinear hP hQ h)

@[simp]

theorem TauCeti.extEulerMatrix_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt 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 : IsEulerAdmissibleOn k P Q) {I : Type u_1} {J : Type u_2} (bP : Module.Basis I ℤ (ExactK0 (ExactStructure.fullSubcategory P hP))) (bQ : Module.Basis J ℤ (ExactK0 (ExactStructure.fullSubcategory Q hQ))) (i : I) (j : J) : extEulerMatrix P Q hP hQ h bP bQ i j = ((extEulerPairing hP hQ h) (bP i)) (bQ j)

An entry of the Ext-Euler matrix is the pairing of the corresponding basis vectors.

theorem TauCeti.extEulerMatrix_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] (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 : IsEulerAdmissibleOn k P Q) {I : Type u_1} {J : Type u_2} (bP : Module.Basis I ℤ (ExactK0 (ExactStructure.fullSubcategory P hP))) (bQ : Module.Basis J ℤ (ExactK0 (ExactStructure.fullSubcategory Q hQ))) (i : I) (j : J) (X : P.FullSubcategory) (Y : Q.FullSubcategory) (hi : bP i = ExactK0.of X) (hj : bQ j = ExactK0.of Y) : extEulerMatrix P Q hP hQ h bP bQ i j = extEuler k ⋯

If two basis vectors are classes of objects, their Ext-Euler matrix entry is the object-level Ext-Euler characteristic.

theorem TauCeti.extEulerMatrix_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] (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 : IsEulerAdmissibleOn k 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 ℤ (ExactK0 (ExactStructure.fullSubcategory P hP))) (bQ : Module.Basis J ℤ (ExactK0 (ExactStructure.fullSubcategory Q hQ))) (cP : Module.Basis I' ℤ (ExactK0 (ExactStructure.fullSubcategory P hP))) (cQ : Module.Basis J' ℤ (ExactK0 (ExactStructure.fullSubcategory Q hQ))) : (bP.toMatrix ⇑cP).transpose * extEulerMatrix P Q hP hQ h bP bQ * bQ.toMatrix ⇑cQ = extEulerMatrix P Q hP hQ h cP cQ

Change of basis for the Ext-Euler matrix. The first change-of-basis matrix acts transposed on the left and the second acts on the right, since the pairing is bilinear but not symmetric.