The graded Cartan map of a zigzag algebra

Let Z be the zigzag relation quotient of a finite simple graph, graded by path length, and let P_j = Z e_j be its graded vertex projectives. Each P_j is a finite graded module with projective underlying module, so it has a class [P_j] in the graded Grothendieck group K₀^gr(proj Z), and the graded Cartan map TauCeti.gradedCartanMap sends it to its class in G₀^gr(mod Z). This file reads that image through the idempotent coordinates TauCeti.gradedIdempotentCoordinate of the vertex idempotents e_i, which send the class of a finite graded module M to ∑ₚ dim_k(e_i • Mₚ) qᵖ.

Since e_i • (P_j)ₚ is the degree-p part of the corner e_i Z e_j, the e_i-coordinate of the image of [P_j] is the entry C_G(q)_{ij} of the graded Cartan matrix TauCeti.zigzagGradedCartanMatrix. When the graph has no isolated vertex this entry is 1 + q² on the diagonal, q on an edge and zero otherwise, so the coordinates of the graded Cartan map on the vertex projectives form the matrix

C_G(q) = (1 + q²) I + q A_G.

The determinant of C_G(q) is a nonzero polynomial, as its value at q = 0 is 1. Hence the images of the classes [P_j] are linearly independent over ℤ[q,q⁻¹] in G₀^gr(mod Z), and so are the classes [P_j] themselves in K₀^gr(proj Z). This holds for every finite graph, including graphs with isolated vertices, where the corner at an isolated vertex is spanned by its idempotent.

Every finite graded indecomposable projective is a shift of a vertex projective: the complete vertex idempotents split the regular module, and each vertex projective has a one-dimensional degree-zero endomorphism space. The classes [P_j] therefore form a basis of K₀^gr(proj Z).

The path-length grading of Z is nonnegative, and its degree-zero piece is spanned by the complete orthogonal family of vertex idempotents. The graded simple S_i, the quotient of P_i by its paths of positive length, is therefore simple, every simple finite graded Z-module is a shift S_i{d}, and the classes [S_i] form a basis of G₀^gr(mod Z) over ℤ[q,q⁻¹] whose coordinates are the idempotent coordinates (TauCeti.gradedIdempotentHeadBasis). In this basis the image of [P_j] is the jth column of the graded Cartan matrix:

c^gr [P_j] = ∑ᵢ C_G(q)_{ij} [S_i].

These statements concern the relation quotient. On a component with an edge it is the ordinary zigzag algebra; singleton components of the public algebra TauCeti.zigzagAlgebra instead use the dual numbers.

Main definitions

• TauCeti.zigzagGradedProjectiveClassBasis: the vertex-projective class basis of the actual Laurent Grothendieck group of finite graded projectives.

• TauCeti.zigzagGradedProjectiveClass: the class [P_j] in K₀^gr(proj Z).

• TauCeti.zigzagGradedSimple: the graded vertex simple S_i.

• TauCeti.zigzagGradedSimpleClassBasis: the basis [S_i] of G₀^gr(mod Z).

Main results

• TauCeti.map_subtype_smul_zigzagProjectiveGrade: e_i • (P_j)ₚ is the degree-p part of the corner e_i Z e_j.
• TauCeti.smulGradedDimension_zigzagGradedProjective: the graded dimension of e_i • P_j is the graded Cartan entry C_G(q)_{ij}.
• TauCeti.gradedIdempotentCoordinate_gradedCartanMap_zigzagGradedProjectiveClass_eq_toLaurent: the e_i-coordinate of the image of [P_j] under the graded Cartan map is C_G(q)_{ij}.
• TauCeti.gradedIdempotentCoordinate_gradedCartanMap_zigzagGradedProjectiveClass: its value (1 + q²) δᵢⱼ + q A_{ij} when no vertex is isolated.
• TauCeti.linearIndependent_gradedCartanMap_zigzagGradedProjectiveClass and TauCeti.linearIndependent_zigzagGradedProjectiveClass: the images of the vertex-projective classes in G₀^gr(mod Z), and the classes themselves in K₀^gr(proj Z), are linearly independent over ℤ[q,q⁻¹].
• TauCeti.zigzagGradedSimpleMk_mem_piece: the head projection P_i → S_i preserves degrees.
• TauCeti.simple_zigzagGradedSimple and TauCeti.isExhaustiveGradedSimpleFamily_zigzagGradedSimple: the S_i are simple, and every simple finite graded module is a shift of one of them.
• TauCeti.gradedCartanMap_zigzagGradedProjectiveClass_eq_sum: the image of [P_j] is ∑ᵢ C_G(q)_{ij} [S_i].
• TauCeti.zigzagGradedSimpleClassBasis_repr_gradedCartanMap_zigzagGradedProjectiveClass: its [S_i]-coordinate is (1 + q²) δᵢⱼ + q A_{ij} when no vertex is isolated.
• TauCeti.isExhaustiveGradedIndecomposableProjectiveFamily_zigzagGradedProjective: every finite graded indecomposable projective is an internal shift of a vertex projective.
• TauCeti.indecomposable_zigzagGradedProjective: each vertex projective is indecomposable in the category of finite graded projectives.
• TauCeti.gradedCartanMatrix_zigzag: the graded Cartan matrix is the matrix of the graded Cartan map in the vertex-projective and vertex-simple class bases.

