A common three-term complex for zigzag braid products

The pair of vertex tensor products maps to the two vertex bimodules by a signed evaluation matrix, followed by the sum of the vertex evaluations to the regular bimodule. The two composites of factor evaluations agree, so this is a complex. For adjacent vertices i and j, the intended contraction target for B_i B_j B_i and B_j B_i B_j is this common evaluation complex. The swap isomorphism exchanges the two vertex orders in that common target.

It is constructed as Mathlib's mapping cone of a map from a two-term complex to the regular bimodule in degree zero. The negated differential in that two-term complex cancels the mapping-cone sign.

noncomputable def TauCeti.zigzagBraidNormalFirstDifferential (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ⊞ GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G i) ⟶ zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j

The signed evaluation matrix from the two ordered vertex tensor products.

@[simp]

theorem TauCeti.zigzagBraidNormalFirstDifferential_inl_fst (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) CategoryTheory.Limits.biprod.fst) = -zigzagBraidTensorEvaluationRight k G i j

The first-column first-row component of the signed evaluation matrix.

theorem TauCeti.zigzagBraidNormalFirstDifferential_inl_fst_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h)) = CategoryTheory.CategoryStruct.comp (-zigzagBraidTensorEvaluationRight k G i j) h

The first-column first-row component of the signed evaluation matrix.

@[simp]

theorem TauCeti.zigzagBraidNormalFirstDifferential_inl_snd (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) CategoryTheory.Limits.biprod.snd) = zigzagBraidTensorEvaluationLeft k G i j

The first-column second-row component of the signed evaluation matrix.

theorem TauCeti.zigzagBraidNormalFirstDifferential_inl_snd_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G j ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h)) = CategoryTheory.CategoryStruct.comp (zigzagBraidTensorEvaluationLeft k G i j) h

The first-column second-row component of the signed evaluation matrix.

@[simp]

theorem TauCeti.zigzagBraidNormalFirstDifferential_inr_fst (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) CategoryTheory.Limits.biprod.fst) = zigzagBraidTensorEvaluationLeft k G j i

The second-column first-row component of the signed evaluation matrix.

theorem TauCeti.zigzagBraidNormalFirstDifferential_inr_fst_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h)) = CategoryTheory.CategoryStruct.comp (zigzagBraidTensorEvaluationLeft k G j i) h

The second-column first-row component of the signed evaluation matrix.

@[simp]

theorem TauCeti.zigzagBraidNormalFirstDifferential_inr_snd (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) CategoryTheory.Limits.biprod.snd) = -zigzagBraidTensorEvaluationRight k G j i

The second-column second-row component of the signed evaluation matrix.

theorem TauCeti.zigzagBraidNormalFirstDifferential_inr_snd_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G j ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h)) = CategoryTheory.CategoryStruct.comp (-zigzagBraidTensorEvaluationRight k G j i) h

The second-column second-row component of the signed evaluation matrix.

theorem TauCeti.zigzagBraidNormalFirstDifferential_comp_evaluations (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) (CategoryTheory.Limits.biprod.desc (zigzagBraidEvaluationHom k G i) (zigzagBraidEvaluationHom k G j)) = 0

The signed matrix is annihilated by the sum of the vertex evaluations.

theorem TauCeti.zigzagBraidNormalFirstDifferential_comp_evaluations_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBimodule k G ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc (zigzagBraidEvaluationHom k G i) (zigzagBraidEvaluationHom k G j)) h) = CategoryTheory.CategoryStruct.comp 0 h

The signed matrix is annihilated by the sum of the vertex evaluations.

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

The common three-term graded complex of ordered pair and vertex evaluations.

noncomputable def TauCeti.zigzagBraidNormalComplexXMinusTwoIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : (zigzagBraidNormalComplex k G i j).X (-2) ≅ GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ⊞ GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G i)

The degree-minus-two term is the sum of the two ordered vertex tensor products.

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

The degree-minus-one term is the sum of the two vertex bimodules.

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

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

theorem TauCeti.isZero_zigzagBraidNormalComplex_X (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {n : ℤ} (h₂ : n ≠ -2) (h₁ : n ≠ -1) (h₀ : n ≠ 0) : CategoryTheory.Limits.IsZero ((zigzagBraidNormalComplex k G i j).X n)

The common evaluation complex is supported in cohomological degrees -2, -1, and 0.

@[simp]

theorem TauCeti.zigzagBraidNormalComplex_d_minusTwo (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalComplex k G i j).d (-2) (-1)) (zigzagBraidNormalComplexXMinusOneIso k G i j).hom = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusTwoIso k G i j).hom (zigzagBraidNormalFirstDifferential k G i j)

