Associativity of the tensor product of modules

The associator of the relative tensor of internal modules over a commutative monoid. Both directions are double descents: the outer coequalizer is covered through the whiskered inner projection, the associator of the ambient category reassociates the cover, and the two balance conditions are pure slides through associator naturality together with the coequalizer conditions of source and target.

• modTensorπ_actRight: on the tensor product of modules the braided right action, precomposed with the projection, is the right action on the second factor.
• modTensorAssocHom/modTensorAssocInv: the two descents, with defining equations against the covers.
• modTensorAssocIso: the packaged isomorphism, inverted on the covers by cancelling the ambient associators.
• modTensorAssocModIso: the associator as an isomorphism of bundled modules; inverse linearity follows by cancelling the forward map.

theorem RS.modTensorπ_actRight {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] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) A) (CategoryTheory.CategoryStruct.comp (β_ (modTensor A M N) A).hom (modTensorAct A M N)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X N.X A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (actRight A N.X)) (modTensorπ A M N))

The braided right action on the tensor product of modules, precomposed with the projection, is the right action on the second factor.

theorem RS.modTensorπ_actRight_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] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) {Z : D} (h : modTensor A M N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) A) (CategoryTheory.CategoryStruct.comp (β_ (modTensor A M N) A).hom (CategoryTheory.CategoryStruct.comp (modTensorAct A M N) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X N.X A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (actRight A N.X)) (CategoryTheory.CategoryStruct.comp (modTensorπ A M N) h))

The braided right action on the tensor product of modules, precomposed with the projection, is the right action on the second factor.

theorem RS.whiskerLeft_actRight_modTensorπ {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] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (actRight A N.X)) (modTensorπ A M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X N.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) A) (CategoryTheory.CategoryStruct.comp (β_ (modTensor A M N) A).hom (modTensorAct A M N)))

Companion form of modTensorπ_actRight: the right action on the second factor descends to the braided right action on the tensor product of modules.

theorem RS.whiskerLeft_actRight_modTensorπ_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] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) {Z : D} (h : modTensor A M N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (actRight A N.X)) (CategoryTheory.CategoryStruct.comp (modTensorπ A M N) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X N.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) A) (CategoryTheory.CategoryStruct.comp (β_ (modTensor A M N) A).hom (CategoryTheory.CategoryStruct.comp (modTensorAct A M N) h)))

Companion form of modTensorπ_actRight: the right action on the second factor descends to the braided right action on the tensor product of modules.

theorem RS.modTensor_condition_right {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight A M.X) (modTensor A N P)) (modTensorπ A M (modTensorMod A N P)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X A (modTensor A N P)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorAct A N P)) (modTensorπ A M (modTensorMod A N P)))

The coequalizer condition of the right-nested tensor product, stated over the underlying objects.

theorem RS.modTensor_condition_left {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (β_ (modTensor A M N) A).hom (modTensorAct A M N)) P.X) (modTensorπ A (modTensorMod A M N) P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (modTensor A M N) A P.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A M N) (actLeft A P.X)) (modTensorπ A (modTensorMod A M N) P))

The coequalizer condition of the left-nested tensor product, stated over the underlying objects.

noncomputable def RS.modTensorAssocCover {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) P.X ⟶ modTensor A M (modTensorMod A N P)

The cover of the associator: reassociate and project through both tensor products of the right-nested side.

Equations

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

theorem RS.modTensorAssocCover_cond {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegM A M N) P.X) (modTensorAssocCover A M N P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegN A M N) P.X) (modTensorAssocCover A M N P)

The cover of the associator coequalizes the whiskered inner balance relation: the monoid sliding between M and N slides onto N through the conditions of the target.

noncomputable def RS.modTensorAssocMid {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A M N) P.X ⟶ modTensor A M (modTensorMod A N P)

The half-descended associator, on the cover of the outer coequalizer of the left-nested side.

Equations

• RS.modTensorAssocMid A M N P = RS.modTensorWhiskerRDesc A M N P.X (RS.modTensorAssocCover A M N P) ⋯

@[simp]

theorem RS.whiskerRight_modTensorπ_assocMid {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) P.X) (modTensorAssocMid A M N P) = modTensorAssocCover A M N P

Defining equation of the half-descended associator.

@[simp]

