The braid complexes of a zigzag algebra

Let Z be the zigzag algebra TauCeti.zigzagAlgebra of a finite simple graph, with vertex idempotents e_i, arrows a_d and volume classes x_i, the vectors of the basis TauCeti.zigzagAlgebraBasis. A Z-bimodule is a left module over the enveloping algebra Z ⊗[k] Zᵐᵒᵖ, x ⊗ y acting by m ↦ x m y; Z itself is the bimodule TauCeti.Bimodule (AlgHom.id k Z). For a vertex i, the bimodule P_i ⊗_k e_i Z, where P_i = Z e_i, is the cyclic left ideal of Z ⊗[k] Zᵐᵒᵖ generated by the idempotent e_i ⊗ e_i.

Khovanov and Seidel attach to i two two-term complexes of Z-bimodules:

B_i  = [P_i ⊗_k e_i Z ⟶ Z],         x e_i ⊗ e_i y ↦ x e_i y,
B_i' = [Z ⟶ P_i ⊗_k e_i Z],         1 ↦ e_i ⊗ x_i + x_i ⊗ e_i + ∑_{d.fst = i} a_d ⊗ a_{d.symm}.

The first is in cohomological degrees -1, 0 and its differential is multiplication, of internal degree 0. The second is in cohomological degrees 0, 1; its differential, the coevaluation, raises internal degree by 2, so with internal grading it is the map Z → (P_i ⊗_k e_i Z){-2}. Both complexes live in the category TauCeti.GradedModuleCat of graded modules over the enveloping algebra, graded by TauCeti.zigzagEnvelopingGrading: their terms are graded bimodules, the shift M{d}_p = M_{p-d} is TauCeti.GradedModuleCat.shiftFunctor, and their differentials are morphisms of graded bimodules, that is, bimodule maps of internal degree 0. Tensoring with these complexes is how Khovanov--Seidel and Huerfano--Khovanov let the braid group of the graph act on the homotopy category of graded Z-modules; this file constructs the complexes and their gradings, not the braid relations.

Everything is stated for the public componentwise algebra, so it covers every vertex of every finite simple graph. At an isolated vertex i the factor of Z is the dual numbers, there is no dart at i, and the coevaluation is 1 ↦ e_i ⊗ x_i + x_i ⊗ e_i, with x_i the infinitesimal generator.

The coevaluation is a map of bimodules because its value at 1 is the image of the Casimir element TauCeti.zigzagCasimir, ∑_b b ⊗ b^∨ for the symmetric Frobenius trace TauCeti.zigzagAlgebraTrace, under u ↦ u (e_i ⊗ e_i), with b running over the vertex, arrow and volume basis and b^∨ over its dual basis, and the Casimir element commutes with the algebra (TauCeti.tmul_one_mul_zigzagCasimir).

Main definitions

• TauCeti.zigzagBraidBimodule: the bimodule P_i ⊗_k e_i Z.
• TauCeti.zigzagBraidEvaluation: the multiplication map P_i ⊗_k e_i Z → Z.
• TauCeti.zigzagBraidCoevaluation: the coevaluation Z → P_i ⊗_k e_i Z.
• TauCeti.zigzagEnvelopingGrading: the internal grading of Z ⊗[k] Zᵐᵒᵖ.
• TauCeti.zigzagBimoduleGrade, TauCeti.zigzagBraidBimoduleGrade: the internal gradings of the bimodules Z and P_i ⊗_k e_i Z.
• TauCeti.zigzagGradedBimodule, TauCeti.zigzagGradedBraidBimodule: Z and P_i ⊗_k e_i Z as graded bimodules, objects of TauCeti.GradedModuleCat.
• TauCeti.zigzagBraidEvaluationHom, TauCeti.zigzagBraidCoevaluationHom: the evaluation P_i ⊗_k e_i Z ⟶ Z and the coevaluation Z ⟶ (P_i ⊗_k e_i Z){-2} as morphisms of graded bimodules.
• TauCeti.zigzagBraidComplex, TauCeti.zigzagBraidInverseComplex: the complexes B_i and B_i' of graded bimodules.

Main results

