The trace of the componentwise zigzag algebra

The public zigzag algebra is a product over the connected components of a finite simple graph. This file equips each factor with its canonical trace and sums those traces over the product. On a component containing an edge this is TauCeti.zigzagTrace, transported from the relation-quotient presentation. On a singleton component it is the infinitesimal coordinate of the dual numbers.

The resulting functional is one on every volume basis vector and zero on vertex and arrow basis vectors, including at isolated vertices. It is a trace: tr (x * y) = tr (y * x), and the vertex--arrow--volume basis is dual, for (x, y) ↦ tr (x * y), to its reindexing by TauCeti.zigzagDualIndex. Its restriction to a single embedded factor recovers that factor's trace, giving the trace part of the connected- component decomposition.

Main definitions

• TauCeti.zigzagComponentTrace: the trace on one connected-component factor.
• TauCeti.zigzagAlgebraTrace: the sum of the component traces on the public zigzag algebra.

Main results

• TauCeti.zigzagAlgebraTrace_zigzagAlgebraBasis_mul: the Gram matrix of the trace pairing is the permutation matrix of TauCeti.zigzagDualIndex.
• TauCeti.zigzagAlgebraTrace_mul_zigzagAlgebraBasis_zigzagDualIndex: pairing against the dual basis vector reads off a coordinate.

References

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

@[instance_reducible]

noncomputable def TauCeti.zigzagTraceConnectedComponentFintype {V : Type u} [Finite V] (G : SimpleGraph V) : Fintype G.ConnectedComponent

The finite indexing type used internally for the componentwise trace.

The trace of one component

noncomputable def TauCeti.zigzagComponentTrace (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) : ↑(zigzagComponentAlgebra k G C) →ₗ[k] k

The canonical trace on one connected-component factor of the public zigzag algebra. It is zero on the vertex and arrow blocks of TauCeti.zigzagComponentBasis and one on its volume block. For a nontrivial component this is the transported relation-quotient trace; for a singleton it is the infinitesimal coordinate of the dual numbers.

@[simp]

theorem TauCeti.zigzagComponentTrace_zigzagComponentBasis (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) (b : ZigzagBasisIndex C.toSimpleGraph) : (zigzagComponentTrace k G C) ((zigzagComponentBasis k G C) b) = Sum.elim (fun (x : ↥C) => 0) (Sum.elim (fun (x : C.toSimpleGraph.Dart) => 0) fun (x : ↥C) => 1) b

The component trace is zero on vertex and arrow basis vectors and one on volume basis vectors.

theorem TauCeti.zigzagComponentTrace_apply_nontrivial (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Nontrivial ↥C] (x : ↑(zigzagComponentAlgebra k G C)) : (zigzagComponentTrace k G C) x = (zigzagTrace k C.toSimpleGraph ⋯) ((zigzagComponentAlgebraEquivNonisolated k G C) x)

On a component containing an edge, the component trace is the relation-quotient zigzag trace under the canonical presentation equivalence.

theorem TauCeti.zigzagComponentTrace_apply_subsingleton (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Subsingleton ↥C] (x : ↑(zigzagComponentAlgebra k G C)) : (zigzagComponentTrace k G C) x = TrivSqZeroExt.snd ((zigzagComponentAlgebraEquivULiftDualNumber k G C) x).down

On a singleton component, the component trace is the infinitesimal coordinate under the canonical dual-number presentation.

theorem TauCeti.zigzagComponentTrace_mul_comm (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) (x y : ↑(zigzagComponentAlgebra k G C)) : (zigzagComponentTrace k G C) (x * y) = (zigzagComponentTrace k G C) (y * x)

The trace on one component is cyclic.

The trace of the public algebra

noncomputable def TauCeti.zigzagAlgebraTrace (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) : ↑(zigzagAlgebra k G) →ₗ[k] k

The trace of the public zigzag algebra, obtained by summing the canonical traces of all its connected-component factors.

theorem TauCeti.zigzagAlgebraTrace_apply (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (x : ↑(zigzagAlgebra k G)) : (zigzagAlgebraTrace k G) x = ∑ C : G.ConnectedComponent, (zigzagComponentTrace k G C) ((zigzagComponentProjection k G C) x)

The public trace is the sum of the traces of the component projections.

@[simp]

theorem TauCeti.zigzagAlgebraTrace_zigzagAlgebraMk_single (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) (x : ↑(zigzagComponentAlgebra k G C)) : (zigzagAlgebraTrace k G) (zigzagAlgebraMk k G (Pi.single C x)) = (zigzagComponentTrace k G C) x

Restricting the public trace to an embedded component factor recovers that component's canonical trace.

@[simp]

theorem TauCeti.zigzagAlgebraTrace_zigzagAlgebraBasis (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) (b : ZigzagBasisIndex C.toSimpleGraph) : (zigzagAlgebraTrace k G) ((zigzagAlgebraBasis k G) ((zigzagComponentBasisIndexEquiv G) ⟨C, b⟩)) = Sum.elim (fun (x : ↥C) => 0) (Sum.elim (fun (x : C.toSimpleGraph.Dart) => 0) fun (x : ↥C) => 1) b

The public trace is zero on vertex and arrow basis vectors and one on volume basis vectors.

theorem TauCeti.zigzagAlgebraTrace_mul_comm (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (x y : ↑(zigzagAlgebra k G)) : (zigzagAlgebraTrace k G) (x * y) = (zigzagAlgebraTrace k G) (y * x)

The trace of the public zigzag algebra is cyclic.

The dual basis

@[simp]

theorem TauCeti.zigzagAlgebraTrace_zigzagAlgebraBasis_inl (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : (zigzagAlgebraTrace k G) ((zigzagAlgebraBasis k G) (Sum.inl i)) = 0

The public trace vanishes on vertex basis vectors.

@[simp]

theorem TauCeti.zigzagAlgebraTrace_zigzagAlgebraBasis_inr_inl (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (d : G.Dart) : (zigzagAlgebraTrace k G) ((zigzagAlgebraBasis k G) (Sum.inr (Sum.inl d))) = 0

The public trace vanishes on arrow basis vectors.

@[simp]

theorem TauCeti.zigzagAlgebraTrace_zigzagAlgebraBasis_inr_inr (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : (zigzagAlgebraTrace k G) ((zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i))) = 1

The public trace is one on volume basis vectors, including at isolated vertices.

theorem TauCeti.zigzagAlgebraTrace_zigzagAlgebraBasis_mul (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (b c : ZigzagBasisIndex G) : (zigzagAlgebraTrace k G) ((zigzagAlgebraBasis k G) b * (zigzagAlgebraBasis k G) c) = if c = zigzagDualIndex G b then 1 else 0

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

theorem TauCeti.zigzagAlgebraTrace_mul_zigzagAlgebraBasis_zigzagDualIndex (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (x : ↑(zigzagAlgebra k G)) (b : ZigzagBasisIndex G) : (zigzagAlgebraTrace k G) (x * (zigzagAlgebraBasis k G) (zigzagDualIndex G b)) = ((zigzagAlgebraBasis k G).repr x) b

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