Specializing the graded Cartan matrix

The graded Cartan matrix has Laurent-polynomial entries. Specializing the projective and module bases coefficientwise shows that its value at a unit ε is the matrix of the specialized Cartan map. At q = 1, the forgetful square identifies this matrix with the ordinary Cartan matrix whenever forgetting grading carries the two specialized bases to the chosen ordinary bases.

No assertion that forgetting grading is an equivalence is needed. The basis compatibility hypotheses already force the two forgetful maps to preserve coordinates, which is precisely the information needed for the matrix comparison. In applications, the hypotheses are discharged by graded projective and simple class bases whose underlying modules give the corresponding ordinary bases.

Main results

• TauCeti.toMatrix_gradedCartanMapSpecialized: specialization evaluates every entry of the graded Cartan matrix.
• TauCeti.toMatrix_cartanMap_eq_map_gradedCartanMatrix: at q = 1, compatible graded and ordinary bases give the ordinary Cartan matrix.

The convention is that rows are module coordinates and columns are projective coordinates, as in Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Section 2.2.

theorem TauCeti.toMatrix_gradedCartanMapSpecialized {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {I : Type uI} {J : Type uJ} [Fintype I] [DecidableEq I] [Finite J] (ε : ℤˣ) (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (bM : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) : (LinearMap.toMatrix (LaurentSpecialization.basis ε bP) (LaurentSpecialization.basis ε bM)) (gradedCartanMapSpecialized 𝒜 ε) = (gradedCartanMatrix 𝒜 bP bM).map ⇑(laurentEval ε)

Specializing the graded Cartan matrix evaluates its entries. The matrix of the Cartan map specialized at q = ε, in the coefficientwise-specialized bases, is obtained by evaluating the Laurent-polynomial graded Cartan matrix at ε.

theorem TauCeti.toMatrix_cartanMap_eq_map_gradedCartanMatrix {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {I : Type uI} {J : Type uJ} [Fintype I] [DecidableEq I] [Finite J] (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (bM : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) (cP : Module.Basis I ℤ (ExactK0 (finiteProjectiveModulesExactStructure A))) (cM : Module.Basis J ℤ (ExactK0 (finiteModulesExactStructure A))) (hP : ∀ (j : I), (gradedFiniteProjectiveModulesForgetK0 𝒜) ((LaurentSpecialization.basis 1 bP) j) = cP j) (hM : ∀ (i : J), (gradedFiniteModulesForgetK0 𝒜) ((LaurentSpecialization.basis 1 bM) i) = cM i) : (LinearMap.toMatrix cP cM) (cartanMap A).toIntLinearMap = (gradedCartanMatrix 𝒜 bP bM).map ⇑(laurentEval 1)

At q = 1, forgetting grading recovers the ordinary Cartan matrix. Suppose the coefficientwise specializations of graded projective and module bases become chosen bases of ordinary projective K₀ and module G₀ after forgetting grading. Then evaluating the graded Cartan matrix at one gives the matrix of the ordinary Cartan map in those bases.