Vertices, oriented edges, and backtracks in a doubled path algebra

For a simple graph G, the zigzag relation quotient is obtained from the path algebra of TauCeti.DoubledQuiver G by relations among length-two paths and by killing longer paths. This file names the short paths and their path-algebra elements, and computes their products. The public zigzag algebra uses a separate dual-numbers convention on isolated vertices.

A length-one path is the arrow of an adjacency, and a length-two path from a vertex back to itself is a backtrack: it leaves along an edge and returns along the same edge. The two decomposition results below show that these are the only short paths, so that the zigzag relations, which are imposed on length-two paths, can be enumerated by adjacencies.

Products are computed in Tau Ceti's later-factor-first convention: for a path a from i to j the vertex idempotents satisfy e_j * a = a = a * e_i, and traversing h : G.Adj i j and then returning is the product ofArrow (arrow G h.symm) * ofArrow (arrow G h).

Main definitions

• TauCeti.DoubledQuiver.arrowPath: the length-one path along an adjacency.
• TauCeti.DoubledQuiver.backtrackPath: the length-two path leaving along an edge and returning.
• TauCeti.DoubledQuiver.backtrackElem: the path-algebra element of a backtrack.

Main results

• TauCeti.DoubledQuiver.exists_eq_comp_arrowPath and TauCeti.DoubledQuiver.exists_eq_backtrackPath: every length-two path is a composite of two arrows, and every length-two path returning to its source is a backtrack.
• TauCeti.DoubledQuiver.ofArrow_symm_mul_ofArrow: a backtrack element is the product of an arrow with its reverse.
• the corner identities TauCeti.DoubledQuiver.vertexIdempotent_mul_ofArrow, TauCeti.DoubledQuiver.ofArrow_mul_vertexIdempotent, TauCeti.DoubledQuiver.vertexIdempotent_mul_backtrackElem, TauCeti.DoubledQuiver.backtrackElem_mul_vertexIdempotent, and their vanishing counterparts.
• TauCeti.DoubledQuiver.linearIndependent_vertexIdempotent_ofArrow_backtrackElem: the vertex idempotents, the oriented-edge elements, and the backtrack elements are linearly independent.

References

See Huerfano--Khovanov, A category for the adjoint representation, Section 3.

Short paths in a doubled quiver

