Relabeling a Young tableau conjugates its Young symmetrizer

A Young symmetrizer, and with it the left ideal ℚ[Sₙ] c_t it generates, is built from a μ-tableau t, while the Specht module it presents is meant to depend only on the shape μ. This file supplies that independence.

Relabeling the labels of t by a permutation σ conjugates the row group and the column group of t, hence conjugates the row symmetrizer, the column antisymmetrizer, and the Young symmetrizer:

c_{σt} = σ c_t σ⁻¹.

Consequently ℚ[Sₙ] c_{σt} = (ℚ[Sₙ] c_t) σ⁻¹, and right multiplication by σ is an isomorphism of representations from ℚ[Sₙ] c_{σt} to ℚ[Sₙ] c_t. Since any two tableaux of the same shape differ by a relabeling, the representation ℚ[Sₙ] c_t, and in particular its dimension and its character, depend only on the shape of t.

Main results

• YoungTableau.youngSymmetrizer_relabel: the Young symmetrizer of a relabeled tableau is the conjugate of the Young symmetrizer, and YoungTableau.youngSymmetrizerOver_relabel says the same for its transport to a ℚ-algebra.
• YoungTableau.spechtIdealRelabelRepEquiv: right multiplication by σ as an isomorphism of representations ℚ[Sₙ] c_{σt} ≅ ℚ[Sₙ] c_t.
• YoungTableau.spechtIdealRepIso, YoungTableau.finrank_spechtIdeal_eq and YoungTableau.character_spechtIdealRep_eq: the representation, its dimension, and its character depend only on the shape of the tableau.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 4.
• Schur--Weyl roadmap, Layers 2 and 3: the Layer 3 Specht module spechtModule μ is indexed by the shape μ alone, while the Layer 2 Young symmetrizer and its left ideal are built from a tableau, so the tableau-independence proved here is what makes the Layer 3 indexing legitimate.

The row and column groups of a relabeled tableau

theorem TauCeti.YoungTableau.rowSubgroup_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).rowSubgroup = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj σ)) t.rowSubgroup

Relabeling by σ conjugates the row group by σ.

theorem TauCeti.YoungTableau.colSubgroup_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).colSubgroup = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj σ)) t.colSubgroup

Relabeling by σ conjugates the column group by σ.

theorem TauCeti.YoungTableau.mem_rowSubgroup_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) {τ : Equiv.Perm (Fin μ.card)} : τ ∈ (relabel σ t).rowSubgroup ↔ σ⁻¹ * τ * σ ∈ t.rowSubgroup

A permutation preserves the rows of the relabeled tableau exactly when its conjugate preserves the rows of the original one.

Not a simp lemma: mem_rowSubgroup and rowIndex_relabel already simplify the left-hand side past this normal form, to the pointwise condition on rows.

theorem TauCeti.YoungTableau.mem_colSubgroup_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) {τ : Equiv.Perm (Fin μ.card)} : τ ∈ (relabel σ t).colSubgroup ↔ σ⁻¹ * τ * σ ∈ t.colSubgroup

A permutation preserves the columns of the relabeled tableau exactly when its conjugate preserves the columns of the original one.

Not a simp lemma: mem_colSubgroup and colIndex_relabel already simplify the left-hand side past this normal form, to the pointwise condition on columns.

The symmetrizers of a relabeled tableau

@[simp]

theorem TauCeti.YoungTableau.rowSymmetrizer_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).rowSymmetrizer = MonoidAlgebra.single σ 1 * t.rowSymmetrizer * MonoidAlgebra.single σ⁻¹ 1

Relabeling by σ conjugates the row symmetrizer by σ.

@[simp]

theorem TauCeti.YoungTableau.columnAntisymmetrizer_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).columnAntisymmetrizer = MonoidAlgebra.single σ 1 * t.columnAntisymmetrizer * MonoidAlgebra.single σ⁻¹ 1

Relabeling by σ conjugates the column antisymmetrizer by σ; the signs are unchanged, conjugate permutations having equal signs.

@[simp]

theorem TauCeti.YoungTableau.youngSymmetrizer_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).youngSymmetrizer = MonoidAlgebra.single σ 1 * t.youngSymmetrizer * MonoidAlgebra.single σ⁻¹ 1

Relabeling by σ conjugates the Young symmetrizer by σ: c_{σt} = σ c_t σ⁻¹.

theorem TauCeti.YoungTableau.youngSymmetrizerOver_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (k : Type u_1) [CommSemiring k] [Algebra ℚ k] : youngSymmetrizerOver k (relabel σ t) = MonoidAlgebra.single σ 1 * youngSymmetrizerOver k t * MonoidAlgebra.single σ⁻¹ 1

Relabeling by σ conjugates the transported Young symmetrizer, as it does the rational one.

The Young-symmetrizer left ideal of a relabeled tableau

theorem TauCeti.YoungTableau.mem_spechtIdeal_relabel_iff {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) {x : MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card))} : x ∈ (relabel σ t).spechtIdeal ↔ x * MonoidAlgebra.single σ 1 ∈ t.spechtIdeal

Membership in the left ideal generated by c_{σt} is membership in the right translate by σ⁻¹ of the left ideal generated by c_t.

noncomputable def TauCeti.YoungTableau.spechtIdealRelabelEquiv {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : ↥(relabel σ t).spechtIdeal ≃ₗ[MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card))] ↥t.spechtIdeal

Right multiplication by σ as an equivalence of left ℚ[Sₙ]-modules from ℚ[Sₙ] c_{σt} to ℚ[Sₙ] c_t: it is right multiplication by the unit σ of the group algebra, restricted to the two ideals.

Equations

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

@[simp]

theorem TauCeti.YoungTableau.spechtIdealRelabelEquiv_apply_coe {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (x : ↥(relabel σ t).spechtIdeal) : ↑((spechtIdealRelabelEquiv σ t) x) = ↑x * MonoidAlgebra.single σ 1

@[simp]

theorem TauCeti.YoungTableau.spechtIdealRelabelEquiv_symm_apply_coe {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (y : ↥t.spechtIdeal) : ↑((spechtIdealRelabelEquiv σ t).symm y) = ↑y * MonoidAlgebra.single σ⁻¹ 1

noncomputable def TauCeti.YoungTableau.spechtIdealRelabelRepEquiv {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).spechtIdealRep.ρ.Equiv t.spechtIdealRep.ρ

Right multiplication by σ is an isomorphism of representations from ℚ[Sₙ] c_{σt} to ℚ[Sₙ] c_t: being a map of left modules over the group algebra, it commutes with the action.

Equations

• TauCeti.YoungTableau.spechtIdealRelabelRepEquiv σ t = Representation.Equiv.mk (LinearEquiv.restrictScalars ℚ (TauCeti.YoungTableau.spechtIdealRelabelEquiv σ t)) ⋯

@[simp]

theorem TauCeti.YoungTableau.spechtIdealRelabelRepEquiv_apply_coe {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (x : ↥(relabel σ t).spechtIdeal) : ↑((spechtIdealRelabelRepEquiv σ t) x) = ↑x * MonoidAlgebra.single σ 1

noncomputable def TauCeti.YoungTableau.spechtIdealRelabelRepIso {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).spechtIdealRep ≅ t.spechtIdealRep

The left ideals of the Young symmetrizers of a tableau and of its relabelings are isomorphic representations.

Equations

• TauCeti.YoungTableau.spechtIdealRelabelRepIso σ t = Rep.mkIso (TauCeti.YoungTableau.spechtIdealRelabelRepEquiv σ t)

@[simp]

theorem TauCeti.YoungTableau.spechtIdealRelabelRepIso_hom_hom_apply_coe {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) (x : ↥(relabel σ t).spechtIdeal) : ↑((Rep.Hom.hom (spechtIdealRelabelRepIso σ t).hom) x) = ↑x * MonoidAlgebra.single σ 1

theorem TauCeti.YoungTableau.finrank_spechtIdeal_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : Module.finrank ℚ ↥(relabel σ t).spechtIdeal = Module.finrank ℚ ↥t.spechtIdeal

Relabeling does not change the dimension of the Young-symmetrizer left ideal.

@[simp]

theorem TauCeti.YoungTableau.character_spechtIdealRep_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).spechtIdealRep.ρ.character = t.spechtIdealRep.ρ.character

Relabeling does not change the character of the Young-symmetrizer left ideal.

theorem TauCeti.YoungTableau.character_spechtIdealFDRep_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) : (relabel σ t).spechtIdealFDRep.character = t.spechtIdealFDRep.character

Relabeling does not change the character of the bundled Young-symmetrizer representation.

Independence of the tableau

noncomputable def TauCeti.YoungTableau.spechtIdealRepIso {μ : YoungDiagram} (t t' : YoungTableau μ) : t.spechtIdealRep ≅ t'.spechtIdealRep

The Young-symmetrizer left ideals of two tableaux of the same shape are isomorphic representations: up to isomorphism the representation depends only on the shape.

Equations

• t.spechtIdealRepIso t' = (TauCeti.YoungTableau.spechtIdealRelabelRepIso (t.relabelPerm t') t).symm ≪≫ CategoryTheory.eqToIso ⋯

theorem TauCeti.YoungTableau.finrank_spechtIdeal_eq {μ : YoungDiagram} (t t' : YoungTableau μ) : Module.finrank ℚ ↥t.spechtIdeal = Module.finrank ℚ ↥t'.spechtIdeal

The dimension of the Young-symmetrizer left ideal depends only on the shape of the tableau.

theorem TauCeti.YoungTableau.character_spechtIdealRep_eq {μ : YoungDiagram} (t t' : YoungTableau μ) : t.spechtIdealRep.ρ.character = t'.spechtIdealRep.ρ.character

The character of the Young-symmetrizer left ideal depends only on the shape of the tableau.

theorem TauCeti.YoungTableau.character_spechtIdealFDRep_eq {μ : YoungDiagram} (t t' : YoungTableau μ) : t.spechtIdealFDRep.character = t'.spechtIdealFDRep.character

The character of the bundled Young-symmetrizer representation depends only on the shape of the tableau.