The first differential is the signed pair-evaluation matrix.

theorem TauCeti.zigzagBraidNormalComplex_d_minusTwo_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalComplex k G i j).d (-2) (-1)) (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusOneIso k G i j).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusTwoIso k G i j).hom (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) h)

The first differential is the signed pair-evaluation matrix.

@[simp]

theorem TauCeti.zigzagBraidNormalComplex_d_minusOne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalComplex k G i j).d (-1) 0) (zigzagBraidNormalComplexXZeroIso k G i j).hom = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusOneIso k G i j).hom (CategoryTheory.Limits.biprod.desc (zigzagBraidEvaluationHom k G i) (zigzagBraidEvaluationHom k G j))

The last differential is the sum of the two vertex evaluations.

theorem TauCeti.zigzagBraidNormalComplex_d_minusOne_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBimodule k G ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalComplex k G i j).d (-1) 0) (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXZeroIso k G i j).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusOneIso k G i j).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc (zigzagBraidEvaluationHom k G i) (zigzagBraidEvaluationHom k G j)) h)

The last differential is the sum of the two vertex evaluations.

@[simp]

theorem TauCeti.zigzagBraidNormalComplex_d_eq_zero₀ (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {a : ℤ} (b : ℤ) (ha₂ : a ≠ -2) (ha₁ : a ≠ -1) : (zigzagBraidNormalComplex k G i j).d a b = 0

A differential with source outside the two nonzero differential degrees vanishes.

@[simp]

theorem TauCeti.zigzagBraidNormalComplex_d_eq_zero₁ (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (a : ℤ) {b : ℤ} (hb₁ : b ≠ -1) (hb₀ : b ≠ 0) : (zigzagBraidNormalComplex k G i j).d a b = 0

A differential with target outside the two nonzero differential degrees vanishes.

theorem TauCeti.zigzagBraidNormalFirstDifferential_swap (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G i))).hom (zigzagBraidNormalFirstDifferential k G j i) = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) (CategoryTheory.Limits.biprod.braiding (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)).hom

Swapping both pairs of summands preserves the signed evaluation matrix.

theorem TauCeti.zigzagBraidNormalFirstDifferential_swap_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G j ⊞ zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G i))).hom (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G j i) h) = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalFirstDifferential k G i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)).hom h)

Swapping both pairs of summands preserves the signed evaluation matrix.

noncomputable def TauCeti.zigzagBraidNormalSwapIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : zigzagBraidNormalComplex k G i j ≅ zigzagBraidNormalComplex k G j i

Exchange the ordered pair and vertex summands of the common evaluation complex.

@[simp]

theorem TauCeti.zigzagBraidNormalSwapIso_hom_f_minusTwo (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalSwapIso k G i j).hom.f (-2)) (zigzagBraidNormalComplexXMinusTwoIso k G j i).hom = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusTwoIso k G i j).hom (CategoryTheory.Limits.biprod.braiding (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G i))).hom

In degree minus two the swap exchanges the two ordered tensor-product summands.

theorem TauCeti.zigzagBraidNormalSwapIso_hom_f_minusTwo_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G i) ⊞ GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalSwapIso k G i j).hom.f (-2)) (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusTwoIso k G j i).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusTwoIso k G i j).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G i))).hom h)

In degree minus two the swap exchanges the two ordered tensor-product summands.

@[simp]

theorem TauCeti.zigzagBraidNormalSwapIso_hom_f_minusOne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalSwapIso k G i j).hom.f (-1)) (zigzagBraidNormalComplexXMinusOneIso k G j i).hom = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusOneIso k G i j).hom (CategoryTheory.Limits.biprod.braiding (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)).hom

In degree minus one the swap exchanges the two vertex summands.

theorem TauCeti.zigzagBraidNormalSwapIso_hom_f_minusOne_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBraidBimodule k G j ⊞ zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalSwapIso k G i j).hom.f (-1)) (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusOneIso k G j i).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXMinusOneIso 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 swap exchanges the two vertex summands.

@[simp]

theorem TauCeti.zigzagBraidNormalSwapIso_hom_f_zero (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalSwapIso k G i j).hom.f 0) (zigzagBraidNormalComplexXZeroIso k G j i).hom = (zigzagBraidNormalComplexXZeroIso k G i j).hom

The swap acts as the identity on the regular bimodule in degree zero.

theorem TauCeti.zigzagBraidNormalSwapIso_hom_f_zero_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBimodule k G ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidNormalSwapIso k G i j).hom.f 0) (CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXZeroIso k G j i).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBraidNormalComplexXZeroIso k G i j).hom h

The swap acts as the identity on the regular bimodule in degree zero.