Documentation

TauCeti.RepresentationTheory.Symmetric.Specht.Module

Polytabloids and the Specht module #

The Young permutation module M^μ is the rational representation of Sₙ on the μ-tabloids, which are the left cosets of the Young subgroup of the shape of μ. A μ-tableau t names one of them, its tabloid {t}, and antisymmetrizing that tabloid over the column group of t produces the polytabloid

e_t = b_t · {t} ∈ M^μ.

The Specht module S^μ is the submodule of M^μ spanned by the polytabloids. It is a subrepresentation, because relabeling a tableau translates its polytabloid: e_{σt} = σ · e_t. Since the symmetric group acts transitively on tableaux, S^μ is in fact the span of the orbit of a single polytabloid.

The conventions here are the ones the Schur-Weyl roadmap pins, and they have to be used together: M^μ is a left module on the left cosets of the Young subgroup, the polytabloid is the column antisymmetrization b_t · {t} of the tabloid, and the Young symmetrizer is c_t = a_t b_t. The opposite choices produce the dual Specht module.

The bridge between the two indexings is rowYoungConjugator t, the permutation carrying the consecutive-block labeling of the shape of μ to the labeling of t: its coset is the tabloid of t, and conjugation by it carries the Young subgroup onto the row group of t. The tabloid of t is therefore fixed exactly by the row group, which is what makes the polytabloid nonzero: the column group meets the row group trivially, so the tabloids appearing in e_t are pairwise distinct and the coefficient of {t} itself is 1.

The identification of S^μ with the left ideal ℚ[Sₙ] c_t of TauCeti/RepresentationTheory/Symmetric/Specht/Ideal/Basic.lean is a separate milestone and is not proved here. Neither is James's submodule theorem, which rests on the nonvanishing recorded below and lives in TauCeti/RepresentationTheory/Symmetric/Specht/SubmoduleTheorem.lean together with the irreducibility it yields.

Main definitions #

Main results #

References #

The tabloid of a tableau #

source
noncomputable def TauCeti.YoungTableau.tabloid {μ : YoungDiagram} (t : YoungTableau μ) :
Equiv.Perm (Fin μ.card) ⧸ youngSubgroup (shapePartition μ)

The tabloid {t} of a μ-tableau t: the row-equivalence class of t, presented as the coset of the Young subgroup of the shape of μ given by rowYoungConjugator t.

