Endpoint terms of an inverse braid-complex product

The cochain tensor product of the braid complex Bᵢ with its inverse Bᵢ' has one term in cohomological degree -1 and one in degree 1. The balanced tensor unitors identify them with the vertex bimodule Pᵢ ⊗ₖ eᵢ Z and its internal shift by -2. These identifications are the outer terms of TauCeti.zigzagBraidComplexTensorInverseHomotopyEquiv, which cancels the middle terms to show that Bᵢ ⊗ Bᵢ' is homotopy equivalent to the regular graded bimodule Z in degree zero.

The calculation is valid for the public componentwise zigzag algebra, 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).

@[reducible, inline]

noncomputable abbrev TauCeti.zigzagBraidInverseComplexTensor (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CochainComplex (GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) ℤ

The cochain tensor product of the braid complex and its inverse at one vertex.

theorem TauCeti.isZero_zigzagBraidInverseComplexTensor_pair (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (p q : ℤ) (h : ¬((p = -1 ∨ p = 0) ∧ (q = 0 ∨ q = 1))) : CategoryTheory.Limits.IsZero (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj ((zigzagBraidComplex k G i).X p)).obj ((zigzagBraidInverseComplex k G i).X q))

A summand of Bᵢ ⊗ Bᵢ' vanishes unless its degrees lie in {-1, 0} × {0, 1}.

noncomputable def TauCeti.zigzagBraidInverseTensorXMinusOneIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidInverseComplexTensor k G i).X (-1) ≅ zigzagGradedBraidBimodule k G i

The degree -1 term of Bᵢ ⊗ Bᵢ' is the vertex bimodule.

noncomputable def TauCeti.zigzagBraidInverseTensorXOneIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidInverseComplexTensor k G i).X 1 ≅ (GradedModuleCat.shiftFunctor (-2)).obj (zigzagGradedBraidBimodule k G i)

The degree 1 term of Bᵢ ⊗ Bᵢ' is the vertex bimodule shifted by -2.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidInverseTensorXMinusOneIso_hom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidInverseComplex k G i) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) 0 (-1) ιMapBifunctor_zigzagBraidInverseTensorXMinusOneIso_hom._proof_1) (zigzagBraidInverseTensorXMinusOneIso k G i).hom = ((((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidInverseComplex k G i).X 0)).mapIso (zigzagBraidComplexXIso₀ k G i) ≪≫ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).mapIso (zigzagBraidInverseComplexXIso₀ k G i)) ≪≫ zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i)).hom

The degree (-1, 0) summand includes into degree -1 as the right unitor.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidInverseTensorXMinusOneIso_hom_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidInverseComplex k G i) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) 0 (-1) ιMapBifunctor_zigzagBraidInverseTensorXMinusOneIso_hom._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidInverseTensorXMinusOneIso k G i).hom h) = CategoryTheory.CategoryStruct.comp ((((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidInverseComplex k G i).X 0)).mapIso (zigzagBraidComplexXIso₀ k G i) ≪≫ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).mapIso (zigzagBraidInverseComplexXIso₀ k G i)) ≪≫ zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i)).hom h

The degree (-1, 0) summand includes into degree -1 as the right unitor.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidInverseTensorXOneIso_hom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidInverseComplex k G i) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 1 1 ιMapBifunctor_zigzagBraidInverseTensorXOneIso_hom._proof_1) (zigzagBraidInverseTensorXOneIso k G i).hom = ((((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidInverseComplex k G i).X 1)).mapIso (zigzagBraidComplexXIso₁ k G i) ≪≫ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).mapIso (zigzagBraidInverseComplexXIso₁ k G i)) ≪≫ zigzagBimoduleLeftUnitor k G ((GradedModuleCat.shiftFunctor (-2)).obj (zigzagGradedBraidBimodule k G i))).hom

The degree (0, 1) summand includes into degree 1 as the left unitor.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidInverseTensorXOneIso_hom_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : (GradedModuleCat.shiftFunctor (-2)).obj (zigzagGradedBraidBimodule k G i) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidInverseComplex k G i) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 1 1 ιMapBifunctor_zigzagBraidInverseTensorXOneIso_hom._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidInverseTensorXOneIso k G i).hom h) = CategoryTheory.CategoryStruct.comp ((((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidInverseComplex k G i).X 1)).mapIso (zigzagBraidComplexXIso₁ k G i) ≪≫ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).mapIso (zigzagBraidInverseComplexXIso₁ k G i)) ≪≫ zigzagBimoduleLeftUnitor k G ((GradedModuleCat.shiftFunctor (-2)).obj (zigzagGradedBraidBimodule k G i))).hom h

The degree (0, 1) summand includes into degree 1 as the left unitor.