• TauCeti.zigzagBraidComplex_d, TauCeti.zigzagBraidInverseComplex_d: the differentials of B_i and B_i' are the evaluation and the coevaluation.
• TauCeti.isInternal_zigzagBimoduleGrade, TauCeti.isInternal_zigzagBraidBimoduleGrade: the gradings of Z and of P_i ⊗_k e_i Z are internal direct sums.
• TauCeti.mul_mem_zigzagEnvelopingGrading, TauCeti.smul_mem_zigzagBimoduleGrade, TauCeti.smul_mem_zigzagBraidBimoduleGrade: the enveloping algebra is graded, and acts on both bimodules compatibly with the gradings.
• TauCeti.coe_zigzagBraidCoevaluation_of: the explicit formula for the coevaluation.
• TauCeti.isHomogeneous_zigzagBraidEvaluation: the evaluation is a degree-0 map P_i ⊗_k e_i Z → Z.
• TauCeti.isHomogeneous_zigzagBraidCoevaluation: the coevaluation has internal degree 2, so it is a degree-0 map Z → (P_i ⊗_k e_i Z){-2}.

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).

The bimodule P_i ⊗_k e_i Z and the evaluation

noncomputable def TauCeti.zigzagBraidBimodule (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Ideal (TensorProduct k (↑(zigzagAlgebra k G)) (↑(zigzagAlgebra k G))ᵐᵒᵖ)

The bimodule P_i ⊗_k e_i Z, the first term of the braid complex at i: the cyclic left ideal of the enveloping algebra Z ⊗[k] Zᵐᵒᵖ generated by the idempotent e_i ⊗ e_i. Its elements are the sums of the x e_i ⊗ e_i y.

theorem TauCeti.mem_zigzagBraidBimodule_iff {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {i : V} {u : TensorProduct k (↑(zigzagAlgebra k G)) (↑(zigzagAlgebra k G))ᵐᵒᵖ} : u ∈ zigzagBraidBimodule k G i ↔ u * (zigzagAlgebraBasis k G) (Sum.inl i) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inl i)) = u

An element lies in P_i ⊗_k e_i Z exactly when it is fixed by right multiplication by the idempotent e_i ⊗ e_i.

theorem TauCeti.tmul_mem_zigzagBraidBimodule {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) (x y : ↑(zigzagAlgebra k G)) : (x * (zigzagAlgebraBasis k G) (Sum.inl i)) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inl i) * y) ∈ zigzagBraidBimodule k G i

The pure tensor x e_i ⊗ e_i y lies in P_i ⊗_k e_i Z.

noncomputable def TauCeti.zigzagBraidEvaluation (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : ↥(zigzagBraidBimodule k G i) →ₗ[TensorProduct k (↑(zigzagAlgebra k G)) (↑(zigzagAlgebra k G))ᵐᵒᵖ] Bimodule (AlgHom.id k ↑(zigzagAlgebra k G))

The evaluation P_i ⊗_k e_i Z → Z, the differential of the braid complex at i: the map of bimodules x e_i ⊗ e_i y ↦ x e_i y, the restriction of the action of the enveloping algebra on 1.

theorem TauCeti.zigzagBraidEvaluation_apply {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {i : V} (u : ↥(zigzagBraidBimodule k G i)) : (zigzagBraidEvaluation k G i) u = ↑u • (Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))) 1

The evaluation acts on P_i ⊗_k e_i Z as the enveloping algebra acts on 1.

theorem TauCeti.zigzagBraidEvaluation_tmul {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) (x y : ↑(zigzagAlgebra k G)) : (zigzagBraidEvaluation k G i) ⟨(x * (zigzagAlgebraBasis k G) (Sum.inl i)) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inl i) * y), ⋯⟩ = (Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))) (x * (zigzagAlgebraBasis k G) (Sum.inl i) * y)

The evaluation is multiplication: x e_i ⊗ e_i y ↦ x e_i y.

The coevaluation

theorem TauCeti.zigzagCasimir_mul_mem_zigzagBraidBimodule {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : zigzagCasimir k G * (zigzagAlgebraBasis k G) (Sum.inl i) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inl i)) ∈ zigzagBraidBimodule k G i

The Casimir element cut down at i lies in P_i ⊗_k e_i Z.

