The graded self-tensor of a zigzag vertex bimodule

The middle factor in the balanced self-tensor of U_i = Z e_i ⊗[k] e_i Z is e_i Z e_i, with vertex and volume basis vectors in internal degrees zero and two. Extracting that factor identifies the carrier with two copies of U_i. The two insertions are enveloping-algebra linear and have the required degrees, so reflection of isomorphisms by the existing graded-module forgetful functor upgrades the carrier calculation to U_i ⊗[Z] U_i ≅ U_i ⊞ U_i{2}.

This is a prerequisite for the inverse braid homotopy equivalence. It does not construct that homotopy. The calculation includes isolated vertices.

References

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

noncomputable def TauCeti.zigzagBraidSelfTensorInl (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : zigzagGradedBraidBimodule k G i ⟶ GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G i)

Insert the vertex component of the middle diagonal corner into the self-tensor.

noncomputable def TauCeti.zigzagBraidSelfTensorInr (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagGradedBraidBimodule k G i).shiftObj 2 ⟶ GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G i)

Insert the volume component of the middle corner; its internal degree is two.

noncomputable def TauCeti.zigzagBraidSelfTensorIso (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G i) ≅ zigzagGradedBraidBimodule k G i ⊞ (zigzagGradedBraidBimodule k G i).shiftObj 2

The graded vertex-bimodule self-tensor splits into the vertex and volume summands.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorIso_inv (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidSelfTensorIso k G i).inv = CategoryTheory.Limits.biprod.desc (zigzagBraidSelfTensorInl k G i) (zigzagBraidSelfTensorInr k G i)

The inverse self-tensor isomorphism assembles the vertex and volume insertions.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInl_iso_hom (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorInl k G i) (zigzagBraidSelfTensorIso k G i).hom = CategoryTheory.Limits.biprod.inl

The forward self-tensor isomorphism sends the vertex insertion to the first summand.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInl_iso_hom_assoc (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⊞ (zigzagGradedBraidBimodule k G i).shiftObj 2 ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorInl k G i) (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorIso k G i).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h

The forward self-tensor isomorphism sends the vertex insertion to the first summand.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInr_iso_hom (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorInr k G i) (zigzagBraidSelfTensorIso k G i).hom = CategoryTheory.Limits.biprod.inr

The forward self-tensor isomorphism sends the volume insertion to the second summand.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInr_iso_hom_assoc (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⊞ (zigzagGradedBraidBimodule k G i).shiftObj 2 ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorInr k G i) (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorIso k G i).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h

The forward self-tensor isomorphism sends the volume insertion to the second summand.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInl_hom_factors (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (l : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) (r : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) : (zigzagBraidSelfTensorInl k G i).hom ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] r)) = GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G i) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] spanSingletonGenerator (MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)))) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ⊗ₜ[k] r))

The vertex insertion separates the two outer ideal factors by the vertex idempotent.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInr_hom_factors (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (l : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) (r : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) : (zigzagBraidSelfTensorInr k G i).hom ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] r)) = GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G i) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] spanSingletonGenerator (MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)))) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (((zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i)) • spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)) ⊗ₜ[k] r))

The volume insertion has the same outer factors and inserts the degree-two middle vector.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInl_evaluationRight (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorInl k G i) (zigzagBraidTensorEvaluationRight k G i i) = CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G i)

The degree-zero self-tensor insertion followed by right evaluation is the identity.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInl_evaluationRight_assoc (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorInl k G i) (CategoryTheory.CategoryStruct.comp (zigzagBraidTensorEvaluationRight k G i i) h) = h

The degree-zero self-tensor insertion followed by right evaluation is the identity.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInl_evaluationLeft (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorInl k G i) (zigzagBraidTensorEvaluationLeft k G i i) = CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G i)

The degree-zero self-tensor insertion followed by left evaluation is the identity.

@[simp]

theorem TauCeti.zigzagBraidSelfTensorInl_evaluationLeft_assoc (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorInl k G i) (CategoryTheory.CategoryStruct.comp (zigzagBraidTensorEvaluationLeft k G i i) h) = h

The degree-zero self-tensor insertion followed by left evaluation is the identity.