Tensor product of internal modules over a commutative monoid

Module theory over a monoid object, after Deligne (2002), §§2.2–2.3. Throughout, D is a monoidal category and A : D a monoid object in Mathlib's internal sense: MonObj A, with internal left modules given by ModObj A X over the self-action of D and bundled as Mod D A.

• actLeft: the action morphism of a module object, typed at the tensor product A ⊗ X rather than at the action synonym ⊙ₗ, with the module laws restated in this form.
• tensorRightModObj: a left module tensored with an object on the right is again a left module; freeModObj/freeMod specialize to the free module A ⊗ V. The regular module is Mathlib's Mod.regular A.
• actRight: on a left module over a commutative monoid in a braided category, the braiding induces a right action; the compatibility lemmas actLeft_actRight and actRight_actRight express that left and right actions commute and that actRight is associative.
• modTensor A M N: the tensor product of modules, the coequalizer of the pair (M.X ⊗ A) ⊗ N.X ⇉ M.X ⊗ N.X whose first leg modTensorLegM acts on M through actRight and whose second leg modTensorLegN associates and acts on N.
• modTensorModObj: the A-action descends to the coequalizer when every tensorLeft X preserves coequalizers; more generally modTensorDescModObj descends any monoid action on M.X that commutes with actRight.
• modTensorUnitLeft/modTensorUnitRight: the regular module is a two-sided unit, compatibly with the actions.
• modTensorMap: functoriality in both slots.
• restrictRegular/baseChange: base change along a morphism of commutative monoid objects.

The development is scoped to the structures above; associativity of modTensor is outside this module's scope.

def RS.actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ X

The action morphism of a module object, typed at the tensor product.

Equations

• RS.actLeft A X = CategoryTheory.ModObj.smul

@[simp]

theorem RS.one_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) (actLeft A X) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom

Unitality of the action, in tensor form.

@[simp]

theorem RS.one_actLeft_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) (CategoryTheory.CategoryStruct.comp (actLeft A X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h

Unitality of the action, in tensor form.

theorem RS.mul_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) (actLeft A X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actLeft A X)) (actLeft A X))

Associativity of the action, in tensor form.

theorem RS.mul_actLeft_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) (CategoryTheory.CategoryStruct.comp (actLeft A X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actLeft A X)) (CategoryTheory.CategoryStruct.comp (actLeft A X) h))

Associativity of the action, in tensor form.

theorem RS.actLeft_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actLeft A X)) (actLeft A X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) (actLeft A X))

Associativity of the action, associator on the right.

theorem RS.actLeft_actLeft_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actLeft A X)) (CategoryTheory.CategoryStruct.comp (actLeft A X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) (CategoryTheory.CategoryStruct.comp (actLeft A X) h))

Associativity of the action, associator on the right.

@[simp]

theorem RS.actLeft_natural {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] : CategoryTheory.CategoryStruct.comp (actLeft A X) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) (actLeft A Y)

actLeft is natural in module morphisms.

@[simp]

theorem RS.actLeft_natural_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (actLeft A X) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) (CategoryTheory.CategoryStruct.comp (actLeft A Y) h)

actLeft is natural in module morphisms.

@[reducible]

def RS.regularMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] : CategoryTheory.Mod D A

The regular module, with underlying object reducibly A; it is definitionally Mathlib's Mod.regular A.

Equations

• RS.regularMod A = { X := A, mod := CategoryTheory.ModObj.regular A }

theorem RS.one_act_tensorRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ X) (hone : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) act = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (CategoryTheory.MonoidalCategoryStruct.tensorObj X V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight act V)) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X V)).hom

Unitality of an action transported to a right tensor factor.

theorem RS.mul_act_tensorRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ X) (hmul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A act) act)) (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj X V)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight act V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.MonoidalCategoryStruct.tensorObj X V)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight act V))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight act V)))

Associativity of an action transported to a right tensor factor.

@[implicit_reducible]

def RS.tensorRightModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (V : D) : CategoryTheory.ModObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj X V)

A left module tensored with an object on the right: the action of A on X ⊗ V through the left factor.

Equations

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

@[simp]

theorem RS.tensorRightModObj_smul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (V : D) : CategoryTheory.ModObj.smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A X) V)

@[implicit_reducible]

def RS.freeModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) : CategoryTheory.ModObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)

The free module on an object: A ⊗ V with the action given by multiplication on the left factor.

