The symmetric Frobenius trace of a zigzag algebra

The zigzag algebra of a simple graph with no isolated vertex is a symmetric Frobenius algebra. This file constructs the trace that witnesses it: the linear functional TauCeti.zigzagTrace which is 1 on every volume class and 0 on the vertex idempotents and on the arrows, and proves that the pairing (x, y) ↦ tr (x * y) is symmetric, associative and perfect.

Both the symmetry and the nondegeneracy come from one computation. Write ι for the involution TauCeti.zigzagDualIndex of the basis indices, which exchanges the idempotent and the volume class at a vertex and reverses a dart. The multiplication table shows that the trace of a product of two basis classes is 1 when the second index is ι of the first and 0 otherwise: the only products with a volume component are e_i x_i = x_i = x_i e_i and a_d a_{d.symm} = x_{d.snd}. So the Gram matrix of the pairing in the vertex, arrow and volume basis is the permutation matrix of ι. Symmetry is then the fact that ι is an involution. The dual-basis identity TauCeti.zigzagTracePairing_apply_zigzagBasisFun_zigzagDualIndex says that pairing an element against ι b reads off its b-th coordinate. Since ι is a bijection, the pairing therefore carries the vertex, arrow and volume basis to the dual basis reindexed along ι, so it is perfect over the commutative base ring: TauCeti.zigzagTracePairing_isPerfPair, whence the isomorphism LinearMap.toPerfPair (TauCeti.zigzagTracePairing k G hns) : Z(G) ≃ₗ[k] Module.Dual k Z(G) onto the dual. It also implies TauCeti.zigzagTracePairing_nondegenerate, where Mathlib's LinearMap.BilinForm.Nondegenerate records the weaker separating condition.

Thus perfectness together with symmetry and associativity gives the symmetric Frobenius property over an arbitrary commutative ring; the permutation Gram matrix requires no scalar to be inverted. What is not proved here is self-injectivity, which needs that isomorphism onto the dual promoted to one of bimodules and an injectivity criterion for modules over a general base.

Main definitions

• TauCeti.zigzagDualIndex: the involution of the basis indices pairing an idempotent with a volume class and a dart with its reverse.
• TauCeti.zigzagTrace: the Frobenius trace, the sum of the volume coordinates.
• TauCeti.zigzagTracePairing: the bilinear form (x, y) ↦ tr (x * y).

Main results

• TauCeti.zigzagTrace_mul_comm: the trace is a trace, tr (x * y) = tr (y * x).
• TauCeti.zigzagTracePairing_isSymm and TauCeti.zigzagTracePairing_nondegenerate: the pairing is symmetric and nondegenerate.
• TauCeti.zigzagTracePairing_mul_assoc: the pairing is associative, (xy, z) = (x, yz).
• TauCeti.zigzagTracePairing_apply_zigzagBasisFun_zigzagDualIndex: the classes indexed by ι are the dual basis of the pairing.
• TauCeti.zigzagTracePairing_isPerfPair: the pairing is perfect, so LinearMap.toPerfPair is an isomorphism of the zigzag algebra onto its k-linear dual.

References

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

The pairing involution of the basis indices

def TauCeti.zigzagDualIndex {V : Type u} (G : SimpleGraph V) : ZigzagBasisIndex G → ZigzagBasisIndex G

The involution of the zigzag basis indices under which the trace pairing is a permutation matrix: it exchanges the idempotent and the volume class at a vertex, and sends a dart to its reverse. The basis class it names is the one pairing to 1 with the given basis class.

@[simp]

theorem TauCeti.zigzagDualIndex_inl {V : Type u} (G : SimpleGraph V) (i : V) : zigzagDualIndex G (Sum.inl i) = Sum.inr (Sum.inr i)

@[simp]

theorem TauCeti.zigzagDualIndex_inr_inl {V : Type u} (G : SimpleGraph V) (d : G.Dart) : zigzagDualIndex G (Sum.inr (Sum.inl d)) = Sum.inr (Sum.inl d.symm)

@[simp]

theorem TauCeti.zigzagDualIndex_inr_inr {V : Type u} (G : SimpleGraph V) (i : V) : zigzagDualIndex G (Sum.inr (Sum.inr i)) = Sum.inl i

