The graded Cartan matrix of a zigzag algebra

For a finite simple graph without isolated vertices, the vertex idempotents e_i of the zigzag relation quotient Z are primitive, so Z e_i is the indecomposable projective at i and the corner e_i Z e_j records the homomorphisms from Z e_i to Z e_j. This file computes those corners degree by degree for the path-length grading and assembles the resulting graded Cartan matrix.

The three nonzero graded corners are read off the vertex-arrow-volume basis: the vertex idempotent e_i spans the degree-zero corner at (i, i), the arrow of the dart from j to i spans the degree-one corner at (i, j), and the volume class x_i spans the degree-two corner at (i, i). Everything else vanishes, so

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

with A_G the adjacency matrix of the graph. At q = 0 it is the identity, so its polynomial determinant is nonzero. At q = 1 it is the ungraded Cartan matrix 2I + A_G, whose column sums are the dimensions of the vertex projectives; at q = -1 it is the generalized Cartan matrix 2I - A_G of the graph.

Main definitions

• TauCeti.zigzagCorner: the corner e_i Z e_j, as a k-submodule of the relation quotient.
• TauCeti.zigzagGradedCorner: its degree-n piece for the path-length grading.
• TauCeti.zigzagGradedCartanMatrix: the matrix of graded dimensions of the corners, a matrix of polynomials in q.

Main results

• TauCeti.restrictScalars_zigzagProjective_eq_iSup_zigzagCorner: the vertex projective Z e_j is the sum of the corners e_i Z e_j.
• TauCeti.zigzagGradedCorner_zero_self_eq_span, TauCeti.zigzagGradedCorner_one_eq_span_of_adj and TauCeti.zigzagGradedCorner_two_self_eq_span: the three nonvanishing graded corners, each spanned by a single basis vector, together with the vanishing of all the others.
• TauCeti.zigzagGradedCartanMatrix_apply: the entrywise graded Cartan formula.
• TauCeti.zigzagGradedCartanMatrix_eq: the same formula in matrix notation, C_G(q) = (1 + q²) I + q A_G.
• TauCeti.zigzagGradedCartanMatrix_map_eval_zero and TauCeti.det_zigzagGradedCartanMatrix_ne_zero: the specialization at q = 0 is the identity, so the determinant is a nonzero polynomial.
• TauCeti.zigzagGradedCartanMatrix_map_eval_one and TauCeti.zigzagGradedCartanMatrix_map_eval_neg_one: the two specializations 2I + A_G and 2I - A_G.
• TauCeti.sum_eval_one_zigzagGradedCartanMatrix_eq_finrank_zigzagProjective: the column sums at q = 1 are the dimensions of the vertex projectives.

Implementation notes

The graded Cartan entry is defined as the truncated sum ∑_{n < 3} dim (e_i Z e_j)_n q^n rather than as a sum over all degrees. The truncation loses nothing: TauCeti.finrank_zigzagGradedCorner_of_three_le proves that every corner of degree at least three vanishes, because the whole degree-n piece of the zigzag quotient does.

The corners here are the graded homomorphism spaces of the vertex projectives only through the standard dictionary Hom_Z(Z e_i, Z e_j) ≅ e_i Z e_j, which this file does not construct; what it does prove about the projectives themselves is TauCeti.restrictScalars_zigzagProjective_eq_iSup_zigzagCorner, that Z e_j is the sum of the corners e_i Z e_j over i, together with the resulting numerical comparison TauCeti.sum_eval_one_zigzagGradedCartanMatrix_eq_finrank_zigzagProjective.

References

See Huerfano--Khovanov, A category for the adjoint representation, Section 3, and Ehrig--Tubbenhauer, Algebraic properties of zigzag algebras, Section 2.

The corners of a zigzag algebra