Equations

• RS.freeModObj A V = RS.tensorRightModObj A A V

theorem RS.whiskerLeft_one_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (W : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one W))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul W)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A W)

Inserting the unit of A and then acting on the free module is the identity.

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

The free module on an object, bundled.

Equations

• RS.freeMod A V = { X := CategoryTheory.MonoidalCategoryStruct.tensorObj A V, mod := RS.freeModObj A V }

theorem RS.freeMod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) : (freeMod A V).X = CategoryTheory.MonoidalCategoryStruct.tensorObj A V

The carrier of the free module. This is definitional, and is stated for use by name: as a simp rule it would rewrite the type arguments of every application of the module interface at a free module and so stop that interface firing.

def RS.actRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.MonoidalCategoryStruct.tensorObj X A ⟶ X

The right action of A on a left module, induced by the braiding.

Equations

• RS.actRight A X = CategoryTheory.CategoryStruct.comp (β_ X A).hom (RS.actLeft A X)

theorem RS.actRight_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one) (actRight A X) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom

Unitality of the braided right action.

theorem RS.actRight_one_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.ModObj A X] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one) (CategoryTheory.CategoryStruct.comp (actRight A X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h

Unitality of the braided right action.

theorem RS.actRight_natural {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] : CategoryTheory.CategoryStruct.comp (actRight A X) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A) (actRight A Y)

actRight is natural in module morphisms.

theorem RS.actRight_natural_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (actRight A X) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A) (CategoryTheory.CategoryStruct.comp (actRight A Y) h)

actRight is natural in module morphisms.

theorem RS.actRight_natural_mod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (actRight A M.X) f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom A) (actRight A N.X)

actRight is natural in maps of module objects.

theorem RS.actRight_natural_mod_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M N : CategoryTheory.Mod D A} (f : M ⟶ N) {Z : D} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (actRight A M.X) (CategoryTheory.CategoryStruct.comp f.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom A) (CategoryTheory.CategoryStruct.comp (actRight A N.X) h)

actRight is natural in maps of module objects.

def RS.freeModShuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (V W : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) (CategoryTheory.MonoidalCategoryStruct.tensorObj A W) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)

The shuffle of two free modules: multiply the two algebra factors, having carried the first generator past the second algebra factor. This is at once the head absorption that folds an incoming free letter into an accumulated head.

Equations

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

theorem RS.actLeft_actRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actRight A X)) (actLeft A X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A X) A) (actRight A X))

Two-sided compatibility for a commutative monoid: the left action and the braided right action on a module commute.

theorem RS.actLeft_actRight_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actRight A X)) (CategoryTheory.CategoryStruct.comp (actLeft A X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A X) A) (CategoryTheory.CategoryStruct.comp (actRight A X) h))

Two-sided compatibility for a commutative monoid: the left action and the braided right action on a module commute.

theorem RS.actRight_actRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight A X) A) (actRight A X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.mul) (actRight A X))

For a commutative monoid, the braided right action is associative.

theorem RS.actRight_actRight_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight A X) A) (CategoryTheory.CategoryStruct.comp (actRight A X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.mul) (CategoryTheory.CategoryStruct.comp (actRight A X) h))

For a commutative monoid, the braided right action is associative.

def RS.modTensorLegM {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X

First leg of the module-tensor parallel pair on (M.X ⊗ A) ⊗ N.X: act on M through the braided right action.

Equations

• RS.modTensorLegM A M N = CategoryTheory.MonoidalCategoryStruct.whiskerRight (RS.actRight A M.X) N.X

def RS.modTensorLegN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X

Second leg of the module-tensor parallel pair on (M.X ⊗ A) ⊗ N.X: associate and act on N.

Equations

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

theorem RS.whiskerLeft_modTensorLegM_act {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) (P : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj P M.X ⟶ M.X) (compat : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (actRight A M.X)) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A) (actRight A M.X))) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorLegM A M N)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight act N.X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A)) N.X)) (modTensorLegM A M N)

A P-action on M.X commuting with the braided right A-action intertwines the first leg with the induced actions on (M.X ⊗ A) ⊗ N.X and M.X ⊗ N.X.

theorem RS.whiskerLeft_modTensorLegN_act {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (P : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj P M.X ⟶ M.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorLegN A M N)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight act N.X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A)) N.X)) (modTensorLegN A M N)

