The row and column groups of a Young tableau

A μ-tableau t is the datum a Young symmetrizer is built from: the row symmetrizer sums over the permutations of the labels that stay inside their row of t, and the column antisymmetrizer sums with signs over those that stay inside their column.

This file defines the two subgroups YoungTableau.rowSubgroup t and YoungTableau.colSubgroup t of Equiv.Perm (Fin μ.card) cut out by those conditions, and proves the two facts the symmetrizer theory rests on: the row and column groups meet trivially, because a cell is determined by its row together with its column; and each of them is the product of the symmetric groups of the rows, respectively columns, of μ. It also records the transpositions that the two groups contain: swapping two labels of a common row lies in the row group, and swapping two labels of a common column lies in the column group. Finally it recognises the two extreme shapes: the row group is everything exactly when the diagram has at most one row, the column group is everything exactly when it has at most one column, and either of those forces the other group to be trivial.

References

• W. Fulton, Young Tableaux, Section 7.1.
• Schur--Weyl roadmap, Layers 0 and 2.

def TauCeti.YoungTableau.rowSubgroup {μ : YoungDiagram} (t : YoungTableau μ) : Subgroup (Equiv.Perm (Fin μ.card))

The row group of a μ-tableau: the permutations of the labels that keep every label in its own row of t.

Equations

• t.rowSubgroup = TauCeti.fiberSubgroup t.rowIndex

def TauCeti.YoungTableau.colSubgroup {μ : YoungDiagram} (t : YoungTableau μ) : Subgroup (Equiv.Perm (Fin μ.card))

The column group of a μ-tableau: the permutations of the labels that keep every label in its own column of t.

Equations

• t.colSubgroup = TauCeti.fiberSubgroup t.colIndex

@[simp]

theorem TauCeti.YoungTableau.mem_rowSubgroup {μ : YoungDiagram} {t : YoungTableau μ} {σ : Equiv.Perm (Fin μ.card)} : σ ∈ t.rowSubgroup ↔ ∀ (k : Fin μ.card), t.rowIndex (σ k) = t.rowIndex k

@[simp]

theorem TauCeti.YoungTableau.mem_colSubgroup {μ : YoungDiagram} {t : YoungTableau μ} {σ : Equiv.Perm (Fin μ.card)} : σ ∈ t.colSubgroup ↔ ∀ (k : Fin μ.card), t.colIndex (σ k) = t.colIndex k

theorem TauCeti.YoungTableau.rowSubgroup_def {μ : YoungDiagram} (t : YoungTableau μ) : t.rowSubgroup = fiberSubgroup t.rowIndex

The row group of t is the group of permutations preserving the fibers of rowIndex t.

theorem TauCeti.YoungTableau.colSubgroup_def {μ : YoungDiagram} (t : YoungTableau μ) : t.colSubgroup = fiberSubgroup t.colIndex

The column group of t is the group of permutations preserving the fibers of colIndex t.

theorem TauCeti.YoungTableau.swap_mem_rowSubgroup {μ : YoungDiagram} {t : YoungTableau μ} {x y : Fin μ.card} (h : t.rowIndex x = t.rowIndex y) : Equiv.swap x y ∈ t.rowSubgroup

The transposition of two labels lying in a common row of t belongs to the row group.

theorem TauCeti.YoungTableau.swap_mem_colSubgroup {μ : YoungDiagram} {t : YoungTableau μ} {x y : Fin μ.card} (h : t.colIndex x = t.colIndex y) : Equiv.swap x y ∈ t.colSubgroup

The transposition of two labels lying in a common column of t belongs to the column group.

theorem TauCeti.YoungTableau.rowSubgroup_inf_colSubgroup_eq_bot {μ : YoungDiagram} (t : YoungTableau μ) : t.rowSubgroup ⊓ t.colSubgroup = ⊥

The row and column groups of a μ-tableau meet only in the identity: a permutation of the labels that stays inside the rows and inside the columns fixes every cell.

theorem TauCeti.YoungTableau.disjoint_rowSubgroup_colSubgroup {μ : YoungDiagram} (t : YoungTableau μ) : Disjoint t.rowSubgroup t.colSubgroup

The row and column groups of a μ-tableau are disjoint subgroups of the symmetric group on the labels.

def TauCeti.YoungTableau.rowSubgroupMulEquiv {μ : YoungDiagram} (t : YoungTableau μ) : ↥t.rowSubgroup ≃* ((i : ℕ) → Equiv.Perm ↥(μ.row i))

The row group of a μ-tableau is the product, over the rows of μ, of the symmetric groups of the rows. Rows beyond the last one of μ are empty and contribute trivial factors.

Equations

• t.rowSubgroupMulEquiv = (MulEquiv.subgroupCongr ⋯).trans ((TauCeti.fiberSubgroupMulEquivPiPerm t.rowIndex).trans (MulEquiv.piCongrRight fun (i : ℕ) => (t.rowFiberEquiv i).permCongrHom))

