Documentation

TauCeti.RepresentationTheory.Quiver.Zigzag.Componentwise.Decomposition

The vertex–arrow–volume basis of the public zigzag algebra #

The public zigzag algebra is a finite product of component algebras. Its basis has one idempotent and one volume for every vertex, including isolated vertices, and one arrow for every dart. On a singleton component the volume is the infinitesimal generator of the dual numbers. On all other components it is the canonical backtrack class.

zigzagAlgebraBasis assembles the component bases with Pi.basis and reindexes them by ZigzagBasisIndex G. Its coordinate theorem computes a coefficient by projecting to the appropriate component. The projection lemmas describe both the supported component and vanishing on the other components.

References #

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

source
def TauCeti.zigzagComponentBasisIndexEquiv {V : Type u} (G : SimpleGraph V) :
(C : G.ConnectedComponent) × ZigzagBasisIndex C.toSimpleGraph ≃ ZigzagBasisIndex G

Forgetting the component labels identifies componentwise vertex–arrow–volume indices with those of the original graph. The endpoints of a dart lie in the same connected component.

Instances For
    source
    @[simp]
    theorem TauCeti.zigzagComponentBasisIndexEquiv_inl {V : Type u} (G : SimpleGraph V) (C : G.ConnectedComponent) (i : ↥C) :
    (zigzagComponentBasisIndexEquiv G) ⟨C, Sum.inl i⟩ = Sum.inl ↑i
    source
    @[simp]
    theorem TauCeti.zigzagComponentBasisIndexEquiv_inr_inl {V : Type u} (G : SimpleGraph V) (C : G.ConnectedComponent) (d : C.toSimpleGraph.Dart) :
    (zigzagComponentBasisIndexEquiv G) ⟨C, Sum.inr (Sum.inl d)⟩ = Sum.inr (Sum.inl { fst := ↑d.toProd.1, snd := ↑d.toProd.2, adj := ⋯ })
    source
    @[simp]
    theorem TauCeti.zigzagComponentBasisIndexEquiv_inr_inr {V : Type u} (G : SimpleGraph V) (C : G.ConnectedComponent) (i : ↥C) :
    (zigzagComponentBasisIndexEquiv G) ⟨C, Sum.inr (Sum.inr i)⟩ = Sum.inr (Sum.inr ↑i)
    source
    @[simp]
    theorem TauCeti.zigzagComponentBasisIndexEquiv_symm_inl {V : Type u} (G : SimpleGraph V) (i : V) :
    (zigzagComponentBasisIndexEquiv G).symm (Sum.inl i) = ⟨G.connectedComponentMk i, Sum.inl ⟨i, ⋯⟩⟩
    source
    @[simp]
    theorem TauCeti.zigzagComponentBasisIndexEquiv_symm_inr_inl {V : Type u} (G : SimpleGraph V) (d : G.Dart) :
    (zigzagComponentBasisIndexEquiv G).symm (Sum.inr (Sum.inl d)) = ⟨G.connectedComponentMk d.toProd.1, Sum.inr (Sum.inl { fst := ⟨d.toProd.1, ⋯⟩, snd := ⟨d.toProd.2, ⋯⟩, adj := ⋯ })⟩
    source
    @[simp]
    theorem TauCeti.zigzagComponentBasisIndexEquiv_symm_inr_inr {V : Type u} (G : SimpleGraph V) (i : V) :
    (zigzagComponentBasisIndexEquiv G).symm (Sum.inr (Sum.inr i)) = ⟨G.connectedComponentMk i, Sum.inr (Sum.inr ⟨i, ⋯⟩)⟩
    source
    noncomputable def TauCeti.zigzagAlgebraBasis {V : Type u} [Finite V] (k : Type w) [CommRing k] (G : SimpleGraph V) :
    Module.Basis (ZigzagBasisIndex G) k ↑(zigzagAlgebra k G)

    The vertex–arrow–volume basis of the public zigzag algebra. Isolated vertices contribute both the unit and the infinitesimal generator of their dual-number factor.

    Instances For
      source
      theorem TauCeti.zigzagAlgebraBasis_apply {V : Type u} (G : SimpleGraph V) (k : Type w) [CommRing k] [Finite V] (b : ZigzagBasisIndex G) :
      (zigzagAlgebraBasis k G) b = zigzagAlgebraMk k G (Pi.single ((zigzagComponentBasisIndexEquiv G).symm b).fst ((zigzagComponentBasis k G ((zigzagComponentBasisIndexEquiv G).symm b).fst) ((zigzagComponentBasisIndexEquiv G).symm b).snd))

      A global basis vector is the corresponding component basis vector, extended by zero.

      source
      @[simp]
      theorem TauCeti.zigzagAlgebraBasis_repr {V : Type u} (G : SimpleGraph V) (k : Type w) [CommRing k] [Finite V] (x : ↑(zigzagAlgebra k G)) (b : (C : G.ConnectedComponent) × ZigzagBasisIndex C.toSimpleGraph) :
      ((zigzagAlgebraBasis k G).repr x) ((zigzagComponentBasisIndexEquiv G) b) = ((zigzagComponentBasis k G b.fst).repr ((zigzagComponentProjection k G b.fst) x)) b.snd

      The global coefficient at a component-labelled index is the coefficient of its projection in the basis of that component.

      source
      @[simp]
      theorem TauCeti.zigzagComponentProjection_zigzagAlgebraBasis {V : Type u} (G : SimpleGraph V) (k : Type w) [CommRing k] [Finite V] (C : G.ConnectedComponent) (b : ZigzagBasisIndex C.toSimpleGraph) :
      (zigzagComponentProjection k G C) ((zigzagAlgebraBasis k G) ((zigzagComponentBasisIndexEquiv G) ⟨C, b⟩)) = (zigzagComponentBasis k G C) b

      Projection to the supporting component recovers the component basis vector.

      source
      @[simp]
      theorem TauCeti.zigzagComponentProjection_zigzagAlgebraBasis_of_ne {V : Type u} (G : SimpleGraph V) (k : Type w) [CommRing k] [Finite V] (C D : G.ConnectedComponent) (h : D ≠ C) (b : ZigzagBasisIndex C.toSimpleGraph) :
      (zigzagComponentProjection k G D) ((zigzagAlgebraBasis k G) ((zigzagComponentBasisIndexEquiv G) ⟨C, b⟩)) = 0

      A basis vector vanishes on every component other than its supporting component.