Wreath Product Orbits and Young Diagrams (Lemma 6.8)

This file formalizes Lemma 6.8 from Stanley's Algebraic Combinatorics: every orbit of the wreath product G_{mn} = Sₙ ≀ Sₘ acting on subsets of the m × n rectangle contains exactly one Young diagram.

The wreath product G_{mn} acts on Fin m × Fin n by permuting elements within each row (via Sₙ) and permuting rows (via Sₘ). Two subsets are in the same orbit if and only if they have the same multiset of row sizes.

Main results

• WreathOrbits.WreathElem: The wreath product G_{mn} = Sₙ ≀ Sₘ acting on the grid.
• WreathOrbits.SameOrbit: Two subsets are in the same G_{mn}-orbit.
• WreathOrbits.sameOrbit_iff_rowSizeMultiset_eq: Two subsets are in the same orbit iff they have the same multiset of row sizes.
• WreathOrbits.gridYoung_unique: Two Young diagrams in the grid with the same row-size multiset are equal (uniqueness part of Lemma 6.8).
• WreathOrbits.exists_gridYoung_of_rowSizeMultiset: For any subset of the grid, there exists a Young diagram with the same row-size multiset (existence part).
• WreathOrbits.existsUnique_gridYoung_sameOrbit: Every orbit of G_{mn} contains exactly one Young diagram.

Row sizes and multisets

def WreathOrbits.rowSize {m n : ℕ} (S : Finset (Fin m × Fin n)) (i : Fin m) : ℕ

The number of elements in row i of a subset S ⊆ Fin m × Fin n.

def WreathOrbits.rowSizeMultiset {m n : ℕ} (S : Finset (Fin m × Fin n)) : Multiset ℕ

The multiset of row sizes of a subset S ⊆ Fin m × Fin n.

Wreath product action

The wreath product G_{mn} = Sₙ ≀ Sₘ is represented by a pair (σ, τ) where σ : Perm (Fin m) permutes rows and τ i : Perm (Fin n) permutes elements within row i. The action on the grid Fin m × Fin n sends (i, j) to (σ i, τ i j).

structure WreathOrbits.WreathElem (m n : ℕ) : Type

An element of the wreath product G_{mn} = Sₙ ≀ Sₘ, represented as a row permutation σ and a family of within-row permutations τ.

• σ : Equiv.Perm (Fin m)

  The row permutation σ ∈ Sₘ.

• τ : Fin m → Equiv.Perm (Fin n)

  The within-row permutations τ_i ∈ Sₙ for each row i.

def WreathOrbits.WreathElem.actOn {m n : ℕ} (g : WreathElem m n) (p : Fin m × Fin n) : Fin m × Fin n

The wreath product action on the grid: (i, j) ↦ (σ i, τ i j). This first permutes within row i (applying τ i), then permutes rows (applying σ).

def WreathOrbits.WreathElem.actOnSet {m n : ℕ} (g : WreathElem m n) (S : Finset (Fin m × Fin n)) : Finset (Fin m × Fin n)

The induced action on subsets of the grid.

def WreathOrbits.SameOrbit {m n : ℕ} (S T : Finset (Fin m × Fin n)) : Prop

Two subsets S and T of the grid are in the same G_{mn}-orbit if some wreath product element maps S to T.

theorem WreathOrbits.WreathElem.actOn_injective {m n : ℕ} (g : WreathElem m n) : Function.Injective g.actOn

The wreath product action on grid points is injective.

theorem WreathOrbits.rowSize_actOnSet {m n : ℕ} (g : WreathElem m n) (S : Finset (Fin m × Fin n)) (i : Fin m) : rowSize (g.actOnSet S) (g.σ i) = rowSize S i

The wreath product action preserves row sizes: the size of row σ i in the image equals the size of row i in the original set.

def WreathOrbits.rowCols {m n : ℕ} (S : Finset (Fin m × Fin n)) (i : Fin m) : Finset (Fin n)

The set of columns occupied in row i of a subset S.

theorem WreathOrbits.mem_rowCols_iff {m n : ℕ} (S : Finset (Fin m × Fin n)) (i : Fin m) (j : Fin n) : j ∈ rowCols S i ↔ (i, j) ∈ S

theorem WreathOrbits.rowCols_card {m n : ℕ} (S : Finset (Fin m × Fin n)) (i : Fin m) : (rowCols S i).card = rowSize S i

theorem WreathOrbits.exists_perm_image_eq {n : ℕ} (A B : Finset (Fin n)) (h : A.card = B.card) : ∃ (σ : Equiv.Perm (Fin n)), Finset.image (⇑σ) A = B

Given two finsets of Fin n with the same cardinality, there is a permutation of Fin n mapping one to the other.

theorem WreathOrbits.fiber_card_eq {m n : ℕ} (S T : Finset (Fin m × Fin n)) (h : rowSizeMultiset S = rowSizeMultiset T) (v : ℕ) : Fintype.card { i : Fin m // rowSize S i = v } = Fintype.card { i : Fin m // rowSize T i = v }

Equal row-size multisets imply equal fiber cardinalities.

Forward direction: same orbit implies same row-size multiset

theorem WreathOrbits.rowSizeMultiset_eq_of_sameOrbit {m n : ℕ} (S T : Finset (Fin m × Fin n)) (h : SameOrbit S T) : rowSizeMultiset S = rowSizeMultiset T

If two subsets are in the same G_{mn}-orbit, they have the same row-size multiset.

Backward direction: same row-size multiset implies same orbit

theorem WreathOrbits.sameOrbit_of_rowSizeMultiset_eq {m n : ℕ} (S T : Finset (Fin m × Fin n)) (h : rowSizeMultiset S = rowSizeMultiset T) : SameOrbit S T

If two subsets have the same row-size multiset, they are in the same G_{mn}-orbit. The proof constructs a wreath product element by:

1. Using fiber equivalences to build a row permutation σ matching row sizes.
2. For each row, building a column permutation τ_i mapping occupied columns.

theorem WreathOrbits.sameOrbit_iff_rowSizeMultiset_eq {m n : ℕ} (S T : Finset (Fin m × Fin n)) : SameOrbit S T ↔ rowSizeMultiset S = rowSizeMultiset T

Two subsets of the m × n grid are in the same G_{mn}-orbit if and only if they have the same multiset of row sizes.

theorem WreathOrbits.rowSize_le {m n : ℕ} (S : Finset (Fin m × Fin n)) (i : Fin m) : rowSize S i ≤ n

Row sizes are bounded by n.

Left-justified subsets and Young diagrams

def WreathOrbits.IsLeftJustified {m n : ℕ} (S : Finset (Fin m × Fin n)) : Prop

A subset S of the grid is left-justified if whenever (i, j) ∈ S and j' < j, then (i, j') ∈ S.

def WreathOrbits.IsGridYoung {m n : ℕ} (S : Finset (Fin m × Fin n)) : Prop

A subset S is a Young diagram in the grid if it is left-justified and its row sizes are weakly decreasing (antitone).

Left-justified sets are determined by row sizes

theorem WreathOrbits.mem_iff_lt_rowSize {m n : ℕ} {S : Finset (Fin m × Fin n)} (hS : IsLeftJustified S) (i : Fin m) (j : Fin n) : (i, j) ∈ S ↔ ↑j < rowSize S i

For a left-justified set, (i, j) ∈ S iff j.val < rowSize S i. This is the key characterization: left-justified rows are initial segments.

theorem WreathOrbits.leftJustified_eq_of_rowSize_eq {m n : ℕ} {S T : Finset (Fin m × Fin n)} (hS : IsLeftJustified S) (hT : IsLeftJustified T) (h : ∀ (i : Fin m), rowSize S i = rowSize T i) : S = T

Two left-justified subsets with the same row sizes are equal.

Antitone functions are determined by their multisets

theorem WreathOrbits.antitone_eq_of_multiset_eq {m : ℕ} {f g : Fin m → ℕ} (hf : Antitone f) (hg : Antitone g) (h : Multiset.map f Finset.univ.val = Multiset.map g Finset.univ.val) : f = g

Two antitone functions Fin m → ℕ with the same multiset of values are equal. This is because the multiset, sorted in decreasing order, gives back the original function (which is already sorted).

Main theorem: uniqueness of Young diagrams (Lemma 6.8)

theorem WreathOrbits.gridYoung_unique {m n : ℕ} {S T : Finset (Fin m × Fin n)} (hS : IsGridYoung S) (hT : IsGridYoung T) (h : rowSizeMultiset S = rowSizeMultiset T) : S = T

