Signed differentials of triple zigzag braid products

The actual left-associated totalization evaluates each of its three factors. The lowest differential has signs +,-,+, while the next differential evaluates one of each pair with the signs determined by its cohomological position. These are the differential blocks used in the adjacent braid cancellation.

noncomputable def TauCeti.zigzagBraidTripleFirstDifferential (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (zigzagGradedBraidBimodule k G l) ⟶ 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 i) (zigzagGradedBraidBimodule k G l) ⊞ GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G l)

The signed three-factor evaluation from the triple tensor to its three pair terms.

@[simp]

theorem TauCeti.zigzagBraidTripleFirstDifferential_fst (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidTripleFirstDifferential k G i j l) CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (CategoryTheory.CategoryStruct.id (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j))) (zigzagBraidEvaluationHom k G l)) (zigzagBimoduleRightUnitor k G (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j))).hom

Evaluating the third factor gives the first pair component.

theorem TauCeti.zigzagBraidTripleFirstDifferential_fst_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.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidTripleFirstDifferential k G i j l) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (CategoryTheory.CategoryStruct.id (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j))) (zigzagBraidEvaluationHom k G l)) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j))).hom h)

Evaluating the third factor gives the first pair component.

@[simp]

theorem TauCeti.zigzagBraidTripleFirstDifferential_snd_fst (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidTripleFirstDifferential k G i j l) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) = -GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidTensorEvaluationRight k G i j) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G l))

Evaluating the middle factor gives the negative of the second pair component.

theorem TauCeti.zigzagBraidTripleFirstDifferential_snd_fst_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.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G l) ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidTripleFirstDifferential k G i j l) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h)) = CategoryTheory.CategoryStruct.comp (-GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidTensorEvaluationRight k G i j) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G l))) h

Evaluating the middle factor gives the negative of the second pair component.

@[simp]

theorem TauCeti.zigzagBraidTripleFirstDifferential_snd_snd (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidTripleFirstDifferential k G i j l) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.snd) = GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidTensorEvaluationLeft k G i j) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G l))

Evaluating the first factor gives the third pair component.

theorem TauCeti.zigzagBraidTripleFirstDifferential_snd_snd_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.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G l) ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidTripleFirstDifferential k G i j l) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h)) = CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidTensorEvaluationLeft k G i j) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G l))) h

Evaluating the first factor gives the third pair component.

noncomputable def TauCeti.zigzagBraidTripleSecondDifferential (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : 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 i) (zigzagGradedBraidBimodule k G l) ⊞ GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G j) (zigzagGradedBraidBimodule k G l) ⟶ (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j) ⊞ zigzagGradedBraidBimodule k G l

The signed pair evaluations from three pair terms to three vertex terms.

@[simp]

theorem TauCeti.zigzagBraidTripleSecondDifferential_inl (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (zigzagBraidTripleSecondDifferential k G i j l) = CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift (-zigzagBraidTensorEvaluationRight k G i j) (zigzagBraidTensorEvaluationLeft k G i j)) 0

The first pair evaluates to the first two vertex components.

theorem TauCeti.zigzagBraidTripleSecondDifferential_inl_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 CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (zigzagBraidTripleSecondDifferential k G i j l) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift (-zigzagBraidTensorEvaluationRight k G i j) (zigzagBraidTensorEvaluationLeft k G i j)) 0) h

The first pair evaluates to the first two vertex components.

@[simp]

theorem TauCeti.zigzagBraidTripleSecondDifferential_inl_inr (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (zigzagBraidTripleSecondDifferential k G i j l)) = CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift (-zigzagBraidTensorEvaluationRight k G i l) 0) (zigzagBraidTensorEvaluationLeft k G i l)

The second pair evaluates to the first and third vertex components.

theorem TauCeti.zigzagBraidTripleSecondDifferential_inl_inr_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 CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (zigzagBraidTripleSecondDifferential k G i j l) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift (-zigzagBraidTensorEvaluationRight k G i l) 0) (zigzagBraidTensorEvaluationLeft k G i l)) h

The second pair evaluates to the first and third vertex components.

@[simp]

theorem TauCeti.zigzagBraidTripleSecondDifferential_inr_inr (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (zigzagBraidTripleSecondDifferential k G i j l)) = CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift 0 (-zigzagBraidTensorEvaluationRight k G j l)) (zigzagBraidTensorEvaluationLeft k G j l)

The third pair evaluates to the second and third vertex components.

theorem TauCeti.zigzagBraidTripleSecondDifferential_inr_inr_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 CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (zigzagBraidTripleSecondDifferential k G i j l) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift 0 (-zigzagBraidTensorEvaluationRight k G j l)) (zigzagBraidTensorEvaluationLeft k G j l)) h

The third pair evaluates to the second and third vertex components.

theorem TauCeti.zigzagBraidComplexTriple_d_minusThree (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplexTriple k G i j l).d (-3) (-2)) (zigzagBraidComplexTripleXMinusTwoIso k G i j l).hom = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusThreeIso k G i j l).hom (zigzagBraidTripleFirstDifferential k G i j l)

The lowest actual triple differential has the signed three-factor evaluation matrix.

theorem TauCeti.zigzagBraidComplexTriple_d_minusThree_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).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 ((zigzagBraidComplexTriple k G i j l).d (-3) (-2)) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusTwoIso k G i j l).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusThreeIso k G i j l).hom (CategoryTheory.CategoryStruct.comp (zigzagBraidTripleFirstDifferential k G i j l) h)

The lowest actual triple differential has the signed three-factor evaluation matrix.

theorem TauCeti.zigzagBraidComplexTriple_d_minusTwo (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplexTriple k G i j l).d (-2) (-1)) (zigzagBraidComplexTripleXMinusOneIso k G i j l).hom = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusTwoIso k G i j l).hom (zigzagBraidTripleSecondDifferential k G i j l)

The middle actual triple differential has the three signed pair-evaluation columns.

theorem TauCeti.zigzagBraidComplexTriple_d_minusTwo_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : (zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j) ⊞ zigzagGradedBraidBimodule k G l ⟶ Z) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplexTriple k G i j l).d (-2) (-1)) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusOneIso k G i j l).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusTwoIso k G i j l).hom (CategoryTheory.CategoryStruct.comp (zigzagBraidTripleSecondDifferential k G i j l) h)

The middle actual triple differential has the three signed pair-evaluation columns.

theorem TauCeti.zigzagBraidComplexTriple_d_minusOne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j l : V) : CategoryTheory.CategoryStruct.comp ((zigzagBraidComplexTriple k G i j l).d (-1) 0) (zigzagBraidComplexTripleXZeroIso k G i j l).hom = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTripleXMinusOneIso k G i j l).hom (CategoryTheory.Limits.biprod.desc (CategoryTheory.Limits.biprod.desc (zigzagBraidEvaluationHom k G i) (zigzagBraidEvaluationHom k G j)) (zigzagBraidEvaluationHom k G l))

The final actual triple differential is the sum of the three vertex evaluations.

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

The final actual triple differential is the sum of the three vertex evaluations.