Composition of permutation fragments

The multiplication law of the symmetric-group generators (accompanying paper §3.1): composing permutation fragments composes the permutations, Pσ ∘ Pτ ≃ P(τσ). The proof is pure calculus: a permutation fragment is the strand bundle with outgoing labels permuted (permFragmentRelabelOutPerm), the outgoing permutation crosses the interface by interfaceShift, the bare bundle is absorbed by the identity law, and the residual incoming permutation is traded for a strand re-indexing of the bundle (strandBundleRelabelBoth), which is invisible up to equivalence.

noncomputable def RS.permFragmentRelabelOutPerm {t : ℕ} (σ : Equiv.Perm (Fin t)) : (permFragment σ).Equiv ((strandBundle t).relabel (outPermEquiv t σ))

A permutation fragment is the strand bundle with its outgoing labels permuted by outPermEquiv.

Equations

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

noncomputable def RS.strandBundleRelabelBoth {t : ℕ} (δ : Equiv.Perm (Fin t)) : ((strandBundle t).relabel ((inPermEquiv δ t).trans (outPermEquiv t δ))).Equiv (strandBundle t)

Re-indexing the strands of the bundle — permuting both ends of each strand by the same permutation — is invisible up to equivalence.

Equations

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

theorem RS.outPerm_shift_both {t : ℕ} (σ τ : Equiv.Perm (Fin t)) : (outPermEquiv t τ).trans (inPermEquiv (Equiv.symm σ) t) = ((inPermEquiv (Equiv.symm σ) t).trans (outPermEquiv t (Equiv.symm σ))).trans (outPermEquiv t (τ * σ))

Label algebra: shifting the outgoing permutation τ across the interface against σ re-associates into a strand re-indexing by σ⁻¹ followed by the outgoing composite permutation.

noncomputable def RS.permFragmentCompose {t : ℕ} (σ τ : Equiv.Perm (Fin t)) : ((permFragment σ).compose (permFragment τ)).Equiv (permFragment (τ * σ))

Permutation fragments compose (accompanying paper §3.1): the composition of the permutation fragments of σ and τ is the permutation fragment of the composite τ * σ (first through σ, then through τ).

Equations

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