Documentation

TauCeti.RepresentationTheory.Quiver.Zigzag.Braid.PairTerms

Terms of graded zigzag braid tensor products #

The actual signed tensor product of two braid complexes is supported in cohomological degrees −2, −1 and 0. These terms identify with the tensor of the vertex bimodules, the biproduct of the two vertex bimodules, and the regular bimodule. Unit identifications preserve internal grading and both outer actions.

The supported-inclusion equations compute the component maps. Under these identifications, the differential from degree −1 to 0 is the sum of the two evaluations. These formulas supply the pair terms used in commuting and triple braid calculations.

source
noncomputable def TauCeti.zigzagBraidComplexTensorXMinusTwoIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
(zigzagBraidComplexTensor k G i j).X (-2) ≅ ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j)

The degree-minus-two term of a braid tensor product is the tensor of the vertex bimodules.

Instances For
    source
    noncomputable def TauCeti.zigzagBraidComplexTensorXZeroIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
    (zigzagBraidComplexTensor k G i j).X 0 ≅ zigzagGradedBimodule k G

    The degree-zero term of the actual braid tensor product is the regular bimodule.

    Instances For
      source
      @[simp]
      theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTensorXZeroIso_hom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
      CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidComplex k G j) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 0 0 ιMapBifunctor_zigzagBraidComplexTensorXZeroIso_hom._proof_1) (zigzagBraidComplexTensorXZeroIso k G i j).hom = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map (zigzagBraidComplexXIso₁ k G i).hom).app ((zigzagBraidComplex k G j).X 0)) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).map (zigzagBraidComplexXIso₁ k G j).hom) (zigzagBimoduleLeftUnitor k G (zigzagGradedBimodule k G)).hom)

      The regular summand in degree zero evaluates through the two component unit maps.

      source
      @[simp]
      theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTensorXZeroIso_hom_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBimodule k G ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidComplex k G j) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 0 0 ιMapBifunctor_zigzagBraidComplexTensorXZeroIso_hom._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXZeroIso k G i j).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map (zigzagBraidComplexXIso₁ k G i).hom).app ((zigzagBraidComplex k G j).X 0)) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).map (zigzagBraidComplexXIso₁ k G j).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G (zigzagGradedBimodule k G)).hom h))

      The regular summand in degree zero evaluates through the two component unit maps.

      source
      noncomputable def TauCeti.zigzagBraidComplexTensorXMinusOneIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
      (zigzagBraidComplexTensor k G i j).X (-1) ≅ zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j

      The degree-minus-one term is the biproduct of the two actual vertex bimodules.

      Instances For
        source
        @[simp]
        theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTensorXMinusOneIso_hom_left (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
        CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidComplex k G j) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) 0 (-1) ιMapBifunctor_zigzagBraidComplexTensorXMinusOneIso_hom_left._proof_1) (zigzagBraidComplexTensorXMinusOneIso k G i j).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map (zigzagBraidComplexXIso₀ k G i).hom).app ((zigzagBraidComplex k G j).X 0)) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).map (zigzagBraidComplexXIso₁ k G j).hom) (zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i)).hom)) CategoryTheory.Limits.biprod.inl

        The (-1,0) summand identifies with the first vertex summand via the right unitor.

        source
        @[simp]
        theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTensorXMinusOneIso_hom_left_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j ⟶ Z) :
        CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidComplex k G j) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) 0 (-1) ιMapBifunctor_zigzagBraidComplexTensorXMinusOneIso_hom_left._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXMinusOneIso k G i j).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map (zigzagBraidComplexXIso₀ k G i).hom).app ((zigzagBraidComplex k G j).X 0)) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).map (zigzagBraidComplexXIso₁ k G j).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i)).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)))

        The (-1,0) summand identifies with the first vertex summand via the right unitor.

        source
        @[simp]
        theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTensorXMinusOneIso_hom_right (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
        CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidComplex k G j) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 (-1) (-1) ιMapBifunctor_zigzagBraidComplexTensorXMinusOneIso_hom_right._proof_1) (zigzagBraidComplexTensorXMinusOneIso k G i j).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map (zigzagBraidComplexXIso₁ k G i).hom).app ((zigzagBraidComplex k G j).X (-1))) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).map (zigzagBraidComplexXIso₀ k G j).hom) (zigzagBimoduleLeftUnitor k G (zigzagGradedBraidBimodule k G j)).hom)) CategoryTheory.Limits.biprod.inr

        The (0,-1) summand identifies with the second vertex summand via the left unitor.

        source
        @[simp]
        theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTensorXMinusOneIso_hom_right_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : zigzagGradedBraidBimodule k G i ⊞ zigzagGradedBraidBimodule k G j ⟶ Z) :
        CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidComplex k G j) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) 0 (-1) (-1) ιMapBifunctor_zigzagBraidComplexTensorXMinusOneIso_hom_right._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXMinusOneIso k G i j).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map (zigzagBraidComplexXIso₁ k G i).hom).app ((zigzagBraidComplex k G j).X (-1))) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).map (zigzagBraidComplexXIso₀ k G j).hom) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G (zigzagGradedBraidBimodule k G j)).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h)))

        The (0,-1) summand identifies with the second vertex summand via the left unitor.

        source
        theorem TauCeti.zigzagBraidComplexTensor_d (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
        CategoryTheory.CategoryStruct.comp ((zigzagBraidComplexTensor k G i j).d (-1) 0) (zigzagBraidComplexTensorXZeroIso k G i j).hom = CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXMinusOneIso k G i j).hom (CategoryTheory.Limits.biprod.desc (zigzagBraidEvaluationHom k G i) (zigzagBraidEvaluationHom k G j))

        Under the component identifications, the mixed differential is the pair of evaluations.

        source
        @[simp]
        theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTensorXMinusTwoIso_hom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
        CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidComplex k G j) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) (-1) (-2) ιMapBifunctor_zigzagBraidComplexTensorXMinusTwoIso_hom._proof_1) (zigzagBraidComplexTensorXMinusTwoIso k G i j).hom = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G j).X (-1))).map (zigzagBraidComplexXIso₀ k G i).hom) (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).map (zigzagBraidComplexXIso₀ k G j).hom)

        The lowest pair summand is identified by the two existing vertex component maps.

        source
        @[simp]
        theorem TauCeti.ιMapBifunctor_zigzagBraidComplexTensorXMinusTwoIso_hom_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : ((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).obj (zigzagGradedBraidBimodule k G j) ⟶ Z) :
        CategoryTheory.CategoryStruct.comp ((zigzagBraidComplex k G i).ιMapBifunctor (zigzagBraidComplex k G j) (GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)) (ComplexShape.up ℤ) (-1) (-1) (-2) ιMapBifunctor_zigzagBraidComplexTensorXMinusTwoIso_hom._proof_1) (CategoryTheory.CategoryStruct.comp (zigzagBraidComplexTensorXMinusTwoIso k G i j).hom h) = CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).flip.obj ((zigzagBraidComplex k G j).X (-1))).map (zigzagBraidComplexXIso₀ k G i).hom) (CategoryTheory.CategoryStruct.comp (((GradedModuleCat.bimoduleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).map (zigzagBraidComplexXIso₀ k G j).hom) h)

        The lowest pair summand is identified by the two existing vertex component maps.