noncomputable def TauCeti.zigzagCornerMap (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : nonisolatedZigzagQuotient k G →ₗ[k] nonisolatedZigzagQuotient k G

Cutting an element of the zigzag relation quotient down to the corner at (i, j), that is, multiplying it by e_i on the left and by e_j on the right.

@[simp]

theorem TauCeti.zigzagCornerMap_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (x : nonisolatedZigzagQuotient k G) : (zigzagCornerMap k G i j) x = zigzagVertexIdempotent k G i * x * zigzagVertexIdempotent k G j

noncomputable def TauCeti.zigzagCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : Submodule k (nonisolatedZigzagQuotient k G)

The corner e_i Z e_j of a zigzag algebra, as a k-submodule of the relation quotient: the elements which e_i fixes on the left and e_j fixes on the right.

@[simp]

theorem TauCeti.mem_zigzagCorner_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {x : nonisolatedZigzagQuotient k G} : x ∈ zigzagCorner k G i j ↔ zigzagVertexIdempotent k G i * x * zigzagVertexIdempotent k G j = x

Membership in the corner e_i Z e_j: an element belongs to it exactly when multiplying it by e_i on the left and by e_j on the right fixes it.

theorem TauCeti.mem_zigzagProjective_of_mem_zigzagCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {x : nonisolatedZigzagQuotient k G} (hx : x ∈ zigzagCorner k G i j) : x ∈ zigzagProjective k G j

The corner e_i Z e_j sits inside the vertex projective Z e_j.

theorem TauCeti.zigzagVertexIdempotent_mem_zigzagCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagVertexIdempotent k G i ∈ zigzagCorner k G i i

The vertex idempotent at i lies in the corner at (i, i).

theorem TauCeti.zigzagMk_ofArrow_mem_zigzagCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) : (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) ∈ zigzagCorner k G d.toProd.2 d.toProd.1

The arrow of a dart lies in the corner at (head, tail): in the later-factor-first convention the arrow of d is fixed on the left by the idempotent at the head of d and on the right by the idempotent at its tail.

theorem TauCeti.zigzagVolume_mem_zigzagCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagVolume k G i ∈ zigzagCorner k G i i

The volume class at i lies in the corner at (i, i).

theorem TauCeti.restrictScalars_zigzagProjective_eq_iSup_zigzagCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (j : V) : Submodule.restrictScalars k (zigzagProjective k G j) = ⨆ (i : V), zigzagCorner k G i j

The vertex projective Z e_j is the sum of the corners e_i Z e_j. Cutting the vertex-arrow-volume basis down by e_j leaves the idempotent e_j, the arrows leaving j, and the volume class x_j, and each of them lies in one corner.

The graded corners

noncomputable def TauCeti.zigzagGradedCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (n : ℕ) : Submodule k (nonisolatedZigzagQuotient k G)

The degree-n part of the corner e_i Z e_j for the path-length grading of the zigzag relation quotient.

@[simp]

theorem TauCeti.mem_zigzagGradedCorner_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {n : ℕ} {x : nonisolatedZigzagQuotient k G} : x ∈ zigzagGradedCorner k G i j n ↔ x ∈ zigzagCorner k G i j ∧ x ∈ zigzagGrade k G n

Membership in a graded corner: an element belongs to it exactly when it lies in the corner and is homogeneous of that degree.

theorem TauCeti.zigzagGradedCorner_le_zigzagCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (n : ℕ) : zigzagGradedCorner k G i j n ≤ zigzagCorner k G i j

A graded corner sits inside the corner it grades.

theorem TauCeti.zigzagGradedCorner_zero_self_eq_span (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagGradedCorner k G i i 0 = k ∙ zigzagVertexIdempotent k G i

The degree-zero corner at a vertex is spanned by its idempotent.

theorem TauCeti.zigzagGradedCorner_zero_eq_bot_of_ne (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : i ≠ j) : zigzagGradedCorner k G i j 0 = ⊥

The degree-zero corner between distinct vertices vanishes.

theorem TauCeti.zigzagGradedCorner_one_eq_span_of_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) : zigzagGradedCorner k G i j 1 = k ∙ (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G h))

The degree-one corner over an edge is spanned by the arrow crossing it. The corner at (i, j) sees the arrow which starts at j and ends at i.