Any morphism P ⊗ M.X ⟶ M.X intertwines the second leg with the induced maps on (M.X ⊗ A) ⊗ N.X and M.X ⊗ N.X.

noncomputable def RS.modTensor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] : D

The tensor product of two modules over A: the coequalizer of modTensorLegM and modTensorLegN.

Equations

• RS.modTensor A M N = CategoryTheory.Limits.coequalizer (RS.modTensorLegM A M N) (RS.modTensorLegN A M N)

noncomputable def RS.modTensorπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X ⟶ modTensor A M N

The projection onto the tensor product of modules.

Equations

• RS.modTensorπ A M N = CategoryTheory.Limits.coequalizer.π (RS.modTensorLegM A M N) (RS.modTensorLegN A M N)

theorem RS.modTensor_condition {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] : CategoryTheory.CategoryStruct.comp (modTensorLegM A M N) (modTensorπ A M N) = CategoryTheory.CategoryStruct.comp (modTensorLegN A M N) (modTensorπ A M N)

The two legs agree after the projection.

theorem RS.modTensor_condition_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] {Z : D} (h : modTensor A M N ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorLegM A M N) (CategoryTheory.CategoryStruct.comp (modTensorπ A M N) h) = CategoryTheory.CategoryStruct.comp (modTensorLegN A M N) (CategoryTheory.CategoryStruct.comp (modTensorπ A M N) h)

The two legs agree after the projection.

noncomputable def RS.modTensorDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X ⟶ W) (h : CategoryTheory.CategoryStruct.comp (modTensorLegM A M N) k = CategoryTheory.CategoryStruct.comp (modTensorLegN A M N) k) : modTensor A M N ⟶ W

Descend a morphism coequalizing the two legs to the tensor product of modules.

Equations

• RS.modTensorDesc A M N k h = CategoryTheory.Limits.coequalizer.desc k h

@[simp]

theorem RS.modTensorπ_desc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X ⟶ W) (h : CategoryTheory.CategoryStruct.comp (modTensorLegM A M N) k = CategoryTheory.CategoryStruct.comp (modTensorLegN A M N) k) : CategoryTheory.CategoryStruct.comp (modTensorπ A M N) (modTensorDesc A M N k h) = k

The descent factors the given morphism through the projection.

@[simp]

theorem RS.modTensorπ_desc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X ⟶ W) (h : CategoryTheory.CategoryStruct.comp (modTensorLegM A M N) k = CategoryTheory.CategoryStruct.comp (modTensorLegN A M N) k) {Z : D} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A M N) (CategoryTheory.CategoryStruct.comp (modTensorDesc A M N k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The descent factors the given morphism through the projection.

theorem RS.modTensor_hom_ext {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] {W : D} {k l : modTensor A M N ⟶ W} (h : CategoryTheory.CategoryStruct.comp (modTensorπ A M N) k = CategoryTheory.CategoryStruct.comp (modTensorπ A M N) l) : k = l

Morphisms out of the tensor product of modules are determined by their composite with the projection.

noncomputable def RS.modTensorWhiskerIsColimit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) ⋯)

Whiskering the module-tensor coequalizer by tensorLeft P yields a colimit cofork.

Equations

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

theorem RS.modTensor_whisker_hom_ext {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) {W : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modTensor A M N) ⟶ W} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) l) : k = l

Morphisms out of a whiskered tensor product of modules are determined by their composite with the whiskered projection.

noncomputable def RS.modTensorWhiskerDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj P (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) ⟶ W) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorLegM A M N)) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorLegN A M N)) k) : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modTensor A M N) ⟶ W

Descend a morphism along the whiskered coequalizer.

Equations

• RS.modTensorWhiskerDesc A M N P k h = CategoryTheory.Limits.Cofork.IsColimit.desc (RS.modTensorWhiskerIsColimit A M N P) k h

@[simp]

theorem RS.whiskerLeft_modTensorπ_whiskerDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj P (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) ⟶ W) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorLegM A M N)) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorLegN A M N)) k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) (modTensorWhiskerDesc A M N P k h) = k

The whiskered descent factors the given morphism through the whiskered projection.

@[simp]

theorem RS.whiskerLeft_modTensorπ_whiskerDesc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj P (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) ⟶ W) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorLegM A M N)) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorLegN A M N)) k) {Z : D} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) (CategoryTheory.CategoryStruct.comp (modTensorWhiskerDesc A M N P k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The whiskered descent factors the given morphism through the whiskered projection.

noncomputable def RS.modTensorWhiskerRIsColimit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (W : D) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) W) ⋯)

