The zigzag relations and their quadratic presentation

The zigzag algebra of a simple graph G is the path algebra of the doubled quiver TauCeti.DoubledQuiver G modulo the uniform relation family: every length-two path whose endpoints differ, the difference of any two length-two backtracks based at one vertex, and every path of length at least three. This file introduces those relators, the two-sided ideal they span, and the resulting quotient algebra with its universal property.

The long-path generators are convenient rather than necessary: the main result below shows that for a connected graph with at least three vertices they are already consequences of the two quadratic families, so the algebra really is quadratic there. The proof is the usual local one. A length-three path either contains a length-two subpath with distinct endpoints, in which case it already lies in the quadratic ideal, or it is an arrow following a backtrack. Backtrack independence lets that backtrack be moved onto any incident edge, and connectedness with at least three vertices produces a third vertex adjacent to one of the two vertices involved; moving the backtrack there exposes a length-two subpath with distinct endpoints.

The graphs excluded by the hypotheses are exactly those the roadmap treats separately: the one-vertex graph, whose zigzag algebra is the dual numbers rather than a relation quotient, and the two-vertex graph A₂, whose zigzag algebra is genuinely radical-cube-zero and not quadratic.

Main definitions

• TauCeti.IsQuadraticZigzagRelator: the two quadratic relation families.
• TauCeti.IsZigzagRelator: the uniform relation family, adding the long paths.
• TauCeti.zigzagIdeal and TauCeti.quadraticZigzagIdeal: the two-sided ideals they span, with named unfolding lemmas for callers that reason about the spans.
• TauCeti.nonisolatedZigzagQuotient: the relation quotient, with quotient map TauCeti.zigzagMk and universal property TauCeti.zigzagLift.

Main results

• TauCeti.zigzagIdeal_eq_quadraticZigzagIdeal: for a connected graph with at least three vertices the long-path generators are redundant.
• TauCeti.zigzagLiftOfQuadratic: consequently an algebra map killing the quadratic relators factors through the zigzag quotient.
• TauCeti.zigzagMk_ofPath_eq_zero_of_ne, TauCeti.zigzagMk_backtrackElem_eq and TauCeti.zigzagMk_ofPath_eq_zero_of_three_le: the defining relations in the quotient.

References

This is the relation-quotient clause of Layer 0 and the redundancy theorem of Layer 1 of TauCetiRoadmap/ZigzagPreprojective/README.md; the relator names follow the target-signature prototype in TauCetiRoadmap/ZigzagPreprojective/Suggested.lean. See Huerfano--Khovanov, A category for the adjoint representation, Section 3.

The relators

inductive TauCeti.IsQuadraticZigzagRelator (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) : pathAlgebra k (DoubledQuiver G) → Prop

The quadratic zigzag relators of a simple graph: the length-two paths whose endpoints differ, and the differences of two length-two paths returning to a common source. By TauCeti.DoubledQuiver.exists_eq_backtrackPath the latter are exactly the differences of two backtracks based at one vertex.

• nonreturn {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {i j : DoubledQuiver G} (p : Quiver.Path i j) (length_eq : p.length = 2) (different_endpoints : i ≠ j) : IsQuadraticZigzagRelator k G (PathAlgebra.ofPath ⟨i, ⟨j, p⟩⟩)
• equal_backtracks {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {i : DoubledQuiver G} (p q : Quiver.Path i i) (p_length : p.length = 2) (q_length : q.length = 2) : IsQuadraticZigzagRelator k G (PathAlgebra.ofPath ⟨i, ⟨i, p⟩⟩ - PathAlgebra.ofPath ⟨i, ⟨i, q⟩⟩)

inductive TauCeti.IsZigzagRelator (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) : pathAlgebra k (DoubledQuiver G) → Prop

The uniform zigzag relators of a simple graph: the quadratic relators together with every path of length at least three. The long generators make the quotient radical-cube-zero for every graph, including the two-vertex graph A₂ where they are not consequences of the quadratic relators.

• quadratic {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {x : pathAlgebra k (DoubledQuiver G)} (h : IsQuadraticZigzagRelator k G x) : IsZigzagRelator k G x
• long_path {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} (x : Quiver.TotalPath (DoubledQuiver G)) (three_le : 3 ≤ x.snd.snd.length) : IsZigzagRelator k G (PathAlgebra.ofPath x)

The relation ideals

noncomputable def TauCeti.quadraticZigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) : TwoSidedIdeal (pathAlgebra k (DoubledQuiver G))

The two-sided ideal spanned by the quadratic zigzag relators.

Equations

• TauCeti.quadraticZigzagIdeal k G = TwoSidedIdeal.span {x : TauCeti.pathAlgebra k (TauCeti.DoubledQuiver G) | TauCeti.IsQuadraticZigzagRelator k G x}

noncomputable def TauCeti.zigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) : TwoSidedIdeal (pathAlgebra k (DoubledQuiver G))

The two-sided ideal spanned by the uniform zigzag relators.

Equations

• TauCeti.zigzagIdeal k G = TwoSidedIdeal.span {x : TauCeti.pathAlgebra k (TauCeti.DoubledQuiver G) | TauCeti.IsZigzagRelator k G x}

theorem TauCeti.quadraticZigzagIdeal_eq_span (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) : quadraticZigzagIdeal k G = TwoSidedIdeal.span {x : pathAlgebra k (DoubledQuiver G) | IsQuadraticZigzagRelator k G x}

The quadratic relation ideal is the two-sided span of the quadratic relators.

theorem TauCeti.zigzagIdeal_eq_span (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) : zigzagIdeal k G = TwoSidedIdeal.span {x : pathAlgebra k (DoubledQuiver G) | IsZigzagRelator k G x}

The uniform relation ideal is the two-sided span of the uniform relators.

theorem TauCeti.mem_quadraticZigzagIdeal_of_isQuadraticZigzagRelator (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) {x : pathAlgebra k (DoubledQuiver G)} (hx : IsQuadraticZigzagRelator k G x) : x ∈ quadraticZigzagIdeal k G

Every quadratic relator lies in the ideal it spans.

theorem TauCeti.mem_zigzagIdeal_of_isZigzagRelator (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) {x : pathAlgebra k (DoubledQuiver G)} (hx : IsZigzagRelator k G x) : x ∈ zigzagIdeal k G

Every uniform relator lies in the ideal it spans.

theorem TauCeti.quadraticZigzagIdeal_le_zigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) : quadraticZigzagIdeal k G ≤ zigzagIdeal k G