noncomputable def TauCeti.zigzagBraidCoevaluation (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Bimodule (AlgHom.id k ↑(zigzagAlgebra k G)) →ₗ[TensorProduct k (↑(zigzagAlgebra k G)) (↑(zigzagAlgebra k G))ᵐᵒᵖ] ↥(zigzagBraidBimodule k G i)

The coevaluation Z → P_i ⊗_k e_i Z, the differential of the inverse braid complex at i: the map of bimodules sending 1 to the Casimir element cut down at i, e_i ⊗ x_i + x_i ⊗ e_i + ∑_{d.fst = i} a_d ⊗ a_{d.symm}.

theorem TauCeti.zigzagCasimir_mul_tmul_zigzagAlgebraBasis_inl {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] [DecidableEq V] (i : V) : zigzagCasimir k G * (zigzagAlgebraBasis k G) (Sum.inl i) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inl i)) = (zigzagAlgebraBasis k G) (Sum.inl i) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i))) + (zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i)) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inl i)) + ∑ d : G.Dart with d.toProd.1 = i, (zigzagAlgebraBasis k G) (Sum.inr (Sum.inl d)) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inr (Sum.inl d.symm)))

The Casimir element cut down at a vertex: C (e_i ⊗ e_i) = e_i ⊗ x_i + x_i ⊗ e_i + ∑_{d.fst = i} a_d ⊗ a_{d.symm}.

theorem TauCeti.coe_zigzagBraidCoevaluation_of {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] [DecidableEq V] (i : V) (x : ↑(zigzagAlgebra k G)) : ↑((zigzagBraidCoevaluation k G i) ((Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))) x)) = (x * (zigzagAlgebraBasis k G) (Sum.inl i)) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i))) + (x * (zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i))) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inl i)) + ∑ d : G.Dart with d.toProd.1 = i, (x * (zigzagAlgebraBasis k G) (Sum.inr (Sum.inl d))) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inr (Sum.inl d.symm)))

The coevaluation sends x to x times the Casimir element cut down at i.

theorem TauCeti.coe_zigzagBraidCoevaluation_of_one {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] [DecidableEq V] (i : V) : ↑((zigzagBraidCoevaluation k G i) ((Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))) 1)) = (zigzagAlgebraBasis k G) (Sum.inl i) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i))) + (zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i)) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inl i)) + ∑ d : G.Dart with d.toProd.1 = i, (zigzagAlgebraBasis k G) (Sum.inr (Sum.inl d)) ⊗ₜ[k] MulOpposite.op ((zigzagAlgebraBasis k G) (Sum.inr (Sum.inl d.symm)))

The coevaluation sends 1 to e_i ⊗ x_i + x_i ⊗ e_i + ∑_{d.fst = i} a_d ⊗ a_{d.symm}.

Internal degrees

@[reducible, inline]

noncomputable abbrev TauCeti.zigzagEnvelopingGrading (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : InternalGrading k (TensorProduct k (↑(zigzagAlgebra k G)) (↑(zigzagAlgebra k G))ᵐᵒᵖ) ℤ

The internal grading of the enveloping algebra Z ⊗[k] Zᵐᵒᵖ: the tensor product of the signed path-length grading of Z with its transport to Zᵐᵒᵖ, so that x ⊗ op y has degree deg x + deg y.

noncomputable def TauCeti.zigzagBimoduleGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : ℤ) : Submodule k (Bimodule (AlgHom.id k ↑(zigzagAlgebra k G)))

The internal grading of the bimodule Z: its degree-d piece is the signed degree-d piece of Z.

noncomputable def TauCeti.zigzagBraidBimoduleGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (d : ℤ) : Submodule k ↥(zigzagBraidBimodule k G i)

The internal grading of the bimodule P_i ⊗_k e_i Z, induced from the grading of the enveloping algebra.

@[simp]

theorem TauCeti.mem_zigzagBimoduleGrade_iff {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {d : ℤ} {x : Bimodule (AlgHom.id k ↑(zigzagAlgebra k G))} : x ∈ zigzagBimoduleGrade k G d ↔ (Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))).symm x ∈ zigzagAlgebraIntegerGrade k G d

@[simp]