Whiskering the module-tensor coequalizer by tensorRight W yields a colimit cofork.

Equations

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

theorem RS.modTensor_whiskerR_hom_ext {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (W : D) {Z : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A M N) W ⟶ Z} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) W) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) W) l) : k = l

Morphisms out of a right-whiskered tensor product of modules are determined by their composite with the whiskered projection.

noncomputable def RS.modTensorWhiskerRDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (W : D) {Z : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) W ⟶ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegM A M N) W) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegN A M N) W) k) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A M N) W ⟶ Z

Descend a morphism along the right-whiskered coequalizer.

Equations

• RS.modTensorWhiskerRDesc A M N W k h = CategoryTheory.Limits.Cofork.IsColimit.desc (RS.modTensorWhiskerRIsColimit A M N W) k h

@[simp]

theorem RS.whiskerRight_modTensorπ_whiskerRDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (W : D) {Z : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) W ⟶ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegM A M N) W) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegN A M N) W) k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) W) (modTensorWhiskerRDesc A M N W k h) = k

The right-whiskered descent factors the given morphism through the whiskered projection.

@[simp]

theorem RS.whiskerRight_modTensorπ_whiskerRDesc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (W : D) {Z : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) W ⟶ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegM A M N) W) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegN A M N) W) k) {Z✝ : D} (h✝ : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M N) W) (CategoryTheory.CategoryStruct.comp (modTensorWhiskerRDesc A M N W k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The right-whiskered descent factors the given morphism through the whiskered projection.

noncomputable def RS.modTensorDescAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj P M.X ⟶ M.X) (compat : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (actRight A M.X)) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A) (actRight A M.X))) : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modTensor A M N) ⟶ modTensor A M N

Descend a compatible action along the module-tensor projection.

Equations

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

@[simp]

theorem RS.whiskerLeft_modTensorπ_descAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj P M.X ⟶ M.X) (compat : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (actRight A M.X)) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A) (actRight A M.X))) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) (modTensorDescAct A M N P act compat) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight act N.X)) (modTensorπ A M N)

Defining equation of the descended action.

@[simp]

theorem RS.whiskerLeft_modTensorπ_descAct_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj P M.X ⟶ M.X) (compat : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (actRight A M.X)) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A) (actRight A M.X))) {Z : D} (h : modTensor A M N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) (CategoryTheory.CategoryStruct.comp (modTensorDescAct A M N P act compat) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X N.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act N.X) (CategoryTheory.CategoryStruct.comp (modTensorπ A M N) h))

Defining equation of the descended action.

theorem RS.modTensorDescAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) [CategoryTheory.MonObj P] (act : CategoryTheory.MonoidalCategoryStruct.tensorObj P M.X ⟶ M.X) (compat : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (actRight A M.X)) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A) (actRight A M.X))) (hone : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one M.X) act = (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).hom) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (modTensor A M N)) (modTensorDescAct A M N P act compat) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (modTensor A M N)).hom

Unitality descends to the tensor product of modules.

theorem RS.modTensorDescAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) [CategoryTheory.MonObj P] (act : CategoryTheory.MonoidalCategoryStruct.tensorObj P M.X ⟶ M.X) (compat : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (actRight A M.X)) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A) (actRight A M.X))) (hmul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul M.X) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P P M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P act) act)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (modTensor A M N)) (modTensorDescAct A M N P act compat) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P P (modTensor A M N)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorDescAct A M N P act compat)) (modTensorDescAct A M N P act compat))

Associativity descends to the tensor product of modules.

theorem RS.modTensorDescAct_desc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj P M.X ⟶ M.X) (compat : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (actRight A M.X)) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A) (actRight A M.X))) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X ⟶ W) (hk : CategoryTheory.CategoryStruct.comp (modTensorLegM A M N) k = CategoryTheory.CategoryStruct.comp (modTensorLegN A M N) k) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj P W ⟶ W) (hw : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X N.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act N.X) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P k) w) : CategoryTheory.CategoryStruct.comp (modTensorDescAct A M N P act compat) (modTensorDesc A M N k hk) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorDesc A M N k hk)) w

The descended action intertwines descended morphisms with actions on the target: if k coequalizes the legs and carries the induced action on M.X ⊗ N.X to w, then the descent of k is equivariant.

@[implicit_reducible]

