The twist shuffle

The relative tensor of two twisted modules is the twist of the relative tensor by the tensor of the twisting objects: the middle twisting object crosses the first module through the braiding. The cover-level shuffle is the middle-four interchange, so the committed interchange toolbox applies; the twisting is fully general, and the sign phenomena of the odd line enter only at the symmetriser conjugation downstream.

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

The twist of a module by an object on the left, bundled.

Equations

• RS.tensorLeftMod A V M = { X := CategoryTheory.MonoidalCategoryStruct.tensorObj V M.X, mod := RS.tensorLeftModObj A V M.X }

@[simp]

theorem RS.tensorLeftMod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (M : CategoryTheory.Mod D A) : (tensorLeftMod A V M).X = CategoryTheory.MonoidalCategoryStruct.tensorObj V M.X

noncomputable def RS.twistShuffleCover {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V R.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj W S.X) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensor A R S)

The cover map of the twist shuffle: the middle-four interchange followed by the projection under the twists.

Equations

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

theorem RS.twistShuffleCover_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (tensorLeftMod A V R) (tensorLeftMod A W S)) (twistShuffleCover A V W R S) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (tensorLeftMod A V R) (tensorLeftMod A W S)) (twistShuffleCover A V W R S)

The cover map coequalizes the twisted balance relation.

noncomputable def RS.twistShuffleHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (V W : D) (R S : CategoryTheory.Mod D A) : modTensor A (tensorLeftMod A V R) (tensorLeftMod A W S) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensor A R S)

The twist shuffle: the relative tensor of two twisted modules maps to the twist of the relative tensor.

Equations

• RS.twistShuffleHom A V W R S = RS.modTensorDesc A (RS.tensorLeftMod A V R) (RS.tensorLeftMod A W S) (RS.twistShuffleCover A V W R S) ⋯

@[simp]

theorem RS.modTensorπ_twistShuffleHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorπ A (tensorLeftMod A V R) (tensorLeftMod A W S)) (twistShuffleHom A V W R S) = twistShuffleCover A V W R S

Defining equation of the twist shuffle.

@[simp]

theorem RS.modTensorπ_twistShuffleHom_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (V W : D) (R S : CategoryTheory.Mod D A) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensor A R S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A (tensorLeftMod A V R) (tensorLeftMod A W S)) (CategoryTheory.CategoryStruct.comp (twistShuffleHom A V W R S) h) = CategoryTheory.CategoryStruct.comp (twistShuffleCover A V W R S) h

Defining equation of the twist shuffle.

noncomputable def RS.twistShuffleInvCover {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (CategoryTheory.MonoidalCategoryStruct.tensorObj R.X S.X) ⟶ modTensor A (tensorLeftMod A V R) (tensorLeftMod A W S)

The cover map of the inverse twist shuffle: split into the twisted pairs and project.

Equations

• RS.twistShuffleInvCover A V W R S = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ V R.X W S.X) (RS.modTensorπ A (RS.tensorLeftMod A V R) (RS.tensorLeftMod A W S))

instance RS.isIso_tensorμ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X₁ X₂ Y₁ Y₂ : D) : CategoryTheory.IsIso (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂)

The interchange splitting is invertible.

theorem RS.tensorδ_slide_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (actLeft A S.X))) (CategoryTheory.MonoidalCategory.tensorδ V R.X W S.X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ V R.X W (CategoryTheory.MonoidalCategoryStruct.tensorObj A S.X)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj V R.X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (actLeft A S.X)))

The second-slot action slides through the splitting.

theorem RS.tensorδ_slide_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A R.X) S.X)) (CategoryTheory.MonoidalCategory.tensorδ V R.X W S.X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ V (CategoryTheory.MonoidalCategoryStruct.tensorObj A R.X) W S.X) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (actLeft A R.X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj W S.X))

The first-slot action slides through the splitting.

theorem RS.twistShuffleInvCover_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensorLegM A R S)) (twistShuffleInvCover A V W R S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensorLegN A R S)) (twistShuffleInvCover A V W R S)

The inverse cover coequalizes the whiskered balance relation.

noncomputable def RS.twistShuffleInv {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] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensor A R S) ⟶ modTensor A (tensorLeftMod A V R) (tensorLeftMod A W S)

The inverse twist shuffle.

Equations

• RS.twistShuffleInv A V W R S = RS.modTensorWhiskerDesc A R S (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (RS.twistShuffleInvCover A V W R S) ⋯

theorem RS.whiskerLeft_π_twistShuffleInv {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] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensorπ A R S)) (twistShuffleInv A V W R S) = twistShuffleInvCover A V W R S

Defining equation of the inverse twist shuffle.

theorem RS.whiskerLeft_π_twistShuffleInv_assoc {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] (V W : D) (R S : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (tensorLeftMod A V R) (tensorLeftMod A W S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensorπ A R S)) (CategoryTheory.CategoryStruct.comp (twistShuffleInv A V W R S) h) = CategoryTheory.CategoryStruct.comp (twistShuffleInvCover A V W R S) h

Defining equation of the inverse twist shuffle.