@[simp]

theorem TauCeti.zigzagDualIndex_zigzagDualIndex {V : Type u} (G : SimpleGraph V) (b : ZigzagBasisIndex G) : zigzagDualIndex G (zigzagDualIndex G b) = b

theorem TauCeti.zigzagDualIndex_involutive {V : Type u} (G : SimpleGraph V) : Function.Involutive (zigzagDualIndex G)

theorem TauCeti.zigzagDualIndex_injective {V : Type u} (G : SimpleGraph V) : Function.Injective (zigzagDualIndex G)

The trace

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

The Frobenius trace of a zigzag algebra: the sum of the coordinates of an element in the volume classes. It is 1 on each volume class and 0 on the vertex idempotents and the arrows.

theorem TauCeti.zigzagTrace_zigzagBasisFun (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) : (zigzagTrace k G hns) (zigzagBasisFun k G b) = Sum.elim (fun (x : V) => 0) (Sum.elim (fun (x : G.Dart) => 0) fun (x : V) => 1) b

The trace on the vertex, arrow and volume basis: it is 1 on the volume block and 0 on the other two.

@[simp]

theorem TauCeti.zigzagTrace_zigzagMk_vertexIdempotent (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : (zigzagTrace k G hns) ((zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i))) = 0

The trace vanishes on a vertex idempotent.

theorem TauCeti.zigzagTrace_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) : (zigzagTrace k G hns) ((zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯))) = 0

The trace vanishes on an arrow.

@[simp]

theorem TauCeti.zigzagTrace_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) : (zigzagTrace k G hns) (zigzagVolume k G i) = 1

The trace is one on every volume class.

The trace pairing

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

The Frobenius pairing of a zigzag algebra, (x, y) ↦ tr (x * y).

@[simp]

theorem TauCeti.zigzagTracePairing_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (x y : nonisolatedZigzagQuotient k G) : ((zigzagTracePairing k G hns) x) y = (zigzagTrace k G hns) (x * y)

theorem TauCeti.zigzagTracePairing_mul_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (x y z : nonisolatedZigzagQuotient k G) : ((zigzagTracePairing k G hns) (x * y)) z = ((zigzagTracePairing k G hns) x) (y * z)

The trace pairing is associative: it is computed from the product of all three factors, so the bracketing is immaterial.

The Gram matrix of the pairing

theorem TauCeti.zigzagTracePairing_zigzagBasisFun (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) : ((zigzagTracePairing k G hns) (zigzagBasisFun k G b)) (zigzagBasisFun k G c) = if c = zigzagDualIndex G b then 1 else 0

The Gram matrix of the trace pairing is the permutation matrix of zigzagDualIndex. The trace of a product of two basis classes is 1 exactly when the second index is the dual of the first, and 0 otherwise.

Symmetry, the dual basis, and nondegeneracy

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

The trace pairing is symmetric. Its Gram matrix is the permutation matrix of an involution.

theorem TauCeti.zigzagTrace_mul_comm (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (x y : nonisolatedZigzagQuotient k G) : (zigzagTrace k G hns) (x * y) = (zigzagTrace k G hns) (y * x)

The trace is a trace: tr (x * y) = tr (y * x). The Gram matrix of the pairing is the permutation matrix of an involution, hence symmetric.

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

The dual basis of the trace pairing. Pairing an element against the basis class of the dual index of b reads off its b-th coordinate.

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

The trace pairing is nondegenerate. Its Gram matrix is the permutation matrix of a bijection, so an element orthogonal to every basis class has every coordinate zero.

The isomorphism onto the dual

instance TauCeti.zigzagTracePairing_isPerfPair (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) : LinearMap.IsPerfPair (zigzagTracePairing k G hns)

The trace pairing is perfect. It carries the vertex, arrow and volume basis to the dual basis reindexed along the involution zigzagDualIndex, so both of its induced maps to the dual are bijective; no scalar is inverted, so a commutative base ring suffices. The isomorphism onto the dual this gives, the packaging the Frobenius property is used through, is Mathlib's LinearMap.toPerfPair (zigzagTracePairing k G hns) : _ ≃ₗ[k] Module.Dual k _, evaluated by LinearMap.toPerfPair_apply.