Splitting a permutation at the top slot

A permutation of Fin (n + 1) is determined by where it sends the top slot, Fin.last n, together with the permutation it induces on the remaining slots once both sides are compressed order-preservingly. This is the decomposition the symmetric-group action on a tensor power recurses on.

Equiv.Perm.decomposeFin is the analogous splitting at slot 0, but it compresses by swap 0 p rather than order-preservingly, so its induced permutation is not the one a tensor power's factors see. The compression here is finSuccAboveEquiv.

def RS.topImage {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) : Fin (n + 1)

Where a permutation sends the top slot.

Equations

• RS.topImage σ = σ (Fin.last n)

@[simp]

theorem RS.topImage_one {n : ℕ} : topImage 1 = Fin.last n

The identity leaves the top slot alone.

def RS.restPerm {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) : Equiv.Perm (Fin n)

The induced permutation of the remaining slots. Both the source slots other than the top one and the target slots other than topImage σ are compressed to Fin n order-preservingly, and σ carries one to the other.

Equations

• RS.restPerm σ = (finSuccAboveEquiv (Fin.last n)).trans ((Equiv.subtypeEquiv σ ⋯).trans (finSuccAboveEquiv (RS.topImage σ)).symm)

theorem RS.succAbove_restPerm {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) (j : Fin n) : (topImage σ).succAbove ((restPerm σ) j) = σ j.castSucc

The defining property of restPerm: reinserting the compressed image at topImage σ recovers the action of σ.

@[simp]

theorem RS.restPerm_one {n : ℕ} : restPerm 1 = 1

The identity induces the identity on the lower slots.

Permutations fixing the top slot

The standard embedding S_n ↪ S_{n+1}, extending by the identity on the top slot. It is the embedding symCast uses, so the tower's compatibility field sees exactly these permutations.

noncomputable def RS.extPerm {n : ℕ} (τ : Equiv.Perm (Fin n)) : Equiv.Perm (Fin (n + 1))

A permutation of the lower slots, extended by fixing the top slot.

Equations

• RS.extPerm τ = τ.viaEmbedding Fin.castSuccEmb

@[simp]

theorem RS.extPerm_castSucc {n : ℕ} (τ : Equiv.Perm (Fin n)) (j : Fin n) : (extPerm τ) j.castSucc = (τ j).castSucc

On a lower slot the extension acts by τ.

@[simp]

theorem RS.extPerm_last {n : ℕ} (τ : Equiv.Perm (Fin n)) : (extPerm τ) (Fin.last n) = Fin.last n

The extension fixes the top slot.

@[simp]

theorem RS.extPerm_mul {n : ℕ} (τ ρ : Equiv.Perm (Fin n)) : extPerm (τ * ρ) = extPerm τ * extPerm ρ

Extending by the top slot is a monoid map.

@[simp]

theorem RS.extPerm_one {n : ℕ} : extPerm 1 = 1

Extending the identity gives the identity.

@[simp]

theorem RS.topImage_mul_extPerm {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) (τ : Equiv.Perm (Fin n)) : topImage (σ * extPerm τ) = topImage σ

Precomposing with a permutation of the lower slots leaves the top slot's image alone.

theorem RS.restPerm_mul_extPerm {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) (τ : Equiv.Perm (Fin n)) : restPerm (σ * extPerm τ) = restPerm σ * τ

Precomposing with a permutation of the lower slots acts on the induced permutation by precomposition, with no interaction with the top slot.

@[simp]

theorem RS.topImage_extPerm {n : ℕ} (τ : Equiv.Perm (Fin n)) : topImage (extPerm τ) = Fin.last n

A top-fixing permutation fixes the top slot.

@[simp]

theorem RS.restPerm_extPerm {n : ℕ} (τ : Equiv.Perm (Fin n)) : restPerm (extPerm τ) = τ

A top-fixing permutation induces itself on the lower slots.

Iterating the standard embedding

The tower's compatibility field extends a permutation of Fin m all the way to Fin n in one step, along Fin.castLEEmb. The action recurses one slot at a time, so the two descriptions have to be identified: extending along Fin.castLEEmb is iterated extPerm.

theorem RS.viaEmbedding_viaEmbedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} (σ : Equiv.Perm α) (ι : α ↪ β) (κ : β ↪ γ) : (σ.viaEmbedding ι).viaEmbedding κ = σ.viaEmbedding (ι.trans κ)

