Documentation

Atlas.TensorCategories.code.ModuleRigidityCompat

source
class CategoryTheory.ExactModuleCategory.ModuleEvalCoeval (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [LeftRigidCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] :
Type (max u₁ v₁)

Data of evaluation and coevaluation morphisms compatible with a module action on M, together with the zigzag identities relating them to the module structure on M.

Instances
    source
    theorem CategoryTheory.ExactModuleCategory.actWhiskerLeft_comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [ExactModuleCategory C M] (X : C) {N₁ N₂ N₃ : M} (f : N₁ ⟶ N₂) (g : N₂ ⟶ N₃) :
    LeftModuleCategoryStruct.actWhiskerLeft X (CategoryStruct.comp f g) = CategoryStruct.comp (LeftModuleCategoryStruct.actWhiskerLeft X f) (LeftModuleCategoryStruct.actWhiskerLeft X g)

    Left whiskering of a module action distributes over composition of morphisms in M.

    source
    @[reducible, inline]
    abbrev CategoryTheory.ExactModuleCategory.ev {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [LeftRigidCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [ExactModuleCategory C M] [hMEC : ModuleEvalCoeval C M] (P : C) :
    MonoidalCategoryStruct.tensorObj (ᘁP) P ⟶ MonoidalCategoryStruct.tensorUnit C

    Shorthand for the evaluation morphism (ᘁP) ⊗ P ⟶ 𝟙_ C supplied by ModuleEvalCoeval.

    Instances For
      source
      @[reducible, inline]
      abbrev CategoryTheory.ExactModuleCategory.coev {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [LeftRigidCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [ExactModuleCategory C M] [hMEC : ModuleEvalCoeval C M] (P : C) :
      MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorObj P ᘁP

      Shorthand for the coevaluation morphism 𝟙_ C ⟶ P ⊗ (ᘁP) supplied by ModuleEvalCoeval.

      Instances For
        source
        @[implicit_reducible]
        noncomputable instance CategoryTheory.ExactModuleCategory.ofEvalCoeval {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [LeftRigidCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [ExactModuleCategory C M] [hMEC : ModuleEvalCoeval C M] :
        ModuleRigidityCompat C M

        A ModuleEvalCoeval structure on (C, M) produces a ModuleRigidityCompat instance, using the supplied evaluation/coevaluation and zigzag identities.

        source
        theorem CategoryTheory.ExactModuleCategory.braided_zigzag_left (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] [LeftRigidCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] (P : C) (N A : M) (g : LeftModuleCategoryStruct.actObj (ᘁP) A ⟶ N) :
        CategoryStruct.comp (LeftModuleCategoryStruct.actWhiskerLeft (ᘁP) (CategoryStruct.comp (LeftModuleCategoryStruct.actLeftUnitor A).inv (CategoryStruct.comp (LeftModuleCategoryStruct.actWhiskerRight (CategoryStruct.comp (η_ (ᘁP) P) (β_ P ᘁP).inv) A) (CategoryStruct.comp (LeftModuleCategoryStruct.actAssociator P (ᘁP) A).hom (LeftModuleCategoryStruct.actWhiskerLeft P g))))) (CategoryStruct.comp (LeftModuleCategoryStruct.actAssociator (ᘁP) P N).inv (CategoryStruct.comp (LeftModuleCategoryStruct.actWhiskerRight (CategoryStruct.comp (β_ (ᘁP) P).hom (ε_ (ᘁP) P)) N) (LeftModuleCategoryStruct.actLeftUnitor N).hom)) = g

        Left zigzag identity for the braided-category construction of evaluation and coevaluation from the braiding and the rigid structure of C.

        source
        theorem CategoryTheory.ExactModuleCategory.braided_zigzag_right (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] [LeftRigidCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] (P : C) (N A : M) (f : A ⟶ LeftModuleCategoryStruct.actObj P N) :
        CategoryStruct.comp (LeftModuleCategoryStruct.actLeftUnitor A).inv (CategoryStruct.comp (LeftModuleCategoryStruct.actWhiskerRight (CategoryStruct.comp (η_ (ᘁP) P) (β_ P ᘁP).inv) A) (CategoryStruct.comp (LeftModuleCategoryStruct.actAssociator P (ᘁP) A).hom (LeftModuleCategoryStruct.actWhiskerLeft P (CategoryStruct.comp (LeftModuleCategoryStruct.actWhiskerLeft (ᘁP) f) (CategoryStruct.comp (LeftModuleCategoryStruct.actAssociator (ᘁP) P N).inv (CategoryStruct.comp (LeftModuleCategoryStruct.actWhiskerRight (CategoryStruct.comp (β_ (ᘁP) P).hom (ε_ (ᘁP) P)) N) (LeftModuleCategoryStruct.actLeftUnitor N).hom)))))) = f

        Right zigzag identity for the braided-category construction of evaluation and coevaluation from the braiding and the rigid structure of C.

        source
        @[implicit_reducible]
        noncomputable instance CategoryTheory.ExactModuleCategory.instModuleEvalCoevalBraided (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] [LeftRigidCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] :
        ModuleEvalCoeval C M

        For a braided rigid monoidal category C, the braiding combined with the rigid duality defines a canonical ModuleEvalCoeval instance on any exact module category M.