Documentation

TauCeti.RepresentationTheory.Quiver.Zigzag.Braid.TensorEvaluation

Evaluation on tensor products of zigzag vertex bimodules #

Evaluate either factor of a balanced vertex tensor using its multiplication map and the appropriate unit identification. Both orders of evaluation agree as maps to the regular bimodule. These maps and their pure-tensor computations are used by the differential matrices of braid products.

source
noncomputable def TauCeti.zigzagBraidTensorEvaluationLeft (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ⟶ zigzagGradedBraidBimodule k G j

Evaluate the first vertex factor of a balanced tensor product.

Instances For
    source
    noncomputable def TauCeti.zigzagBraidTensorEvaluationRight (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
    GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ⟶ zigzagGradedBraidBimodule k G i

    Evaluate the second vertex factor of a balanced tensor product.

    Instances For
      source
      @[simp]
      theorem TauCeti.zigzagBraidTensorEvaluationLeft_tmul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (x : (zigzagGradedBraidBimodule k G i).carrier) (y : (zigzagGradedBraidBimodule k G j).carrier) :
      (zigzagBraidTensorEvaluationLeft k G i j).hom (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) x y) = (Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))).symm ((zigzagBraidEvaluationHom k G i).hom x) ⊗ₜ[k] 1 • y

      Left evaluation on a pure balanced tensor is the left action of its evaluated factor.

      source
      @[simp]
      theorem TauCeti.zigzagBraidTensorEvaluationRight_tmul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (x : (zigzagGradedBraidBimodule k G i).carrier) (y : (zigzagGradedBraidBimodule k G j).carrier) :
      (zigzagBraidTensorEvaluationRight k G i j).hom (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) x y) = 1 ⊗ₜ[k] MulOpposite.op ((Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))).symm ((zigzagBraidEvaluationHom k G j).hom y)) • x

      Right evaluation on a pure balanced tensor is the right action of its evaluated factor.

      source
      theorem TauCeti.zigzagBraidTensorEvaluationLeft_eq (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
      zigzagBraidTensorEvaluationLeft k G i j = CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidEvaluationHom k G i) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G j))) (zigzagBimoduleLeftUnitor k G (zigzagGradedBraidBimodule k G j)).hom

      Left evaluation is the tensor of evaluation with the identity, followed by the unitor.

      source
      theorem TauCeti.zigzagBraidTensorEvaluationLeft_eq_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 j ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (zigzagBraidTensorEvaluationLeft k G i j) h = CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagBraidEvaluationHom k G i) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G j))) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G (zigzagGradedBraidBimodule k G j)).hom h)

      Left evaluation is the tensor of evaluation with the identity, followed by the unitor.

      source
      theorem TauCeti.zigzagBraidTensorEvaluationRight_eq (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
      zigzagBraidTensorEvaluationRight k G i j = CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G i)) (zigzagBraidEvaluationHom k G j)) (zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i)).hom

      Right evaluation is the tensor of the identity with evaluation, followed by the unitor.

      source
      theorem TauCeti.zigzagBraidTensorEvaluationRight_eq_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 ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (zigzagBraidTensorEvaluationRight k G i j) h = CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (CategoryTheory.CategoryStruct.id (zigzagGradedBraidBimodule k G i)) (zigzagBraidEvaluationHom k G j)) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G (zigzagGradedBraidBimodule k G i)).hom h)

      Right evaluation is the tensor of the identity with evaluation, followed by the unitor.

      source
      theorem TauCeti.zigzagBraidTensorEvaluation_comm (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) :
      CategoryTheory.CategoryStruct.comp (zigzagBraidTensorEvaluationLeft k G i j) (zigzagBraidEvaluationHom k G j) = CategoryTheory.CategoryStruct.comp (zigzagBraidTensorEvaluationRight k G i j) (zigzagBraidEvaluationHom k G i)

      Both orders of factor evaluation give the same map to the regular bimodule.

      source
      theorem TauCeti.zigzagBraidTensorEvaluation_comm_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 (zigzagBraidTensorEvaluationLeft k G i j) (CategoryTheory.CategoryStruct.comp (zigzagBraidEvaluationHom k G j) h) = CategoryTheory.CategoryStruct.comp (zigzagBraidTensorEvaluationRight k G i j) (CategoryTheory.CategoryStruct.comp (zigzagBraidEvaluationHom k G i) h)

      Both orders of factor evaluation give the same map to the regular bimodule.