The basis and dimension of a skew-zigzag relation quotient

A skew-zigzag parameter c labels each ordered pair of incident edges of a finite simple graph by a unit-valued ratio, and TauCeti.skewZigzagQuotient imposes backtrack(h) = c.ratio h h' • backtrack(h') on top of the relations killing non-returning quadratic paths and paths of length at least three. For a graph with no isolated vertices, this file proves that the resulting algebra has the same vertex, arrow and volume basis as the ordinary zigzag relation quotient, and hence the same dimension 2|V| + 2|E|.

For a general skew parameter, the backtracks based at a vertex are unit multiples of one another, so the volume class may depend on a chosen incident edge. The full basis therefore requires a choice t of one incident edge at every vertex. Its third block is the class of the backtrack along the chosen edge. The resulting basis also gives a linear isomorphism with the ordinary relation quotient.

Main definitions

• TauCeti.skewZigzagVolume: the volume class of a vertex relative to a chosen incident edge.
• TauCeti.skewZigzagBasisFun: the vertex, arrow and chosen-volume family.
• TauCeti.skewZigzagBasis: that family, as a basis of the skew-zigzag relation quotient.
• TauCeti.skewZigzagQuotientLinearEquiv: the induced linear isomorphism with the ordinary zigzag relation quotient.

Main results

• TauCeti.linearIndependent_skewZigzagBasisFun and TauCeti.span_range_skewZigzagBasisFun_eq_top: the family is independent and spans.
• TauCeti.skewZigzagMk_backtrackElem_ne_zero and TauCeti.skewZigzagVolume_ne_zero: no backtrack class vanishes.
• TauCeti.skewZigzagMk_ofArrow_ne_zero: no arrow class vanishes.
• TauCeti.skewZigzagMk_ofArrow_smul_left_injective: scalar multiplication of an arrow class is injective, so the coefficient of an element of an arrow's span is unique.
• TauCeti.skewZigzagMk_vertexIdempotent_mul_mul_vertexIdempotent_mem_span: the corner between the endpoints of an arrow is spanned by that arrow.
• TauCeti.skewZigzagMk_vertexIdempotent_mul_mul_vertexIdempotent_eq_zero: the corner between two distinct nonadjacent vertices vanishes.
• TauCeti.finrank_skewZigzagQuotient: when there are no isolated vertices, the dimension is 2|V| + 2|E|, as in the ordinary case.

References

See C. Couture, Skew-Zigzag Algebras, Section 3, https://arxiv.org/abs/1509.08405, and S. Huerfano and M. Khovanov, A category for the adjoint representation, Section 3, https://arxiv.org/abs/math/0002060.

The backtracks of darts

The rescaling of the path basis

The rescaling carries the skew relations to the ordinary ones

The volume classes

noncomputable def TauCeti.skewZigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] {i : V} (e : { j : V // G.Adj i j }) : skewZigzagQuotient k G c

The volume class of a vertex in a skew-zigzag relation quotient, relative to a chosen incident edge: the class of the backtrack along that edge. For a general skew parameter this class may depend on the choice, since the backtracks at a vertex are unit multiples of one another.

theorem TauCeti.skewZigzagVolume_def (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] {i : V} (e : { j : V // G.Adj i j }) : skewZigzagVolume k G c e = (skewZigzagMk k G c) (DoubledQuiver.backtrackElem G k ⋯)

The chosen skew-zigzag volume is represented by the backtrack along its chosen incident edge.

theorem TauCeti.skewZigzagMk_backtrackElem_eq_smul_skewZigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] {i j : V} (e : { j' : V // G.Adj i j' }) (h : G.Adj i j) : (skewZigzagMk k G c) (DoubledQuiver.backtrackElem G k h) = ↑(c.ratio h ⋯) • skewZigzagVolume k G c e

The class of any backtrack is the prescribed unit multiple of the volume class of its base vertex. The reference edge e must be supplied explicitly: it cannot be inferred from the backtrack on the left-hand side, so this is intentionally not a global simp lemma.

The basis

noncomputable def TauCeti.skewZigzagBasisFun (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) : ZigzagBasisIndex G → skewZigzagQuotient k G c

The vertex, arrow and volume family of a skew-zigzag relation quotient: the class of a vertex idempotent, the class of the arrow of a dart, and the volume class of a vertex relative to the chosen incident edge.

@[simp]

theorem TauCeti.skewZigzagBasisFun_inl (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) (i : V) : skewZigzagBasisFun k G c t (Sum.inl i) = (skewZigzagMk k G c) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i))

@[simp]

theorem TauCeti.skewZigzagBasisFun_inr_inl (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) (d : G.Dart) : skewZigzagBasisFun k G c t (Sum.inr (Sum.inl d)) = (skewZigzagMk k G c) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯))

@[simp]

theorem TauCeti.skewZigzagBasisFun_inr_inr (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) (i : V) : skewZigzagBasisFun k G c t (Sum.inr (Sum.inr i)) = skewZigzagVolume k G c (t i)

theorem TauCeti.linearIndependent_skewZigzagBasisFun (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) : LinearIndependent k (skewZigzagBasisFun k G c t)

The vertex, arrow and volume classes of a skew-zigzag quotient are independent.

theorem TauCeti.span_range_skewZigzagBasisFun_eq_top (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) : Submodule.span k (Set.range (skewZigzagBasisFun k G c t)) = ⊤

The vertex, arrow and volume classes of a skew-zigzag quotient span.

noncomputable def TauCeti.skewZigzagBasis (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) : Module.Basis (ZigzagBasisIndex G) k (skewZigzagQuotient k G c)

The basis of a skew-zigzag relation quotient. For a finite simple graph with a choice of an incident edge at every vertex, the vertex idempotents, the oriented edges, and the volume classes of the chosen edges are a basis of the skew-zigzag relation quotient, whatever the parameter.

