The multiplication table of a zigzag algebra

The zigzag relation quotient TauCeti.nonisolatedZigzagQuotient of a simple graph G is spanned by the vertex idempotents e_i, the oriented edges a_d of the darts of G, and the volume classes x_i; TauCeti.zigzagBasis shows these are a basis when no vertex is isolated. This file computes every product of two of them, which is what makes the algebra explicit.

The table is short. The idempotents are orthogonal and act as the local units they are; an arrow is absorbed by the idempotent at its head on the left and by the one at its tail on the right; a volume class is absorbed by the idempotent at its base on either side. Two arrows multiply to a volume class exactly when the later factor is the reverse dart of the earlier one, since a length-two path survives the relations only if it returns to its source. Everything else vanishes: a product landing in path length at least three is killed by the long generators, and a product of two paths that do not meet is already zero in the path algebra.

In Tau Ceti's later-factor-first convention the product a_d * a_e traverses e first, so it is nonzero exactly when e = d.symm, and then it is the volume class at d.snd, the vertex where the composite begins and ends.

All the statements are unconditional: at an isolated vertex the volume class is the junk value 0, and each identity below degenerates to a true statement about 0 there.

Main results

• TauCeti.zigzagMk_ofArrow_mul_ofArrow_symm and TauCeti.zigzagMk_ofArrow_mul_ofArrow_of_ne: two arrows multiply to a volume class when the second is the reverse of the first, and to zero otherwise.
• TauCeti.zigzagMk_ofArrow_mul and TauCeti.mul_zigzagMk_ofArrow: left and right multiplication by an arrow read off two coordinates in the vertex-arrow-volume basis.
• TauCeti.zigzagMk_vertexIdempotent_mul_zigzagVolume and its three companions: the idempotent at the base of a volume class is a two-sided unit for it, and the other idempotents kill it.
• TauCeti.zigzagMk_ofArrow_mul_zigzagVolume, TauCeti.zigzagVolume_mul_zigzagMk_ofArrow and TauCeti.zigzagVolume_mul_zigzagVolume: every product reaching path length three vanishes.
• TauCeti.zigzagBasis_mul: the whole table, as products of basis vectors.
• TauCeti.zigzagBasis_coord_dart_mul: the arrow coordinates of a product, which only see the idempotents at the two ends of the arrow.
• TauCeti.zigzagVolume_mul and TauCeti.mul_zigzagVolume: a volume class absorbs only the idempotent coordinate at its base.

References

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

noncomputable def TauCeti.zigzagBasisMul {V : Type u} (G : SimpleGraph V) : ZigzagBasisIndex G → ZigzagBasisIndex G → Option (ZigzagBasisIndex G)

The product index for the vertex--dart--volume basis of the public componentwise zigzag algebra. none denotes a zero product in that algebra. In the nonisolated relation quotient, a returned volume index at an isolated vertex still denotes the zero junk value. The left factor is traversed second.

@[simp]

theorem TauCeti.zigzagBasisMul_vertex_vertex {V : Type u} (G : SimpleGraph V) (i j : V) : zigzagBasisMul G (Sum.inl i) (Sum.inl j) = if i = j then some (Sum.inl i) else none

The product index of two vertex vectors.

@[simp]

theorem TauCeti.zigzagBasisMul_vertex_dart {V : Type u} (G : SimpleGraph V) (i : V) (d : G.Dart) : zigzagBasisMul G (Sum.inl i) (Sum.inr (Sum.inl d)) = if i = d.toProd.2 then some (Sum.inr (Sum.inl d)) else none

The product index of a vertex vector and a dart vector.

@[simp]

theorem TauCeti.zigzagBasisMul_vertex_volume {V : Type u} (G : SimpleGraph V) (i j : V) : zigzagBasisMul G (Sum.inl i) (Sum.inr (Sum.inr j)) = if i = j then some (Sum.inr (Sum.inr j)) else none

The product index of a vertex vector and a volume vector.

@[simp]

theorem TauCeti.zigzagBasisMul_dart_vertex {V : Type u} (G : SimpleGraph V) (d : G.Dart) (i : V) : zigzagBasisMul G (Sum.inr (Sum.inl d)) (Sum.inl i) = if i = d.toProd.1 then some (Sum.inr (Sum.inl d)) else none

The product index of a dart vector and a vertex vector.

@[simp]

theorem TauCeti.zigzagBasisMul_dart_dart {V : Type u} (G : SimpleGraph V) (d e : G.Dart) : zigzagBasisMul G (Sum.inr (Sum.inl d)) (Sum.inr (Sum.inl e)) = if e = d.symm then some (Sum.inr (Sum.inr d.toProd.2)) else none