noncomputable def RS.modTensorDescModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (P : D) [CategoryTheory.MonObj P] (act : CategoryTheory.MonoidalCategoryStruct.tensorObj P M.X ⟶ M.X) (compat : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (actRight A M.X)) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight act A) (actRight A M.X))) (hone : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one M.X) act = (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).hom) (hmul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul M.X) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P P M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P act) act)) : CategoryTheory.ModObj P (modTensor A M N)

Descend a compatible monoid action on M.X to a module structure on the tensor product.

Equations

• RS.modTensorDescModObj A M N P act compat hone hmul = { smul := RS.modTensorDescAct A M N P act compat, one_smul := ⋯, mul_smul := ⋯ }

@[implicit_reducible]

noncomputable def RS.modTensorModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.ModObj A (modTensor A M N)

The A-module structure on the tensor product of modules over a commutative monoid: the action on the M-factor descends.

Equations

• RS.modTensorModObj A M N = RS.modTensorDescModObj A M N A (RS.actLeft A M.X) ⋯ ⋯ ⋯

noncomputable def RS.modTensorAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.MonoidalCategoryStruct.tensorObj A (modTensor A M N) ⟶ modTensor A M N

The action of A on the tensor product of modules.

Equations

• RS.modTensorAct A M N = CategoryTheory.ModObj.smul

@[simp]

theorem RS.whiskerLeft_modTensorπ_act {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorπ A M N)) (modTensorAct A M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M.X N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A M.X) N.X)) (modTensorπ A M N)

Defining equation of the A-action on the tensor product of modules.

@[simp]

theorem RS.whiskerLeft_modTensorπ_act_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] {Z : D} (h : modTensor A M N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorπ A M N)) (CategoryTheory.CategoryStruct.comp (modTensorAct A M N) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M.X N.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A M.X) N.X) (CategoryTheory.CategoryStruct.comp (modTensorπ A M N) h))

Defining equation of the A-action on the tensor product of modules.

theorem RS.modTensorAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (modTensor A M N)) (modTensorAct A M N) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (modTensor A M N)).hom

Unitality of the descended action.

theorem RS.modTensorAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (modTensor A M N)) (modTensorAct A M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (modTensor A M N)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorAct A M N)) (modTensorAct A M N))

Associativity of the descended action.

noncomputable def RS.modTensorMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.Mod D A

The tensor product of modules, bundled as a module.

Equations

• RS.modTensorMod A M N = { X := RS.modTensor A M N, mod := RS.modTensorModObj A M N }

theorem RS.modTensorMod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : (modTensorMod A M N).X = modTensor A M N

The carrier of the bundled tensor product. Definitional, and stated for use by name, for the reason given for freeMod_X.

theorem RS.whiskerLeft_modTensorπ_act_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.SymmetricCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorπ A M N)) (modTensorAct A M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M.X N.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A M.X).hom N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (actLeft A N.X)) (modTensorπ A M N))))

The descended action through the second factor: over a symmetric base, the monoid braids past the first module and acts on the second. The balance relation of the coequalizer carries the first-factor action across.

theorem RS.whiskerLeft_modTensorπ_act_snd_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.SymmetricCategory D] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] {Z : D} (h : modTensor A M N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorπ A M N)) (CategoryTheory.CategoryStruct.comp (modTensorAct A M N) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M.X N.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A M.X).hom N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (actLeft A N.X)) (CategoryTheory.CategoryStruct.comp (modTensorπ A M N) h))))

The descended action through the second factor: over a symmetric base, the monoid braids past the first module and acts on the second. The balance relation of the coequalizer carries the first-factor action across.

theorem RS.modTensorLegM_regular_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (regularMod A) N) (actLeft A N.X) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (regularMod A) N) (actLeft A N.X)

The action of N coequalizes the legs at M = A.

theorem RS.modTensorLegM_regular_actRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegM A M (regularMod A)) (actRight A M.X) = CategoryTheory.CategoryStruct.comp (modTensorLegN A M (regularMod A)) (actRight A M.X)

The right action of M coequalizes the legs at N = A.

noncomputable def RS.modTensorUnitLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] : modTensor A (regularMod A) N ≅ N.X

The regular module is a left unit for the module tensor product.

Equations

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

@[simp]

theorem RS.modTensorUnitLeft_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] : (modTensorUnitLeft A N).hom = modTensorDesc A (regularMod A) N (actLeft A N.X) ⋯

@[simp]