Equations
Instances For
    source
    theorem TauCeti.YoungTableau.tabloid_def {μ : YoungDiagram} (t : YoungTableau μ) :
    t.tabloid = ↑t.rowYoungConjugator
    source
    @[simp]
    theorem TauCeti.YoungTableau.tabloid_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) :
    (relabel σ t).tabloid = σ • t.tabloid

    Relabeling a tableau translates its tabloid.

    source
    theorem TauCeti.YoungTableau.tabloid_surjective {μ : YoungDiagram} :
    Function.Surjective tabloid

    Every μ-tabloid is the tabloid of a tableau.

    source
    @[simp]
    theorem TauCeti.YoungTableau.smul_tabloid_eq_self_iff {μ : YoungDiagram} {t : YoungTableau μ} {σ : Equiv.Perm (Fin μ.card)} :
    σ • t.tabloid = t.tabloid ↔ σ ∈ t.rowSubgroup

    The stabilizer of a tabloid is the row group. A permutation fixes the tabloid of t exactly when it preserves the rows of t.

    source
    @[simp]
    theorem TauCeti.YoungTableau.smul_tabloid_eq_iff {μ : YoungDiagram} {t : YoungTableau μ} {σ τ : Equiv.Perm (Fin μ.card)} :
    σ • t.tabloid = τ • t.tabloid ↔ σ⁻¹ * τ ∈ t.rowSubgroup

    Two permutations send the tabloid of t to the same tabloid exactly when they differ by an element of the row group of t.

    source
    @[simp]
    theorem TauCeti.YoungTableau.tabloid_eq_iff_rowIndex_eq {μ : YoungDiagram} {t u : YoungTableau μ} :
    t.tabloid = u.tabloid ↔ t.rowIndex = u.rowIndex

    Two tableaux have the same tabloid exactly when they put every label in the same row.

    source
    theorem TauCeti.YoungTableau.smul_tabloid_injective {μ : YoungDiagram} (t : YoungTableau μ) :
    Function.Injective fun (q : ↥t.colSubgroup) => ↑q • t.tabloid

    Distinct elements of the column group of t move the tabloid of t to distinct tabloids: the column group meets the row group, which is the stabilizer, only in the identity.

    Polytabloids #

    source
    noncomputable def TauCeti.YoungTableau.polytabloid {μ : YoungDiagram} (t : YoungTableau μ) :
    ↑(permutationModule (shapePartition μ))

    The polytabloid e_t = b_t · {t}: the column antisymmetrizer of t acting on the tabloid of t inside the Young permutation module of the shape of μ.

    Equations
    Instances For
      source
      theorem TauCeti.YoungTableau.polytabloid_def {μ : YoungDiagram} (t : YoungTableau μ) :
      t.polytabloid = ((permutationModule (shapePartition μ)).ρ.asAlgebraHom t.columnAntisymmetrizer) (MonoidAlgebra.single t.tabloid 1)

      The polytabloid is the column antisymmetrizer applied to the tabloid.

      source
      @[simp]
      theorem TauCeti.YoungTableau.polytabloid_eq_single_of_colSubgroup_eq_bot {μ : YoungDiagram} (t : YoungTableau μ) (h : t.colSubgroup = ⊥) :
      t.polytabloid = MonoidAlgebra.single t.tabloid 1

      A polytabloid with trivial column group is the bare tabloid. The column antisymmetrizer of t is then 1, so there is nothing to antisymmetrize. A shape with at most one row is the case of interest, by TauCeti.YoungTableau.colSubgroup_eq_bot_of_rowSubgroup_eq_top.

      source
      theorem TauCeti.YoungTableau.polytabloid_eq_sum {μ : YoungDiagram} (t : YoungTableau μ) :
      t.polytabloid = ∑ q : ↥t.colSubgroup, ↑↑(Equiv.Perm.sign ↑q) • MonoidAlgebra.single (↑q • t.tabloid) 1

      The polytabloid is the signed sum of the tabloids obtained from {t} by the column group.

      source
      @[simp]
      theorem TauCeti.YoungTableau.polytabloid_relabel {μ : YoungDiagram} (σ : Equiv.Perm (Fin μ.card)) (t : YoungTableau μ) :
      (relabel σ t).polytabloid = ((permutationModule (shapePartition μ)).ρ σ) t.polytabloid

      Relabeling a tableau translates its polytabloid: e_{σt} = σ · e_t.

      source
      theorem TauCeti.YoungTableau.polytabloid_relabel_of_mem_colSubgroup {μ : YoungDiagram} {t : YoungTableau μ} {q : Equiv.Perm (Fin μ.card)} (hq : q ∈ t.colSubgroup) :
      (relabel q t).polytabloid = ↑↑(Equiv.Perm.sign q) • t.polytabloid

      Relabeling by a column permutation of t scales the polytabloid by its sign: e_{qt} = sgn(q) e_t for q in the column group of t. So the tableaux in one column-group orbit all carry, up to sign, the same polytabloid.

      This is not a simp lemma: its left-hand side is the one of TauCeti.YoungTableau.polytabloid_relabel, which applies to every permutation.

      source
      @[simp]
      theorem TauCeti.YoungTableau.polytabloid_coeff_smul_tabloid {μ : YoungDiagram} (t : YoungTableau μ) (q : ↥t.colSubgroup) :
      t.polytabloid.coeff (↑q • t.tabloid) = ↑↑(Equiv.Perm.sign ↑q)

      The coefficient, in the polytabloid e_t, of the tabloid obtained from {t} by a column permutation q of t is the sign of q.

      source
      @[simp]
      theorem TauCeti.YoungTableau.polytabloid_coeff_tabloid {μ : YoungDiagram} (t : YoungTableau μ) :
      t.polytabloid.coeff t.tabloid = 1

      The coefficient of the tabloid {t} in the polytabloid e_t is 1; in particular e_t is a nonzero element of M^μ.

      source
      theorem TauCeti.YoungTableau.polytabloid_coeff_eq_zero_of_forall_ne {μ : YoungDiagram} (t : YoungTableau μ) {X : Equiv.Perm (Fin μ.card) ⧸ youngSubgroup (shapePartition μ)} (h : ∀ q ∈ t.colSubgroup, q • t.tabloid ≠ X) :
      t.polytabloid.coeff X = 0

      Only the tabloids reachable from {t} by a column permutation occur in the polytabloid e_t.

      source
      @[simp]
      theorem TauCeti.YoungTableau.polytabloid_ne_zero {μ : YoungDiagram} (t : YoungTableau μ) :
      t.polytabloid ≠ 0

      Polytabloids are nonzero.

      source
      theorem TauCeti.YoungTableau.tabloidForm_polytabloid_self {μ : YoungDiagram} (t : YoungTableau μ) :
      ((tabloidForm (shapePartition μ)) t.polytabloid) t.polytabloid = ↑(Nat.card ↥t.colSubgroup)

      The tabloid form evaluates a polytabloid against itself to the order of the column group. This nonvanishing is the input that James's submodule theorem converts into irreducibility of the Specht module.

      The Specht module #

      source
      noncomputable def TauCeti.spechtSubrepresentation (μ : YoungDiagram) :
      Subrepresentation (permutationModule (shapePartition μ)).ρ

      The Specht module S^μ, in its concrete presentation: the subrepresentation of the Young permutation module M^μ spanned by the polytabloids of the μ-tableaux.

      It is stable under the symmetric group because relabeling a tableau translates its polytabloid, and the polytabloids of the relabelings of a fixed tableau are all of them.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.spechtSubrepresentation_toSubmodule (μ : YoungDiagram) :
        (spechtSubrepresentation μ).toSubmodule = Submodule.span ℚ (Set.range YoungTableau.polytabloid)

        The underlying submodule of the Specht module is the span of the polytabloids.

        source
        theorem TauCeti.polytabloid_mem_spechtSubrepresentation {μ : YoungDiagram} (t : YoungTableau μ) :
        t.polytabloid ∈ spechtSubrepresentation μ

        Every polytabloid lies in the Specht module.

        source
        theorem TauCeti.spechtSubrepresentation_eq_span_orbit {μ : YoungDiagram} (t : YoungTableau μ) :
        (spechtSubrepresentation μ).toSubmodule = Submodule.span ℚ (Set.range fun (σ : Equiv.Perm (Fin μ.card)) => ((permutationModule (shapePartition μ)).ρ σ) t.polytabloid)

        The Specht module is cyclic. It is the span of the orbit of a single polytabloid, because the symmetric group permutes the μ-tableaux transitively.

        source
        @[simp]
        theorem TauCeti.spechtSubrepresentation_ne_bot (μ : YoungDiagram) :
        spechtSubrepresentation μ ≠ ⊥

        The Specht module is nonzero.

        source
        instance TauCeti.instFiniteDimensionalRatSubtypeVPermFinCardPermutationModuleShapePartitionMemSubmoduleToSubmoduleSpechtSubrepresentation (μ : YoungDiagram) :
        FiniteDimensional ℚ ↥(spechtSubrepresentation μ).toSubmodule

        The Specht module is finite-dimensional, being a submodule of the finite-dimensional Young permutation module. This is what lets it be bundled as an FDRep.

        source
        @[reducible, inline]
        noncomputable abbrev TauCeti.spechtModule {n : ℕ} (μ : n.Partition) :
        FDRep ℚ (Equiv.Perm (Fin n))

        The Specht module S^μ of a partition μ of n, bundled as a finite-dimensional representation of Sₙ: the span of the polytabloids of the tableaux of the Young diagram diagramOf μ, with the symmetric group on the (diagramOf μ).card entries of such a tableau identified with Sₙ along card_diagramOf.

        The tabloid combinatorics is indexed by a diagram, since a tableau is a filling of one, while the classification the Specht modules feed is indexed by partitions; this is the partition-indexed name. Its representation unfolds to spechtSubrepresentation (diagramOf μ) by FDRep.of_ρ', and spechtSubrepresentation_toSubmodule identifies the underlying module with the span of the polytabloids.

        Equations
        Instances For
          source
          theorem TauCeti.finrank_spechtModule_pos {n : ℕ} (μ : n.Partition) :
          0 < Module.finrank ℚ ↑(spechtModule μ).V

          The Specht module is nontrivial, so it has positive dimension.