Tableau row groups and Young subgroups

The row group of a tableau depends on its labeling, whereas the Young subgroup attached to its shape uses consecutive blocks. This file constructs the permutation sending the consecutive-block labeling to a given tableau and proves that it conjugates the corresponding Young subgroup onto the tableau's row group.

References

• G. James, The Representation Theory of the Symmetric Groups, Chapter 3.
• Schur--Weyl roadmap, Layer 1.

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

The permutation carrying the consecutive-block labeling of a Young diagram to the labeling of t. It sends each block of the shape partition to the correspondingly numbered row of t.

Equations

• t.rowYoungConjugator = (TauCeti.youngBlocksEquiv (TauCeti.shapePartition μ)).symm.trans ((TauCeti.YoungTableau.sortedBlocksEquivRows✝ μ).trans ((TauCeti.YoungTableau.rowCellsEquiv✝ μ).trans t))

@[simp]

theorem TauCeti.YoungTableau.rowIndex_rowYoungConjugator {μ : YoungDiagram} (t : YoungTableau μ) (k : Fin μ.card) : t.rowIndex (t.rowYoungConjugator k) = ↑(youngBlock (shapePartition μ) k)

The row of a label after applying rowYoungConjugator t is its consecutive-block number.

theorem TauCeti.YoungTableau.rowYoungConjugator_youngBlocksEquiv {μ : YoungDiagram} (t : YoungTableau μ) (x : (i : Fin ((shapePartition μ).parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) × Fin (((shapePartition μ).parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).get i)) : t.rowYoungConjugator ((youngBlocksEquiv (shapePartition μ)) x) = t ⟨(↑x.fst, ↑x.snd), ⋯⟩

On consecutive-block coordinates, rowYoungConjugator t sends position j in block i to the label in position j of row i of t.

@[simp]

theorem TauCeti.YoungTableau.rowYoungConjugator_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).rowYoungConjugator = σ * t.rowYoungConjugator

Relabeling a tableau translates its conjugator on the left: the consecutive-block labeling is carried to the relabeled tableau by first carrying it to t and then applying σ.

theorem TauCeti.YoungTableau.youngSubgroup_map_conj_eq_rowSubgroup {μ : YoungDiagram} (t : YoungTableau μ) : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj t.rowYoungConjugator)) (youngSubgroup (shapePartition μ)) = t.rowSubgroup

Conjugation by rowYoungConjugator t carries the Young subgroup of the shape partition onto the row group of t.

noncomputable def TauCeti.YoungTableau.youngSubgroupConjMulEquiv {μ : YoungDiagram} (t : YoungTableau μ) : ↥(youngSubgroup (shapePartition μ)) ≃* ↥t.rowSubgroup

Conjugation by rowYoungConjugator t as a multiplicative equivalence from the Young subgroup of the shape partition to the row group of t.

Equations

• t.youngSubgroupConjMulEquiv = (MulEquiv.subgroupMap (MulAut.conj t.rowYoungConjugator) (TauCeti.youngSubgroup (TauCeti.shapePartition μ))).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem TauCeti.YoungTableau.youngSubgroupConjMulEquiv_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (σ : ↥(youngSubgroup (shapePartition μ))) : ↑(t.youngSubgroupConjMulEquiv σ) = t.rowYoungConjugator * ↑σ * t.rowYoungConjugator⁻¹

The subgroup equivalence acts by conjugation with rowYoungConjugator t.

@[simp]

theorem TauCeti.YoungTableau.youngSubgroupConjMulEquiv_symm_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (τ : ↥t.rowSubgroup) : ↑(t.youngSubgroupConjMulEquiv.symm τ) = t.rowYoungConjugator⁻¹ * ↑τ * t.rowYoungConjugator

The inverse subgroup equivalence acts by conjugation with the inverse of rowYoungConjugator t.