theorem RS.modTensorUnitLeft_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] : (modTensorUnitLeft A N).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor N.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one N.X) (modTensorπ A (regularMod A) N))

noncomputable def RS.modTensorUnitRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] : modTensor A M (regularMod A) ≅ M.X

The regular module is a right unit for the module tensor product of a commutative monoid.

Equations

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

@[simp]

theorem RS.modTensorUnitRight_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] : (modTensorUnitRight A M).hom = modTensorDesc A M (regularMod A) (actRight A M.X) ⋯

@[simp]

theorem RS.modTensorUnitRight_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] : (modTensorUnitRight A M).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X CategoryTheory.MonObj.one) (modTensorπ A M (regularMod A)))

theorem RS.modTensorUnitLeft_hom_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (modTensorAct A (regularMod A) N) (modTensorUnitLeft A N).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorUnitLeft A N).hom) (actLeft A N.X)

The left unit isomorphism is a morphism of modules.

theorem RS.modTensorUnitLeft_hom_actLeft_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (N : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] {Z : D} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorAct A (regularMod A) N) (CategoryTheory.CategoryStruct.comp (modTensorUnitLeft A N).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorUnitLeft A N).hom) (CategoryTheory.CategoryStruct.comp (actLeft A N.X) h)

The left unit isomorphism is a morphism of modules.

theorem RS.modTensorUnitRight_hom_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (modTensorAct A M (regularMod A)) (modTensorUnitRight A M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorUnitRight A M).hom) (actLeft A M.X)

The right unit isomorphism is a morphism of modules.

theorem RS.modTensorUnitRight_hom_actLeft_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (M : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] {Z : D} (h : M.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorAct A M (regularMod A)) (CategoryTheory.CategoryStruct.comp (modTensorUnitRight A M).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorUnitRight A M).hom) (CategoryTheory.CategoryStruct.comp (actLeft A M.X) h)

The right unit isomorphism is a morphism of modules.

theorem RS.modTensorLegM_tensorHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M M' N N' : CategoryTheory.Mod D A} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (modTensorLegM A M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom A) g.hom) (modTensorLegM A M' N')

Module morphisms intertwine the first legs.

theorem RS.modTensorLegN_tensorHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {M M' N N' : CategoryTheory.Mod D A} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (modTensorLegN A M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom A) g.hom) (modTensorLegN A M' N')

Module morphisms intertwine the second legs.

noncomputable def RS.modTensorMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M M' N N' : CategoryTheory.Mod D A} [CategoryTheory.Limits.HasCoequalizers D] (f : M ⟶ M') (g : N ⟶ N') : modTensor A M N ⟶ modTensor A M' N'

Functoriality of the module tensor product in both slots.

Equations

• RS.modTensorMap A f g = RS.modTensorDesc A M N (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom) (RS.modTensorπ A M' N')) ⋯

@[simp]

theorem RS.modTensorπ_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M M' N N' : CategoryTheory.Mod D A} [CategoryTheory.Limits.HasCoequalizers D] (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (modTensorπ A M N) (modTensorMap A f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom) (modTensorπ A M' N')

Defining equation of the functorial map.

@[simp]

theorem RS.modTensorπ_map_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M M' N N' : CategoryTheory.Mod D A} [CategoryTheory.Limits.HasCoequalizers D] (f : M ⟶ M') (g : N ⟶ N') {Z : D} (h : modTensor A M' N' ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A M N) (CategoryTheory.CategoryStruct.comp (modTensorMap A f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom) (CategoryTheory.CategoryStruct.comp (modTensorπ A M' N') h)

Defining equation of the functorial map.

theorem RS.modTensorMap_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M N : CategoryTheory.Mod D A} [CategoryTheory.Limits.HasCoequalizers D] : modTensorMap A (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (modTensor A M N)

The functorial map preserves identities.

theorem RS.modTensorMap_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M M' M'' N N' N'' : CategoryTheory.Mod D A} [CategoryTheory.Limits.HasCoequalizers D] (f : M ⟶ M') (f' : M' ⟶ M'') (g : N ⟶ N') (g' : N' ⟶ N'') : modTensorMap A (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (modTensorMap A f g) (modTensorMap A f' g')

The functorial map preserves composition.

theorem RS.modTensorAct_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M M' N N' : CategoryTheory.Mod D A} [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (modTensorAct A M N) (modTensorMap A f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorMap A f g)) (modTensorAct A M' N')