Lemma 6.8 (Uniqueness). Two Young diagrams in the m × n grid with the same row-size multiset are equal. Since two subsets of the grid are in the same G_{mn}-orbit iff they have the same row-size multiset, this says each orbit contains at most one Young diagram.

Existence: constructing the canonical Young diagram

The canonical Young diagram for a subset S is obtained by sorting the row sizes in weakly decreasing order and left-justifying each row.

noncomputable def WreathOrbits.sortedRowSizes {m n : ℕ} (S : Finset (Fin m × Fin n)) : List ℕ

The row sizes of S sorted in weakly decreasing order.

theorem WreathOrbits.sortedRowSizes_length {m n : ℕ} (S : Finset (Fin m × Fin n)) : (sortedRowSizes S).length = m

theorem WreathOrbits.sortedRowSizes_pairwise {m n : ℕ} (S : Finset (Fin m × Fin n)) : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≥ x2) (sortedRowSizes S)

theorem WreathOrbits.sortedRowSizes_multiset_eq {m n : ℕ} (S : Finset (Fin m × Fin n)) : ↑(sortedRowSizes S) = Multiset.map (rowSize S) Finset.univ.val

theorem WreathOrbits.sortedRowSizes_le {m n : ℕ} (S : Finset (Fin m × Fin n)) (k : ℕ) (hk : k < (sortedRowSizes S).length) : (sortedRowSizes S)[k] ≤ n

theorem WreathOrbits.getD_le_n {m n : ℕ} (S : Finset (Fin m × Fin n)) (i : Fin m) : (sortedRowSizes S).getD (↑i) 0 ≤ n

noncomputable def WreathOrbits.canonicalYoung {m n : ℕ} (S : Finset (Fin m × Fin n)) : Finset (Fin m × Fin n)

The canonical Young diagram: cell (i, j) is included iff j < λ_i, where λ is the sorted (decreasing) row-size sequence.

theorem WreathOrbits.mem_canonicalYoung {m n : ℕ} (S : Finset (Fin m × Fin n)) (i : Fin m) (j : Fin n) : (i, j) ∈ canonicalYoung S ↔ ↑j < (sortedRowSizes S).getD (↑i) 0

theorem WreathOrbits.canonicalYoung_isLeftJustified {m n : ℕ} (S : Finset (Fin m × Fin n)) : IsLeftJustified (canonicalYoung S)

theorem WreathOrbits.rowSize_canonicalYoung {m n : ℕ} (S : Finset (Fin m × Fin n)) (i : Fin m) : rowSize (canonicalYoung S) i = (sortedRowSizes S).getD (↑i) 0

theorem WreathOrbits.canonicalYoung_antitone {m n : ℕ} (S : Finset (Fin m × Fin n)) : Antitone (rowSize (canonicalYoung S))

theorem WreathOrbits.canonicalYoung_isGridYoung {m n : ℕ} (S : Finset (Fin m × Fin n)) : IsGridYoung (canonicalYoung S)

theorem WreathOrbits.rowSizeMultiset_canonicalYoung {m n : ℕ} (S : Finset (Fin m × Fin n)) : rowSizeMultiset (canonicalYoung S) = rowSizeMultiset S

theorem WreathOrbits.exists_gridYoung_of_rowSizeMultiset {m n : ℕ} (S : Finset (Fin m × Fin n)) : ∃ (T : Finset (Fin m × Fin n)), IsGridYoung T ∧ rowSizeMultiset T = rowSizeMultiset S

Lemma 6.8 (Existence). For any subset S of the m × n grid, there exists a Young diagram with the same row-size multiset. The construction sorts the row sizes in decreasing order and left-justifies each row.

Unique Young diagram in each orbit (Lemma 6.8)

theorem WreathOrbits.existsUnique_gridYoung_sameOrbit {m n : ℕ} (S : Finset (Fin m × Fin n)) : ∃! T : Finset (Fin m × Fin n), IsGridYoung T ∧ SameOrbit S T

Lemma 6.8. Every orbit of the wreath product G_{mn} = Sₙ ≀ Sₘ acting on subsets of the m × n grid contains exactly one Young diagram D (i.e., a left-justified subset with weakly decreasing row sizes).