def TauCeti.YoungTableau.colSubgroupMulEquiv {μ : YoungDiagram} (t : YoungTableau μ) : ↥t.colSubgroup ≃* ((j : ℕ) → Equiv.Perm ↥(μ.col j))

The column group of a μ-tableau is the product, over the columns of μ, of the symmetric groups of the columns.

Equations

• t.colSubgroupMulEquiv = (MulEquiv.subgroupCongr ⋯).trans ((TauCeti.fiberSubgroupMulEquivPiPerm t.colIndex).trans (MulEquiv.piCongrRight fun (j : ℕ) => (t.colFiberEquiv j).permCongrHom))

@[simp]

theorem TauCeti.YoungTableau.rowSubgroupMulEquiv_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (σ : ↥t.rowSubgroup) (i : ℕ) (k : { k : Fin μ.card // t.rowIndex k = i }) : ↑((t.rowSubgroupMulEquiv σ i) ((t.rowFiberEquiv i) k)) = ↑((Equiv.symm t) (↑σ ↑k))

The i-th component of rowSubgroupMulEquiv t σ moves the cell carrying the label k to the cell carrying the label σ k.

@[simp]

theorem TauCeti.YoungTableau.colSubgroupMulEquiv_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (σ : ↥t.colSubgroup) (j : ℕ) (k : { k : Fin μ.card // t.colIndex k = j }) : ↑((t.colSubgroupMulEquiv σ j) ((t.colFiberEquiv j) k)) = ↑((Equiv.symm t) (↑σ ↑k))

The j-th component of colSubgroupMulEquiv t σ moves the cell carrying the label k to the cell carrying the label σ k.

@[simp]

theorem TauCeti.YoungTableau.rowSubgroupMulEquiv_symm_apply {μ : YoungDiagram} (t : YoungTableau μ) (σ : (i : ℕ) → Equiv.Perm ↥(μ.row i)) (k : Fin μ.card) : ↑(t.rowSubgroupMulEquiv.symm σ) k = ↑((t.rowFiberEquiv (t.rowIndex k)).symm ((σ (t.rowIndex k)) ((t.rowFiberEquiv (t.rowIndex k)) ⟨k, ⋯⟩)))

The permutation of the labels assembled from a family of permutations of the rows of μ moves each label by the permutation of its own row.

@[simp]

theorem TauCeti.YoungTableau.colSubgroupMulEquiv_symm_apply {μ : YoungDiagram} (t : YoungTableau μ) (σ : (j : ℕ) → Equiv.Perm ↥(μ.col j)) (k : Fin μ.card) : ↑(t.colSubgroupMulEquiv.symm σ) k = ↑((t.colFiberEquiv (t.colIndex k)).symm ((σ (t.colIndex k)) ((t.colFiberEquiv (t.colIndex k)) ⟨k, ⋯⟩)))

The permutation of the labels assembled from a family of permutations of the columns of μ moves each label by the permutation of its own column.

The extreme shapes

theorem TauCeti.YoungTableau.rowIndex_eq_zero_of_colLen_le_one {μ : YoungDiagram} (t : YoungTableau μ) (h : μ.colLen 0 ≤ 1) (k : Fin μ.card) : t.rowIndex k = 0

A diagram whose zeroth column has at most one cell has only one row, so every label of a tableau on it lies in row 0.

theorem TauCeti.YoungTableau.colIndex_eq_zero_of_rowLen_le_one {μ : YoungDiagram} (t : YoungTableau μ) (h : μ.rowLen 0 ≤ 1) (k : Fin μ.card) : t.colIndex k = 0

A diagram whose zeroth row has at most one cell has only one column, so every label of a tableau on it lies in column 0.

@[simp]

theorem TauCeti.YoungTableau.rowSubgroup_eq_top_iff {μ : YoungDiagram} (t : YoungTableau μ) : t.rowSubgroup = ⊤ ↔ μ.colLen 0 ≤ 1

The row group of a tableau is everything exactly when its shape has at most one row: with a single row every permutation of the labels preserves it, while two rows are separated by a transposition.

@[simp]

theorem TauCeti.YoungTableau.colSubgroup_eq_top_iff {μ : YoungDiagram} (t : YoungTableau μ) : t.colSubgroup = ⊤ ↔ μ.rowLen 0 ≤ 1

The column group of a tableau is everything exactly when its shape has at most one column: with a single column every permutation of the labels preserves it, while two columns are separated by a transposition.

theorem TauCeti.YoungTableau.colSubgroup_eq_bot_of_rowSubgroup_eq_top {μ : YoungDiagram} (t : YoungTableau μ) (h : t.rowSubgroup = ⊤) : t.colSubgroup = ⊥

The row and column groups meet trivially, so a full row group forces a trivial column group.

theorem TauCeti.YoungTableau.rowSubgroup_eq_bot_of_colSubgroup_eq_top {μ : YoungDiagram} (t : YoungTableau μ) (h : t.colSubgroup = ⊤) : t.rowSubgroup = ⊥

The row and column groups meet trivially, so a full column group forces a trivial row group.