Composition multiplicities and vertex dimensions for path algebras

For a finite acyclic quiver, the multiplicity of the vertex simple Sᵢ in a finite-dimensional path-algebra module is the dimension of its ith vertex space. This identifies the exact Grothendieck group with the integral lattice of vertex dimensions. For a vertex projective Pⱼ, this identifies its multiplicity of Sᵢ with the number of paths from j to i. These are the columns of the Cartan matrix in the left-module convention.

See Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 3.

@[simp]

theorem TauCeti.jordanHolderCoordinate_vertexSimpleModuleFG_eq_dimVector (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (i : Q) (x : ExactK0 (finiteModulesExactStructure (pathAlgebra k Q))) : (jordanHolderCoordinate (pathAlgebra k Q) ↑(vertexSimpleModuleFG k Q i)) x = (pathAlgebraDimensionVectorK0 k Q) x i

The ith Jordan--Hölder coordinate on G₀(mod kQ) equals the ith vertex dimension.

noncomputable def TauCeti.pathAlgebraDimensionVectorK0Equiv (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] : ExactK0 (finiteModulesExactStructure (pathAlgebra k Q)) ≃+ (Q → ℤ)

The exact Grothendieck group of finite-dimensional kQ-modules is the integral lattice of vertex dimensions. The inverse sends a dimension vector to the corresponding integral combination of vertex-simple classes.

@[simp]

theorem TauCeti.pathAlgebraDimensionVectorK0Equiv_apply (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (x : ExactK0 (finiteModulesExactStructure (pathAlgebra k Q))) : (pathAlgebraDimensionVectorK0Equiv k Q) x = (pathAlgebraDimensionVectorK0 k Q) x

The forward Grothendieck-group equivalence is the dimension-vector map.

theorem TauCeti.pathAlgebraDimensionVectorK0Equiv_vertexSimple (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] [DecidableEq Q] (i : Q) : (pathAlgebraDimensionVectorK0Equiv k Q) (ExactK0.of (vertexSimpleModuleFG k Q i)) = Pi.single i 1

A vertex simple maps to the corresponding standard basis vector.

@[simp]

theorem TauCeti.pathAlgebraDimensionVectorK0Equiv_symm_apply (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (d : Q → ℤ) : (pathAlgebraDimensionVectorK0Equiv k Q).symm d = ∑ i : Q, d i • ExactK0.of (vertexSimpleModuleFG k Q i)

The inverse dimension-vector equivalence expands an integral vertex vector in the classes of the vertex simples.

@[simp]

theorem TauCeti.jordanHolderMultiplicity_vertexSimpleModuleFG_eq_dimVector (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (M : FGModuleCat (pathAlgebra k Q)) (i : Q) : jordanHolderMultiplicity (pathAlgebra k Q) ↑M ↑(vertexSimpleModuleFG k Q i) = dimVector ((quiverRepFunctor k Q).obj M.obj) i

The multiplicity of Sᵢ in a finitely generated kQ-module is the dimension of its ith vertex space.

theorem TauCeti.jordanHolderMultiplicity_vertexProjectiveModuleFG_eq_card_path (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (i j : Q) : jordanHolderMultiplicity (pathAlgebra k Q) ↑(vertexProjectiveModuleFG k Q j) ↑(vertexSimpleModuleFG k Q i) = Nat.card (Quiver.Path j i)

The Cartan path-count formula. The multiplicity of Sᵢ in the vertex projective Pⱼ is the number of oriented paths from j to i. With simples in rows and projectives in columns, these are the entries of the Cartan matrix of a finite acyclic path algebra.