def TauCeti.DoubledQuiver.arrowPath {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : Quiver.Path (vertex G i) (vertex G j)

The length-one path of the doubled quiver along an adjacency.

Equations

• TauCeti.DoubledQuiver.arrowPath G h = (TauCeti.DoubledQuiver.arrow G h).toPath

theorem TauCeti.DoubledQuiver.arrowPath_eq_toPath {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : arrowPath G h = (arrow G h).toPath

The length-one path of an adjacency is the path of its arrow.

@[simp]

theorem TauCeti.DoubledQuiver.length_arrowPath {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : (arrowPath G h).length = 1

def TauCeti.DoubledQuiver.backtrackPath {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : Quiver.Path (vertex G i) (vertex G i)

The backtrack at i along an edge to j: the length-two path which traverses the edge and returns along it.

Equations

• TauCeti.DoubledQuiver.backtrackPath G h = (TauCeti.DoubledQuiver.arrowPath G h).comp (TauCeti.DoubledQuiver.arrowPath G ⋯)

theorem TauCeti.DoubledQuiver.backtrackPath_eq_comp {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : backtrackPath G h = (arrowPath G h).comp (arrowPath G ⋯)

A backtrack is the arrow of an adjacency followed by the arrow of the symmetric adjacency.

theorem TauCeti.DoubledQuiver.backtrackPath_eq_cons {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : backtrackPath G h = (arrowPath G h).cons (arrow G ⋯)

A backtrack, written as a path extended by its final arrow.

@[simp]

theorem TauCeti.DoubledQuiver.length_backtrackPath {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : (backtrackPath G h).length = 2

@[simp]

theorem TauCeti.DoubledQuiver.backtrackPath_inj {V : Type u} (G : SimpleGraph V) {i j j' : V} {h : G.Adj i j} {h' : G.Adj i j'} : backtrackPath G h = backtrackPath G h' ↔ j = j'

Two backtracks based at the same vertex are equal exactly when they visit the same neighbour.

theorem TauCeti.DoubledQuiver.exists_eq_arrowPath {V : Type u} (G : SimpleGraph V) {i j : V} (p : Quiver.Path (vertex G i) (vertex G j)) (hp : p.length = 1) : ∃ (h : G.Adj i j), p = arrowPath G h

Every length-one path of a doubled quiver is the arrow of an adjacency.

theorem TauCeti.DoubledQuiver.exists_eq_comp_arrowPath {V : Type u} (G : SimpleGraph V) {i l : V} (p : Quiver.Path (vertex G i) (vertex G l)) (hp : p.length = 2) : ∃ (j : V) (h : G.Adj i j) (h' : G.Adj j l), p = (arrowPath G h).comp (arrowPath G h')

Every length-two path of a doubled quiver traverses two adjacencies in turn.

theorem TauCeti.DoubledQuiver.exists_eq_backtrackPath {V : Type u} (G : SimpleGraph V) {i : V} (p : Quiver.Path (vertex G i) (vertex G i)) (hp : p.length = 2) : ∃ (j : V) (h : G.Adj i j), p = backtrackPath G h

Every length-two path of a doubled quiver returning to its source is a backtrack.

The path-algebra elements of vertices, oriented edges, and backtracks

noncomputable def TauCeti.DoubledQuiver.backtrackElem {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j : V} (h : G.Adj i j) : pathAlgebra k (DoubledQuiver G)

The path-algebra element of the backtrack at i along an edge to j. Its class in the zigzag relation quotient is the volume at i, independent of the chosen incident edge.

Equations

• TauCeti.DoubledQuiver.backtrackElem G k h = TauCeti.PathAlgebra.ofPath ⟨TauCeti.DoubledQuiver.vertex G i, ⟨TauCeti.DoubledQuiver.vertex G i, TauCeti.DoubledQuiver.backtrackPath G h⟩⟩

theorem TauCeti.DoubledQuiver.backtrackElem_eq_ofPath {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j : V} (h : G.Adj i j) : backtrackElem G k h = PathAlgebra.ofPath ⟨vertex G i, ⟨vertex G i, backtrackPath G h⟩⟩

A backtrack element is the basis element of its backtrack path.

theorem TauCeti.DoubledQuiver.backtrackElem_ne_zero {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] [Nontrivial k] {i j : V} (h : G.Adj i j) : backtrackElem G k h ≠ 0

A backtrack element is nonzero: it is a basis path of the path algebra.

@[simp]

theorem TauCeti.DoubledQuiver.vertexIdempotent_mul_backtrackElem {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j : V} (h : G.Adj i j) : PathAlgebra.vertexIdempotent k (vertex G i) * backtrackElem G k h = backtrackElem G k h

The vertex idempotent at the base of a backtrack is a left unit for it.

@[simp]

theorem TauCeti.DoubledQuiver.backtrackElem_mul_vertexIdempotent {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j : V} (h : G.Adj i j) : backtrackElem G k h * PathAlgebra.vertexIdempotent k (vertex G i) = backtrackElem G k h

The vertex idempotent at the base of a backtrack is a right unit for it.

@[simp]

theorem TauCeti.DoubledQuiver.vertexIdempotent_mul_backtrackElem_of_ne {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j v : V} (h : G.Adj i j) (hv : v ≠ i) : PathAlgebra.vertexIdempotent k (vertex G v) * backtrackElem G k h = 0

A vertex idempotent away from the base of a backtrack annihilates it on the left.

@[simp]

theorem TauCeti.DoubledQuiver.backtrackElem_mul_vertexIdempotent_of_ne {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j v : V} (h : G.Adj i j) (hv : v ≠ i) : backtrackElem G k h * PathAlgebra.vertexIdempotent k (vertex G v) = 0

A vertex idempotent away from the base of a backtrack annihilates it on the right.

@[simp]

theorem TauCeti.DoubledQuiver.backtrackElem_mul_backtrackElem_of_ne {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j i' j' : V} (h : G.Adj i j) (h' : G.Adj i' j') (hne : i ≠ i') : backtrackElem G k h * backtrackElem G k h' = 0

Backtracks based at different vertices multiply to zero.

theorem TauCeti.DoubledQuiver.ofArrow_eq_ofPath_arrowPath {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j : V} (h : G.Adj i j) : PathAlgebra.ofArrow (arrow G h) = PathAlgebra.ofPath ⟨vertex G i, ⟨vertex G j, arrowPath G h⟩⟩

The element of an oriented edge is the element of its length-one path.

theorem TauCeti.DoubledQuiver.ofArrow_mul_ofArrow {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j l : V} (h : G.Adj i j) (h' : G.Adj j l) : PathAlgebra.ofArrow (arrow G h') * PathAlgebra.ofArrow (arrow G h) = PathAlgebra.ofPath ⟨vertex G i, ⟨vertex G l, (arrowPath G h).comp (arrowPath G h')⟩⟩

Two composable oriented edges multiply to the length-two path traversing the right-hand factor first.

theorem TauCeti.DoubledQuiver.ofArrow_symm_mul_ofArrow {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j : V} (h : G.Adj i j) : PathAlgebra.ofArrow (arrow G ⋯) * PathAlgebra.ofArrow (arrow G h) = backtrackElem G k h

Traversing an oriented edge and returning along it is the backtrack element.

theorem TauCeti.DoubledQuiver.ofArrow_mul_ofArrow_of_ne {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j a b : V} (h : G.Adj i j) (h' : G.Adj a b) (hne : a ≠ j) : PathAlgebra.ofArrow (arrow G h') * PathAlgebra.ofArrow (arrow G h) = 0

Oriented edges that do not meet multiply to zero.

theorem TauCeti.DoubledQuiver.vertexIdempotent_mul_ofArrow {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j : V} (h : G.Adj i j) : PathAlgebra.vertexIdempotent k (vertex G j) * PathAlgebra.ofArrow (arrow G h) = PathAlgebra.ofArrow (arrow G h)

The vertex idempotent at the target of an oriented edge is a left unit for it.

theorem TauCeti.DoubledQuiver.ofArrow_mul_vertexIdempotent {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j : V} (h : G.Adj i j) : PathAlgebra.ofArrow (arrow G h) * PathAlgebra.vertexIdempotent k (vertex G i) = PathAlgebra.ofArrow (arrow G h)

The vertex idempotent at the source of an oriented edge is a right unit for it.

theorem TauCeti.DoubledQuiver.vertexIdempotent_mul_ofArrow_of_ne {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j v : V} (h : G.Adj i j) (hv : v ≠ j) : PathAlgebra.vertexIdempotent k (vertex G v) * PathAlgebra.ofArrow (arrow G h) = 0

A vertex idempotent away from the target of an oriented edge annihilates it on the left.

theorem TauCeti.DoubledQuiver.ofArrow_mul_vertexIdempotent_of_ne {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] {i j v : V} (h : G.Adj i j) (hv : v ≠ i) : PathAlgebra.ofArrow (arrow G h) * PathAlgebra.vertexIdempotent k (vertex G v) = 0

A vertex idempotent away from the source of an oriented edge annihilates it on the right.

Linear independence of the short basis paths

theorem TauCeti.DoubledQuiver.linearIndependent_vertexIdempotent_ofArrow_backtrackElem {V : Type u} (G : SimpleGraph V) (k : Type w) [Semiring k] : LinearIndependent k (Sum.elim (fun (v : V) => PathAlgebra.vertexIdempotent k (vertex G v)) (Sum.elim (fun (d : G.Dart) => PathAlgebra.ofArrow (arrow G ⋯)) fun (d : G.Dart) => backtrackElem G k ⋯))

The vertex idempotents, the oriented-edge elements, and the backtrack elements are linearly independent in the path algebra of a doubled quiver: they are distinct basis paths, of lengths 0, 1, and 2 respectively.