The inverse graded braid complex followed by the braid complex

The cochain tensor product Bᵢ' ⊗ Bᵢ has the same three graded terms as Bᵢ ⊗ Bᵢ' (TauCeti.zigzagBraidComplexTensorInverseHomotopyEquiv). The second-factor differential carries the cochain sign (-1) ^ p, which is -1 on the block out of the (1, -1) summand, so the Ui{−2} coordinate of the middle term is negated. The two differential blocks are then identities, and the three-term cancellation criterion contracts the totalization to the regular graded bimodule in degree zero: TauCeti.zigzagBraidInverseTensorComplexHomotopyEquiv. The result includes arbitrary finite graphs and commutative coefficient rings, including isolated vertices.

References

• M. Khovanov and P. Seidel, Quivers, Floer cohomology, and braid group actions, J. Amer. Math. Soc. 15 (2002) (the complexes R_i and R_i' of the zigzag algebra A_m).
• R. S. Huerfano and M. Khovanov, A category for the adjoint representation, J. Algebra 246 (2001) (zigzag algebras of arbitrary graphs and the same complexes).

noncomputable def TauCeti.zigzagBraidInverseTensorComplexHomotopyEquiv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : HomotopyEquiv ((zigzagBraidInverseComplex k G i).mapBifunctor (zigzagBraidComplex k G i) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ)) (zigzagBraidUnitComplex k G)

The inverse graded braid complex followed by the braid complex is homotopy equivalent to the regular graded zigzag bimodule in cochain degree zero.