The signless relator of a simple graph

For the doubled quiver TauCeti.DoubledQuiver G of a simple graph G, at any vertex v with finite neighbourhood the signless preprojective relator TauCeti.signlessPreprojectiveRelator is ∑_{j ∼ v} (v → j → v), the sum of the backtracks along the edges at v. This is the relation which Huerfano and Khovanov find in the quadratic dual of the zigzag algebra of G.

For a graph on Fin n, the class of the doubled arrow from i to j in the signless algebra is recorded as a function TauCeti.signlessArrow of two natural numbers, zero unless they are adjacent vertices. Products of these classes are the classes of paths, and the relator at v becomes ∑ w, signlessArrow w v * signlessArrow v w = 0; indexing by natural numbers lets the computations along the arms of a Dynkin diagram use ordinary arithmetic on vertex labels.

A walk is recorded by the list of its vertices, latest vertex first, and TauCeti.signlessWord sends it to the product of its arrow classes; prepending a vertex is left multiplication by an arrow. These classes multiply by concatenation of walks, and every walk class is the class of a path of the doubled quiver.

Main definitions

• TauCeti.signlessArrow: the class of the doubled arrow between two vertices of a graph on Fin n, or zero.
• TauCeti.signlessWord: the class of the walk through a list of vertices.

Main results

• TauCeti.signlessPreprojectiveRelator_vertex: at a vertex with finite neighbourhood, the relator is the sum of the backtracks TauCeti.DoubledQuiver.backtrackElem over the neighbours.
• TauCeti.signlessPreprojectiveMk_ofArrow_eq_signlessArrow: the class of every doubled arrow is a TauCeti.signlessArrow.
• TauCeti.sum_signlessArrow_mul_signlessArrow: the relation at a vertex, as a sum over all vertices.
• TauCeti.signlessWord_mul_signlessWord: walk classes multiply by concatenation.
• TauCeti.exists_ofPath_eq_signlessWord: the class of a walk is the class of a path through the same vertices.

References

S. Huerfano and M. Khovanov, A category for the adjoint representation, Section 3, https://arxiv.org/abs/math/0002060.

theorem TauCeti.signlessPreprojectiveRelator_vertex (k : Type w) {V : Type u} [Semiring k] (G : SimpleGraph V) (v : V) [Fintype ↑(G.neighborSet v)] : signlessPreprojectiveRelator k (DoubledQuiver.vertex G v) = ∑ w : ↑(G.neighborSet v), DoubledQuiver.backtrackElem G k ⋯

The signless relator of a simple graph at v is ∑_{j ∼ v} (v → j → v), the sum of the backtracks along the edges at v.

Arrow classes of a graph on Fin n

noncomputable def TauCeti.signlessArrow (k : Type w) [CommRing k] {n : ℕ} (G : SimpleGraph (Fin n)) [(i : Fin n) → Fintype ↑(G.neighborSet i)] (i j : ℕ) : signlessPreprojectiveAlgebra k (DoubledQuiver G)

The class of the doubled arrow from i to j in the signless algebra of a graph G on Fin n, or zero if i and j are not adjacent vertices of G. The vertices are given as natural numbers, so that arithmetic on vertex labels needs no bounds.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.signlessArrow_of_adj (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] {i j : Fin n} (h : G.Adj i j) : signlessArrow k G ↑i ↑j = (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofArrow (DoubledQuiver.arrow G h))

Between adjacent vertices, signlessArrow is the class of the doubled arrow.

@[simp]

theorem TauCeti.signlessArrow_eq_zero (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] {i j : ℕ} (h : ∀ (hi : i < n) (hj : j < n), ¬G.Adj ⟨i, hi⟩ ⟨j, hj⟩) : signlessArrow k G i j = 0

Between non-adjacent vertices, signlessArrow vanishes.

theorem TauCeti.signlessPreprojectiveMk_ofArrow_eq_signlessArrow (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] {i j : DoubledQuiver G} (e : i ⟶ j) : (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofArrow e) = signlessArrow k G ↑((DoubledQuiver.vertexEquiv G).symm i) ↑((DoubledQuiver.vertexEquiv G).symm j)

The class of an arbitrary doubled arrow of G is the signlessArrow between its endpoints.

@[simp]

theorem TauCeti.signlessArrow_mul_vertexIdempotent (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] (i j : ℕ) (v : Fin n) : signlessArrow k G i j * (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v)) = if i = ↑v then signlessArrow k G i j else 0

Cutting an arrow class on the right selects its source vertex.

@[simp]

theorem TauCeti.vertexIdempotent_mul_signlessArrow (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] (v : Fin n) (i j : ℕ) : (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v)) * signlessArrow k G i j = if j = ↑v then signlessArrow k G i j else 0

Cutting an arrow class on the left selects its target vertex.

theorem TauCeti.sum_signlessArrow_mul_signlessArrow (k : Type w) [CommRing k] {n : ℕ} (G : SimpleGraph (Fin n)) [(i : Fin n) → Fintype ↑(G.neighborSet i)] (v : Fin n) : ∑ w : Fin n, signlessArrow k G ↑w ↑v * signlessArrow k G ↑v ↑w = 0

