Graded vertex projectives of a path algebra

Let kQ carry its path-length grading, extended by zero from ℕ to ℤ. The vertex idempotent e_i has degree zero, so the principal left ideal kQ e_i is a graded module. It is finitely generated and projective over kQ, hence defines a class in the Laurent Grothendieck group K₀^gr(proj kQ).

The image of [kQ e_j] under the graded Cartan map has a concrete path-counting description. Its e_i-coordinate in internal degree n is the dimension of the graded corner e_i kQ e_j, which is the number of paths of length n from j to i. Negative-degree coefficients vanish. These formulas are the projective columns needed to compare the graded Cartan and Ext-Euler matrices for an acyclic quiver.

Main definitions

• TauCeti.PathAlgebra.gradedVertexProjective: the graded principal left ideal kQ e_i.
• TauCeti.PathAlgebra.gradedVertexProjectiveSubtype: its inclusion into the path algebra.
• TauCeti.PathAlgebra.gradedVertexProjectiveClass: its class in K₀^gr(proj kQ).

Main results

• TauCeti.PathAlgebra.coeff_gradedCartanMap_gradedVertexProjectiveClass: the coefficient in degree n of the (i,j) graded Cartan column is the number of length-n paths j ⟶ i.
• TauCeti.PathAlgebra.coeff_gradedCartanMap_gradedVertexProjectiveClass_of_neg: the same coordinate vanishes in negative degrees.

References

• I. Assem, D. Simson and A. Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapters II--III, for path algebras, vertex projectives and Cartan matrices.
• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded projective modules and grading shifts.
• Z. Dancso and A. Licata, "Koszul algebras and flow lattices", Section 2.2, for the graded Cartan map over ℤ[q,q⁻¹].

theorem TauCeti.PathAlgebra.isHomogeneous_span_vertexIdempotent (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] [GradedAlgebra (integerGrade k Q)] (i : Q) : Ideal.IsHomogeneous (integerGrade k Q) (Ideal.span {vertexIdempotent k i})

The left ideal generated by a vertex idempotent is homogeneous for the integer-indexed path-length grading.

noncomputable def TauCeti.PathAlgebra.gradedVertexProjective (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : GradedModuleCat (integerGrade k Q)

The graded vertex projective kQ e_i, with the grading induced by path length. Use gradedVertexProjectiveSubtype to view its elements in the path algebra.

theorem TauCeti.PathAlgebra.gradedVertexProjective_def (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : gradedVertexProjective k Q i = have x := integerGradedAlgebra k Q; GradedModuleCat.ofIdeal (integerGrade k Q) (Ideal.span {vertexIdempotent k i}) ⋯

The graded vertex projective is the degreewise graded principal ideal kQ e_i.

noncomputable def TauCeti.PathAlgebra.gradedVertexProjectiveSubtype (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : (gradedVertexProjective k Q i).carrier →ₗ[pathAlgebra k Q] pathAlgebra k Q

The inclusion of the graded vertex projective kQ e_i into the path algebra.

noncomputable def TauCeti.PathAlgebra.gradedVertexProjectiveEquiv (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : (gradedVertexProjective k Q i).carrier ≃ₗ[pathAlgebra k Q] ↥(Ideal.span {vertexIdempotent k i})

The graded vertex projective kQ e_i is, as a module, the left ideal generated by e_i.

@[simp]

theorem TauCeti.PathAlgebra.coe_gradedVertexProjectiveEquiv_apply (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) (x : (gradedVertexProjective k Q i).carrier) : ↑((gradedVertexProjectiveEquiv k Q i) x) = (gradedVertexProjectiveSubtype k Q i) x

The identification of kQ e_i with the left ideal generated by e_i is compatible with the inclusions into the path algebra.

theorem TauCeti.PathAlgebra.gradedVertexProjectiveSubtype_injective (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : Function.Injective ⇑(gradedVertexProjectiveSubtype k Q i)

The inclusion of kQ e_i into the path algebra is injective.

@[simp]

theorem TauCeti.PathAlgebra.range_gradedVertexProjectiveSubtype (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : (gradedVertexProjectiveSubtype k Q i).range = Ideal.span {vertexIdempotent k i}

The image of kQ e_i in the path algebra is the left ideal generated by e_i.

@[simp]

theorem TauCeti.PathAlgebra.mem_gradedVertexProjective_piece_iff (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) (d : ℤ) (x : (gradedVertexProjective k Q i).carrier) : x ∈ (gradedVertexProjective k Q i).grading.piece ℤ d ↔ (gradedVertexProjectiveSubtype k Q i) x ∈ integerGrade k Q d

An element of kQ e_i has degree d exactly when its image in the path algebra has integer path degree d.

theorem TauCeti.PathAlgebra.gradedFiniteProjectiveModules_gradedVertexProjective (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : gradedFiniteProjectiveModules (integerGrade k Q) (gradedVertexProjective k Q i)

A graded vertex projective is a finite graded module with projective underlying module.

instance TauCeti.PathAlgebra.moduleProjective_gradedVertexProjective (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : Module.Projective (pathAlgebra k Q) (gradedVertexProjective k Q i).carrier

The underlying module of a graded vertex projective is projective over the path algebra.

instance TauCeti.PathAlgebra.projective_gradedVertexProjective (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : CategoryTheory.Projective (gradedVertexProjective k Q i)

A graded vertex projective is projective in the graded module category.

noncomputable def TauCeti.PathAlgebra.gradedVertexProjectiveClass (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : LaurentK0 (gradedFiniteProjectiveModulesExactStructure (integerGrade k Q))

The class of the vertex projective kQ e_i in the Laurent Grothendieck group of finite graded projective modules.

theorem TauCeti.PathAlgebra.gradedVertexProjectiveClass_eq (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [CommRing k] (i : Q) : gradedVertexProjectiveClass k Q i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure (integerGrade k Q)) { obj := gradedVertexProjective k Q i, property := ⋯ }

The vertex-projective class is the Grothendieck class of the corresponding graded left ideal.

@[simp]

theorem TauCeti.PathAlgebra.coeff_gradedCartanMap_gradedVertexProjectiveClass (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [Field k] [FiniteDimensional k (pathAlgebra k Q)] (i j : Q) (n : ℕ) : ((gradedIdempotentCoordinate ⋯ ⋯) ((gradedCartanMap (integerGrade k Q)) (gradedVertexProjectiveClass k Q j))).coeff ↑n = ↑(Nat.card (PathBetween Q n j i))

The graded Cartan column of a vertex projective counts paths by length. The coefficient of q^n in the e_i-coordinate of the image of [kQ e_j] is the number of paths of length n from j to i.

@[simp]

theorem TauCeti.PathAlgebra.coeff_gradedCartanMap_gradedVertexProjectiveClass_of_neg (k : Type w) (Q : Type u) [Quiver Q] [Finite Q] [Field k] [FiniteDimensional k (pathAlgebra k Q)] (i j : Q) (d : ℤ) (hd : d < 0) : ((gradedIdempotentCoordinate ⋯ ⋯) ((gradedCartanMap (integerGrade k Q)) (gradedVertexProjectiveClass k Q j))).coeff d = 0

The graded Cartan column of a vertex projective has no negative-degree coefficients.