@[simp]

theorem RS.twistShuffleHom_twistShuffleInv {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] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (twistShuffleHom A V W R S) (twistShuffleInv A V W R S) = CategoryTheory.CategoryStruct.id (modTensor A (tensorLeftMod A V R) (tensorLeftMod A W S))

The twist shuffle retracts the inverse shuffle.

@[simp]

theorem RS.twistShuffleHom_twistShuffleInv_assoc {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] (V W : D) (R S : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (tensorLeftMod A V R) (tensorLeftMod A W S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistShuffleHom A V W R S) (CategoryTheory.CategoryStruct.comp (twistShuffleInv A V W R S) h) = h

The twist shuffle retracts the inverse shuffle.

@[simp]

theorem RS.twistShuffleInv_twistShuffleHom {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] (V W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (twistShuffleInv A V W R S) (twistShuffleHom A V W R S) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensor A R S))

The inverse shuffle retracts the twist shuffle.

@[simp]

theorem RS.twistShuffleInv_twistShuffleHom_assoc {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] (V W : D) (R S : CategoryTheory.Mod D A) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensor A R S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistShuffleInv A V W R S) (CategoryTheory.CategoryStruct.comp (twistShuffleHom A V W R S) h) = h

The inverse shuffle retracts the twist shuffle.

theorem RS.twistShuffleHom_act {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 W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAct A (tensorLeftMod A V R) (tensorLeftMod A W S)) (twistShuffleHom A V W R S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (twistShuffleHom A V W R S)) (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensor A R S))

The twist shuffle is a module map: it intertwines the descended action of the twisted pair with the twist action of the shuffled pair.

noncomputable def RS.twistShuffleModHom {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 W : D) (R S : CategoryTheory.Mod D A) : modTensorMod A (tensorLeftMod A V R) (tensorLeftMod A W S) ⟶ tensorLeftMod A (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensorMod A R S)

The twist shuffle as a module map: the shuffled pair maps to the twist of the relative tensor.

Equations

• RS.twistShuffleModHom A V W R S = CategoryTheory.Mod.Hom.mk' (RS.twistShuffleHom A V W R S) ⋯

theorem RS.twistShuffleInv_act {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 W : D) (R S : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensor A R S)) (twistShuffleInv A V W R S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (twistShuffleInv A V W R S)) (modTensorAct A (tensorLeftMod A V R) (tensorLeftMod A W S))

The inverse twist shuffle intertwines the actions.

noncomputable def RS.twistShuffleModInv {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 W : D) (R S : CategoryTheory.Mod D A) : tensorLeftMod A (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensorMod A R S) ⟶ modTensorMod A (tensorLeftMod A V R) (tensorLeftMod A W S)

The inverse twist shuffle as a module map.

Equations

• RS.twistShuffleModInv A V W R S = CategoryTheory.Mod.Hom.mk' (RS.twistShuffleInv A V W R S) ⋯

noncomputable def RS.twistShuffleModIso {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 W : D) (R S : CategoryTheory.Mod D A) : modTensorMod A (tensorLeftMod A V R) (tensorLeftMod A W S) ≅ tensorLeftMod A (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) (modTensorMod A R S)

The module-level twist shuffle is an isomorphism.

Equations

• RS.twistShuffleModIso A V W R S = { hom := RS.twistShuffleModHom A V W R S, inv := RS.twistShuffleModInv A V W R S, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.tensorLeftModContextHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] {V V' : D} (f : V ⟶ V') (M : CategoryTheory.Mod D A) : tensorLeftMod A V M ⟶ tensorLeftMod A V' M

An object map in the twist slot, as a module map: the twist action carries past the context naturally.

Equations

• RS.tensorLeftModContextHom A f M = CategoryTheory.Mod.Hom.mk' (CategoryTheory.MonoidalCategoryStruct.whiskerRight f M.X) ⋯

noncomputable def RS.tensorLeftModWhiskerHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) {M N : CategoryTheory.Mod D A} (g : M ⟶ N) : tensorLeftMod A V M ⟶ tensorLeftMod A V N

A module map under the twist, as a module map.

Equations

• RS.tensorLeftModWhiskerHom A V g = CategoryTheory.Mod.Hom.mk' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V g.hom) ⋯

noncomputable def RS.tensorLeftModContextIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] {V V' : D} (e : V ≅ V') (M : CategoryTheory.Mod D A) : tensorLeftMod A V M ≅ tensorLeftMod A V' M

The twist-slot transport of an object isomorphism.

Equations

• RS.tensorLeftModContextIso A e M = { hom := RS.tensorLeftModContextHom A e.hom M, inv := RS.tensorLeftModContextHom A e.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.tensorLeftModWhiskerIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) {M N : CategoryTheory.Mod D A} (f : M ≅ N) : tensorLeftMod A V M ≅ tensorLeftMod A V N

The twist of a module isomorphism.

Equations

• RS.tensorLeftModWhiskerIso A V f = { hom := RS.tensorLeftModWhiskerHom A V f.hom, inv := RS.tensorLeftModWhiskerHom A V f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }