Multiplication in the componentwise zigzag algebra

The vertex, dart and volume basis of the public zigzag algebra has the same path-product table on every nontrivial component. On a singleton component, the vertex vector is the unit and the volume vector is the square-zero generator of the dual numbers. This file gives a single table valid for both kinds of component, and for disconnected graphs. In particular, each vertex basis element is idempotent.

In Tau Ceti's later-factor-first convention, the product of a dart with its reverse is the volume at the head of the first dart.

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

@[simp]

theorem TauCeti.zigzagComponentBasis_mul {V : Type u} (G : SimpleGraph V) (k : Type w) [CommRing k] [Finite V] (C : G.ConnectedComponent) (b c : ZigzagBasisIndex C.toSimpleGraph) : (zigzagComponentBasis k G C) b * (zigzagComponentBasis k G C) c = (zigzagBasisMul C.toSimpleGraph b c).elim 0 ⇑(zigzagComponentBasis k G C)

Multiplication of basis vectors in any connected-component factor, including the singleton dual-number factors.

@[simp]

theorem TauCeti.zigzagBasisMul_component {V : Type u} (G : SimpleGraph V) (C : G.ConnectedComponent) (b c : ZigzagBasisIndex C.toSimpleGraph) : zigzagBasisMul G ((zigzagComponentBasisIndexEquiv G) ⟨C, b⟩) ((zigzagComponentBasisIndexEquiv G) ⟨C, c⟩) = Option.map (fun (d : ZigzagBasisIndex C.toSimpleGraph) => (zigzagComponentBasisIndexEquiv G) ⟨C, d⟩) (zigzagBasisMul C.toSimpleGraph b c)

The product index respects the basis-index equivalence on one component.

@[simp]

theorem TauCeti.zigzagBasisMul_eq_none_of_ne_component {V : Type u} (G : SimpleGraph V) {C D : G.ConnectedComponent} (h : C ≠ D) (b : ZigzagBasisIndex C.toSimpleGraph) (c : ZigzagBasisIndex D.toSimpleGraph) : zigzagBasisMul G ((zigzagComponentBasisIndexEquiv G) ⟨C, b⟩) ((zigzagComponentBasisIndexEquiv G) ⟨D, c⟩) = none

Basis indices from distinct components have zero product.

@[simp]

theorem TauCeti.zigzagAlgebraBasis_mul {V : Type u} (G : SimpleGraph V) (k : Type w) [CommRing k] [Finite V] (b c : ZigzagBasisIndex G) : (zigzagAlgebraBasis k G) b * (zigzagAlgebraBasis k G) c = (zigzagBasisMul G b c).elim 0 ⇑(zigzagAlgebraBasis k G)

The complete multiplication table of the public zigzag algebra. Every product of vertex, dart and volume basis vectors is either another basis vector, with index prescribed by zigzagBasisMul, or zero. This includes the square-zero volume at each isolated vertex.

theorem TauCeti.isIdempotentElem_zigzagAlgebraBasis_inl (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : IsIdempotentElem ((zigzagAlgebraBasis k G) (Sum.inl i))

Each vertex basis element of the componentwise zigzag algebra is idempotent.