The free module inside the relative tensor

Tensoring against a free module changes nothing but the twist: the algebra of the free module is absorbed by the relative tensor and only the generating object survives, carried across by the braiding.

• freeRegTwistIso: the free module on an object is the twist of the regular module by that object, through the braiding.
• freeTensorTwistIso: the relative tensor of a free module with a module is the twist of that module by the generating object.

The free module as a twisted regular module

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

The braiding intertwines the free action on the generator with the twist of the regular action: both hexagon legs multiply the two algebra factors after carrying the generator to the front.

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

The free module is a twisted regular module: the free module on V is the twist by V of the regular module, through the braiding carrying the algebra past the generator.

Equations

• RS.freeRegTwistIso A V = { hom := CategoryTheory.Mod.Hom.mk' (β_ A V).hom ⋯, inv := CategoryTheory.Mod.Hom.mk' (β_ A V).inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Absorbing a free factor

noncomputable def RS.freeTensorTwistIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (M : CategoryTheory.Mod D A) : modTensorMod A (freeMod A V) M ≅ tensorLeftMod A V M

The free factor twists: the relative tensor of the free module on V with a module M is the twist of M by V. The free module is the twisted regular module, the twist shuffle collects both twists in front, and the regular module is the unit of the relative tensor.

Equations

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