Composing embeddings composes the extensions: extending a permutation along ι and then along κ extends it along the composite.

theorem RS.viaEmbedding_castLEEmb_succ {m k : ℕ} (σ : Equiv.Perm (Fin m)) : σ.viaEmbedding (Fin.castLEEmb ⋯) = extPerm (σ.viaEmbedding (Fin.castLEEmb ⋯))

One step of the standard embedding: extending a permutation of Fin m to Fin (m + k + 1) is extending it to Fin (m + k) and then fixing the new top slot.

Reassembling a permutation from its split

A target for the top slot together with a permutation of the rest determines a permutation. The cycle carrying the top slot to p is the case of trivial induced permutation, and the action's functoriality is proved along the factorisation into such a cycle after a top-fixing permutation.

noncomputable def RS.ofSplit {n : ℕ} (p : Fin (n + 1)) (τ : Equiv.Perm (Fin n)) : Equiv.Perm (Fin (n + 1))

The permutation sending the top slot to p and inducing τ on the rest.

Equations

• RS.ofSplit p τ = (finSuccEquiv' (Fin.last n)).trans ((Equiv.optionCongr τ).trans (finSuccEquiv' p).symm)

@[simp]

theorem RS.ofSplit_last {n : ℕ} (p : Fin (n + 1)) (τ : Equiv.Perm (Fin n)) : (ofSplit p τ) (Fin.last n) = p

The reassembled permutation sends the top slot to p.

@[simp]

theorem RS.ofSplit_castSucc {n : ℕ} (p : Fin (n + 1)) (τ : Equiv.Perm (Fin n)) (j : Fin n) : (ofSplit p τ) j.castSucc = p.succAbove (τ j)

On a lower slot the reassembled permutation acts by τ, reinserted above p.

@[simp]

theorem RS.topImage_ofSplit {n : ℕ} (p : Fin (n + 1)) (τ : Equiv.Perm (Fin n)) : topImage (ofSplit p τ) = p

The reassembled permutation has p as its top image.

@[simp]

theorem RS.restPerm_ofSplit {n : ℕ} (p : Fin (n + 1)) (τ : Equiv.Perm (Fin n)) : restPerm (ofSplit p τ) = τ

The reassembled permutation induces τ on the lower slots.

noncomputable def RS.topCycle {n : ℕ} (p : Fin (n + 1)) : Equiv.Perm (Fin (n + 1))

The cycle carrying the top slot down to p, shifting the slots at or above p up by one.

Equations

• RS.topCycle p = RS.ofSplit p 1

@[simp]

theorem RS.topImage_topCycle {n : ℕ} (p : Fin (n + 1)) : topImage (topCycle p) = p

The cycle carries the top slot to p.

@[simp]

theorem RS.restPerm_topCycle {n : ℕ} (p : Fin (n + 1)) : restPerm (topCycle p) = 1

The cycle induces the identity on the lower slots.

theorem RS.topCycle_zero {n : ℕ} : topCycle 0 = finRotate (n + 1)

The cycle carrying the top slot to the bottom is Mathlib's rotation: both send each lower slot one place up and the top slot to 0.

The adjacent transpositions

Equiv.Perm.mclosure_swap_castSucc_succ generates Perm (Fin (n+1)) as a submonoid from the transpositions of adjacent slots. Each of them is either top-fixing — and so an extPerm of an adjacent transposition one arity down — or the transposition of the top two slots, which is the cycle at the second-highest slot.

theorem RS.extPerm_swap {n : ℕ} (a b : Fin n) : extPerm (Equiv.swap a b) = Equiv.swap a.castSucc b.castSucc

Extending a transposition of the lower slots.

theorem RS.swap_castSucc_succ_castSucc {n : ℕ} (i : Fin n) : Equiv.swap i.castSucc.castSucc i.castSucc.succ = extPerm (Equiv.swap i.castSucc i.succ)

An adjacent transposition below the top is top-fixing.

theorem RS.topCycle_castSucc_last {n : ℕ} : topCycle (Fin.last n).castSucc = Equiv.swap (Fin.last n).castSucc (Fin.last (n + 1))

The transposition of the top two slots is the cycle at the second-highest slot.

Precomposing with the top transposition

