Terms of the actual triple braid complex

The left-associated cochain totalization has terms in degrees −3 through 0. Its lowest term is the tensor of the three vertex bimodules; its two middle terms are the three pairwise tensors and the three individual vertex bimodules, and its degree-zero term is the regular graded bimodule. The component isomorphisms preserve internal degrees and both outer actions.

These identifications supply the terms for the adjacent braid cancellation. They reuse the existing degree-zero and degree-minus-one pair comparisons and Mathlib's additive-functor biproduct comparison. The totalization and its cohomological signs are the existing Mathlib construction.

@[reducible, inline]

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

The actual left-associated signed cochain tensor product of three braid complexes.

theorem TauCeti.isZero_zigzagBraidComplexTriple_X (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) (n : ℤ) (h : n < -3 ∨ 0 < n) : CategoryTheory.Limits.IsZero ((zigzagBraidComplexTriple k G i j l).X n)

The actual triple tensor complex vanishes outside cohomological degrees −3 through 0.

noncomputable def TauCeti.zigzagBraidComplexTripleXMinusThreeIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : (zigzagBraidComplexTriple k G i j l).X (-3) ≅ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j))).obj (zigzagGradedBraidBimodule k G l)

The lowest triple term is the left-associated tensor of the three vertex bimodules.

noncomputable def TauCeti.zigzagBraidComplexTripleXZeroIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : (zigzagBraidComplexTriple k G i j l).X 0 ≅ zigzagGradedBimodule k G

The degree-zero triple term is the actual regular graded bimodule.

noncomputable def TauCeti.zigzagBraidComplexTripleXMinusTwoIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : (zigzagBraidComplexTriple k G i j l).X (-2) ≅ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j) ⊞ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G l) ⊞ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G j)).obj (zigzagGradedBraidBimodule k G l)

The degree-minus-two triple term consists of the three pairwise vertex tensor products.

noncomputable def TauCeti.zigzagBraidComplexTripleXMinusOneIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : (zigzagBraidComplexTriple k G i j l).X (-1) ≅ (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j) ⊞ zigzagGradedBraidBimodule k G l

The degree-minus-one triple term consists of the three vertex bimodules.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusThreeIso_hom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-2) (-1) (-3) ιMapBifunctor_zigzagBraidComplexTripleXMinusThreeIso_hom._proof_1) (zigzagBraidComplexTripleXMinusThreeIso k G i j l).hom = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X (-1))).map (zigzagBraidComplexTensorXMinusTwoIso k G i j).hom) (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j))).map (zigzagBraidComplexXIso₀ k G l).hom)

The lowest triple summand uses the pair comparison followed by the third vertex map.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusThreeIso_hom_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j))).obj (zigzagGradedBraidBimodule k G l) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-2) (-1) (-3) ιMapBifunctor_zigzagBraidComplexTripleXMinusThreeIso_hom._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusThreeIso k G i j l).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X (-1))).map (zigzagBraidComplexTensorXMinusTwoIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j))).map (zigzagBraidComplexXIso₀ k G l).hom) h)

The lowest triple summand uses the pair comparison followed by the third vertex map.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXZeroIso_hom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 0 0 ιMapBifunctor_zigzagBraidComplexTripleXZeroIso_hom._proof_1) (zigzagBraidComplexTripleXZeroIso k G i j l).hom = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X 0)).map (zigzagBraidComplexTensorXZeroIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).map (zigzagBraidComplexXIso₁ k G l).hom) (zigzagBimoduleLeftUnitor k G (zigzagGradedBimodule k G)).hom)

The degree-zero triple summand is identified by the regular pair map and left unitor.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXZeroIso_hom_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBimodule k G ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 0 0 ιMapBifunctor_zigzagBraidComplexTripleXZeroIso_hom._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXZeroIso k G i j l).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X 0)).map (zigzagBraidComplexTensorXZeroIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).map (zigzagBraidComplexXIso₁ k G l).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G (zigzagGradedBimodule k G)).hom h))

The degree-zero triple summand is identified by the regular pair map and left unitor.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusTwoIso_hom_left (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-2) 0 (-2) ιMapBifunctor_zigzagBraidComplexTripleXMinusTwoIso_hom_left._proof_1) (zigzagBraidComplexTripleXMinusTwoIso k G i j l).hom = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X 0)).map (zigzagBraidComplexTensorXMinusTwoIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j))).map (zigzagBraidComplexXIso₁ k G l).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j))).hom CategoryTheory.Limits.biprod.inl))

