The Casimir element of the componentwise zigzag algebra

Let Z be the zigzag algebra TauCeti.zigzagAlgebra of a finite simple graph. Its vertex, arrow and volume basis TauCeti.zigzagAlgebraBasis is dual, for the symmetric Frobenius pairing (x, y) ↦ tr (x * y) of TauCeti.zigzagAlgebraTrace, to its reindexing by TauCeti.zigzagDualIndex. This file defines the Casimir element ∑_b b ⊗ b^∨ of that pairing in the enveloping algebra Z ⊗[k] Zᵐᵒᵖ and proves that it commutes with Z, as the Casimir element of any trace does (LinearMap.sum_mul_tmul_eq_sum_tmul_mul).

Main definitions

• TauCeti.zigzagCasimir: the Casimir element ∑_b b ⊗ b^∨ of the trace pairing.

Main results

• TauCeti.zigzagCasimir_eq_sum: the Casimir element as a sum over the basis.
• TauCeti.tmul_one_mul_zigzagCasimir: the Casimir element commutes with Z.

References

• L. Kadison, New examples of Frobenius extensions, University Lecture Series 14, AMS, 1999 (dual bases and Casimir elements of Frobenius algebras).

noncomputable def TauCeti.zigzagCasimir (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : TensorProduct k (↑(zigzagAlgebra k G)) (↑(zigzagAlgebra k G))ᵐᵒᵖ

The Casimir element of the zigzag algebra, ∑_b b ⊗ b^∨ in Z ⊗[k] Zᵐᵒᵖ, with b running over the vertex, arrow and volume basis and b^∨ over its dual basis for the trace pairing, indexed by TauCeti.zigzagDualIndex.

theorem TauCeti.zigzagCasimir_eq_sum {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] [Fintype V] [DecidableRel G.Adj] : zigzagCasimir k G = ∑ b : ZigzagBasisIndex G, (zigzagAlgebraBasis k G) b ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (zigzagDualIndex G b))

The Casimir element as a sum over the basis, for any choice of finiteness and decidability instances.

theorem TauCeti.tmul_one_mul_zigzagCasimir {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (a : ↑(zigzagAlgebra k G)) : a ⊗ₜ[k] 1 * zigzagCasimir k G = 1 ⊗ₜ[k] MulOpposite.op a * zigzagCasimir k G

The Casimir element commutes with the zigzag algebra: (a ⊗ 1) C = (1 ⊗ a) C, that is, a C = C a for the bimodule structure of Z ⊗[k] Zᵐᵒᵖ.