theorem TauCeti.zigzagGradedCorner_one_eq_bot_of_not_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : ¬G.Adj j i) : zigzagGradedCorner k G i j 1 = ⊥

The degree-one corner over a nonedge vanishes.

theorem TauCeti.zigzagGradedCorner_two_self_eq_span (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagGradedCorner k G i i 2 = k ∙ zigzagVolume k G i

The degree-two corner at a vertex is spanned by its volume class.

theorem TauCeti.zigzagGradedCorner_two_eq_bot_of_ne (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : i ≠ j) : zigzagGradedCorner k G i j 2 = ⊥

The degree-two corner between distinct vertices vanishes.

theorem TauCeti.zigzagGradedCorner_eq_bot_of_three_le (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {n : ℕ} (hn : 3 ≤ n) : zigzagGradedCorner k G i j n = ⊥

Every corner of degree at least three vanishes, because the whole degree-n piece does.

The dimensions of the graded corners

theorem TauCeti.finrank_zigzagGradedCorner_zero_self (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Module.finrank k ↥(zigzagGradedCorner k G i i 0) = 1

The degree-zero corner at a vertex is one-dimensional.

theorem TauCeti.finrank_zigzagGradedCorner_zero_of_ne (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : i ≠ j) : Module.finrank k ↥(zigzagGradedCorner k G i j 0) = 0

The degree-zero corner between distinct vertices has dimension zero.

theorem TauCeti.finrank_zigzagGradedCorner_one_of_not_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : ¬G.Adj j i) : Module.finrank k ↥(zigzagGradedCorner k G i j 1) = 0

The degree-one corner over a nonedge has dimension zero.

theorem TauCeti.finrank_zigzagGradedCorner_two_of_ne (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : i ≠ j) : Module.finrank k ↥(zigzagGradedCorner k G i j 2) = 0

The degree-two corner between distinct vertices has dimension zero.

theorem TauCeti.finrank_zigzagGradedCorner_of_three_le (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {n : ℕ} (hn : 3 ≤ n) : Module.finrank k ↥(zigzagGradedCorner k G i j n) = 0

The graded Cartan entries vanish in every degree at least three: this is what makes the truncated sum defining TauCeti.zigzagGradedCartanMatrix lose nothing.

theorem TauCeti.finrank_zigzagGradedCorner_one_of_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) : Module.finrank k ↥(zigzagGradedCorner k G i j 1) = 1

The degree-one corner over an edge is one-dimensional: the arrow crossing the edge is nonzero because traversing it and returning is the nonzero volume class at its head.

theorem TauCeti.finrank_zigzagGradedCorner_two_self_of_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj i j) : Module.finrank k ↥(zigzagGradedCorner k G i i 2) = 1

The degree-two corner at a vertex with a neighbour is one-dimensional.

The graded Cartan matrix

noncomputable def TauCeti.zigzagGradedCartanMatrix (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] : Matrix V V (Polynomial ℤ)

The graded Cartan matrix of a zigzag algebra: the entry at (i, j) is the graded dimension ∑_n dim_k (e_i Z e_j)_n q^n of the corner at (i, j), a polynomial in the internal degree q. The sum is truncated below degree three, which by TauCeti.finrank_zigzagGradedCorner_of_three_le discards only zeros.

theorem TauCeti.zigzagGradedCartanMatrix_apply_eq_sum (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : zigzagGradedCartanMatrix k G i j = ↑(Module.finrank k ↥(zigzagGradedCorner k G i j 0)) + ↑(Module.finrank k ↥(zigzagGradedCorner k G i j 1)) * Polynomial.X + ↑(Module.finrank k ↥(zigzagGradedCorner k G i j 2)) * Polynomial.X ^ 2

theorem TauCeti.zigzagGradedCartanMatrix_apply_of_ne_of_not_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (hne : i ≠ j) (h : ¬G.Adj i j) : zigzagGradedCartanMatrix k G i j = 0

The graded Cartan entry away from the diagonal and from the edges vanishes.

theorem TauCeti.zigzagGradedCartanMatrix_apply_self_of_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj i j) : zigzagGradedCartanMatrix k G i i = 1 + Polynomial.X ^ 2

The diagonal graded Cartan entry at a vertex with a neighbour is 1 + q²: the vertex idempotent in degree zero and the volume class in degree two.

theorem TauCeti.zigzagGradedCartanMatrix_apply_of_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj i j) : zigzagGradedCartanMatrix k G i j = Polynomial.X