theorem RS.whiskerRight_modTensorπ_assocMid_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) {Z : D} (h : modTensor A M (modTensorMod A N P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) P.X) (CategoryTheory.CategoryStruct.comp (modTensorAssocMid A M N P) h) = CategoryTheory.CategoryStruct.comp (modTensorAssocCover A M N P) h

Defining equation of the half-descended associator.

theorem RS.modTensorAssocMid_cond {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (modTensorMod A M N) P) (modTensorAssocMid A M N P) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (modTensorMod A M N) P) (modTensorAssocMid A M N P)

The half-descended associator coequalizes the outer balance relation: the monoid sliding between the (M, N)-block and P slides between N and P through the inner condition of the target.

noncomputable def RS.modTensorAssocHom {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : modTensor A (modTensorMod A M N) P ⟶ modTensor A M (modTensorMod A N P)

The associator of the tensor product of modules: the descent of the ambient associator to the relative tensors.

Equations

• RS.modTensorAssocHom A M N P = RS.modTensorDesc A (RS.modTensorMod A M N) P (RS.modTensorAssocMid A M N P) ⋯

@[simp]

theorem RS.modTensorπ_assocHom {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modTensorMod A M N) P) (modTensorAssocHom A M N P) = modTensorAssocMid A M N P

Defining equation of the associator.

@[simp]

theorem RS.modTensorπ_assocHom_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) {Z : D} (h : modTensor A M (modTensorMod A N P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modTensorMod A M N) P) (CategoryTheory.CategoryStruct.comp (modTensorAssocHom A M N P) h) = CategoryTheory.CategoryStruct.comp (modTensorAssocMid A M N P) h

Defining equation of the associator.

noncomputable def RS.modTensorAssocInvCover {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X (CategoryTheory.MonoidalCategoryStruct.tensorObj N.X P.X) ⟶ modTensor A (modTensorMod A M N) P

The cover of the inverse associator: reassociate backwards and project through both tensor products of the left-nested side.

Equations

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

theorem RS.modTensorAssocInvCover_cond {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorLegM A N P)) (modTensorAssocInvCover A M N P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorLegN A N P)) (modTensorAssocInvCover A M N P)

The inverse cover coequalizes the whiskered inner balance relation: the monoid sliding between N and P slides onto the (M, N)-block through the conditions of the target.

noncomputable def RS.modTensorAssocInvMid {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X (modTensor A N P) ⟶ modTensor A (modTensorMod A M N) P

The half-descended inverse associator, on the cover of the outer coequalizer of the right-nested side.

Equations

• RS.modTensorAssocInvMid A M N P = RS.modTensorWhiskerDesc A N P M.X (RS.modTensorAssocInvCover A M N P) ⋯

@[simp]

theorem RS.whiskerLeft_modTensorπ_assocInvMid {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorπ A N P)) (modTensorAssocInvMid A M N P) = modTensorAssocInvCover A M N P

Defining equation of the half-descended inverse associator.

@[simp]

theorem RS.whiskerLeft_modTensorπ_assocInvMid_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] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (modTensorMod A M N) P ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorπ A N P)) (CategoryTheory.CategoryStruct.comp (modTensorAssocInvMid A M N P) h) = CategoryTheory.CategoryStruct.comp (modTensorAssocInvCover A M N P) h

Defining equation of the half-descended inverse associator.

theorem RS.modTensorAssocInvMid_cond {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegM A M (modTensorMod A N P)) (modTensorAssocInvMid A M N P) = CategoryTheory.CategoryStruct.comp (modTensorLegN A M (modTensorMod A N P)) (modTensorAssocInvMid A M N P)

The half-descended inverse associator coequalizes the outer balance relation: the monoid sliding between M and the (N, P)-block slides between M and N through the inner condition of the target.

noncomputable def RS.modTensorAssocInv {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] (M N P : CategoryTheory.Mod D A) : modTensor A M (modTensorMod A N P) ⟶ modTensor A (modTensorMod A M N) P

The inverse associator of the tensor product of modules.

Equations

• RS.modTensorAssocInv A M N P = RS.modTensorDesc A M (RS.modTensorMod A N P) (RS.modTensorAssocInvMid A M N P) ⋯

@[simp]

theorem RS.modTensorπ_assocInv {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] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorπ A M (modTensorMod A N P)) (modTensorAssocInv A M N P) = modTensorAssocInvMid A M N P

Defining equation of the inverse associator.

@[simp]

