Young subgroups of symmetric groups

For a partition μ of n, this file defines its Young subgroup of Equiv.Perm (Fin n). The decreasing parts of μ cut Fin n into consecutive blocks, and the Young subgroup consists exactly of the permutations preserving those blocks. We identify it with the product of the symmetric groups on the individual blocks and compute its cardinality and index. Counting the labels lying in the first k blocks recovers the partial sums of the decreasing parts (TauCeti.card_filter_youngBlock_lt), which is the form in which the parts enter the dominance order.

The Young subgroups of the shapes that have a name are computed here as well: the coarsest shape (n) gives the whole symmetric group, the finest shape (1ⁿ) the trivial subgroup, and the shape (n+1, 1) the stabilizer of the last label (TauCeti.youngSubgroup_singletonSecondRow), its two blocks being all the labels but the last one and the last one alone.

The construction uses Mathlib's finSigmaFinEquiv to enumerate the consecutive blocks and DomMulAct.stabilizerMulEquiv to decompose their stabilizer.

The consecutive-block design and the principal declaration signatures follow TauCetiRoadmap/RepresentationTheory/SchurWeyl/README.md and its Suggested.lean.

noncomputable def TauCeti.youngBlocksEquiv {n : ℕ} (μ : n.Partition) : (i : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) × Fin ((μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).get i) ≃ Fin n

The equivalence which enumerates the consecutive blocks whose sizes are the decreasing parts of μ.

The coordinate ⟨i, j⟩ denotes position j in block i.

Equations

• TauCeti.youngBlocksEquiv μ = finSigmaFinEquiv.trans (finCongr ⋯)

@[simp]

theorem TauCeti.youngBlocksEquiv_apply {n : ℕ} (μ : n.Partition) (x : (i : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) × Fin ((μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).get i)) : ↑((youngBlocksEquiv μ) x) = ∑ i : Fin ↑x.fst, (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).get (Fin.castLE ⋯ i) + ↑x.snd

The consecutive-block equivalence sends a local coordinate to the preceding block sizes plus that coordinate.

noncomputable def TauCeti.youngBlock {n : ℕ} (μ : n.Partition) (j : Fin n) : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length

The block containing an element of Fin n.

Equations

• TauCeti.youngBlock μ j = ((TauCeti.youngBlocksEquiv μ).symm j).fst

@[simp]

theorem TauCeti.youngBlock_youngBlocksEquiv {n : ℕ} (μ : n.Partition) (x : (i : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) × Fin ((μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).get i)) : youngBlock μ ((youngBlocksEquiv μ) x) = x.fst

The block-coordinate equivalence sends a local coordinate to its block label.

noncomputable def TauCeti.youngBlockEquiv {n : ℕ} (μ : n.Partition) (i : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[↑i] ≃ { j : Fin n // youngBlock μ j = i }

The local coordinates in block i are equivalent to the fiber of youngBlock μ over i.

Equations

• TauCeti.youngBlockEquiv μ i = Equiv.ofBijective (fun (j : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[↑i]) => ⟨(TauCeti.youngBlocksEquiv μ) ⟨i, j⟩, ⋯⟩) ⋯

@[simp]

theorem TauCeti.youngBlockEquiv_apply {n : ℕ} (μ : n.Partition) (i : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) (j : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[↑i]) : (youngBlockEquiv μ i) j = ⟨(youngBlocksEquiv μ) ⟨i, j⟩, ⋯⟩

The block-fiber equivalence is the consecutive-block equivalence with its block-membership proof.

theorem TauCeti.card_filter_youngBlock_lt {n : ℕ} (μ : n.Partition) (k : ℕ) : {x : Fin n | ↑(youngBlock μ x) < k}.card = (List.take k (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).sum

The labels whose μ-block is among the first k are as many as the first k parts of μ add up to.

noncomputable def TauCeti.youngSubgroup {n : ℕ} (μ : n.Partition) : Subgroup (Equiv.Perm (Fin n))

The Young subgroup associated to μ, acting independently on the consecutive blocks whose sizes are the decreasing parts of μ.

Equations

• TauCeti.youngSubgroup μ = (MulAction.stabilizer (Equiv.Perm (Fin n))ᵈᵐᵃ (TauCeti.youngBlock μ)).unop

noncomputable def TauCeti.youngSubgroupMulEquiv {n : ℕ} (μ : n.Partition) : ↥(youngSubgroup μ) ≃* ((i : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) → Equiv.Perm (Fin ((μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).get i)))

The Young subgroup is the product of the symmetric groups on its consecutive blocks.

Equations

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

@[simp]

theorem TauCeti.youngSubgroupMulEquiv_apply_youngBlocksEquiv {n : ℕ} (μ : n.Partition) (σ : ↥(youngSubgroup μ)) (i : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) (j : Fin ((μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).get i)) : (youngBlocksEquiv μ).symm (↑σ ((youngBlocksEquiv μ) ⟨i, j⟩)) = ⟨i, ((youngSubgroupMulEquiv μ) σ i) j⟩

The product decomposition records the local coordinate induced on each consecutive block.

@[simp]

theorem TauCeti.youngSubgroupMulEquiv_symm_apply_youngBlocksEquiv {n : ℕ} (μ : n.Partition) (p : (i : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) → Equiv.Perm (Fin ((μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).get i))) (i : Fin (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) (j : Fin ((μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).get i)) : ↑((youngSubgroupMulEquiv μ).symm p) ((youngBlocksEquiv μ) ⟨i, j⟩) = (youngBlocksEquiv μ) ⟨i, (p i) j⟩

The inverse product decomposition acts on each consecutive block by the corresponding permutation.

theorem TauCeti.card_youngSubgroup {n : ℕ} (μ : n.Partition) : Nat.card ↥(youngSubgroup μ) = (Multiset.map Nat.factorial μ.parts).prod

The order of a Young subgroup is the product of the factorials of the parts.

@[simp]

theorem TauCeti.mem_youngSubgroup_iff {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : σ ∈ youngSubgroup μ ↔ youngBlock μ ∘ ⇑σ = youngBlock μ

Membership in the Young subgroup is equivalent to preserving the consecutive-block label.

theorem TauCeti.youngSubgroup_eq_fiberSubgroup {n : ℕ} (μ : n.Partition) : youngSubgroup μ = fiberSubgroup (youngBlock μ)

The Young subgroup is the subgroup preserving the fibers of its consecutive-block map.

theorem TauCeti.youngSubgroup_index_mul {n : ℕ} (μ : n.Partition) : (youngSubgroup μ).index * (Multiset.map Nat.factorial μ.parts).prod = n.factorial

The index of a Young subgroup times its order is n!.

@[simp]

theorem TauCeti.youngSubgroup_indiscrete (n : ℕ) : youngSubgroup (Nat.Partition.indiscrete n) = ⊤

The Young subgroup of the coarsest partition (n) is the whole symmetric group: its at most one block imposes no condition.

@[simp]

theorem TauCeti.youngSubgroup_ones (n : ℕ) : youngSubgroup (Nat.Partition.ones n) = ⊥

The Young subgroup of the all-ones partition (1ⁿ) is trivial: every block is a singleton, so only the identity preserves them all.

theorem TauCeti.youngSubgroup_index {n : ℕ} (μ : n.Partition) : (youngSubgroup μ).index = n.factorial / (Multiset.map Nat.factorial μ.parts).prod

The index of a Young subgroup is the multinomial quotient by the factorials of the parts.

The shape (n+1, 1)

The blocks of Nat.Partition.singletonSecondRow n = (n+1, 1) are the first n+1 labels and the last one, so its Young subgroup is the stabilizer of Fin.last (n+1).

@[simp]

theorem TauCeti.youngBlock_singletonSecondRow_last (n : ℕ) : ↑(youngBlock (Nat.Partition.singletonSecondRow n) (Fin.last (n + 1))) = 1

The last label lies in the second block of the shape (n+1, 1). The blocks are consecutive with sizes n+1 and 1, so the block-coordinate equivalence sends the single coordinate of the second block to Fin.last (n+1).

@[simp]

theorem TauCeti.youngBlock_singletonSecondRow_eq_zero (n : ℕ) {x : Fin (n + 2)} (hx : x ≠ Fin.last (n + 1)) : ↑(youngBlock (Nat.Partition.singletonSecondRow n) x) = 0

Every other label lies in the first block of the shape (n+1, 1). The first block has n+1 of the n+2 labels, so its complement is the single label already located by TauCeti.youngBlock_singletonSecondRow_last.

@[simp]

theorem TauCeti.youngSubgroup_singletonSecondRow (n : ℕ) : youngSubgroup (Nat.Partition.singletonSecondRow n) = MulAction.stabilizer (Equiv.Perm (Fin (n + 2))) (Fin.last (n + 1))

The Young subgroup of the shape (n+1, 1) is a point stabilizer. Its blocks are the last label alone and all the others, so a permutation preserves them exactly when it fixes the last label.