The product index of two dart vectors.

@[simp]

theorem TauCeti.zigzagBasisMul_dart_volume {V : Type u} (G : SimpleGraph V) (d : G.Dart) (i : V) : zigzagBasisMul G (Sum.inr (Sum.inl d)) (Sum.inr (Sum.inr i)) = none

A dart vector followed by a volume vector has zero product index.

@[simp]

theorem TauCeti.zigzagBasisMul_volume_vertex {V : Type u} (G : SimpleGraph V) (i j : V) : zigzagBasisMul G (Sum.inr (Sum.inr i)) (Sum.inl j) = if i = j then some (Sum.inr (Sum.inr i)) else none

The product index of a volume vector and a vertex vector.

@[simp]

theorem TauCeti.zigzagBasisMul_volume_dart {V : Type u} (G : SimpleGraph V) (i : V) (d : G.Dart) : zigzagBasisMul G (Sum.inr (Sum.inr i)) (Sum.inr (Sum.inl d)) = none

A volume vector followed by a dart vector has zero product index.

@[simp]

theorem TauCeti.zigzagBasisMul_volume_volume {V : Type u} (G : SimpleGraph V) (i j : V) : zigzagBasisMul G (Sum.inr (Sum.inr i)) (Sum.inr (Sum.inr j)) = none

Two volume vectors have zero product index.

Products of vertex idempotents

@[simp]

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

A vertex idempotent is idempotent in the zigzag quotient.

@[simp]

theorem TauCeti.zigzagMk_vertexIdempotent_mul_vertexIdempotent_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : i ≠ j) : (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i)) * (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G j)) = 0

Distinct vertex idempotents are orthogonal in the zigzag quotient.

Products of a vertex idempotent and an arrow

theorem TauCeti.zigzagMk_vertexIdempotent_mul_ofArrow (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) : (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G d.toProd.2)) * (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) = (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯))

The vertex idempotent at the head of a dart is a left unit for its arrow.

theorem TauCeti.zigzagMk_vertexIdempotent_mul_ofArrow_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {v : V} (d : G.Dart) (h : v ≠ d.toProd.2) : (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v)) * (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) = 0

A vertex idempotent away from the head of a dart kills its arrow on the left.

theorem TauCeti.zigzagMk_ofArrow_mul_vertexIdempotent (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) : (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G d.toProd.1)) = (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯))

The vertex idempotent at the tail of a dart is a right unit for its arrow.

theorem TauCeti.zigzagMk_ofArrow_mul_vertexIdempotent_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {v : V} (d : G.Dart) (h : v ≠ d.toProd.1) : (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v)) = 0

A vertex idempotent away from the tail of a dart kills its arrow on the right.

Products of a vertex idempotent and a volume class

@[simp]

theorem TauCeti.zigzagMk_vertexIdempotent_mul_zigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i)) * zigzagVolume k G i = zigzagVolume k G i

The vertex idempotent at the base of a volume class is a left unit for it.

@[simp]

theorem TauCeti.zigzagMk_vertexIdempotent_mul_zigzagVolume_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {v i : V} (h : v ≠ i) : (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v)) * zigzagVolume k G i = 0

A vertex idempotent away from the base of a volume class kills it on the left.

@[simp]

theorem TauCeti.zigzagVolume_mul_zigzagMk_vertexIdempotent (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagVolume k G i * (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i)) = zigzagVolume k G i

The vertex idempotent at the base of a volume class is a right unit for it.

@[simp]

theorem TauCeti.zigzagVolume_mul_zigzagMk_vertexIdempotent_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {v i : V} (h : v ≠ i) : zigzagVolume k G i * (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v)) = 0

A vertex idempotent away from the base of a volume class kills it on the right.

Products of two arrows

theorem TauCeti.zigzagMk_ofArrow_mul_ofArrow_symm (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) : (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) = zigzagVolume k G d.toProd.2

Traversing a dart and returning is its volume class. In the later-factor-first convention the reverse dart is traversed first, so the composite is the backtrack based at the head of d.

theorem TauCeti.zigzagMk_ofArrow_mul_ofArrow_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {d e : G.Dart} (h : e ≠ d.symm) : (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) = 0

Two arrows that are not reverse to one another multiply to zero. Either they do not meet, in which case the product already vanishes in the path algebra, or they meet and the composite is a length-two path with distinct endpoints, which the zigzag relations kill.

Products reaching path length three

