The multiplication table of a skew-zigzag algebra

The skew-zigzag relation quotient TauCeti.skewZigzagQuotient of a finite simple graph is spanned by the vertex idempotents e_i, the oriented edges a_d, and the volume classes TauCeti.skewZigzagVolume, each taken relative to a chosen incident edge. This file computes the products of two of these classes.

The table has the same shape as the ordinary one in TauCeti.RepresentationTheory.Quiver.Zigzag.Multiplication. The idempotents are orthogonal local units; an arrow is absorbed by the idempotent at its head on the left and at its tail on the right; a volume class is absorbed by the idempotent at its base on either side. Two arrows multiply to the volume class along the first of them when the later factor is its reverse, and to zero otherwise. Every product reaching path length three vanishes. The skew parameter only enters when a volume class is compared with one taken along a different incident edge, through TauCeti.skewZigzagMk_backtrackElem_eq_smul_skewZigzagVolume; no statement below needs it.

Main results

• TauCeti.skewZigzagMk_ofArrow_mul_ofArrow_symm and TauCeti.skewZigzagMk_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.skewZigzagMk_vertexIdempotent_mul_skewZigzagVolume 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.skewZigzagMk_ofArrow_mul_skewZigzagVolume, TauCeti.skewZigzagVolume_mul_skewZigzagMk_ofArrow and TauCeti.skewZigzagVolume_mul_skewZigzagVolume: every product reaching path length three vanishes.

References

See C. Couture, Skew-Zigzag Algebras, Section 3, https://arxiv.org/abs/1509.08405.

Products of vertex idempotents and arrows

@[simp]

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

A vertex idempotent is idempotent in the skew-zigzag quotient.

@[simp]

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

Distinct vertex idempotents are orthogonal in the skew-zigzag quotient.

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

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

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

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

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

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

theorem TauCeti.skewZigzagMk_ofArrow_mul_vertexIdempotent_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {v : V} (d : G.Dart) (h : v ≠ d.toProd.1) : (skewZigzagMk k G c) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * (skewZigzagMk k G c) (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.skewZigzagMk_vertexIdempotent_mul_skewZigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {i : V} (e : { j : V // G.Adj i j }) : (skewZigzagMk k G c) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i)) * skewZigzagVolume k G c e = skewZigzagVolume k G c e

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

@[simp]

theorem TauCeti.skewZigzagMk_vertexIdempotent_mul_skewZigzagVolume_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {v i : V} (e : { j : V // G.Adj i j }) (h : v ≠ i) : (skewZigzagMk k G c) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v)) * skewZigzagVolume k G c e = 0

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

@[simp]

theorem TauCeti.skewZigzagVolume_mul_skewZigzagMk_vertexIdempotent (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {i : V} (e : { j : V // G.Adj i j }) : skewZigzagVolume k G c e * (skewZigzagMk k G c) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i)) = skewZigzagVolume k G c e

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

@[simp]

theorem TauCeti.skewZigzagVolume_mul_skewZigzagMk_vertexIdempotent_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {i v : V} (e : { j : V // G.Adj i j }) (h : v ≠ i) : skewZigzagVolume k G c e * (skewZigzagMk k G c) (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.skewZigzagMk_ofArrow_mul_ofArrow_symm (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) (d : G.Dart) : (skewZigzagMk k G c) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * (skewZigzagMk k G c) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) = skewZigzagVolume k G c ⟨d.toProd.1, ⋯⟩

Traversing a dart and returning is a volume class. In the later-factor-first convention the reverse dart is traversed first, so the composite is the volume class at the head of d taken along the edge back to the tail of d.

theorem TauCeti.skewZigzagMk_ofArrow_mul_ofArrow_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {d e : G.Dart} (h : e ≠ d.symm) : (skewZigzagMk k G c) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * (skewZigzagMk k G c) (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 skew-zigzag relations kill.

Products reaching path length three

theorem TauCeti.skewZigzagMk_ofPath_mul_ofPath_eq_zero_of_three_le (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) (x y : Quiver.TotalPath (DoubledQuiver G)) (h : 3 ≤ x.snd.snd.length + y.snd.snd.length) : (skewZigzagMk k G c) (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.skewZigzagMk_ofArrow_mul_skewZigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) (d : G.Dart) {i : V} (e : { j : V // G.Adj i j }) : (skewZigzagMk k G c) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) * skewZigzagVolume k G c e = 0

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

theorem TauCeti.skewZigzagVolume_mul_skewZigzagMk_ofArrow (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {i : V} (e : { j : V // G.Adj i j }) (d : G.Dart) : skewZigzagVolume k G c e * (skewZigzagMk k G c) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) = 0

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

@[simp]

theorem TauCeti.skewZigzagVolume_mul_skewZigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {i i' : V} (e : { j : V // G.Adj i j }) (e' : { j : V // G.Adj i' j }) : skewZigzagVolume k G c e * skewZigzagVolume k G c e' = 0

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