The pair of the first two vertices is the first summand of the degree-minus-two term.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusTwoIso_hom_left_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j) ⊞ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G l) ⊞ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G j)).obj (zigzagGradedBraidBimodule k G l) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-2) 0 (-2) ιMapBifunctor_zigzagBraidComplexTripleXMinusTwoIso_hom_left._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusTwoIso k G i j l).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X 0)).map (zigzagBraidComplexTensorXMinusTwoIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j))).map (zigzagBraidComplexXIso₁ k G l).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j))).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)))

The pair of the first two vertices is the first summand of the degree-minus-two term.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusTwoIso_hom_right (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) (-1) (-2) ιMapBifunctor_zigzagBraidComplexTripleXMinusTwoIso_hom_right._proof_1) (zigzagBraidComplexTripleXMinusTwoIso k G i j l).hom = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X (-1))).map (zigzagBraidComplexTensorXMinusOneIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j)).map (zigzagBraidComplexXIso₀ k G l).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj (zigzagGradedBraidBimodule k G l)).map CategoryTheory.Limits.biprod.fst) (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj (zigzagGradedBraidBimodule k G l)).map CategoryTheory.Limits.biprod.snd)) CategoryTheory.Limits.biprod.inr))

The other two pairwise tensors form the second summand of the degree-minus-two term.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusTwoIso_hom_right_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j) ⊞ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G l) ⊞ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G j)).obj (zigzagGradedBraidBimodule k G l) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) (-1) (-2) ιMapBifunctor_zigzagBraidComplexTripleXMinusTwoIso_hom_right._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusTwoIso k G i j l).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X (-1))).map (zigzagBraidComplexTensorXMinusOneIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j)).map (zigzagBraidComplexXIso₀ k G l).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj (zigzagGradedBraidBimodule k G l)).map CategoryTheory.Limits.biprod.fst) (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj (zigzagGradedBraidBimodule k G l)).map CategoryTheory.Limits.biprod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h)))

The other two pairwise tensors form the second summand of the degree-minus-two term.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusOneIso_hom_left (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) 0 (-1) ιMapBifunctor_zigzagBraidComplexTripleXMinusOneIso_hom_left._proof_1) (zigzagBraidComplexTripleXMinusOneIso k G i j l).hom = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X 0)).map (zigzagBraidComplexTensorXMinusOneIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j)).map (zigzagBraidComplexXIso₁ k G l).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j)).hom CategoryTheory.Limits.biprod.inl))

The first two vertex terms form the first summand of the degree-minus-one term.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusOneIso_hom_left_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j) ⊞ zigzagGradedBraidBimodule k G l ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) 0 (-1) ιMapBifunctor_zigzagBraidComplexTripleXMinusOneIso_hom_left._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusOneIso k G i j l).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X 0)).map (zigzagBraidComplexTensorXMinusOneIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j)).map (zigzagBraidComplexXIso₁ k G l).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j)).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)))

The first two vertex terms form the first summand of the degree-minus-one term.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusOneIso_hom_right (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 (-1) (-1) ιMapBifunctor_zigzagBraidComplexTripleXMinusOneIso_hom_right._proof_1) (zigzagBraidComplexTripleXMinusOneIso k G i j l).hom = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X (-1))).map (zigzagBraidComplexTensorXZeroIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).map (zigzagBraidComplexXIso₀ k G l).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G (zigzagGradedBraidBimodule k G l)).hom CategoryTheory.Limits.biprod.inr))

The third vertex term is the second summand of the degree-minus-one term.

@[simp]

theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTripleXMinusOneIso_hom_right_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j) ⊞ zigzagGradedBraidBimodule k G l ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (zigzagBraidComplexTensor k G i j) (zigzagBraidComplex k G l) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 (-1) (-1) ιMapBifunctor_zigzagBraidComplexTripleXMinusOneIso_hom_right._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusOneIso k G i j l).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G l).X (-1))).map (zigzagBraidComplexTensorXZeroIso k G i j).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).map (zigzagBraidComplexXIso₀ k G l).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G (zigzagGradedBraidBimodule k G l)).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h)))

The third vertex term is the second summand of the degree-minus-one term.