The graded Cartan matrix

The graded Cartan map is a linear map over the Laurent polynomial ring ℤ[q,q⁻¹]. After choosing bases of the projective and module Grothendieck groups, its matrix is the graded Cartan matrix. Rows are coordinates in the module basis and columns are coordinates in the projective basis, matching the convention for the ordinary Cartan matrix.

This file gives the basis-generic matrix interface. An entry is a coordinate of the image of a projective basis vector, a column reconstructs that image, and changing the two bases acts by the usual left and right transition matrices. In particular, the construction does not assume that the chosen bases arise from simple modules and indecomposable projectives; those hypotheses belong to later representation-theoretic identifications of the entries with graded composition multiplicities.

Main definitions

• TauCeti.gradedCartanMatrix: the matrix of TauCeti.gradedCartanMap in independently chosen projective and module bases.

Main results

• TauCeti.gradedCartanMatrix_apply: entries are coordinates of images of projective basis vectors.
• TauCeti.gradedCartanMatrix_apply_of: when a projective basis vector is an object class, its column consists of the coordinates of the same object in the module Grothendieck group.
• TauCeti.gradedCartanMatrix_mulVec_repr: the matrix computes the coordinates of the graded Cartan map on every class.
• TauCeti.gradedCartanMap_basis_apply_eq_sum: a column reconstructs the corresponding image.
• TauCeti.gradedCartanMatrix_basis_change: the change-of-basis law for the graded Cartan matrix.

The matrix convention follows Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Section 2.2.

noncomputable def TauCeti.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] [Finite J] (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (bM : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) : Matrix J I (LaurentPolynomial ℤ)

The graded Cartan matrix in a projective basis bP and a module basis bM: the matrix of the Laurent-linear graded Cartan map. Rows are indexed by bM and columns by bP.

Equations

• TauCeti.gradedCartanMatrix 𝒜 bP bM = (LinearMap.toMatrix bP bM) (TauCeti.gradedCartanMap 𝒜)

@[simp]

theorem TauCeti.gradedCartanMatrix_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {I : Type uI} {J : Type uJ} [Fintype I] [Finite J] (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (bM : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) (i : J) (j : I) : gradedCartanMatrix 𝒜 bP bM i j = (bM.repr ((gradedCartanMap 𝒜) (bP j))) i

A graded Cartan-matrix entry is the corresponding module-basis coordinate of the image of a projective-basis vector.

theorem TauCeti.gradedCartanMatrix_apply_of {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {I : Type uI} {J : Type uJ} [Fintype I] [Finite J] (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (bM : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) (i : J) (j : I) (M : GradedModuleCat 𝒜) (hM : gradedFiniteProjectiveModules 𝒜 M) (hj : bP j = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) { obj := M, property := hM }) : gradedCartanMatrix 𝒜 bP bM i j = (bM.repr (LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) { obj := M, property := ⋯ })) i

If a projective-basis vector is the class of a finite graded projective, its graded Cartan column consists of the module-basis coordinates of the class of that same graded module.

theorem TauCeti.gradedCartanMatrix_col {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {I : Type uI} {J : Type uJ} [Fintype I] [Finite J] (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (bM : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) (j : I) : (gradedCartanMatrix 𝒜 bP bM).col j = ⇑(bM.repr ((gradedCartanMap 𝒜) (bP j)))

A column of the graded Cartan matrix is the coordinate vector of the corresponding projective-basis vector under the graded Cartan map.

theorem TauCeti.gradedCartanMatrix_mulVec_repr {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {I : Type uI} {J : Type uJ} [Fintype I] [Finite J] (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (bM : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) (x : LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜)) : (gradedCartanMatrix 𝒜 bP bM).mulVec ⇑(bP.repr x) = ⇑(bM.repr ((gradedCartanMap 𝒜) x))

The graded Cartan matrix sends the coordinate vector of a class to the coordinate vector of its image under the graded Cartan map.

theorem TauCeti.gradedCartanMap_basis_apply_eq_sum {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {I : Type uI} {J : Type uJ} [Fintype I] [Finite J] [Fintype J] (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (bM : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) (j : I) : (gradedCartanMap 𝒜) (bP j) = ∑ i : J, gradedCartanMatrix 𝒜 bP bM i j • bM i

Reconstruct the image of a projective-basis vector from the corresponding column of the graded Cartan matrix.

theorem TauCeti.gradedCartanMatrix_basis_change {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {I : Type uI} {J : Type uJ} [Fintype I] [Finite J] {I' : Type u_1} {J' : Type u_2} [Fintype I'] [Fintype J] [Finite J'] (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (bM : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) (cP : Module.Basis I' (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (cM : Module.Basis J' (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))) : cM.toMatrix ⇑bM * gradedCartanMatrix 𝒜 bP bM * bP.toMatrix ⇑cP = gradedCartanMatrix 𝒜 cP cM

Change of basis for the graded Cartan matrix. The target transition matrix acts on the left and the source transition matrix acts on the right.