Concatenation of tensor powers and the block embedding #
X ^ ⊗ a ⊗ X ^ ⊗ b reassociates to X ^ ⊗ (a + b), and the
reassociation intertwines the permutation actions: a pair of
permutations acting on the two factors separately corresponds to
their block embedding into S_{a + b}.
The block embedding is conjugation by finSumFinEquiv, which sends
the Fin a summand to the first block {0, …, a − 1} by
Fin.castAdd and the Fin b summand to the last block by
Fin.natAdd; so σ permutes the first a slots and τ the last
b, matching the order of the tensor factors.
Both the embedding and the intertwiners are multiplicative, so the
intertwining reduces to the generator families (σ, 1) and (1, τ).
The first extends by extPerm one slot at a time, following the
recursion of the concatenation isomorphism; the second follows the
recursion of permMor itself, shifted into the last block — its top
cycle bubbles inside the last block only, which is the content of
the insertion lemma. The ℂ-bilinear extension to the group
algebras then holds on basis permutations and extends linearly.
The block embedding of symmetric groups #
The block embedding of S_a × S_b into S_{a + b}:
σ permutes the first a slots and τ the last b. The
convention is that of finSumFinEquiv, which carries the Fin a
summand onto {0, …, a − 1} by Fin.castAdd and the Fin b
summand onto {a, …, a + b − 1} by Fin.natAdd.
Equations
- RS.blockEmbed σ τ = finSumFinEquiv.permCongr (σ.sumCongr τ)
Instances For
On the first block the embedding acts by σ.
On the last block the embedding acts by τ.
The block embedding of the identities is the identity.
The block embedding is multiplicative: it is a homomorphism from the product group.
A block embedding splits into its two one-sided factors.
With an empty second block the embedding is the identity re-indexing.
Growing the second block by an unused slot extends the embedding by fixing the new top slot.
The block embedding of (1, τ) sends the top slot where τ
does, shifted into the last block.
The block embedding of (1, τ) induces the block embedding of
(1, restPerm τ) on the lower slots: the top split of the ambient
permutation happens entirely inside the last block.
The concatenation isomorphism #
The concatenation isomorphism
X ^ ⊗ a ⊗ X ^ ⊗ b ≅ X ^ ⊗ (a + b), by the recursion of
tensorPow itself: the empty second power is absorbed by the right
unitor, and one further factor reassociates off the second power and
whiskers the previous stage.
Equations
- One or more equations did not get rendered due to their size.
- RS.tensorPowConcat X a 0 = CategoryTheory.MonoidalCategoryStruct.rightUnitor (RS.tensorPow A X a)
Instances For
Concatenating with the empty power is the right unitor.
The defining recursion of tensorPowConcat.
Passing endomorphisms across one stage #
The successor stage of the concatenation is an associator followed
by a whiskering of the previous stage. Each helper is stated at
general objects and applied by exact, so that no tensor-power
arity enters the rewriting.
The concatenation isomorphism intertwines the top braiding
of the last block: braiding the top two slots of X ^ ⊗ (a + b + 2)
corresponds to braiding the top two slots of the second factor.
The concatenation isomorphism intertwines bubbling inside the last block: as long as the insertion distance stays within the second factor, inserting the top slot commutes with concatenation.
The intertwining on the first generator family: a permutation of the first block acts on the first tensor factor alone.
The intertwining on the second generator family: a
permutation of the last block acts on the second tensor factor
alone. The proof mirrors the recursion of permMor, shifted into
the last block by restPerm_blockEmbed and topImage_blockEmbed.
The concatenation isomorphism intertwines the block
embedding: under tensorPowConcat, the action of
blockEmbed σ τ on X ^ ⊗ (a + b) is the tensor product of the
actions of σ and τ on the two factors.
The linear extension #
The first-block embedding as a monoid homomorphism.
Equations
- RS.blockEmbedFstHom a b = { toFun := fun (σ : Equiv.Perm (Fin a)) => RS.blockEmbed σ 1, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The second-block embedding as a monoid homomorphism.
Equations
- RS.blockEmbedSndHom a b = { toFun := fun (τ : Equiv.Perm (Fin b)) => RS.blockEmbed 1 τ, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The block embedding of group algebras: the ℂ-bilinear
extension of blockEmbed, carrying a pair of group-algebra elements
to the product of their one-sided embeddings.
Equations
- RS.blockAlgEmbed x y = (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (RS.blockEmbedFstHom a b)) x * (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (RS.blockEmbedSndHom a b)) y
Instances For
On basis permutations the algebra embedding is the block embedding.
The algebra embedding is additive in the first argument.
The algebra embedding is homogeneous in the first argument.
The algebra embedding is additive in the second argument.
The algebra embedding is homogeneous in the second argument.
The concatenation isomorphism intertwines the block embedding
of group algebras: the ℂ-bilinear extension of the intertwining
on basis permutations. Both sides are bilinear in (x, y), so the
statement reduces to tensorPowConcat_permMor.