theorem TauCeti.moduleFinite_skewZigzagQuotient (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) : Module.Finite k (skewZigzagQuotient k G c)

A skew-zigzag relation quotient with an incident edge at every vertex is finite over the base ring.

theorem TauCeti.moduleFree_skewZigzagQuotient (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) : Module.Free k (skewZigzagQuotient k G c)

A skew-zigzag relation quotient with an incident edge at every vertex is free over the base ring.

@[simp]

theorem TauCeti.skewZigzagBasis_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) (b : ZigzagBasisIndex G) : (skewZigzagBasis k G c t) b = skewZigzagBasisFun k G c t b

theorem TauCeti.skewZigzagBasis_coord_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) (b b' : ZigzagBasisIndex G) : ((skewZigzagBasis k G c t).coord b) ((skewZigzagBasis k G c t) b') = if b' = b then 1 else 0

A coordinate of a skew-zigzag basis vector is the corresponding Kronecker delta.

theorem TauCeti.skewZigzagMk_backtrackElem_ne_zero (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] [Nontrivial k] {i j : V} (hij : G.Adj i j) : (skewZigzagMk k G c) (DoubledQuiver.backtrackElem G k hij) ≠ 0

No backtrack dies in a skew-zigzag relation quotient, whatever the parameter or the other components of the graph.

theorem TauCeti.skewZigzagVolume_ne_zero (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] [Nontrivial k] {i : V} (e : { j : V // G.Adj i j }) : skewZigzagVolume k G c e ≠ 0

The volume class of a vertex relative to a chosen incident edge is nonzero.

theorem TauCeti.skewZigzagMk_ofArrow_ne_zero (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] [Nontrivial k] {x y : DoubledQuiver G} (e : x ⟶ y) : (skewZigzagMk k G c) (PathAlgebra.ofArrow e) ≠ 0

No arrow dies in a skew-zigzag relation quotient: followed by its reverse it gives a backtrack class, which is nonzero.

theorem TauCeti.skewZigzagMk_backtrackElem_smul_left_injective (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] {i j : V} (hij : G.Adj i j) : Function.Injective fun (r : k) => r • (skewZigzagMk k G c) (DoubledQuiver.backtrackElem G k hij)

Scalar multiplication of a backtrack class is injective.

theorem TauCeti.skewZigzagMk_ofArrow_smul_left_injective (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] {x y : DoubledQuiver G} (e : x ⟶ y) : Function.Injective fun (r : k) => r • (skewZigzagMk k G c) (PathAlgebra.ofArrow e)

Scalar coefficients of an arrow are unique: scalar multiplication of an arrow class of a skew-zigzag relation quotient is injective, even over a commutative ring with zero divisors.

Corners

theorem TauCeti.skewZigzagMk_vertexIdempotent_mul_mul_vertexIdempotent_mem_span (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] {x y : DoubledQuiver G} (e : x ⟶ y) (z : skewZigzagQuotient k G c) : (skewZigzagMk k G c) (PathAlgebra.vertexIdempotent k y) * z * (skewZigzagMk k G c) (PathAlgebra.vertexIdempotent k x) ∈ k ∙ (skewZigzagMk k G c) (PathAlgebra.ofArrow e)

The corner of an arrow is spanned by the arrow. For an arrow e : x ⟶ y of the doubled quiver, cutting any element of a skew-zigzag relation quotient down by the vertex idempotent at the head on the left and at the tail on the right gives a scalar multiple of the arrow.

@[simp]

theorem TauCeti.skewZigzagMk_vertexIdempotent_mul_mul_vertexIdempotent_eq_zero (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] {i j : V} (hij : i ≠ j) (h : ¬G.Adj i j) (z : skewZigzagQuotient k G c) : (skewZigzagMk k G c) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G j)) * z * (skewZigzagMk k G c) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i)) = 0

The corner between two distinct nonadjacent vertices vanishes. Cutting any element of a skew-zigzag relation quotient down by the vertex idempotent at j on the left and at i on the right gives zero when i ≠ j are not joined by an edge.

The dimension and the comparison with the ordinary quotient

theorem TauCeti.finrank_skewZigzagQuotient (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] [Nontrivial k] [Fintype V] [DecidableRel G.Adj] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) : Module.finrank k (skewZigzagQuotient k G c) = 2 * Fintype.card V + 2 * G.edgeFinset.card

The dimension of a skew-zigzag relation quotient. A finite simple graph with no isolated vertex has dim = 2|V| + 2|E| for every skew parameter, as in the ordinary case.

theorem TauCeti.finrank_skewZigzagQuotient_of_preconnected (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] [Nontrivial k] [Fintype V] [Nontrivial V] [DecidableRel G.Adj] (hconn : G.Preconnected) : Module.finrank k (skewZigzagQuotient k G c) = 2 * Fintype.card V + 2 * G.edgeFinset.card

The dimension of a skew-zigzag quotient of a preconnected graph.

noncomputable def TauCeti.skewZigzagQuotientLinearEquiv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) : skewZigzagQuotient k G c ≃ₗ[k] nonisolatedZigzagQuotient k G

A skew-zigzag relation quotient is a linear twist of the ordinary one: the linear isomorphism matching the two vertex, arrow and volume bases. This constructs an isomorphism of the underlying modules only; no algebra equivalence is constructed here.

@[simp]

theorem TauCeti.skewZigzagQuotientLinearEquiv_skewZigzagBasisFun (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) [hV : Finite V] (t : (i : V) → { j : V // G.Adj i j }) (b : ZigzagBasisIndex G) : (skewZigzagQuotientLinearEquiv k G c t) (skewZigzagBasisFun k G c t b) = zigzagBasisFun k G b