The vertex, arrow and volume basis of a zigzag algebra

The zigzag relation quotient TauCeti.nonisolatedZigzagQuotient of a finite simple graph G kills every length-two path whose endpoints differ, identifies all the backtracks based at one vertex, and kills every path of length at least three. What survives is spanned by the vertex idempotents, the oriented edges, and one volume class per vertex. This file proves that these classes are a basis whenever G has no isolated vertex, and reads off the dimension 2|V| + 2|E|.

Spanning is immediate from the relations. Independence is the substantive half, and is proved by exhibiting a coordinate map. The path algebra is free on the paths of the doubled quiver, so a k-linear map out of it may be prescribed on paths: send a path of length at most one to itself, a length-two path returning to its source to a fixed backtrack there, and everything else to 0. Sandwiching a relator between two basis paths either produces a path of length at least three or, when both outer paths are trivial, the relator itself, so this map kills the relation ideal. It therefore separates the candidate basis classes, which it sends to distinct basis paths.

The hypothesis is that every vertex has a neighbour: an isolated vertex carries no backtrack, so its volume class does not exist. For a preconnected graph with at least two vertices the hypothesis is automatic.

Main definitions

• TauCeti.zigzagVolume: the volume class of a vertex, the common image of its backtracks.
• TauCeti.ZigzagBasisIndex: one index per vertex, carrying its idempotent, one per dart, carrying its arrow, and one more per vertex, carrying its volume class.
• TauCeti.zigzagBasisFun: the vertex, arrow and volume family.
• TauCeti.zigzagBasis: that family, as a basis of the zigzag relation quotient.

Main results

• TauCeti.linearIndependent_zigzagBasisFun and TauCeti.span_range_zigzagBasisFun_eq_top: the family is independent and spans.
• TauCeti.linearIndependent_zigzagVolume: the volume classes are linearly independent.
• TauCeti.zigzagBasis_coord_apply: the basis coordinates of basis vectors are Kronecker deltas.
• TauCeti.finrank_nonisolatedZigzagQuotient: the dimension is 2|V| + 2|E|.
• TauCeti.finrank_nonisolatedZigzagQuotient_of_preconnected: the same count for a preconnected graph with at least two vertices.

References

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

A chosen backtrack at each vertex

Volume classes

noncomputable def TauCeti.zigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : nonisolatedZigzagQuotient k G

The volume class of a vertex of a simple graph: the common image in the zigzag relation quotient of all the backtracks based at that vertex, which TauCeti.zigzagMk_backtrackElem_eq shows is independent of the incident edge chosen. It is the junk value 0 on an isolated vertex, which carries no backtrack.

theorem TauCeti.zigzagVolume_eq_zigzagMk_backtrackElem (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj i j) : zigzagVolume k G i = (zigzagMk k G) (DoubledQuiver.backtrackElem G k h)

The volume class of a vertex is the class of any backtrack based there.

@[simp]

theorem TauCeti.zigzagMk_backtrackElem_eq_zigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj i j) : (zigzagMk k G) (DoubledQuiver.backtrackElem G k h) = zigzagVolume k G i

The class of a backtrack is the volume class of its base vertex. This is the direction automation can use: both endpoints are determined by the adjacency on the left-hand side.

@[simp]

theorem TauCeti.zigzagVolume_eq_zero_of_isIsolated (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i : V} (h : G.IsIsolated i) : zigzagVolume k G i = 0

The volume class of an isolated vertex is the junk value 0: it carries no backtrack.

The vertex, arrow and volume family

@[reducible, inline]

abbrev TauCeti.ZigzagBasisIndex {V : Type u} (G : SimpleGraph V) : Type u

The basis indices of a zigzag algebra: a vertex, carrying its idempotent, an oriented edge, carrying its arrow, and a vertex again, carrying its volume class. The three blocks are represented by paths of length zero, one and two respectively.

noncomputable def TauCeti.zigzagBasisFun (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : ZigzagBasisIndex G → nonisolatedZigzagQuotient k G

The vertex, arrow and volume family of a zigzag algebra: the class of a vertex idempotent, the class of the arrow of a dart, and the volume class of a vertex.

@[simp]

theorem TauCeti.zigzagBasisFun_inl (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagBasisFun k G (Sum.inl i) = (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i))

@[simp]

theorem TauCeti.zigzagBasisFun_inr_inl (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) : zigzagBasisFun k G (Sum.inr (Sum.inl d)) = (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯))

@[simp]

theorem TauCeti.zigzagBasisFun_inr_inr (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagBasisFun k G (Sum.inr (Sum.inr i)) = zigzagVolume k G i

The coordinate map

The coordinate map kills the relation ideal

The basis

theorem TauCeti.linearIndependent_zigzagBasisFun (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) : LinearIndependent k (zigzagBasisFun k G)

The vertex, arrow and volume classes are independent.

theorem TauCeti.linearIndependent_zigzagVolume {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) : LinearIndependent k (zigzagVolume k G)

The volume classes are linearly independent.

theorem TauCeti.span_range_zigzagBasisFun_eq_top (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : Submodule.span k (Set.range (zigzagBasisFun k G)) = ⊤

The vertex, arrow and volume classes span.

noncomputable def TauCeti.zigzagBasis (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) : Module.Basis (ZigzagBasisIndex G) k (nonisolatedZigzagQuotient k G)

The basis of a zigzag algebra. For a finite simple graph with no isolated vertex the vertex idempotents, the oriented edges, and the volume classes are a basis of the zigzag relation quotient. The three blocks are represented by paths of length 0, 1 and 2; the path grading itself is not formalised in this repository, so homogeneity is not stated here.

@[simp]

theorem TauCeti.zigzagBasis_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (b : ZigzagBasisIndex G) : (zigzagBasis k G hns) b = zigzagBasisFun k G b

theorem TauCeti.zigzagBasis_coord_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (b b' : ZigzagBasisIndex G) : ((zigzagBasis k G hns).coord b) ((zigzagBasis k G hns) b') = if b' = b then 1 else 0

A coordinate of a zigzag basis vector is the corresponding Kronecker delta.

theorem TauCeti.zigzagVolume_ne_zero (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] [Nontrivial k] {i j : V} (h : G.Adj i j) : zigzagVolume k G i ≠ 0

The volume class of a vertex with a neighbour is nonzero, whatever the rest of the graph does: its chosen backtrack survives the coordinate map.

theorem TauCeti.zigzagVolume_smul_left_injective (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj i j) : Function.Injective fun (r : k) => r • zigzagVolume k G i

Scalar multiplication of a volume class at a nonisolated vertex is injective.

The dimension

theorem TauCeti.finrank_nonisolatedZigzagQuotient (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] [Nontrivial k] [Fintype V] [DecidableRel G.Adj] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) : Module.finrank k (nonisolatedZigzagQuotient k G) = 2 * Fintype.card V + 2 * G.edgeFinset.card

The dimension of a zigzag algebra. A finite simple graph with no isolated vertex has dim Z(G) = 2|V| + 2|E|: two classes at each vertex and two arrows over each edge.

theorem TauCeti.finrank_nonisolatedZigzagQuotient_of_preconnected (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] [Nontrivial k] [Fintype V] [Nontrivial V] [DecidableRel G.Adj] (hconn : G.Preconnected) : Module.finrank k (nonisolatedZigzagQuotient k G) = 2 * Fintype.card V + 2 * G.edgeFinset.card

The dimension of the zigzag algebra of a preconnected graph. For a preconnected graph with at least two vertices, dim Z(G) = 2|V| + 2|E|: preconnectedness leaves no isolated vertex.