Corners of the componentwise zigzag algebra

For distinct nonadjacent vertices i, j of a finite simple graph, the corner e_i Z e_j of the componentwise zigzag algebra is zero, including when either vertex is isolated. These corners enter the calculation of tensor products of the vertex projective bimodules. The diagonal corner is spanned by the vertex and its volume vector; its coordinates give the two middle summands in the self-tensor calculation used for inverse braid complexes.

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

theorem TauCeti.cornerSubmodule_zigzagAlgebra_eq_bot_of_ne_of_not_adj (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (hij : i ≠ j) (hadj : ¬G.Adj i j) : cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j) = ⊥

Distinct nonadjacent vertex idempotents cut out a zero corner of the public zigzag algebra, including its isolated-vertex dual-number factors.

theorem TauCeti.zigzagAlgebraBasis_inl_mul_mul_eq_zero_of_ne_of_not_adj (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (hij : i ≠ j) (hadj : ¬G.Adj i j) (x : ↑(zigzagAlgebra k G)) : (fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i * x * (fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j = 0

Distinct nonadjacent vertex idempotents kill every algebra element between them.

theorem TauCeti.zigzagAlgebraBasis_inl_mul_mul_self (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (x : ↑(zigzagAlgebra k G)) : (fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i * x * (fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i = ((zigzagAlgebraBasis k G).repr x) (Sum.inl i) • (fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i + ((zigzagAlgebraBasis k G).repr x) (Sum.inr (Sum.inr i)) • (zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i))

Cutting down at the same vertex keeps exactly the vertex and volume coordinates.

theorem TauCeti.cornerSubmodule_zigzagAlgebra_self_eq_span (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) = Submodule.span k {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i, (zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i))}

The diagonal corner consists of the span of the vertex and volume basis vectors.

noncomputable def TauCeti.zigzagAlgebraSelfCornerEquiv (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : ↥(cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)) ≃ₗ[k] k × k

The vertex and volume coordinates identify the diagonal corner with two ground-ring copies.

@[simp]

theorem TauCeti.zigzagAlgebraSelfCornerEquiv_apply (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (x : ↥(cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i))) : (zigzagAlgebraSelfCornerEquiv k G i) x = (((zigzagAlgebraBasis k G).repr ↑x) (Sum.inl i), ((zigzagAlgebraBasis k G).repr ↑x) (Sum.inr (Sum.inr i)))

@[simp]

theorem TauCeti.coe_zigzagAlgebraSelfCornerEquiv_symm_apply (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (a : k × k) : ↑((zigzagAlgebraSelfCornerEquiv k G i).symm a) = a.1 • (fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i + a.2 • (zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i))