Commutation of nonadjacent graded zigzag braid complexes

For distinct nonadjacent vertices, the actual tensor product of braid complexes has only the mixed vertex terms and the regular bimodule term. Unit identifications put these terms in the two-term complex with differential given by the two evaluations. Swapping the two vertex summands then gives commutation.

The component identifications describe the commuting map explicitly: in degree zero it is the identity of the regular bimodule, and in degree minus one it exchanges the two vertex summands by the biproduct braiding. The supported totalization-inclusion formulas identify each individual tensor summand with its unit or vertex component.

noncomputable def TauCeti.zigzagBraidComplexTensorCommIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (hij : i ≠ j) (hadj : ¬G.Adj i j) : zigzagBraidComplexTensor k G i j ≅ zigzagBraidComplexTensor k G j i

The actual graded braid complexes commute under tensoring at distinct nonadjacent vertices.

noncomputable def TauCeti.zigzagBraidComplexTensorCommHomotopyEquiv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (hij : i ≠ j) (hadj : ¬G.Adj i j) : HomotopyEquiv (zigzagBraidComplexTensor k G i j) (zigzagBraidComplexTensor k G j i)

The nonadjacent commuting isomorphism gives a homotopy equivalence of actual graded complexes.

@[simp]

theorem TauCeti.zigzagBraidComplexTensorCommIso_hom_f_zero (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (hij : i ≠ j) (hadj : ¬G.Adj i j) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplexTensorCommIso k G i j hij hadj).hom.f 0) (zigzagBraidComplexTensorXZeroIso k G j i).hom = (zigzagBraidComplexTensorXZeroIso k G i j).hom

In degree zero the commuting map is the identity under the regular-bimodule identifications.

@[simp]

theorem TauCeti.zigzagBraidComplexTensorCommIso_hom_f_zero_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (hij : i ≠ j) (hadj : ¬G.Adj i j) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBimodule k G ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplexTensorCommIso k G i j hij hadj).hom.f 0) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXZeroIso k G j i).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXZeroIso k G i j).hom h

In degree zero the commuting map is the identity under the regular-bimodule identifications.

@[simp]

theorem TauCeti.zigzagBraidComplexTensorCommIso_hom_f_minus_one (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (hij : i ≠ j) (hadj : ¬G.Adj i j) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplexTensorCommIso k G i j hij hadj).hom.f (-1)) (zigzagBraidComplexTensorXMinusOneIso k G j i).hom = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXMinusOneIso k G i j).hom (CategoryTheory.Limits.biprod.braiding (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)).hom

In degree minus one the commuting map exchanges the vertex summands by biproduct braiding.

@[simp]

theorem TauCeti.zigzagBraidComplexTensorCommIso_hom_f_minus_one_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (hij : i ≠ j) (hadj : ¬G.Adj i j) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBraidBimodule k G j ⊞ zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplexTensorCommIso k G i j hij hadj).hom.f (-1)) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXMinusOneIso k G j i).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXMinusOneIso k G i j).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)).hom h)

In degree minus one the commuting map exchanges the vertex summands by biproduct braiding.