theorem TauCeti.mem_zigzagBraidBimoduleGrade_iff {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {i : V} {d : ℤ} {u : ↥(zigzagBraidBimodule k G i)} : u ∈ zigzagBraidBimoduleGrade k G i d ↔ ↑u ∈ (zigzagEnvelopingGrading k G).piece ℤ d

theorem TauCeti.tmul_mem_zigzagEnvelopingGrading {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {p q : ℤ} {x y : ↑(zigzagAlgebra k G)} (hx : x ∈ zigzagAlgebraIntegerGrade k G p) (hy : y ∈ zigzagAlgebraIntegerGrade k G q) : x ⊗ₜ[k] MulOpposite.op y ∈ (zigzagEnvelopingGrading k G).piece ℤ (p + q)

A pure tensor of homogeneous elements is homogeneous of the total degree.

theorem TauCeti.mul_mem_zigzagEnvelopingGrading {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {m n : ℤ} {u v : TensorProduct k (↑(zigzagAlgebra k G)) (↑(zigzagAlgebra k G))ᵐᵒᵖ} (hu : u ∈ (zigzagEnvelopingGrading k G).piece ℤ m) (hv : v ∈ (zigzagEnvelopingGrading k G).piece ℤ n) : u * v ∈ (zigzagEnvelopingGrading k G).piece ℤ (m + n)

Multiplication adds degrees in the enveloping algebra: left multiplication by an element of degree m is the image of tensor products of left multiplications, each homogeneous.

theorem TauCeti.smul_mem_zigzagBimoduleGrade {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {m n : ℤ} {u : TensorProduct k (↑(zigzagAlgebra k G)) (↑(zigzagAlgebra k G))ᵐᵒᵖ} {z : Bimodule (AlgHom.id k ↑(zigzagAlgebra k G))} (hu : u ∈ (zigzagEnvelopingGrading k G).piece ℤ m) (hz : z ∈ zigzagBimoduleGrade k G n) : u • z ∈ zigzagBimoduleGrade k G (m + n)

The enveloping algebra acts on the bimodule Z compatibly with the gradings: x ⊗ op y sends z to x z y, whose degree is the sum of the three.

theorem TauCeti.smul_mem_zigzagBraidBimoduleGrade {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {i : V} {m n : ℤ} {u : TensorProduct k (↑(zigzagAlgebra k G)) (↑(zigzagAlgebra k G))ᵐᵒᵖ} {v : ↥(zigzagBraidBimodule k G i)} (hu : u ∈ (zigzagEnvelopingGrading k G).piece ℤ m) (hv : v ∈ zigzagBraidBimoduleGrade k G i n) : u • v ∈ zigzagBraidBimoduleGrade k G i (m + n)

The enveloping algebra acts on P_i ⊗_k e_i Z compatibly with the gradings.

theorem TauCeti.isInternal_zigzagBimoduleGrade {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] : DirectSum.IsInternal (zigzagBimoduleGrade k G)

The internal grading of the bimodule Z is an internal direct sum: it is the transport of the grading of Z along TauCeti.Bimodule.of.

theorem TauCeti.isHomogeneous_zigzagBraidBimodule {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : DirectSum.SetLike.IsHomogeneous ((zigzagEnvelopingGrading k G).piece ℤ) (Submodule.restrictScalars k (zigzagBraidBimodule k G i))

P_i ⊗_k e_i Z is a homogeneous k-submodule of the enveloping algebra: it is the image of right multiplication by the degree-0 idempotent e_i ⊗ e_i.

theorem TauCeti.isInternal_zigzagBraidBimoduleGrade {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : DirectSum.IsInternal (zigzagBraidBimoduleGrade k G i)

The internal grading of P_i ⊗_k e_i Z is an internal direct sum, the grading of a homogeneous submodule of the enveloping algebra.

theorem TauCeti.isHomogeneous_zigzagBraidEvaluation {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : LinearMap.IsHomogeneous (zigzagBraidEvaluation k G i) (zigzagBraidBimoduleGrade k G i) (zigzagBimoduleGrade k G) 0

The evaluation has internal degree 0: it is a degree-0 map P_i ⊗_k e_i Z → Z of graded bimodules.

theorem TauCeti.isHomogeneous_zigzagBraidCoevaluation {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : LinearMap.IsHomogeneous (zigzagBraidCoevaluation k G i) (zigzagBimoduleGrade k G) (zigzagBraidBimoduleGrade k G i) 2

The coevaluation has internal degree 2: it raises the internal degree by 2.

The graded bimodules and the two braid complexes

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

The graded bimodule Z: the bimodule Z with its signed path-length grading, a graded module over the enveloping algebra.

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

The graded bimodule P_i ⊗_k e_i Z, with the grading induced from the enveloping algebra, with no internal shift.

noncomputable def TauCeti.zigzagBraidEvaluationHom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagGradedBraidBimodule k G i ⟶ zigzagGradedBimodule k G

The evaluation as a degree-0 morphism P_i ⊗_k e_i Z ⟶ Z of graded bimodules.

noncomputable def TauCeti.zigzagBraidCoevaluationHom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagGradedBimodule k G ⟶ (GradedModuleCat.shiftFunctor (-2)).obj (zigzagGradedBraidBimodule k G i)

The coevaluation as a degree-0 morphism Z ⟶ (P_i ⊗_k e_i Z){-2} of graded bimodules, M{d} being the shift GradedModuleCat.shiftFunctor d with M{d}_p = M_{p-d}.

@[simp]

theorem TauCeti.hom_zigzagBraidEvaluationHom {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : (zigzagBraidEvaluationHom k G i).hom = zigzagBraidEvaluation k G i

@[simp]

theorem TauCeti.hom_zigzagBraidCoevaluationHom {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : (zigzagBraidCoevaluationHom k G i).hom = zigzagBraidCoevaluation k G i

noncomputable def TauCeti.zigzagBraidComplex (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : HomologicalComplex (GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) (ComplexShape.up ℤ)

The braid complex B_i = [P_i ⊗_k e_i Z ⟶ Z] of graded Z-bimodules, in cohomological degrees -1 and 0, with the degree-0 evaluation as differential. Its terms and differential are described by TauCeti.zigzagBraidComplexXIso₀, TauCeti.zigzagBraidComplexXIso₁, TauCeti.zigzagBraidComplex_d and TauCeti.isZero_zigzagBraidComplex_X.

noncomputable def TauCeti.zigzagBraidInverseComplex (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : HomologicalComplex (GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) (ComplexShape.up ℤ)

The inverse braid complex B_i' = [Z ⟶ (P_i ⊗_k e_i Z){-2}] of graded Z-bimodules, in cohomological degrees 0 and 1, with the degree-0 coevaluation as differential. Its terms and differential are described by TauCeti.zigzagBraidInverseComplexXIso₀, TauCeti.zigzagBraidInverseComplexXIso₁, TauCeti.zigzagBraidInverseComplex_d and TauCeti.isZero_zigzagBraidInverseComplex_X.

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

The term of B_i in cohomological degree -1 is P_i ⊗_k e_i Z.

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

The term of B_i in cohomological degree 0 is Z.

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

The term of B_i' in cohomological degree 0 is Z.

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

The term of B_i' in cohomological degree 1 is (P_i ⊗_k e_i Z){-2}.

@[simp]

theorem TauCeti.zigzagBraidComplex_d {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : (zigzagBraidComplex k G i).d (-1) 0 = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexXIso₀ k G i).hom (CategoryTheory.CategoryStruct.comp (zigzagBraidEvaluationHom k G i) (zigzagBraidComplexXIso₁ k G i).inv)

The differential of B_i is the evaluation.

@[simp]

theorem TauCeti.zigzagBraidComplex_d_eq_zero₀ {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) {a : ℤ} (b : ℤ) (ha : a ≠ -1) : (zigzagBraidComplex k G i).d a b = 0

The differential of B_i vanishes out of every degree other than -1.

@[simp]

theorem TauCeti.zigzagBraidComplex_d_eq_zero₁ {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) (a : ℤ) {b : ℤ} (hb : b ≠ 0) : (zigzagBraidComplex k G i).d a b = 0

The differential of B_i vanishes into every degree other than 0.

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

B_i vanishes outside cohomological degrees -1 and 0.

@[simp]

theorem TauCeti.zigzagBraidInverseComplex_d {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : (zigzagBraidInverseComplex k G i).d 0 1 = CategoryTheory.CategoryStruct.comp (zigzagBraidInverseComplexXIso₀ k G i).hom (CategoryTheory.CategoryStruct.comp (zigzagBraidCoevaluationHom k G i) (zigzagBraidInverseComplexXIso₁ k G i).inv)

The differential of B_i' is the coevaluation.

@[simp]

theorem TauCeti.zigzagBraidInverseComplex_d_eq_zero₀ {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) {a : ℤ} (b : ℤ) (ha : a ≠ 0) : (zigzagBraidInverseComplex k G i).d a b = 0

The differential of B_i' vanishes out of every degree other than 0.

@[simp]

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

The differential of B_i' vanishes into every degree other than 1.

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

B_i' vanishes outside cohomological degrees 0 and 1.