The symmetric-group action on a tensor power #
In a symmetric monoidal category, the tensor power X ^ ⊗ n carries
an action of S_n permuting its factors. Mathlib has the monoidal
coherence theorem but not the symmetric one, and no presentation of
S_n, so the action is built here by an explicit recursion that
makes no choice of word: the factor in the top slot is bubbled down
to its destination by adjacent braidings (insertTop), and the rest
is handled by the recursion at one lower arity (permMor).
The two primitives are the adjacent braiding on the top two slots
(swapTop) and the insertion cycle (insertTop). Functoriality of
the recursion follows from mere generation of S_n by the adjacent
transpositions — no presentation is needed — and the linear
structure then turns the action into the algebra map permAlg that
a tower's representation field asks for.
The adjacent braiding on the top two slots #
The top transposition: braid the last two factors of
X ^ ⊗ (n + 2). Reassociating exposes the last two tensorands, the
braiding exchanges them, and the associator is undone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The top transposition is an involution: the braiding of a symmetric category squares to the identity.
Bubbling the top factor down #
The insertion cycle: move the factor in the top slot of
X ^ ⊗ (n + 1) down to slot p, shifting slots p, …, n − 1 up by
one. It is defined by bubbling one slot at a time, so no word is
chosen: insertTop X n n is the identity, and each further step
composes one more top transposition, whiskered by the factors above
it. The recursion is on the gap n - p.
Equations
- RS.insertTop X x✝ 0 = CategoryTheory.CategoryStruct.id (RS.tensorPow A X (x✝ + 1))
- RS.insertTop X 0 n.succ = CategoryTheory.CategoryStruct.id (RS.tensorPow A X (0 + 1))
- RS.insertTop X n.succ k.succ = CategoryTheory.CategoryStruct.comp (RS.swapTop X n) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (RS.insertTop X n k) X)
Instances For
Bubbling by no steps is the identity.
At arity one there is nothing to bubble.
One bubbling step: braid the top factor past the one below it, then continue bubbling the result inside the lower part.
Bubbling down by one step is the top swap.
Disjoint slots commute #
The top braiding touches only the top two slots, so it commutes with anything acting on the factors below them. This is what lets the recursion be reorganised when a transposition and a permutation act on disjoint parts of a tensor power.
The top braiding commutes with morphisms below it. The braiding touches only the top two slots, so a morphism of the factors below them passes through. The computation is done at a general object, which keeps the tensor power's arity out of the rewrites.
The braid relation #
Two adjacent top braidings satisfy the braid relation. Reassociating
all three tensorands off the base turns both sides into the base
whiskered onto a morphism of X ⊗ (X ⊗ X), where the relation is
Mathlib's yang_baxter at three copies of X; the reassociation
itself is structural and is discharged by monoidal.
The braid relation for two adjacent top braidings.
The two bubblings and the braiding #
The identity the action's functoriality rests on: precomposing a pair of bubblings with the top braiding exchanges them. The first case is an induction on the arity, whose step is the braid relation together with the fact that the braiding commutes with what lies below it; the second case follows from the first because the braiding is an involution.
The braid identity, first case: when the top factor is bubbled at least as far as the one below it, the two bubblings and the braiding rearrange with the destinations shifted by one.
The braid identity, second case: when the top factor is inserted above the one below it, the two bubblings exchange with the braiding the other way round. It follows from the first case and the involutivity of the braiding.
The action #
A permutation acts by routing the factor in each slot to the slot it
names. The recursion splits off the top slot: the lower n factors
are permuted by restPerm σ, which places them in their compressed
target slots, and the top factor is then bubbled down into slot
topImage σ, which shifts the compressed slots at or above it up by
one — exactly recovering the true targets.
No word in the adjacent transpositions is chosen, so no word-independence is needed; functoriality instead follows from mere generation.
The permutation action on a tensor power: permMor X σ
routes the factor in slot i to slot σ i.
Equations
- RS.permMor X 0 x_2 = CategoryTheory.CategoryStruct.id (RS.tensorPow A X 0)
- RS.permMor X n.succ σ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (RS.permMor X n (RS.restPerm σ)) X) (RS.insertTop X n (n - ↑(RS.topImage σ)))
Instances For
The recursion equation.
The identity permutation acts as the identity.
A top-fixing permutation acts on the lower factors alone.
Functoriality against a top-fixing permutation, granted functoriality one arity down.
The cycles #
topCycle q is the permutation with trivial induced permutation, so
the recursion evaluates it to a single bubbling — which is what
insertTop was defined to be. The top transposition is the cycle at
the second-highest slot, so it acts by the top braiding.
A cycle acts by bubbling.
The top transposition acts by the top braiding. It is the cycle at the second-highest slot, one bubbling step.
The top transposition acts by the top braiding, in the form the generating set uses.
Whiskering the recursion equation by one more factor.
The top braiding passes the lower-lower permutation. Only the bubbling of the lower part can interact with the braiding of the top two slots; the permutation beneath it commutes through.
The top transposition #
Both sides of the generator identity for the top transposition carry the same permutation of the factors below the top two: the braiding commutes past it, and precomposing with the top transposition leaves the twice-restricted permutation alone. What is left is a relation between two bubblings and the braiding, with no permutation in it.
The generator identity for the top transposition, reduced. Granted the braid relation between the two bubblings, the action is functorial against the top transposition.
Functoriality against the top transposition. The two cases are whether the top slot's image lies above or below the image of the slot beneath it; each feeds the corresponding braid identity.
Functoriality #
Every permutation is a product of adjacent transpositions, and each of those is either top-fixing or the top transposition — both already handled. Since the action was defined canonically rather than through a chosen word, generation is all that is needed: no presentation of the symmetric group, and no coherence theorem.
The action is functorial. Composition of permutations goes to
composition of morphisms, in the order End multiplies.
The algebra map #
With functoriality in hand the action is a monoid homomorphism into the endomorphism monoid, and the universal property of the group algebra turns it into the algebra map a tower's representation field asks for. Only this last step needs the linear structure.
The action as a monoid homomorphism.
Equations
- RS.permHom X n = { toFun := RS.permMor X n, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The symmetric-group algebra acting on a tensor power.
Equations
- RS.permAlg X n = (MonoidAlgebra.lift ℂ (CategoryTheory.End (RS.tensorPow A X n)) (Equiv.Perm (Fin n))) (RS.permHom X n)
Instances For
The algebra map sends a group element to its action.