modTensorMap is a morphism of modules.

theorem RS.modTensorAct_map_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M M' N N' : CategoryTheory.Mod D A} [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (f : M ⟶ M') (g : N ⟶ N') {Z : D} (h : modTensor A M' N' ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorAct A M N) (CategoryTheory.CategoryStruct.comp (modTensorMap A f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorMap A f g)) (CategoryTheory.CategoryStruct.comp (modTensorAct A M' N') h)

modTensorMap is a morphism of modules.

noncomputable def RS.modTensorMapMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M M' N N' : CategoryTheory.Mod D A} [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (f : M ⟶ M') (g : N ⟶ N') : modTensorMod A M N ⟶ modTensorMod A M' N'

Functoriality, as a morphism of bundled modules.

Equations

• RS.modTensorMapMod A f g = CategoryTheory.Mod.Hom.mk' (RS.modTensorMap A f g) ⋯

noncomputable def RS.modTensorMapIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {M M' N N' : CategoryTheory.Mod D A} [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (e : M ≅ M') (f : N ≅ N') : modTensorMod A M N ≅ modTensorMod A M' N'

The relative tensor product of two module isomorphisms.

Equations

• RS.modTensorMapIso A e f = { hom := RS.modTensorMapMod A e.hom f.hom, inv := RS.modTensorMapMod A e.inv f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[reducible]

def RS.restrictRegular {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] : CategoryTheory.Mod D A

B as an A-module by restriction along φ, with underlying object reducibly B.

Equations

• RS.restrictRegular φ = { X := B, mod := CategoryTheory.Mod.scalarRestriction φ B }

theorem RS.actRight_restrictRegular {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj B] : actRight A B = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B φ) CategoryTheory.MonObj.mul

For commutative B, the braided right A-action on the restricted module is right multiplication through φ.

theorem RS.mul_actRight_restrictRegular {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj B] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (actRight A B)) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul A) (actRight A B))

Multiplication of B commutes with the right A-action on the restricted module.

noncomputable def RS.baseChange {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] (M : CategoryTheory.Mod D A) : D

Base change along φ: the extension B ⊗[A] M of an A-module M.

Equations

• RS.baseChange φ M = RS.modTensor A (RS.restrictRegular φ) M

@[implicit_reducible]

noncomputable def RS.baseChangeModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (M : CategoryTheory.Mod D A) [CategoryTheory.IsCommMonObj B] : CategoryTheory.ModObj B (baseChange φ M)

The B-module structure on the base change: multiplication on the left factor descends.

Equations

• RS.baseChangeModObj φ M = RS.modTensorDescModObj A (RS.restrictRegular φ) M B CategoryTheory.MonObj.mul ⋯ ⋯ ⋯

noncomputable def RS.baseChangeAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (M : CategoryTheory.Mod D A) [CategoryTheory.IsCommMonObj B] : CategoryTheory.MonoidalCategoryStruct.tensorObj B (baseChange φ M) ⟶ baseChange φ M

The action of B on the base change.

Equations

• RS.baseChangeAct φ M = CategoryTheory.ModObj.smul

@[simp]

theorem RS.whiskerLeft_modTensorπ_baseChangeAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (M : CategoryTheory.Mod D A) [CategoryTheory.IsCommMonObj B] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorπ A (restrictRegular φ) M)) (baseChangeAct φ M) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B M.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul M.X)) (modTensorπ A (restrictRegular φ) M)

Defining equation of the B-action on the base change.

theorem RS.whiskerLeft_modTensorπ_baseChangeAct_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (M : CategoryTheory.Mod D A) [CategoryTheory.IsCommMonObj B] {Z : D} (h : baseChange φ M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorπ A (restrictRegular φ) M)) (baseChangeAct φ M)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul M.X) (modTensorπ A (restrictRegular φ) M))) h

Defining equation of the B-action on the base change.

noncomputable def RS.baseChangeMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (M : CategoryTheory.Mod D A) [CategoryTheory.IsCommMonObj B] : CategoryTheory.Mod D B

Base change, bundled as a B-module.

Equations

• RS.baseChangeMod φ M = { X := RS.baseChange φ M, mod := RS.baseChangeModObj φ M }

@[simp]

theorem RS.baseChangeMod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B : D} [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (M : CategoryTheory.Mod D A) [CategoryTheory.IsCommMonObj B] : (baseChangeMod φ M).X = baseChange φ M