The middle tensor factor at adjacent zigzag vertices

At adjacent vertices i and j, multiplication identifies the balanced product e_i Z ⊗[Z] Z e_j with the corner e_i Z e_j. The corner has one basis vector, the arrow from j to i, so its arrow coordinate identifies the balanced product with the ground ring. The pure-tensor formula records the order of multiplication in Tau Ceti's later-factor-first path convention.

This is the middle factor in the product of adjacent vertex bimodules (Z e_i ⊗[k] e_i Z) ⊗[Z] (Z e_j ⊗[k] e_j Z).

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

noncomputable def TauCeti.zigzagAdjacentBalancedTensorEquiv (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) : BalancedTensorProduct k ↑(zigzagAlgebra k G) ↥(Ideal.span {MulOpposite.op ((fun (v : V) => (zigzagAlgebraBasis k G) (Sum.inl v)) i)}) ↥(Ideal.span {(fun (v : V) => (zigzagAlgebraBasis k G) (Sum.inl v)) j}) ≃ₗ[k] k

Multiplication followed by the arrow coordinate identifies the balanced middle factor of adjacent vertex braid bimodules with one copy of the ground ring.

@[simp]

theorem TauCeti.zigzagAdjacentBalancedTensorEquiv_tmul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) (m : ↥(Ideal.span {MulOpposite.op ((fun (v : V) => (zigzagAlgebraBasis k G) (Sum.inl v)) i)})) (n : ↥(Ideal.span {(fun (v : V) => (zigzagAlgebraBasis k G) (Sum.inl v)) j})) : (zigzagAdjacentBalancedTensorEquiv k G h) (BalancedTensorProduct.tmul k (↑(zigzagAlgebra k G)) m n) = ((zigzagAlgebraBasis k G).repr (MulOpposite.unop ↑m * ↑n)) (Sum.inr (Sum.inl { fst := j, snd := i, adj := h }))

On pure tensors, the adjacent middle-factor coordinate is the arrow coordinate of the product in the zigzag algebra.

@[simp]

theorem TauCeti.zigzagAdjacentBalancedTensorEquiv_symm_apply (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) (a : k) : (zigzagAdjacentBalancedTensorEquiv k G h).symm a = BalancedTensorProduct.tmul k (↑(zigzagAlgebra k G)) (spanSingletonGenerator (MulOpposite.op ((fun (v : V) => (zigzagAlgebraBasis k G) (Sum.inl v)) i))) ⟨↑((zigzagAlgebraAdjacentCornerEquiv k G h).symm a), ⋯⟩

The inverse adjacent middle-factor coordinate inserts the right-ideal generator and the corresponding multiple of the arrow in the left ideal.