theorem TauCeti.zigzagMk_ofPath_mul_ofPath_eq_zero_of_three_le (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (x y : Quiver.TotalPath (DoubledQuiver G)) (h : 3 ≤ x.snd.snd.length + y.snd.snd.length) : (zigzagMk k G) (PathAlgebra.ofPath x * PathAlgebra.ofPath y) = 0

A product of two path classes vanishes when their total path length is at least three.

theorem TauCeti.zigzagMk_ofArrow_mul_zigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) (i : V) : (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * zigzagVolume k G i = 0

An arrow times a volume class vanishes: the composite has path length three.

theorem TauCeti.zigzagVolume_mul_zigzagMk_ofArrow (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (d : G.Dart) : zigzagVolume k G i * (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) = 0

A volume class times an arrow vanishes: the composite has path length three.

@[simp]

theorem TauCeti.zigzagVolume_mul_zigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : zigzagVolume k G i * zigzagVolume k G j = 0

Two volume classes multiply to zero: they either do not meet or compose to path length four.

Left multiplication by an arrow

theorem TauCeti.zigzagMk_ofArrow_mul {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (d : G.Dart) (x : nonisolatedZigzagQuotient k G) : (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * x = ((zigzagBasis k G hns).coord (Sum.inl d.toProd.1)) x • (zigzagBasis k G hns) (Sum.inr (Sum.inl d)) + ((zigzagBasis k G hns).coord (Sum.inr (Sum.inl d.symm))) x • (zigzagBasis k G hns) (Sum.inr (Sum.inr d.toProd.2))

Left multiplication by an arrow reads off two coordinates. Multiplying by the arrow of a dart d keeps only the idempotent at the tail of d, which returns the arrow itself, and the reverse arrow, which returns the volume class at the head of d.

theorem TauCeti.mul_zigzagMk_ofArrow {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (d : G.Dart) (x : nonisolatedZigzagQuotient k G) : x * (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) = ((zigzagBasis k G hns).coord (Sum.inl d.toProd.2)) x • (zigzagBasis k G hns) (Sum.inr (Sum.inl d)) + ((zigzagBasis k G hns).coord (Sum.inr (Sum.inl d.symm))) x • (zigzagBasis k G hns) (Sum.inr (Sum.inr d.toProd.1))

Right multiplication by an arrow reads off two coordinates. Multiplying by the arrow of a dart d on the right keeps only the idempotent at the head of d, which returns the arrow itself, and the reverse arrow, which returns the volume class at the tail of d.

Products and coordinates in the vertex-arrow-volume basis

theorem TauCeti.zigzagBasis_mul {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (b c : ZigzagBasisIndex G) : (zigzagBasis k G hns) b * (zigzagBasis k G hns) c = (zigzagBasisMul G b c).elim 0 ⇑(zigzagBasis k G hns)

The multiplication table in the vertex-arrow-volume basis: the product of two basis vectors is the basis vector indexed by TauCeti.zigzagBasisMul, or zero when that index is none.

theorem TauCeti.zigzagBasis_coord_dart_mul {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (d : G.Dart) (x y : nonisolatedZigzagQuotient k G) : ((zigzagBasis k G hns).coord (Sum.inr (Sum.inl d))) (x * y) = ((zigzagBasis k G hns).coord (Sum.inl d.toProd.2)) x * ((zigzagBasis k G hns).coord (Sum.inr (Sum.inl d))) y + ((zigzagBasis k G hns).coord (Sum.inr (Sum.inl d))) x * ((zigzagBasis k G hns).coord (Sum.inl d.toProd.1)) y

The arrow coordinates of a product. The coefficient of the arrow of a dart d in x * y pairs the idempotent coordinate of x at the head of d with the d-coordinate of y, and the d-coordinate of x with the idempotent coordinate of y at the tail of d: an arrow is a product only of itself with the idempotents at its two ends.

theorem TauCeti.zigzagVolume_mul {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) (y : nonisolatedZigzagQuotient k G) : zigzagVolume k G i * y = ((zigzagBasis k G hns).coord (Sum.inl i)) y • zigzagVolume k G i

A volume class absorbs, from the left, only the idempotent at its base vertex.

theorem TauCeti.mul_zigzagVolume {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) (x : nonisolatedZigzagQuotient k G) : x * zigzagVolume k G i = ((zigzagBasis k G hns).coord (Sum.inl i)) x • zigzagVolume k G i

A volume class absorbs, from the right, only the idempotent at its base vertex.

theorem TauCeti.zigzagBasis_coord_dart_zigzagVolume {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (d : G.Dart) (i : V) : ((zigzagBasis k G hns).coord (Sum.inr (Sum.inl d))) (zigzagVolume k G i) = 0

A volume class has no arrow component.