Forgetting the grading on the Grothendieck group of a path algebra

For a finite quiver with finite-dimensional path algebra, forgetting the path-length grading induces an isomorphism from graded G₀ specialized at q = 1 to ordinary G₀. No grading of every ungraded module is required: the graded vertex-simple classes form a Laurent basis, and both groups have the same integral vertex coordinates after specialization.

The equivalence constructed here has the actual forgetful map as its forward map. Its inverse sends each ordinary vertex-simple class to the specialized graded vertex-simple class; more generally it expands a class using its integral vertex dimensions. The coordinate calculation also supplies the dimension comparison used when specializing the quiver q-Euler form.

Main results

• TauCeti.PathAlgebra.pathAlgebraDimensionVectorK0_forgetGrading: the coordinates of a specialized graded class are the dimension vector after forgetting grading.
• TauCeti.PathAlgebra.gradedFiniteModulesForgetK0Equiv: specialization at q = 1 identifies graded and ordinary G₀ through forgetting grading.

References

• Z. Dancso and A. Licata, Koszul algebras and flow lattices, Section 2.2, for graded Grothendieck groups and specialization at q = 1.
• I. Assem, D. Simson and A. Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 3, for the simple-class basis.

@[simp]

theorem TauCeti.PathAlgebra.laurentEval_one_smulGradedDimension_vertexIdempotent (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] (X : GradedModuleCat (integerGrade k Q)) [Module.Finite k X.carrier] (i : Q) : (laurentEval 1) (GradedModuleCat.smulGradedDimension (vertexIdempotent k i) X) = ↑(dimVector ((quiverRepFunctor k Q).obj (GradedModuleCat.toModuleCat.obj X)) i)

At q = 1 the graded dimension at a vertex is the dimension vector of the underlying kQ-module: gdim(eᵢ • X) evaluated at q = 1 is dim_k(eᵢ X).

theorem TauCeti.PathAlgebra.pathAlgebraDimensionVectorK0_forgetGrading (k : Type (max u v)) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (x : LaurentSpecialization 1 (LaurentK0 (gradedFiniteModulesExactStructure (integerGrade k Q)))) (i : Q) : (pathAlgebraDimensionVectorK0 k Q) ((gradedFiniteModulesForgetK0 (integerGrade k Q)) x) i = ((LaurentSpecialization.basis 1 (gradedVertexSimpleClassBasis k Q)).repr x) i

Specialized graded simple coordinates are the ungraded vertex dimensions. This compares arbitrary classes, including differences of module classes, through the actual forgetful map.

noncomputable def TauCeti.PathAlgebra.gradedFiniteModulesForgetK0Equiv (k : Type (max u v)) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] : LaurentSpecialization 1 (LaurentK0 (gradedFiniteModulesExactStructure (integerGrade k Q))) ≃ₗ[ℤ] ExactK0 (finiteModulesExactStructure (pathAlgebra k Q))

Forgetting grading is an isomorphism on G₀ after specialization at q = 1, for a finite quiver whose path algebra is finite-dimensional. The inverse reconstructs a class from its vertex dimensions using the specialized graded vertex simples.

@[simp]

theorem TauCeti.PathAlgebra.gradedFiniteModulesForgetK0Equiv_toLinearMap (k : Type (max u v)) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] : ↑(gradedFiniteModulesForgetK0Equiv k Q) = gradedFiniteModulesForgetK0 (integerGrade k Q)

The forward map of the comparison equivalence is the map induced by forgetting grading.

theorem TauCeti.PathAlgebra.gradedFiniteModulesForgetK0Equiv_mk_of (k : Type (max u v)) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (M : (gradedFiniteModules (integerGrade k Q)).FullSubcategory) : (gradedFiniteModulesForgetK0Equiv k Q) ((LaurentSpecialization.mk 1) (LaurentK0.of (gradedFiniteModulesExactStructure (integerGrade k Q)) M)) = ExactK0.of ((gradedFiniteModulesForget (integerGrade k Q)).obj M)

On a specialized module class the equivalence returns its underlying ungraded class.

theorem TauCeti.PathAlgebra.gradedFiniteModulesForgetK0Equiv_symm_apply (k : Type (max u v)) (Q : Type u) [Field k] [Quiver Q] [Fintype Q] [FiniteDimensional k (pathAlgebra k Q)] (x : ExactK0 (finiteModulesExactStructure (pathAlgebra k Q))) : (gradedFiniteModulesForgetK0Equiv k Q).symm x = ∑ i : Q, (pathAlgebraDimensionVectorK0 k Q) x i • (LaurentSpecialization.mk 1) (LaurentK0.of (gradedFiniteModulesExactStructure (integerGrade k Q)) { obj := gradedVertexSimple k Q i, property := ⋯ })

The inverse comparison expands an ungraded class in the specialized graded vertex simples, with its integral vertex dimensions as coefficients.

theorem TauCeti.PathAlgebra.gradedFiniteModulesForgetK0Equiv_symm_vertexSimple (k : Type (max u v)) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (i : Q) : (gradedFiniteModulesForgetK0Equiv k Q).symm (ExactK0.of (vertexSimpleModuleFG k Q i)) = (LaurentSpecialization.mk 1) (LaurentK0.of (gradedFiniteModulesExactStructure (integerGrade k Q)) { obj := gradedVertexSimple k Q i, property := ⋯ })

The inverse sends an ordinary vertex-simple class to its graded class at q = 1.