The quadratic relators are among the uniform ones, so their ideal is contained in the uniform one. The reverse inclusion is the redundancy theorem below, and needs hypotheses on the graph.

Membership of the short products

theorem TauCeti.ofArrow_mul_ofArrow_mem_quadraticZigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) {i j l : V} (h : G.Adj i j) (h' : G.Adj j l) (hne : i ≠ l) : PathAlgebra.ofArrow (DoubledQuiver.arrow G h') * PathAlgebra.ofArrow (DoubledQuiver.arrow G h) ∈ quadraticZigzagIdeal k G

A length-two path whose endpoints differ is a quadratic relator, written as a product of two oriented edges.

theorem TauCeti.backtrackElem_sub_backtrackElem_mem_quadraticZigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : DoubledQuiver.backtrackElem G k h - DoubledQuiver.backtrackElem G k h' ∈ quadraticZigzagIdeal k G

Two backtracks based at the same vertex differ by a quadratic relator.

The redundancy of the long relators

theorem TauCeti.zigzagIdeal_eq_quadraticZigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (hconn : G.Connected) (hcard : 3 ≤ Nat.card V) : zigzagIdeal k G = quadraticZigzagIdeal k G

The zigzag relations are quadratic. For a connected graph with at least three vertices the long-path generators are consequences of the two quadratic families, so the uniform and the purely quadratic relation ideals agree.

The hypotheses are sharp for the roadmap's low-rank conventions. On the one-edge graph A₂ the doubled quiver has no length-two path with distinct endpoints and only one backtrack at each vertex, so every quadratic relator is already zero and the quadratic ideal is ⊥, while the uniform ideal kills the length-three paths.

The relation quotient

@[reducible, inline]