The graded Cartan entry over an edge is q: the single arrow crossing it.

theorem TauCeti.isSymm_zigzagGradedCartanMatrix (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] : (zigzagGradedCartanMatrix k G).IsSymm

The graded Cartan matrix is symmetric: the graph is undirected.

@[simp]

theorem TauCeti.zigzagGradedCartanMatrix_map_eval_zero (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Finite V] : (zigzagGradedCartanMatrix k G).map (Polynomial.eval 0) = 1

At q = 0 the graded Cartan matrix is the identity matrix. Only the degree-zero vertex idempotents survive this specialization.

theorem TauCeti.det_zigzagGradedCartanMatrix_ne_zero (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] : (zigzagGradedCartanMatrix k G).det ≠ 0

The determinant of a finite zigzag graded Cartan matrix is a nonzero polynomial. Its value at q = 0 is the determinant of the identity matrix, hence 1.

theorem TauCeti.zigzagGradedCartanMatrix_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) [Finite V] [DecidableEq V] [DecidableRel G.Adj] (i j : V) : zigzagGradedCartanMatrix k G i j = (if i = j then 1 + Polynomial.X ^ 2 else 0) + if G.Adj i j then Polynomial.X else 0

The entrywise graded Cartan formula. The diagonal entries are 1 + q², the entries over an edge are q, and all the others vanish.

theorem TauCeti.zigzagGradedCartanMatrix_eq (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) [Finite V] [DecidableEq V] [DecidableRel G.Adj] : zigzagGradedCartanMatrix k G = (1 + Polynomial.X ^ 2) • 1 + Polynomial.X • SimpleGraph.adjMatrix (Polynomial ℤ) G

The graded Cartan matrix of a zigzag algebra is (1 + q²) I + q A_G.

theorem TauCeti.zigzagGradedCartanMatrix_map_eval_one (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) [Finite V] [DecidableEq V] [DecidableRel G.Adj] : (zigzagGradedCartanMatrix k G).map (Polynomial.eval 1) = 2 • 1 + SimpleGraph.adjMatrix ℤ G

At q = 1 the graded Cartan matrix is the ungraded one, 2I + A_G.

theorem TauCeti.zigzagGradedCartanMatrix_map_eval_neg_one (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) [Finite V] [DecidableEq V] [DecidableRel G.Adj] : (zigzagGradedCartanMatrix k G).map (Polynomial.eval (-1)) = 2 • 1 - SimpleGraph.adjMatrix ℤ G

At q = -1 the graded Cartan matrix is the generalized Cartan matrix 2I - A_G of the graph.

theorem TauCeti.sum_eval_one_zigzagGradedCartanMatrix (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) [Fintype V] [DecidableRel G.Adj] (j : V) : ∑ i : V, Polynomial.eval 1 (zigzagGradedCartanMatrix k G i j) = 2 + ↑(G.degree j)

The column sums of the ungraded Cartan matrix are 2 + deg(j).

theorem TauCeti.sum_eval_one_zigzagGradedCartanMatrix_eq_finrank_zigzagProjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) [Fintype V] (j : V) : ∑ i : V, Polynomial.eval 1 (zigzagGradedCartanMatrix k G i j) = ↑(Module.finrank k ↥(zigzagProjective k G j))

The column sums of the ungraded Cartan matrix are the dimensions of the vertex projectives. The vertex projective Z e_j is the sum of the corners e_i Z e_j over the vertices i, and this is that decomposition read in dimensions.