The free factor on the projection

The relative tensor of a free module with a module is the twist of that module by the generating object, RS.freeTensorTwistIso. This file computes that comparison on the canonical projection: it carries the algebra past the generator, reassociates, and acts.

• modTensorπ_freeTensorTwistIso: the projection formula.
• freeTensorTwistIso_gpair: the same statement for the pairing RS.gpair, which is the form the comparison map of the Γ-modules consumes.

theorem RS.freeTwistInterchange {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A V X : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ A V).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ V A (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.tensorObj A X))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A V).hom X) (CategoryTheory.MonoidalCategoryStruct.associator V A X).hom

The coherence behind the projection formula: crossing the generator, interchanging against the unit factor and collapsing the resulting right unitor is the crossing followed by the reassociation. The interchange meets the tensor unit, so its braiding is a pair of unitors.

theorem RS.modTensorπ_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) : CategoryTheory.CategoryStruct.comp (modTensorπ A (freeMod A V) M) (freeTensorTwistIso A V M).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A V).hom M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V A M.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (actLeft A M.X)))

The free factor on the projection: the isomorphism identifying the relative tensor of a free module with the twist of the module carries the projection to the crossing of the algebra past the generator, followed by the action.

theorem RS.freeTensorTwistIso_gpair {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) {X Y : D} (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A V) (n : Y ⟶ M.X) : CategoryTheory.CategoryStruct.comp (gpair m n) (freeTensorTwistIso A V M).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A V).hom M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V A M.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (actLeft A M.X))))

The free factor on the pairing: the pairing RS.gpair of a morphism into a free module with a morphism into a module is, after the identification of the relative tensor with the twist, the tensor of the two morphisms followed by the crossing and the action.