noncomputable abbrev TauCeti.nonisolatedZigzagQuotient (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : Type (max (max u w) w u)

The zigzag relation quotient of a simple graph: the path algebra of the doubled quiver modulo the uniform relation ideal.

This is the algebra of a connected graph with an edge: on a graph with an isolated vertex it is not the intended zigzag algebra, whose singleton components carry the dual numbers instead. The componentwise public definition is built from this quotient elsewhere.

Equations

• TauCeti.nonisolatedZigzagQuotient k G = (TauCeti.pathAlgebra k (TauCeti.DoubledQuiver G) ⧸ TwoSidedIdeal.asIdeal (TauCeti.zigzagIdeal k G))

noncomputable def TauCeti.zigzagMk (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : pathAlgebra k (DoubledQuiver G) →ₐ[k] nonisolatedZigzagQuotient k G

The quotient map from the path algebra of the doubled quiver onto the zigzag quotient.

Equations

• TauCeti.zigzagMk k G = Ideal.Quotient.mkₐ k (TwoSidedIdeal.asIdeal (TauCeti.zigzagIdeal k G))

theorem TauCeti.zigzagMk_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (x : pathAlgebra k (DoubledQuiver G)) : (zigzagMk k G) x = (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (zigzagIdeal k G))) x

The quotient map is the ring-theoretic quotient map of the relation ideal.

@[simp]

theorem TauCeti.zigzagMk_eq_zero_iff (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {x : pathAlgebra k (DoubledQuiver G)} : (zigzagMk k G) x = 0 ↔ x ∈ zigzagIdeal k G

The kernel of the quotient map is the relation ideal.

theorem TauCeti.zigzagMk_eq_zero_of_isZigzagRelator (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {x : pathAlgebra k (DoubledQuiver G)} (hx : IsZigzagRelator k G x) : (zigzagMk k G) x = 0

Every uniform relator dies in the zigzag quotient.

@[simp]

theorem TauCeti.zigzagMk_ofPath_eq_zero_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : DoubledQuiver G} (p : Quiver.Path i j) (hp : p.length = 2) (hij : i ≠ j) : (zigzagMk k G) (PathAlgebra.ofPath ⟨i, ⟨j, p⟩⟩) = 0

A length-two path whose endpoints differ dies in the zigzag quotient.

@[simp]

theorem TauCeti.zigzagMk_ofPath_eq_zero_of_three_le (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (x : Quiver.TotalPath (DoubledQuiver G)) (hx : 3 ≤ x.snd.snd.length) : (zigzagMk k G) (PathAlgebra.ofPath x) = 0

A path of length at least three dies in the zigzag quotient.

theorem TauCeti.zigzagMk_backtrackElem_eq (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : (zigzagMk k G) (DoubledQuiver.backtrackElem G k h) = (zigzagMk k G) (DoubledQuiver.backtrackElem G k h')

The backtracks based at a vertex all have the same image in the zigzag quotient: this common value is the volume element of the vertex.

theorem TauCeti.zigzagIdeal_le_ker (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {B : Type u_1} [Ring B] [Algebra k B] (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsZigzagRelator k G x → f x = 0) : zigzagIdeal k G ≤ TwoSidedIdeal.ker f

An algebra map killing every uniform relator kills the whole relation ideal.

noncomputable def TauCeti.zigzagLift (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {B : Type u_1} [Ring B] [Algebra k B] (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsZigzagRelator k G x → f x = 0) : nonisolatedZigzagQuotient k G →ₐ[k] B

The universal property of the zigzag quotient: an algebra map out of the path algebra which kills every uniform relator factors through the quotient.

Equations

• TauCeti.zigzagLift k G f hf = Ideal.Quotient.liftₐ (TwoSidedIdeal.asIdeal (TauCeti.zigzagIdeal k G)) f ⋯

@[simp]

theorem TauCeti.zigzagLift_zigzagMk (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {B : Type u_1} [Ring B] [Algebra k B] (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsZigzagRelator k G x → f x = 0) (x : pathAlgebra k (DoubledQuiver G)) : (zigzagLift k G f hf) ((zigzagMk k G) x) = f x

theorem TauCeti.zigzagLift_unique (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {B : Type u_1} [Ring B] [Algebra k B] (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsZigzagRelator k G x → f x = 0) (g : nonisolatedZigzagQuotient k G →ₐ[k] B) (hg : ∀ (x : pathAlgebra k (DoubledQuiver G)), g ((zigzagMk k G) x) = f x) : g = zigzagLift k G f hf

The lift is the unique algebra map whose composite with the quotient map is f.

theorem TauCeti.zigzagIdeal_le_ker_of_quadratic (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {B : Type u_1} [Ring B] [Algebra k B] (hconn : G.Connected) (hcard : 3 ≤ Nat.card V) (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsQuadraticZigzagRelator k G x → f x = 0) : zigzagIdeal k G ≤ TwoSidedIdeal.ker f

On a connected graph with at least three vertices an algebra map killing the quadratic relators already kills the whole relation ideal.

noncomputable def TauCeti.zigzagLiftOfQuadratic (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {B : Type u_1} [Ring B] [Algebra k B] (hconn : G.Connected) (hcard : 3 ≤ Nat.card V) (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsQuadraticZigzagRelator k G x → f x = 0) : nonisolatedZigzagQuotient k G →ₐ[k] B

For a connected graph with at least three vertices only the quadratic relations need to be checked: an algebra map killing them factors through the zigzag quotient.

Equations

• TauCeti.zigzagLiftOfQuadratic k G hconn hcard f hf = TauCeti.zigzagLift k G f ⋯

@[simp]

theorem TauCeti.zigzagLiftOfQuadratic_zigzagMk (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {B : Type u_1} [Ring B] [Algebra k B] (hconn : G.Connected) (hcard : 3 ≤ Nat.card V) (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsQuadraticZigzagRelator k G x → f x = 0) (x : pathAlgebra k (DoubledQuiver G)) : (zigzagLiftOfQuadratic k G hconn hcard f hf) ((zigzagMk k G) x) = f x

theorem TauCeti.zigzagLiftOfQuadratic_unique (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {B : Type u_1} [Ring B] [Algebra k B] (hconn : G.Connected) (hcard : 3 ≤ Nat.card V) (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsQuadraticZigzagRelator k G x → f x = 0) (g : nonisolatedZigzagQuotient k G →ₐ[k] B) (hg : ∀ (x : pathAlgebra k (DoubledQuiver G)), g ((zigzagMk k G) x) = f x) : g = zigzagLiftOfQuadratic k G hconn hcard f hf

The quadratic lift is the unique algebra map whose composite with the quotient map is f.