Shifted self-tensor maps for graded inverse braid complexes

The diagonal corner has a vertex and a volume summand. After internal shift by −2, these give Ui{−2} ⊞ Ui in either tensor order. Evaluation on the vertex insertion and coevaluation followed by the volume projection give identity blocks. These maps are the graded input to cancellation of the actual three-term inverse products. The proofs use a cyclic generator of Ui, balanced tensor composition and the diagonal corner calculation; no adjacency or nonzero coefficient hypothesis is needed.

noncomputable def TauCeti.zigzagBraidSelfTensorShiftRightIso (k : Type w) [CommRing k] {V : Type u} (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).shiftObj (-2)) ≅ (zigzagGradedBraidBimodule k G i).shiftObj (-2) ⊞ zigzagGradedBraidBimodule k G i

The internally shifted right self-tensor decomposes as Ui{−2} ⊞ Ui.

theorem TauCeti.zigzagBraidSelfTensorShiftRightIso_snd_tmul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (m n : (zigzagGradedBraidBimodule k G i).carrier) : (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftRightIso k G i).hom CategoryTheory.Limits.biprod.snd).hom (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) ((zigzagGradedBraidBimodule k G i).shiftObj (-2)) m n) = (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorIso k G i).hom CategoryTheory.Limits.biprod.snd).hom (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G i) m n)

The right shifted volume projection agrees with the unshifted self-tensor projection.

noncomputable def TauCeti.zigzagBraidSelfTensorShiftRightInl (k : Type w) [CommRing k] {V : Type u} (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).shiftObj (-2))

The shifted degree-zero insertion into Ui tensor_Z Ui{−2}.

theorem TauCeti.zigzagBraidSelfTensorShiftRightInl_evaluation (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftRightInl k G i) (CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidEvaluationHom k G i) (CategoryTheory.CategoryStruct.id ((zigzagGradedBraidBimodule k G i).shiftObj (-2)))) (zigzagBimoduleLeftUnitor k G ((zigzagGradedBraidBimodule k G i).shiftObj (-2))).hom) = CategoryTheory.CategoryStruct.id ((zigzagGradedBraidBimodule k G i).shiftObj (-2))

Left evaluation on the shifted right insertion is the identity.

theorem TauCeti.zigzagBraidSelfTensorShiftRightInl_evaluation_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : (zigzagGradedBraidBimodule k G i).shiftObj (-2) ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftRightInl k G i) (CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidEvaluationHom k G i) (CategoryTheory.CategoryStruct.id ((zigzagGradedBraidBimodule k G i).shiftObj (-2)))) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G ((zigzagGradedBraidBimodule k G i).shiftObj (-2))).hom h)) = h

Left evaluation on the shifted right insertion is the identity.

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

The internally shifted left self-tensor decomposes as Ui{−2} ⊞ Ui.

theorem TauCeti.zigzagBraidSelfTensorShiftLeftIso_snd_tmul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (m n : (zigzagGradedBraidBimodule k G i).carrier) : (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftLeftIso k G i).hom CategoryTheory.Limits.biprod.snd).hom (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) ((zigzagGradedBraidBimodule k G i).shiftObj (-2)) (zigzagGradedBraidBimodule k G i) m n) = (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorIso k G i).hom CategoryTheory.Limits.biprod.snd).hom (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G i) m n)

The left shifted volume projection agrees with the unshifted self-tensor projection.

noncomputable def TauCeti.zigzagBraidSelfTensorShiftLeftInl (k : Type w) [CommRing k] {V : Type u} (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).shiftObj (-2)) (zigzagGradedBraidBimodule k G i)

The shifted degree-zero insertion into Ui{−2} tensor_Z Ui.

theorem TauCeti.zigzagBraidSelfTensorShiftLeftInl_evaluation (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftLeftInl k G i) (CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (CategoryTheory.CategoryStruct.id ((zigzagGradedBraidBimodule k G i).shiftObj (-2))) (zigzagBraidEvaluationHom k G i)) (zigzagBimoduleRightUnitor k G ((zigzagGradedBraidBimodule k G i).shiftObj (-2))).hom) = CategoryTheory.CategoryStruct.id ((zigzagGradedBraidBimodule k G i).shiftObj (-2))

Right evaluation on the shifted left insertion is the identity.

theorem TauCeti.zigzagBraidSelfTensorShiftLeftInl_evaluation_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (h : (zigzagGradedBraidBimodule k G i).shiftObj (-2) ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftLeftInl k G i) (CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (CategoryTheory.CategoryStruct.id ((zigzagGradedBraidBimodule k G i).shiftObj (-2))) (zigzagBraidEvaluationHom k G i)) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G ((zigzagGradedBraidBimodule k G i).shiftObj (-2))).hom h)) = h

Right evaluation on the shifted left insertion is the identity.

theorem TauCeti.zigzagBraidSelfTensorShiftRightIso_coevaluation_snd (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).map (zigzagBraidCoevaluationHom k G i)) (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftRightIso k G i).hom CategoryTheory.Limits.biprod.snd) = (zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i)).hom

Coevaluation followed by the right volume projection is the right unitor.

theorem TauCeti.zigzagBraidSelfTensorShiftRightIso_coevaluation_snd_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).map (zigzagBraidCoevaluationHom k G i)) (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftRightIso k G i).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h)) = CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i)).hom h

Coevaluation followed by the right volume projection is the right unitor.

theorem TauCeti.zigzagBraidSelfTensorShiftRightIso_inl_inv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (zigzagBraidSelfTensorShiftRightIso k G i).inv = zigzagBraidSelfTensorShiftRightInl k G i

The first summand of the right shifted decomposition is the shifted insertion.

theorem TauCeti.zigzagBraidSelfTensorShiftRightIso_inl_inv_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : 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 i).shiftObj (-2)) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftRightIso k G i).inv h) = CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftRightInl k G i) h

The first summand of the right shifted decomposition is the shifted insertion.

theorem TauCeti.zigzagBraidSelfTensorShiftLeftIso_coevaluation_snd (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidCoevaluationHom k G i) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G i))) (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftLeftIso k G i).hom CategoryTheory.Limits.biprod.snd) = (zigzagBimoduleLeftUnitor k G (zigzagGradedBraidBimodule k G i)).hom

Coevaluation followed by the left volume projection is the left unitor.

theorem TauCeti.zigzagBraidSelfTensorShiftLeftIso_coevaluation_snd_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⟶ Z) : CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidCoevaluationHom k G i) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G i))) (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftLeftIso k G i).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h)) = CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G (zigzagGradedBraidBimodule k G i)).hom h

Coevaluation followed by the left volume projection is the left unitor.

theorem TauCeti.zigzagBraidSelfTensorShiftLeftIso_inl_inv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (zigzagBraidSelfTensorShiftLeftIso k G i).inv = zigzagBraidSelfTensorShiftLeftInl k G i

The first summand of the left shifted decomposition is the shifted insertion.

theorem TauCeti.zigzagBraidSelfTensorShiftLeftIso_inl_inv_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : 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).shiftObj (-2)) (zigzagGradedBraidBimodule k G i) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftLeftIso k G i).inv h) = CategoryTheory.CategoryStruct.comp (zigzagBraidSelfTensorShiftLeftInl k G i) h

The first summand of the left shifted decomposition is the shifted insertion.