Point powers and the trivial permutation action on unit strands

The tensor powers of a point of an object, and their invariance under the permutation action: permutations act trivially on powers of the unit object, and naturality carries the invariance onto the point powers. In a rigid category the point powers of a monomorphism are monomorphisms. The substrate of the nonvanishing of the local splitting algebra.

theorem RS.swapTop_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (n : ℕ) : swapTop (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) n = CategoryTheory.CategoryStruct.id (tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (n + 2))

The top transposition on a power of the unit is the identity.

theorem RS.permMor_unit_adjSwap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (n : ℕ) (i : Fin (n + 1)) : permMor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (n + 2) (Equiv.swap i.castSucc i.succ) = CategoryTheory.CategoryStruct.id (tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (n + 2))

Every adjacent transposition acts trivially on a power of the unit.

theorem RS.permMor_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (n : ℕ) (σ : Equiv.Perm (Fin n)) : permMor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) n σ = CategoryTheory.CategoryStruct.id (tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) n)

Permutations act trivially on powers of the unit: every adjacent transposition does, and the action and the trivial character are both multiplicative.

noncomputable def RS.unitPow {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (n : ℕ) : tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) n ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

The powers of the unit collapse onto the unit.

Equations

• RS.unitPow 0 = CategoryTheory.Iso.refl (RS.tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) 0)
• RS.unitPow n.succ = CategoryTheory.MonoidalCategoryStruct.rightUnitor (RS.tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) n) ≪≫ RS.unitPow n

noncomputable def RS.tensorPowPoint {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {Y : D} (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ tensorPow D Y n

The power of a point: the collapsed unit power carried into the power of the target.

Equations

• RS.tensorPowPoint pt n = CategoryTheory.CategoryStruct.comp (RS.unitPow n).inv (RS.tensorPowMap pt n)

theorem RS.tensorPowPoint_mono {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {Y : D} (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) [CategoryTheory.RigidCategory D] [CategoryTheory.Mono pt] (n : ℕ) : CategoryTheory.Mono (tensorPowPoint pt n)

In a rigid category the power of a monic point is monic.

theorem RS.tensorPowPoint_mono' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {Y : D} (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) [∀ (Z : D), (CategoryTheory.MonoidalCategory.tensorLeft Z).PreservesMonomorphisms] [∀ (Z : D), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms] [CategoryTheory.Mono pt] (n : ℕ) : CategoryTheory.Mono (tensorPowPoint pt n)

The power of a monic point is monic, from mono preservation of the tensor factors alone.

theorem RS.tensorPowPoint_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {Y : D} (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) : tensorPowPoint pt 0 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

The empty point power is the identity.

theorem RS.tensorPowPoint_succ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {Y : D} (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) (n : ℕ) : tensorPowPoint pt (n + 1) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowPoint pt n) pt)

The recursion of the point powers: one more letter joins on the right.

theorem RS.tensorPowPoint_concat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {Y : D} (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) (m n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowPoint pt m) (tensorPowPoint pt n)) (tensorPowConcat Y m n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).hom (tensorPowPoint pt (m + n))

Point powers concatenate: the tensor of two point powers meets the concatenation as the joint point power.

theorem RS.tensorPowPoint_permMor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] {Y : D} (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) (n : ℕ) (σ : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (tensorPowPoint pt n) (permMor Y n σ) = tensorPowPoint pt n

The permutation action fixes point powers: naturality carries the action onto the unit strands, where it is trivial.

theorem RS.tensorPowPoint_symPowIdem {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (tensorPowPoint pt n) (CategoryTheory.CategoryStruct.comp (modPowπ A X n) (symPowIdem A X n)) = CategoryTheory.CategoryStruct.comp (tensorPowPoint pt n) (modPowπ A X n)

The symmetriser fixes point powers in the module power: every permutation fixes them, so their average does.

theorem RS.point_symPow_ne_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.RigidCategory D] (X : D) (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ X) [CategoryTheory.Mono pt] (h1 : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (tensorPowPoint pt n) (CategoryTheory.CategoryStruct.comp (modPowπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X n) (symPowπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X n)) ≠ 0

Nonvanishing of point powers in symmetric powers over the unit monoid: for a monic point of an object in a rigid category with nonzero unit, no symmetrised point power vanishes.

theorem RS.point_symPow_ne_zero' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (X : D) [∀ (Z : D), (CategoryTheory.MonoidalCategory.tensorLeft Z).PreservesMonomorphisms] [∀ (Z : D), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms] (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ X) [CategoryTheory.Mono pt] (h1 : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (tensorPowPoint pt n) (CategoryTheory.CategoryStruct.comp (modPowπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X n) (symPowπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X n)) ≠ 0

The nonvanishing of symmetrised point powers, from mono preservation of the tensor factors alone.