Young-symmetrizer left ideals

For a Young tableau t, this file constructs the principal left ideal ℚ[Sₙ] c_t generated by its Young symmetrizer and bundles that ideal as a finite-dimensional representation of the symmetric group.

This instantiates the roadmap's named representation-theory plumbing, "idempotent-generated submodules and left ideals as representations", for the Young symmetrizer, and it is the abstract half of the presentation that the Specht module target consumes. Nothing here uses the essential idempotence c_t * c_t = κ • c_t -- that runs the other way, since identifying the scalar needs the dimension of the ideal: it is proved downstream in TauCeti.RepresentationTheory.Symmetric.Specht.Ideal.Idempotent, in the form κ = n! / finrank ℚ (ℚ[Sₙ] c_t), and the roadmap's reading κ = n! / f^λ waits on the standard basis theorem dim S^λ = f^λ -- and nothing here identifies this representation with the span of the polytabloids inside the Young permutation module: that identification is the Specht module milestone itself, and it is deliberately not claimed here.

Main definitions

• YoungTableau.spechtIdeal is the principal left ideal generated by c_t.
• YoungTableau.spechtIdealRep is its symmetric-group representation.
• YoungTableau.spechtIdealFDRep is the finite-dimensional bundled form.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 2.
• Schur--Weyl roadmap, “What is missing (build here)”: the representation-theory plumbing item “idempotent-generated submodules and left ideals as representations”, which the Layer 3 Specht module target consumes.

noncomputable def TauCeti.YoungTableau.spechtIdeal {μ : YoungDiagram} (t : YoungTableau μ) : Submodule (MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card))) (MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card)))

The principal left ideal ℚ[Sₙ] c_t generated by the Young symmetrizer of t.

Equations

• t.spechtIdeal = MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card)) ∙ t.youngSymmetrizer

@[simp]

theorem TauCeti.YoungTableau.spechtIdeal_le_iff {μ : YoungDiagram} (t : YoungTableau μ) (I : Submodule (MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card))) (MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card)))) : t.spechtIdeal ≤ I ↔ t.youngSymmetrizer ∈ I

The Young-symmetrizer left ideal is contained in a submodule exactly when that submodule contains its generator.

@[simp]

theorem TauCeti.YoungTableau.mem_spechtIdeal_iff {μ : YoungDiagram} (t : YoungTableau μ) (x : MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card))) : x ∈ t.spechtIdeal ↔ ∃ (a : MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card))), a * t.youngSymmetrizer = x

An element lies in ℚ[Sₙ] c_t exactly when it is a left multiple of c_t.

theorem TauCeti.YoungTableau.youngSymmetrizer_mem_spechtIdeal {μ : YoungDiagram} (t : YoungTableau μ) : t.youngSymmetrizer ∈ t.spechtIdeal

The Young symmetrizer belongs to the left ideal that it generates.

@[simp]

theorem TauCeti.YoungTableau.spechtIdeal_eq_bot_iff {μ : YoungDiagram} (t : YoungTableau μ) : t.spechtIdeal = ⊥ ↔ t.youngSymmetrizer = 0

The Young-symmetrizer left ideal is zero exactly when its generator is zero.

theorem TauCeti.YoungTableau.spechtIdeal_ne_bot {μ : YoungDiagram} (t : YoungTableau μ) : t.spechtIdeal ≠ ⊥

The Young-symmetrizer left ideal is nonzero.

instance TauCeti.YoungTableau.instNontrivialSpechtIdeal {μ : YoungDiagram} (t : YoungTableau μ) : Nontrivial ↥t.spechtIdeal

A Young-symmetrizer left ideal is a nontrivial module.

@[reducible, inline]

noncomputable abbrev TauCeti.YoungTableau.spechtIdealRep {μ : YoungDiagram} (t : YoungTableau μ) : Rep ℚ (Equiv.Perm (Fin μ.card))

The representation of the symmetric group on ℚ[Sₙ] c_t by left multiplication.

Equations

• t.spechtIdealRep = Rep.of (Representation.ofModule' ↥t.spechtIdeal)

@[simp]

theorem TauCeti.YoungTableau.spechtIdealRep_ρ_apply_coe {μ : YoungDiagram} (t : YoungTableau μ) (g : Equiv.Perm (Fin μ.card)) (x : ↥t.spechtIdeal) : ↑((t.spechtIdealRep.ρ g) x) = MonoidAlgebra.single g 1 * ↑x

The action on the Young-symmetrizer left ideal is multiplication on the left by the corresponding group-algebra basis element.

instance TauCeti.YoungTableau.instModuleFiniteSpechtIdeal {μ : YoungDiagram} (t : YoungTableau μ) : Module.Finite ℚ ↥t.spechtIdeal

A Young-symmetrizer left ideal is finite-dimensional over ℚ.

@[reducible, inline]

noncomputable abbrev TauCeti.YoungTableau.spechtIdealFDRep {μ : YoungDiagram} (t : YoungTableau μ) : FDRep ℚ (Equiv.Perm (Fin μ.card))

The left ideal generated by a Young symmetrizer, bundled as a finite-dimensional representation.

Equations

• t.spechtIdealFDRep = FDRep.of t.spechtIdealRep.ρ

theorem TauCeti.YoungTableau.finrank_spechtIdeal_pos {μ : YoungDiagram} (t : YoungTableau μ) : 0 < Module.finrank ℚ ↑t.spechtIdealFDRep.V

The Young-symmetrizer left ideal has positive dimension.

theorem TauCeti.YoungTableau.finrank_spechtIdeal_le_factorial {μ : YoungDiagram} (t : YoungTableau μ) : Module.finrank ℚ ↑t.spechtIdealFDRep.V ≤ μ.card.factorial

The dimension of ℚ[Sₙ] c_t is at most n!, the dimension of the regular representation.