Module powers over the unit monoid

Over the trivial monoid the module relations collapse: both slot legs are the same unitor slide, the assembled relation pair is equal, and the module power projection is an isomorphism onto the plain tensor power. Symmetric powers of a bare object are thereby the general machinery instantiated at the unit, with every multiplication law inherited — the substrate of the local splitting algebra.

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

Over the unit monoid the action is the left unitor.

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

Over the unit monoid the braided right action is the right unitor.

theorem RS.winLeg_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (X : D) : winLegM (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X = winLegN (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X

Over the unit monoid the two slot legs coincide.

theorem RS.modPowLeg_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (X : D) (n : ℕ) : modPowLegFst (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X n = modPowLegSnd (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X n

Over the unit monoid the assembled relation legs coincide.

noncomputable def RS.modPowUnitIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X : D) (n : ℕ) : modPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X n ≅ tensorPow D X n

The module power over the unit monoid is the plain tensor power: the relation pair is equal, so the coequalizer collapses onto its target.

Equations

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

instance RS.instIsIsoModPowπTensorUnit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X : D) (n : ℕ) : CategoryTheory.IsIso (modPowπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X n)

The projection onto the module power over the unit monoid is invertible.