The signless relation at a vertex v: the backtracks v → w → v sum to zero, the sum running over all vertices w, of which only the neighbours of v contribute.

theorem TauCeti.signlessArrow_relation_of_consecutive (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] (hconsecutive : ∀ (i j : Fin n), G.Adj i j → ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) (v : ℕ) : signlessArrow k G (v + 1) v * signlessArrow k G v (v + 1) + signlessArrow k G (v - 1) v * signlessArrow k G v (v - 1) = 0

The signless relation at a vertex v of a graph whose edges join consecutive vertices: the backtrack through v + 1 cancels the backtrack through v - 1. At an end vertex the missing backtrack is zero.

Classes of walks given by their vertices

noncomputable def TauCeti.signlessWord (k : Type w) [CommRing k] {n : ℕ} (G : SimpleGraph (Fin n)) [(i : Fin n) → Fintype ↑(G.neighborSet i)] : List (Fin n) → signlessPreprojectiveAlgebra k (DoubledQuiver G)

The class in the signless algebra of a graph G on Fin n of the walk through the vertices l, latest vertex first: [v] is the vertex idempotent at v, and j :: i :: r is the arrow class TauCeti.signlessArrow G i j times the class of i :: r. Prepending a vertex is thus left multiplication by an arrow, in the later-factor-first convention. A list which is not a walk has class 0, as does the empty list.

Equations

• TauCeti.signlessWord k G [] = 0
• TauCeti.signlessWord k G [v] = (TauCeti.signlessPreprojectiveMk k (TauCeti.DoubledQuiver G)) (TauCeti.PathAlgebra.vertexIdempotent k (TauCeti.DoubledQuiver.vertex G v))
• TauCeti.signlessWord k G (j :: i :: r) = TauCeti.signlessArrow k G ↑i ↑j * TauCeti.signlessWord k G (i :: r)

@[simp]

theorem TauCeti.signlessWord_nil (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] : signlessWord k G [] = 0

The empty list has class 0.

@[simp]

theorem TauCeti.signlessWord_singleton (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] (v : Fin n) : signlessWord k G [v] = (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v))

The class of a one-vertex walk is its vertex idempotent.

@[simp]

theorem TauCeti.signlessWord_cons_cons (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] (j i : Fin n) (r : List (Fin n)) : signlessWord k G (j :: i :: r) = signlessArrow k G ↑i ↑j * signlessWord k G (i :: r)

Extending a walk by a vertex multiplies its class on the left by the arrow to that vertex.

theorem TauCeti.signlessWord_cons (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] {j i : Fin n} {l : List (Fin n)} (hl : l.head? = some i) : signlessWord k G (j :: l) = signlessArrow k G ↑i ↑j * signlessWord k G l

TauCeti.signlessWord_cons_cons for a walk given together with its latest vertex.

theorem TauCeti.vertexIdempotent_mul_signlessWord (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] (v j : Fin n) (r : List (Fin n)) : (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v)) * signlessWord k G (j :: r) = if j = v then signlessWord k G (j :: r) else 0

The vertex idempotent at the latest vertex of a walk is a left unit for its class, and the other vertex idempotents annihilate it.

theorem TauCeti.signlessArrow_mul_signlessWord (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] (i j i' : Fin n) (r : List (Fin n)) : signlessArrow k G ↑i ↑j * signlessWord k G (i' :: r) = if i = i' then signlessWord k G (j :: i' :: r) else 0

An arrow class times the class of a walk extends the walk if the arrow starts at its latest vertex, and vanishes otherwise.

theorem TauCeti.signlessWord_eq_zero_of_not_isChain (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] {l : List (Fin n)} (hl : ¬List.IsChain G.Adj l) : signlessWord k G l = 0

A list of vertices which is not a walk has class 0.

theorem TauCeti.exists_ofPath_eq_signlessWord (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] (i : Fin n) (r : List (Fin n)) (hw : List.IsChain G.Adj (i :: r)) : ∃ (a : Fin n) (p : Quiver.Path (DoubledQuiver.vertex G a) (DoubledQuiver.vertex G i)), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofPath ⟨DoubledQuiver.vertex G a, ⟨DoubledQuiver.vertex G i, p⟩⟩) = signlessWord k G (i :: r) ∧ p.vertices = List.map (DoubledQuiver.vertex G) (i :: r).reverse

The class of a walk is the class of a path of the doubled quiver through the same vertices.

theorem TauCeti.signlessWord_mul_signlessWord (k : Type w) [CommRing k] {n : ℕ} {G : SimpleGraph (Fin n)} [(i : Fin n) → Fintype ↑(G.neighborSet i)] (s : List (Fin n)) {j : Fin n} {t : List (Fin n)} (hs : s ≠ []) : signlessWord k G s * signlessWord k G (j :: t) = if s.getLast hs = j then signlessWord k G (s.dropLast ++ j :: t) else 0

Classes of walks multiply by concatenation, later factor first, when the earliest vertex of the left factor is the latest vertex of the right factor; otherwise their product is 0.