Tensor composition of zigzag braid bimodules and complexes

The internally graded balanced tensor bifunctor GradedModuleCat.bimoduleTensor of the zigzag algebra's internal grading composes the actual enveloping-algebra modules used in the zigzag braid complexes. Mathlib's cochain totalization supplies the cohomological signs; internal degrees add without a further sign.

The full tensor product of vertex braid bimodules vanishes at distinct nonadjacent vertices. This is the degree--2 vanishing needed for the commuting equivalence of braid complexes.

References

• R. S. Huerfano and M. Khovanov, A category for the adjoint representation.
• B. Keller, Deriving DG categories, Section 6.1.

@[reducible, inline]

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

The cochain tensor product of the existing two-term graded braid complexes.

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

A tensor summand vanishes if either braid-complex degree is outside {-1, 0}.

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

Every actual braid-complex tensor product is supported in degrees -2, -1, and 0.

theorem TauCeti.zigzagBraidBimodule_tmul_eq_zero_of_ne_of_not_adj {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {i j : V} (hij : i ≠ j) (hadj : ¬G.Adj i j) (m : (zigzagGradedBraidBimodule k G i).carrier) (n : (zigzagGradedBraidBimodule k G j).carrier) : GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) m n = 0

Every pure tensor of distinct nonadjacent vertex braid bimodules vanishes.

theorem TauCeti.subsingleton_zigzagGradedBraidBimodule_tensor_of_ne_of_not_adj {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {i j : V} (hij : i ≠ j) (hadj : ¬G.Adj i j) : Subsingleton (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j)).carrier

The full graded tensor product of distinct nonadjacent vertex braid bimodules vanishes.

theorem TauCeti.isZero_zigzagGradedBraidBimodule_tensor_of_ne_of_not_adj {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.Limits.IsZero (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j))

The full vertex-bimodule tensor is a zero object for distinct nonadjacent vertices.

theorem TauCeti.isZero_zigzagBraidComplexTensor_X_of_ne_of_not_adj {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {i j : V} (hij : i ≠ j) (hadj : ¬G.Adj i j) {d : ℤ} (h₀ : d ≠ -1) (h₁ : d ≠ 0) : CategoryTheory.Limits.IsZero ((zigzagBraidComplexTensor k G i j).X d)

The actual nonadjacent braid-complex product is supported in degrees -1 and 0.