References

• Huerfano--Khovanov, A category for the adjoint representation, Section 3, for the quantum Cartan matrix of a zigzag algebra.
• Ehrig--Tubbenhauer, Algebraic properties of zigzag algebras, Section 2.
• Dancso--Licata, Koszul algebras and flow lattices, Section 2.2, for the graded Cartan matrix as the matrix of the graded Cartan map.

The vertex projectives as finite graded projectives

theorem TauCeti.gradedFiniteProjectiveModules_zigzagGradedProjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (j : V) : gradedFiniteProjectiveModules (zigzagIntegerGrade k G) (zigzagGradedProjective k G j)

A graded vertex projective is a finite graded module with projective underlying module, so it has a class in K₀^gr(proj Z).

noncomputable def TauCeti.zigzagGradedProjectiveClass (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (j : V) : LaurentK0 (gradedFiniteProjectiveModulesExactStructure (zigzagIntegerGrade k G))

The class [P_j] of the graded vertex projective P_j = Z e_j in the graded Grothendieck group K₀^gr(proj Z) of finite graded projective modules.

theorem TauCeti.zigzagGradedProjectiveClass_def (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (j : V) : zigzagGradedProjectiveClass k G j = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure (zigzagIntegerGrade k G)) { obj := zigzagGradedProjective k G j, property := ⋯ }

The class [P_j] is the Grothendieck class of the graded vertex projective.

Idempotent pieces of the vertex projectives

theorem TauCeti.map_subtype_smul_zigzagProjectiveGrade (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (p : ℤ) : Submodule.map (↑k (Submodule.subtype (zigzagProjective k G j))) (zigzagVertexIdempotent k G i • zigzagProjectiveGrade k G j p) = zigzagIntegerGradedCorner k G i j p

The idempotent pieces of a vertex projective are graded corners: e_i • (P_j)ₚ, viewed inside Z, is the degree-p part of the corner e_i Z e_j.

theorem TauCeti.finrank_smul_zigzagProjectiveGrade (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (p : ℤ) : Module.finrank k ↥(zigzagVertexIdempotent k G i • zigzagProjectiveGrade k G j p) = Module.finrank k ↥(zigzagIntegerGradedCorner k G i j p)

The dimension of e_i • (P_j)ₚ is the dimension of the degree-p corner of e_i Z e_j.

theorem TauCeti.smulGradedDimension_zigzagGradedProjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : GradedModuleCat.smulGradedDimension (zigzagVertexIdempotent k G i) (zigzagGradedProjective k G j) = Polynomial.toLaurent (zigzagGradedCartanMatrix k G i j)

The graded dimension of e_i • P_j is the graded Cartan entry C_G(q)_{ij}.

The graded Cartan map on the vertex projectives

theorem TauCeti.gradedIdempotentCoordinate_gradedCartanMap_zigzagGradedProjectiveClass_eq_toLaurent (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : (gradedIdempotentCoordinate ⋯ ⋯) ((gradedCartanMap (zigzagIntegerGrade k G)) (zigzagGradedProjectiveClass k G j)) = Polynomial.toLaurent (zigzagGradedCartanMatrix k G i j)

The coordinates of the graded Cartan map are the graded Cartan matrix. The e_i-coordinate of the image of [P_j] in G₀^gr(mod Z) is the entry C_G(q)_{ij}.

theorem TauCeti.gradedIdempotentCoordinate_gradedCartanMap_zigzagGradedProjectiveClass (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] [DecidableEq V] [DecidableRel G.Adj] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i j : V) : (gradedIdempotentCoordinate ⋯ ⋯) ((gradedCartanMap (zigzagIntegerGrade k G)) (zigzagGradedProjectiveClass k G j)) = (if i = j then 1 + LaurentPolynomial.T 2 else 0) + if G.Adj i j then LaurentPolynomial.T 1 else 0

The graded Cartan map of a zigzag algebra has matrix (1 + q²) I + q A_G in the idempotent coordinates on the vertex projectives, for a graph without isolated vertices: the e_i-coordinate of the image of [P_j] is 1 + q² for i = j, q on an edge and zero otherwise.

theorem TauCeti.linearIndependent_gradedCartanMap_zigzagGradedProjectiveClass (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] : LinearIndependent (LaurentPolynomial ℤ) (⇑(gradedCartanMap (zigzagIntegerGrade k G)) ∘ zigzagGradedProjectiveClass k G)

The images of the vertex-projective classes under the graded Cartan map are linearly independent over ℤ[q,q⁻¹]: their idempotent coordinates form the graded Cartan matrix, whose determinant is a nonzero polynomial.

theorem TauCeti.linearIndependent_zigzagGradedProjectiveClass (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] : LinearIndependent (LaurentPolynomial ℤ) (zigzagGradedProjectiveClass k G)

The vertex-projective classes are linearly independent in K₀^gr(proj Z) over ℤ[q,q⁻¹], since their images under the graded Cartan map are.

The graded simples and the simple-class basis

noncomputable def TauCeti.zigzagGradedSimple (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : GradedModuleCat (zigzagIntegerGrade k G)

The graded simple module S_i at a vertex: the head of the graded vertex projective P_i = Z e_i, its quotient by the span of the paths of positive length starting at i.

theorem TauCeti.zigzagGradedSimple_def (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagGradedSimple k G i = have x := zigzagIntegerGradedAlgebra k G; gradedPositiveMulQuotient (zigzagIntegerGrade k G) ⋯

A graded vertex simple is the generic graded head of its vertex idempotent.

noncomputable def TauCeti.zigzagGradedSimpleMk (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : ↥(Ideal.span {zigzagVertexIdempotent k G i}) →ₗ[nonisolatedZigzagQuotient k G] (zigzagGradedSimple k G i).carrier

The class of a vertex-projective element in its graded simple head.

theorem TauCeti.zigzagGradedSimpleMk_def (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagGradedSimpleMk k G i = let x := zigzagIntegerGradedAlgebra k G; (CategoryTheory.eqToHom ⋯).hom ∘ₗ gradedPositiveMulQuotientMk ⋯

The head projection is the generic quotient map, transported to the graded vertex simple.

theorem TauCeti.zigzagGradedSimpleMk_surjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Function.Surjective ⇑(zigzagGradedSimpleMk k G i)

Every element of the graded simple head has a vertex-projective representative.

@[simp]

theorem TauCeti.zigzagGradedSimpleMk_eq_zero_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (x : ↥(Ideal.span {zigzagVertexIdempotent k G i})) : (zigzagGradedSimpleMk k G i) x = 0 ↔ ↑x ∈ gradedPositiveMulIdeal (zigzagIntegerGrade k G) (zigzagVertexIdempotent k G i)

A representative vanishes in the graded head exactly when it lies in the positive-degree ideal of its vertex projective.

theorem TauCeti.zigzagGradedSimpleMk_mem_piece (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) {p : ℤ} (x : ↥(Ideal.span {zigzagVertexIdempotent k G i})) (hx : ↑x ∈ zigzagIntegerGrade k G p) : (zigzagGradedSimpleMk k G i) x ∈ (zigzagGradedSimple k G i).grading.piece ℤ p

The head projection preserves degrees: the class of a homogeneous representative of degree p lies in the degree-p piece of the graded vertex simple.

theorem TauCeti.gradedFiniteModules_zigzagGradedSimple (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : gradedFiniteModules (zigzagIntegerGrade k G) (zigzagGradedSimple k G i)

A graded vertex simple is a finite graded module.

theorem TauCeti.simple_zigzagGradedSimple (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.Simple (zigzagGradedSimple k G i)

The graded vertex simples are simple graded modules.

instance TauCeti.instFiniteCarrierNonisolatedZigzagQuotientZigzagGradedSimple (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Module.Finite k (zigzagGradedSimple k G i).carrier

A graded vertex simple is finite-dimensional.

@[simp]

theorem TauCeti.smulGradedDimension_zigzagGradedSimple (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] [DecidableEq V] (j i : V) : GradedModuleCat.smulGradedDimension (zigzagVertexIdempotent k G j) (zigzagGradedSimple k G i) = if j = i then 1 else 0

The graded dimension of e_j • S_i is δ_{ji}: the graded vertex simple S_i is one-dimensional, concentrated in degree zero, and the vertex idempotent e_j acts on it by δ_{ji}.

theorem TauCeti.isExhaustiveGradedSimpleFamily_zigzagGradedSimple (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] : IsExhaustiveGradedSimpleFamily fun (i : V) => { obj := zigzagGradedSimple k G i, property := ⋯ }

Every simple finite graded Z-module is a shift S_i{d} of a graded vertex simple.

noncomputable def TauCeti.zigzagGradedSimpleClassBasis (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] : Module.Basis V (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure (zigzagIntegerGrade k G)))

The simple-class basis of G₀^gr(mod Z) over ℤ[q,q⁻¹]: its vector at i is the class [S_i] of the graded vertex simple.

@[simp]

theorem TauCeti.zigzagGradedSimpleClassBasis_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagGradedSimpleClassBasis k G) i = LaurentK0.of (gradedFiniteModulesExactStructure (zigzagIntegerGrade k G)) { obj := zigzagGradedSimple k G i, property := ⋯ }

The basis vector of TauCeti.zigzagGradedSimpleClassBasis at i is the class [S_i].

@[simp]

theorem TauCeti.zigzagGradedSimpleClassBasis_repr_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (x : LaurentK0 (gradedFiniteModulesExactStructure (zigzagIntegerGrade k G))) (i : V) : ((zigzagGradedSimpleClassBasis k G).repr x) i = (gradedIdempotentCoordinate ⋯ ⋯) x

The coordinates in the basis [S_i] are the idempotent coordinates of the vertex idempotents: the ith coordinate of [M] is ∑ₚ dim_k(e_i • Mₚ) qᵖ.

The graded Cartan map in the simple basis

theorem TauCeti.zigzagGradedSimpleClassBasis_repr_gradedCartanMap_zigzagGradedProjectiveClass_eq_toLaurent (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : ((zigzagGradedSimpleClassBasis k G).repr ((gradedCartanMap (zigzagIntegerGrade k G)) (zigzagGradedProjectiveClass k G j))) i = Polynomial.toLaurent (zigzagGradedCartanMatrix k G i j)

The graded Cartan matrix records the composition factors of the vertex projectives. The [S_i]-coordinate of the image of [P_j] in G₀^gr(mod Z) is the graded Cartan entry C_G(q)_{ij}.

theorem TauCeti.gradedCartanMap_zigzagGradedProjectiveClass_eq_sum (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] [Fintype V] (j : V) : (gradedCartanMap (zigzagIntegerGrade k G)) (zigzagGradedProjectiveClass k G j) = ∑ i : V, Polynomial.toLaurent (zigzagGradedCartanMatrix k G i j) • (zigzagGradedSimpleClassBasis k G) i

The image of [P_j] under the graded Cartan map is ∑ᵢ C_G(q)_{ij} [S_i] in G₀^gr(mod Z): the jth column of the graded Cartan matrix in the simple basis.

theorem TauCeti.zigzagGradedSimpleClassBasis_repr_gradedCartanMap_zigzagGradedProjectiveClass (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] [DecidableEq V] [DecidableRel G.Adj] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i j : V) : ((zigzagGradedSimpleClassBasis k G).repr ((gradedCartanMap (zigzagIntegerGrade k G)) (zigzagGradedProjectiveClass k G j))) i = (if i = j then 1 + LaurentPolynomial.T 2 else 0) + if G.Adj i j then LaurentPolynomial.T 1 else 0

The graded Cartan matrix (1 + q²) I + q A_G in the simple basis, for a graph without isolated vertices: the [S_i]-coordinate of the image of [P_j] is 1 + q² for i = j, q on an edge and zero otherwise.

The projective-class basis and the categorical Cartan matrix

theorem TauCeti.indecomposable_zigzagGradedProjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.Indecomposable { obj := zigzagGradedProjective k G i, property := ⋯ }

A zigzag vertex projective is indecomposable as a finite graded projective: its degree-zero endomorphism space is one-dimensional, including at an isolated vertex.

theorem TauCeti.isExhaustiveGradedIndecomposableProjectiveFamily_zigzagGradedProjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] : IsExhaustiveGradedIndecomposableProjectiveFamily fun (i : V) => { obj := zigzagGradedProjective k G i, property := ⋯ }

Every finite graded indecomposable projective of the zigzag relation quotient is an internal shift of a vertex projective. This includes graphs with isolated vertices.

noncomputable def TauCeti.zigzagGradedProjectiveClassBasis (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] : Module.Basis V (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure (zigzagIntegerGrade k G)))

The vertex-projective classes form a basis of the actual graded projective Grothendieck group over ℤ[q,q⁻¹]. Internal shifts are represented by Laurent scalar multiplication.

@[simp]

theorem TauCeti.zigzagGradedProjectiveClassBasis_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagGradedProjectiveClassBasis k G) i = zigzagGradedProjectiveClass k G i

The basis vector at i is the class of the graded vertex projective Z e_i.

theorem TauCeti.gradedCartanMatrix_zigzag (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] [Fintype V] : gradedCartanMatrix (zigzagIntegerGrade k G) (zigzagGradedProjectiveClassBasis k G) (zigzagGradedSimpleClassBasis k G) = (zigzagGradedCartanMatrix k G).map ⇑Polynomial.toLaurent

The combinatorial graded Cartan matrix is the matrix of the categorical graded Cartan map in the vertex-projective and vertex-simple class bases.