The transposition of the top two slots exchanges the two source slots the action's recursion peels off first, so it exchanges the two targets they consume. Everything below them is untouched.

noncomputable def RS.topSwap {n : ℕ} : Equiv.Perm (Fin (n + 2))

The transposition of the top two slots.

Equations

• RS.topSwap = Equiv.swap (Fin.last n).castSucc (Fin.last (n + 1))

theorem RS.topSwap_eq_topCycle {n : ℕ} : topSwap = topCycle (Fin.last n).castSucc

The top transposition is the cycle at the second-highest slot.

@[simp]

theorem RS.topSwap_last {n : ℕ} : topSwap (Fin.last (n + 1)) = (Fin.last n).castSucc

The top transposition carries the top slot one place down.

@[simp]

theorem RS.topSwap_castSucc_last {n : ℕ} : topSwap (Fin.last n).castSucc = Fin.last (n + 1)

The top transposition carries the slot below the top one place up.

@[simp]

theorem RS.topSwap_castSucc_castSucc {n : ℕ} (j : Fin n) : topSwap j.castSucc.castSucc = j.castSucc.castSucc

The top transposition fixes every slot below the top two.

theorem RS.topImage_mul_topSwap {n : ℕ} (σ : Equiv.Perm (Fin (n + 2))) : topImage (σ * topSwap) = (topImage σ).succAbove (topImage (restPerm σ))

The top slot's new image: precomposing with the top transposition sends the top slot where the slot below it went.

theorem RS.succAbove_topImage_restPerm_mul_topSwap {n : ℕ} (σ : Equiv.Perm (Fin (n + 2))) : (topImage (σ * topSwap)).succAbove (topImage (restPerm (σ * topSwap))) = topImage σ

The two consumed targets are exchanged: reinserting the new second target recovers the old first one.

theorem RS.topImage_restPerm_mul_topSwap {n : ℕ} (σ : Equiv.Perm (Fin (n + 2))) : topImage (restPerm (σ * topSwap)) = (topImage (restPerm σ)).predAbove (topImage σ)

The new second target is the old first one, compressed. This is the Fin simplicial identity: reinserting m.predAbove p at p.succAbove m recovers p.

theorem RS.restPerm_restPerm_mul_topSwap {n : ℕ} (σ : Equiv.Perm (Fin (n + 2))) : restPerm (restPerm (σ * topSwap)) = restPerm (restPerm σ)

Nothing below the top two slots moves. Precomposing with the top transposition exchanges the two targets the top two source slots consume, but the order-preserving embedding of the remaining slots into their complement is the same either way, so the twice-restricted permutation is unchanged.

The two consumed targets, by value

The bubbling distances the action's recursion uses are n minus these values, so the braid identity is fed them in numeric form. The two cases are whether the top slot's image lies above or below the image of the slot beneath it.

theorem RS.topImage_mul_topSwap_val_of_lt {n : ℕ} (σ : Equiv.Perm (Fin (n + 2))) (h : (topImage (restPerm σ)).castSucc < topImage σ) : ↑(topImage (σ * topSwap)) = ↑(topImage (restPerm σ))

Above the threshold, the top slot's new image is the old inner one.

theorem RS.topImage_restPerm_mul_topSwap_val_of_lt {n : ℕ} (σ : Equiv.Perm (Fin (n + 2))) (h : (topImage (restPerm σ)).castSucc < topImage σ) : ↑(topImage (restPerm (σ * topSwap))) = ↑(topImage σ) - 1

Above the threshold, the new inner image is the old top one, lowered by one.

theorem RS.topImage_mul_topSwap_val_of_le {n : ℕ} (σ : Equiv.Perm (Fin (n + 2))) (h : topImage σ ≤ (topImage (restPerm σ)).castSucc) : ↑(topImage (σ * topSwap)) = ↑(topImage (restPerm σ)) + 1

Below the threshold, the top slot's new image is the old inner one, raised by one.

theorem RS.topImage_restPerm_mul_topSwap_val_of_le {n : ℕ} (σ : Equiv.Perm (Fin (n + 2))) (h : topImage σ ≤ (topImage (restPerm σ)).castSucc) : ↑(topImage (restPerm (σ * topSwap))) = ↑(topImage σ)

Below the threshold, the new inner image is the old top one.