theorem RS.modTensorπ_assocInv_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] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (modTensorMod A M N) P ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A M (modTensorMod A N P)) (CategoryTheory.CategoryStruct.comp (modTensorAssocInv A M N P) h) = CategoryTheory.CategoryStruct.comp (modTensorAssocInvMid A M N P) h

Defining equation of the inverse associator.

@[simp]

theorem RS.modTensorAssocHom_assocInv {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAssocHom A M N P) (modTensorAssocInv A M N P) = CategoryTheory.CategoryStruct.id (modTensor A (modTensorMod A M N) P)

The associator retracts the inverse associator.

@[simp]

theorem RS.modTensorAssocHom_assocInv_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (modTensorMod A M N) P ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorAssocHom A M N P) (CategoryTheory.CategoryStruct.comp (modTensorAssocInv A M N P) h) = h

The associator retracts the inverse associator.

@[simp]

theorem RS.modTensorAssocInv_assocHom {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAssocInv A M N P) (modTensorAssocHom A M N P) = CategoryTheory.CategoryStruct.id (modTensor A M (modTensorMod A N P))

The inverse associator retracts the associator.

@[simp]

theorem RS.modTensorAssocInv_assocHom_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) {Z : D} (h : modTensor A M (modTensorMod A N P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorAssocInv A M N P) (CategoryTheory.CategoryStruct.comp (modTensorAssocHom A M N P) h) = h

The inverse associator retracts the associator.

noncomputable def RS.modTensorAssocIso {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : modTensor A (modTensorMod A M N) P ≅ modTensor A M (modTensorMod A N P)

The associator isomorphism of the tensor product of modules (Deligne 2002, §2.3): the relative tensor is associative up to the descended ambient associator.

Equations

• RS.modTensorAssocIso A M N P = { hom := RS.modTensorAssocHom A M N P, inv := RS.modTensorAssocInv A M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem RS.modTensorAssocHom_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAct A (modTensorMod A M N) P) (modTensorAssocHom A M N P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorAssocHom A M N P)) (modTensorAct A M (modTensorMod A N P))

The associator is a morphism of modules: it intertwines the descended actions of the two nestings.

theorem RS.modTensorAssocHom_act_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) {Z : D} (h : modTensor A M (modTensorMod A N P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorAct A (modTensorMod A M N) P) (CategoryTheory.CategoryStruct.comp (modTensorAssocHom A M N P) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorAssocHom A M N P)) (CategoryTheory.CategoryStruct.comp (modTensorAct A M (modTensorMod A N P)) h)

The associator is a morphism of modules: it intertwines the descended actions of the two nestings.

theorem RS.modTensorAssocInv_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAct A M (modTensorMod A N P)) (modTensorAssocInv A M N P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorAssocInv A M N P)) (modTensorAct A (modTensorMod A M N) P)

The inverse associator intertwines the actions.

theorem RS.modTensorAssocInv_act_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (modTensorMod A M N) P ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorAct A M (modTensorMod A N P)) (CategoryTheory.CategoryStruct.comp (modTensorAssocInv A M N P) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorAssocInv A M N P)) (CategoryTheory.CategoryStruct.comp (modTensorAct A (modTensorMod A M N) P) h)

The inverse associator intertwines the actions.

noncomputable def RS.modTensorAssocModHom {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : modTensorMod A (modTensorMod A M N) P ⟶ modTensorMod A M (modTensorMod A N P)

The associator as a morphism of bundled modules.

Equations

• RS.modTensorAssocModHom A M N P = CategoryTheory.Mod.Hom.mk' (RS.modTensorAssocHom A M N P) ⋯

noncomputable def RS.modTensorAssocModInv {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : modTensorMod A M (modTensorMod A N P) ⟶ modTensorMod A (modTensorMod A M N) P

The inverse associator as a morphism of bundled modules.

Equations

• RS.modTensorAssocModInv A M N P = CategoryTheory.Mod.Hom.mk' (RS.modTensorAssocInv A M N P) ⋯

noncomputable def RS.modTensorAssocModIso {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M N P : CategoryTheory.Mod D A) : modTensorMod A (modTensorMod A M N) P ≅ modTensorMod A M (modTensorMod A N P)

The associator of the tensor product of modules, as an isomorphism of bundled modules.

Equations

• RS.modTensorAssocModIso A M N P = { hom := RS.modTensorAssocModHom A M N P, inv := RS.modTensorAssocModInv A M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ }