The sign action on tensor powers of an odd line

The permutation action on a tensor power of an odd line is the sign character. The line's self-braiding is −1, so the top braiding of any tensor power is the negated identity; every adjacent transposition therefore acts by −1, and functoriality of the action, together with generation of the symmetric group by the adjacent transpositions, forces a general permutation to act by its sign. The linear extension evaluates the group algebra's action on a single group element accordingly.

theorem RS.oddLine_swapTop {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (n : ℕ) : swapTop L.obj n = -CategoryTheory.CategoryStruct.id (tensorPow D L.obj (n + 2))

The top braiding of an odd line's tensor power is −1: the braiding of the top two factors is the line's self-braiding, whiskered by the factors below, and negation passes through the whiskering.

theorem RS.oddLine_permMor_adjSwap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (n : ℕ) (i : Fin (n + 1)) : permMor L.obj (n + 2) (Equiv.swap i.castSucc i.succ) = -CategoryTheory.CategoryStruct.id (tensorPow D L.obj (n + 2))

Every adjacent transposition acts by −1 on a tensor power of an odd line: the top one is the top braiding, and the lower ones are whiskered copies of the same evaluation one arity down.

theorem RS.oddLine_permMor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] (L : OddLine D) (n : ℕ) (σ : Equiv.Perm (Fin n)) : permMor L.obj n σ = ↑↑(Equiv.Perm.sign σ) • CategoryTheory.CategoryStruct.id (tensorPow D L.obj n)

The permutation action on a tensor power of an odd line is the sign character. Both the action and the sign are multiplicative, and every adjacent transposition acts by −1, so generation of the symmetric group by the adjacent transpositions gives the general permutation.