Adjacent vertex corners of the componentwise zigzag algebra

If j and i are adjacent, the corner e_i Z e_j is the free rank-one module generated by the arrow from j to i. This supplies the middle corner in a tensor product of adjacent vertex braid bimodules. The statement uses the public componentwise zigzag algebra, so it also applies when the graph is disconnected or has isolated vertices elsewhere. The arrow coordinate gives an explicit equivalence with the coefficient ring.

The calculation follows the vertex--arrow--volume multiplication table of Huerfano--Khovanov, A category for the adjoint representation, Section 3.

theorem TauCeti.cornerSubmodule_zigzagAlgebra_eq_span_of_adj {V : Type u_1} [Finite V] (k : Type u_2) [CommRing k] (G : SimpleGraph V) {i j : V} (h : G.Adj j i) : cornerSubmodule k ((zigzagAlgebraBasis k G) (Sum.inl i)) ((zigzagAlgebraBasis k G) (Sum.inl j)) = k ∙ (zigzagAlgebraBasis k G) (Sum.inr (Sum.inl { fst := j, snd := i, adj := h }))

The corner between adjacent vertices is exactly the span of the arrow from its right idempotent to its left idempotent. This holds over every commutative coefficient ring.

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

The adjacent corner e_i Z e_j is free on the arrow from j to i. Its coordinate equivalence works over every commutative coefficient ring.

@[simp]

theorem TauCeti.zigzagAlgebraAdjacentCornerEquiv_apply {V : Type u_1} [Finite V] (k : Type u_2) [CommRing k] (G : SimpleGraph V) {i j : V} (h : G.Adj j i) (x : ↥(cornerSubmodule k ((fun (v : V) => (zigzagAlgebraBasis k G) (Sum.inl v)) i) ((fun (v : V) => (zigzagAlgebraBasis k G) (Sum.inl v)) j))) : (zigzagAlgebraAdjacentCornerEquiv k G h) x = ((zigzagAlgebraBasis k G).repr ↑x) (Sum.inr (Sum.inl { fst := j, snd := i, adj := h }))

The coordinate of an adjacent corner element is its coefficient at the arrow.

@[simp]

theorem TauCeti.coe_zigzagAlgebraAdjacentCornerEquiv_symm_apply {V : Type u_1} [Finite V] (k : Type u_2) [CommRing k] (G : SimpleGraph V) {i j : V} (h : G.Adj j i) (a : k) : ↑((zigzagAlgebraAdjacentCornerEquiv k G h).symm a) = a • (zigzagAlgebraBasis k G) (Sum.inr (Sum.inl { fst := j, snd := i, adj := h }))

The inverse arrow coordinate sends a scalar to its multiple of the adjacent arrow.

theorem TauCeti.finrank_cornerSubmodule_zigzagAlgebra_of_adj {V : Type u_1} [Finite V] (k : Type u_2) [Field k] (G : SimpleGraph V) {i j : V} (h : G.Adj j i) : Module.finrank k ↥(cornerSubmodule k ((zigzagAlgebraBasis k G) (Sum.inl i)) ((zigzagAlgebraBasis k G) (Sum.inl j))) = 1

An adjacent pair of vertex idempotents cuts out a one-dimensional corner.