Sliding a head along a word of free letters

The head of a free letter splits off as a trailing scalar and slides into the next letter. Splitting and acting back on the same letter is the identity, so the slot relation of the module power says exactly that the slide is invisible after the projection.

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

Splitting the head off a free letter: the head becomes a trailing scalar and the letter keeps the unit.

Equations

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

theorem RS.freeSplit_actRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) : CategoryTheory.CategoryStruct.comp (freeSplit A V) (actRight A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)

Splitting and acting back is the identity: the scalar returns to the head it came from.

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

The slide window: split the head off the first letter and act with it on the second.

Equations

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

theorem RS.freeSplit_winLegM {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (freeSplit A V) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) (winLegM A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) (CategoryTheory.MonoidalCategoryStruct.tensorObj A V))

Splitting and acting back through the first slot leg is the identity of the window.

theorem RS.freeSlideWin_modPowπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {n : ℕ} (a b : ℕ) (hab : a + 2 + b = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) a) (freeSlideWin A V)) (tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) b)) (CategoryTheory.CategoryStruct.comp (modPowGlue (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) a b) (CategoryTheory.CategoryStruct.comp (powCast (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) hab) (modPowπ A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) n))) = CategoryTheory.CategoryStruct.comp (modPowGlue (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) a b) (CategoryTheory.CategoryStruct.comp (powCast (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) hab) (modPowπ A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) n))

The slide is invisible in the module power: it is the difference of the two slot legs at a window whose first leg is the identity.

noncomputable def RS.freeSlideTop {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (k : ℕ) : tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) (k + 2) ⟶ tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) (k + 2)

The top slide: slide the head of the penultimate letter into the last one.

Equations

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

theorem RS.freeSlideTop_modPowπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (k : ℕ) : CategoryTheory.CategoryStruct.comp (freeSlideTop A V k) (modPowπ A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) (k + 2)) = modPowπ A (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) (k + 2)

The top slide is invisible in the module power.