Modules over the tensor unit

Over the tensor unit as base algebra, relative module theory collapses to the ambient category.

• unitMod: any object, as a module over the unit through the trivial action; the unit law forces the action of any module over the unit to be the left unitor (modObj_unitBase_smul).
• modTensorUnitBase: over the trivial base the two coequalizer legs agree, so the module tensor product collapses to the plain tensor product of the carriers.
• freeModUnitBase: the free module on V over the unit is V itself, via the left unitor.
• modBiprodZeroLeft: over any base, the biproduct with a module whose carrier is zero collapses to the other summand.

def RS.unitMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) : CategoryTheory.Mod D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

Any object, as a module over the tensor unit through the trivial action.

Equations

• RS.unitMod X = { X := X, mod := CategoryTheory.ModObj.instTensorUnit X }

@[simp]

theorem RS.unitMod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) : (unitMod X).X = X

theorem RS.modObj_unitBase_smul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) [inst : CategoryTheory.ModObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X] : CategoryTheory.ModObj.smul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom

Any action of the tensor unit is the left unitor: the unit law forces it, since the unit of the trivial base is the identity. The instance is quantified, so the lemma applies to the action of any module over the unit, not only the trivial one.

theorem RS.actLeft_unitBase {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) [inst : CategoryTheory.ModObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X] : actLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom

The action of any module over the unit, in actLeft form.

theorem RS.actRight_unitBase {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (X : D) [inst : CategoryTheory.ModObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X] : actRight (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom

The braided right action of any module over the unit is the right unitor.

theorem RS.modTensorLegM_unitBase_eq {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) : modTensorLegM (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) M N = modTensorLegN (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) M N

Over the trivial base the two coequalizer legs of the module tensor product are equal morphisms.

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

Over the trivial base the module tensor product is the plain tensor product: the coequalizer of a pair of equal legs is the target itself.

Equations

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

@[simp]

theorem RS.modTensorUnitBase_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) [CategoryTheory.Limits.HasCoequalizers D] : (modTensorUnitBase M N).hom = modTensorDesc (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) M N (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X)) ⋯

@[simp]

theorem RS.modTensorUnitBase_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (M N : CategoryTheory.Mod D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) [CategoryTheory.Limits.HasCoequalizers D] : (modTensorUnitBase M N).inv = modTensorπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) M N

theorem RS.freeModUnitBase_linear {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).hom V)) (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom) (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom

The left unitor intertwines the free action over the unit with the trivial action.

theorem RS.freeModUnitBase_linear_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).hom V))

The left unitor intertwines the trivial action with the free action over the unit.

noncomputable def RS.freeModUnitBase {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (V : D) : freeMod (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V ≅ unitMod V

The free module over the trivial base is its generator, via the left unitor.

Equations

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

noncomputable def RS.modBiprodZeroLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (Z N : CategoryTheory.Mod D A) (hZ : CategoryTheory.Limits.IsZero Z.X) : modBiprod A Z N ≅ N

Collapse of a zero summand: over any base, the module biproduct with a module whose carrier is zero is the other summand.

Equations

• RS.modBiprodZeroLeft A Z N hZ = { hom := RS.modBiprodSnd A Z N, inv := RS.modBiprodInr A Z N, hom_inv_id := ⋯, inv_hom_id := ⋯ }