Documentation

TauCeti.RepresentationTheory.Quiver.PathAlgebra.GradedCartanMatrix

The graded Cartan matrix of a path algebra #

Let Q be a finite acyclic quiver, so that its path algebra kQ is finite-dimensional, and give kQ its path-length grading. The degree-zero piece is spanned by the vertex idempotents eᵢ, so the graded vertex projectives kQ eᵢ form a basis of K₀^gr(proj kQ) over ℤ[q,q⁻¹] (TauCeti.gradedIdempotentProjectiveBasis), just as the graded vertex simples form a basis of G₀^gr(mod kQ).

In these two bases the graded Cartan matrix is the path-counting matrix: the coefficient of qⁿ in its (i, j) entry is the number of paths of length n from j to i, and there are no negative powers of q. Rows are indexed by simples and columns by projectives, following the left-module convention for Cartan matrices.

Counting paths by their last arrow turns this into a closed formula. If the (i, j) entry of A counts arrows i ⟶ j, then the graded Cartan matrix is (1 - q Aᵀ)⁻¹. Applying q ↦ q⁻¹ entrywise and transposing, its conjugate transpose inverts 1 - q⁻¹ A, the matrix of the graded Ringel form; this is the input for identifying the q-Euler matrix of the graded vertex simples with the inverse conjugate-transposed graded Cartan matrix.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.PathAlgebra.gradedVertexProjectiveClassBasis (k : Type w) (Q : Type u) [Quiver Q] [Field k] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] :
Module.Basis Q (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure (integerGrade k Q)))

The vertex-projective basis of K₀^gr(proj kQ) over ℤ[q,q⁻¹], for a finite acyclic quiver: its vector at i is the class [kQ eᵢ] of the graded vertex projective.

Instances For
    source
    @[simp]
    theorem TauCeti.PathAlgebra.gradedVertexProjectiveClassBasis_apply (k : Type w) (Q : Type u) [Quiver Q] [Field k] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (i : Q) :
    (gradedVertexProjectiveClassBasis k Q) i = gradedVertexProjectiveClass k Q i

    The basis vector of TauCeti.PathAlgebra.gradedVertexProjectiveClassBasis at i is the class [kQ eᵢ].

    source
    theorem TauCeti.PathAlgebra.coeff_gradedCartanMatrix_gradedVertexProjectiveClassBasis (k : Type w) (Q : Type u) [Quiver Q] [Field k] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] [Fintype Q] (i j : Q) (n : ℕ) :
    (gradedCartanMatrix (integerGrade k Q) (gradedVertexProjectiveClassBasis k Q) (gradedVertexSimpleClassBasis k Q) i j).coeff ↑n = ↑(Nat.card (PathBetween Q n j i))

    The graded Cartan matrix of a path algebra counts paths by length. In the bases of graded vertex projectives and graded vertex simples, the coefficient of qⁿ in the (i, j) entry is the number of paths of length n from j to i.

    source
    theorem TauCeti.PathAlgebra.coeff_gradedCartanMatrix_gradedVertexProjectiveClassBasis_of_neg (k : Type w) (Q : Type u) [Quiver Q] [Field k] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] [Fintype Q] (i j : Q) (d : ℤ) (hd : d < 0) :
    (gradedCartanMatrix (integerGrade k Q) (gradedVertexProjectiveClassBasis k Q) (gradedVertexSimpleClassBasis k Q) i j).coeff d = 0

    The entries of the graded Cartan matrix of a path algebra have no negative powers of q.

    source
    theorem TauCeti.PathAlgebra.one_sub_T_smul_transpose_mul_gradedCartanMatrix_eq_one (k : Type w) (Q : Type u) [Quiver Q] [Field k] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] [Fintype Q] [DecidableEq Q] :
    (1 - LaurentPolynomial.T 1 • (Matrix.of fun (i j : Q) => ↑(Nat.card (i ⟶ j))).transpose) * gradedCartanMatrix (integerGrade k Q) (gradedVertexProjectiveClassBasis k Q) (gradedVertexSimpleClassBasis k Q) = 1

    The graded Cartan matrix of a path algebra inverts 1 - q Aᵀ, where the (i, j) entry of A counts arrows i ⟶ j, in the bases of graded vertex projectives and graded vertex simples. On coefficients of qⁿ this is the last-arrow recursion for path counts: the paths of length n + 1 from j to i are the paths of length n from j to some l followed by an arrow l ⟶ i, and the only path of length zero is the trivial path.

    source
    theorem TauCeti.PathAlgebra.gradedCartanMatrix_eq_inv_one_sub_T_smul_transpose (k : Type w) (Q : Type u) [Quiver Q] [Field k] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] [Fintype Q] [DecidableEq Q] :
    gradedCartanMatrix (integerGrade k Q) (gradedVertexProjectiveClassBasis k Q) (gradedVertexSimpleClassBasis k Q) = (1 - LaurentPolynomial.T 1 • (Matrix.of fun (i j : Q) => ↑(Nat.card (i ⟶ j))).transpose)⁻¹

    The graded Cartan matrix of a path algebra is (1 - q Aᵀ)⁻¹, where the (i, j) entry of A counts arrows i ⟶ j, in the bases of graded vertex projectives and graded vertex simples.

    source
    theorem TauCeti.PathAlgebra.gradedCartanMatrix_map_invert_transpose_mul_one_sub_T_neg_smul_eq_one (k : Type w) (Q : Type u) [Quiver Q] [Field k] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] [Fintype Q] [DecidableEq Q] :
    ((gradedCartanMatrix (integerGrade k Q) (gradedVertexProjectiveClassBasis k Q) (gradedVertexSimpleClassBasis k Q)).map ⇑LaurentPolynomial.invert).transpose * (1 - LaurentPolynomial.T (-1) • Matrix.of fun (i j : Q) => ↑(Nat.card (i ⟶ j))) = 1

    The conjugate-transposed graded Cartan matrix of a path algebra inverts 1 - q⁻¹ A, where the (i, j) entry of A counts arrows i ⟶ j. This is the conjugate transpose of TauCeti.PathAlgebra.one_sub_T_smul_transpose_mul_gradedCartanMatrix_eq_one. The matrix 1 - q⁻¹ A is the graded Ringel matrix, the q-Euler matrix of the graded vertex simples (TauCeti.PathAlgebra.gradedExtEulerForm_basis).