Unit, associativity and functoriality of the left twist

The twist of a module by an object on the left is unital and associative, is functorial in both of its slots, and carries the free modules along the braiding. Every isomorphism here is a structural isomorphism of the ambient category, promoted to the category of modules by checking that it intertwines the twisted actions.

• tensorLeftUnitMod: twisting by the tensor unit is the left unitor.
• tensorLeftAssocMod: nested twists collapse to a single twist by the tensor of the twisting objects.
• functoriality in the module slot and in the twisting object: RS.tensorLeftModWhiskerIso and RS.tensorLeftModContextIso of TwistShuffle.lean.
• freeTwistIso: the free module on a twisted object is the twist of the free module, through the carrying isomorphism.

The unit twist

theorem RS.actAcross_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X) (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) (actLeft A X)

The left unitor intertwines the twist by the tensor unit with the plain action.

noncomputable def RS.tensorLeftUnitMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A) : tensorLeftMod A (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) M ≅ M

The unit twist collapses: twisting a module by the tensor unit is the left unitor, as a module isomorphism.

Equations

• One or more equations did not get rendered due to their size.

Nested twists

theorem RS.actAcross_assoc_split {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V W : D) (M : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) M.X) (CategoryTheory.MonoidalCategoryStruct.associator V W M.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator V W M.X).hom) (actAcross A V (tensorLeftMod A W M).X)

The associator intertwines the twist by a tensor of twisting objects with the nested twist.

noncomputable def RS.tensorLeftAssocMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V W : D) (M : CategoryTheory.Mod D A) : tensorLeftMod A V (tensorLeftMod A W M) ≅ tensorLeftMod A (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) M

Nested twists collapse: twisting by W and then by V is twisting by V ⊗ W, through the associator.

Equations

• One or more equations did not get rendered due to their size.

The free module on a twisted object

theorem RS.braidPast_natural_head {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] {P Q : D} (f : P ⟶ Q) (V T : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj V T)) (braidPast Q V T).hom = CategoryTheory.CategoryStruct.comp (braidPast P V T).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (CategoryTheory.MonoidalCategoryStruct.whiskerRight f T))

The carrying isomorphism is natural in the crossing object.

theorem RS.freeTwist_act {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V X : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.MonoidalCategoryStruct.tensorObj V X)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj V X))) (braidPast A V X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (braidPast A V X).hom) (actAcross A V (freeMod A X).X)

The carrying isomorphism intertwines the free action on a twisted object with the twist of the free action.

noncomputable def RS.freeTwistIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V X : D) : freeMod A (CategoryTheory.MonoidalCategoryStruct.tensorObj V X) ≅ tensorLeftMod A V (freeMod A X)

The free module on a twisted object: the free module on V ⊗ X is the twist by V of the free module on X, through the isomorphism carrying the algebra across the twisting object.

Equations

• RS.freeTwistIso A V X = { hom := CategoryTheory.Mod.Hom.mk' (RS.braidPast A V X).hom ⋯, inv := CategoryTheory.Mod.Hom.mk' (RS.braidPast A V X).inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }