Documentation

TauCeti.RepresentationTheory.ClassicalGroups.Weight.Weyl

The Weyl group of GL n acting on weights #

The permutation matrices normalize the diagonal torus and conjugation by them relabels its entries, so they permute the joint eigenspaces of the torus: a permutation σ carries the weight space of l : Fin n → ℤ isomorphically onto the weight space of l ∘ σ⁻¹ (TauCeti.weightSpace_map_permutationGL). This is the GL n shadow of the Weyl group acting on the weight lattice, and its first consequence is that weight multiplicities are constant on Sₙ-orbits (TauCeti.finrank_weightSpace_comp_perm).

Every Sₙ-orbit on Fin n → ℤ contains exactly one weakly decreasing sequence, that is, exactly one TauCeti.DominantWeight (TauCeti.existsUnique_dominantWeight). So the dominant weights are a set of orbit representatives, and whether a weight occurs, and with what multiplicity, can be read off its dominant representative (TauCeti.finrank_weightSpace_dominantWeightOf, TauCeti.weightSpace_eq_bot_dominantWeightOf_iff). The highest-weight classification that indexes the irreducibles of GL n by dominant weights is not proved here.

Implementation notes #

The σ⁻¹ in TauCeti.weightSpace_map_permutationGL is the relabelling convention of TauCeti.permutationGL_mul_diagGL_mul_inv, by which conjugating diagGL t by permutationGL σ gives diagGL (t ∘ σ⁻¹). The orbit statements below are stated with a bare σ where no image is involved, since σ ↦ σ⁻¹ is a bijection of Sₙ.

Main definitions #

Main results #

References #

Permuting the weight characters #

source
theorem TauCeti.weightChar_comp_perm {n : ℕ} {k : Type u} [CommRing k] (l : Fin n → ℤ) (σ : Equiv.Perm (Fin n)) (t : Fin n → kˣ) :
(weightChar k (l ∘ ⇑σ⁻¹)) t = (weightChar k l) fun (i : Fin n) => t (σ i)

Permuting a weight is permuting the point of the torus the other way.

The Weyl group acting on the weight spaces #

source
theorem TauCeti.mem_weightSpace_comp_perm_iff {n : ℕ} {k : Type u} [CommRing k] {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (σ : Equiv.Perm (Fin n)) (l : Fin n → ℤ) (w : W) :
(ρ (permutationGL σ)) w ∈ weightSpace ρ (l ∘ ⇑σ⁻¹) ↔ w ∈ weightSpace ρ l

A permutation matrix carries the weight vectors of l exactly onto those of l ∘ σ⁻¹.

source
theorem TauCeti.weightSpace_map_permutationGL {n : ℕ} {k : Type u} [CommRing k] {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (σ : Equiv.Perm (Fin n)) (l : Fin n → ℤ) :
Submodule.map (ρ (permutationGL σ)) (weightSpace ρ l) = weightSpace ρ (l ∘ ⇑σ⁻¹)

The permutation matrix of σ carries the weight space of l onto the weight space of l ∘ σ⁻¹.

source
noncomputable def TauCeti.weightSpaceEquivCompPerm {n : ℕ} {k : Type u} [CommRing k] {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (σ : Equiv.Perm (Fin n)) (l : Fin n → ℤ) :
↥(weightSpace ρ l) ≃ₗ[k] ↥(weightSpace ρ (l ∘ ⇑σ))

The linear equivalence between the weight spaces of l and of l ∘ σ cut out by the permutation matrix of σ⁻¹.

Instances For
    source
    @[simp]
    theorem TauCeti.coe_weightSpaceEquivCompPerm_apply {n : ℕ} {k : Type u} [CommRing k] {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (σ : Equiv.Perm (Fin n)) (l : Fin n → ℤ) (w : ↥(weightSpace ρ l)) :
    ↑((weightSpaceEquivCompPerm ρ σ l) w) = (ρ (permutationGL σ⁻¹)) ↑w

    The equivalence between the weight spaces of l and of l ∘ σ is the action of the permutation matrix of σ⁻¹.

    source
    @[simp]
    theorem TauCeti.coe_weightSpaceEquivCompPerm_symm_apply {n : ℕ} {k : Type u} [CommRing k] {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (σ : Equiv.Perm (Fin n)) (l : Fin n → ℤ) (w : ↥(weightSpace ρ (l ∘ ⇑σ))) :
    ↑((weightSpaceEquivCompPerm ρ σ l).symm w) = (ρ (permutationGL σ)) ↑w

    Its inverse is the action of the permutation matrix of σ.

    source
    @[simp]
    theorem TauCeti.finrank_weightSpace_comp_perm {n : ℕ} {k : Type u} [CommRing k] {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (σ : Equiv.Perm (Fin n)) (l : Fin n → ℤ) :
    Module.finrank k ↥(weightSpace ρ (l ∘ ⇑σ)) = Module.finrank k ↥(weightSpace ρ l)

    Weight multiplicities are constant on Sₙ-orbits.

    source
    @[simp]
    theorem TauCeti.weightSpace_eq_bot_comp_perm_iff {n : ℕ} {k : Type u} [CommRing k] {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (σ : Equiv.Perm (Fin n)) (l : Fin n → ℤ) :
    weightSpace ρ (l ∘ ⇑σ) = ⊥ ↔ weightSpace ρ l = ⊥

    Being a weight at all is constant on Sₙ-orbits.

    source
    @[simp]
    theorem TauCeti.finrank_weightSpace_dominantWeightOf {n : ℕ} {k : Type u} [CommRing k] {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (l : Fin n → ℤ) :
    Module.finrank k ↥(weightSpace ρ ↑(dominantWeightOf l)) = Module.finrank k ↥(weightSpace ρ l)

    The dominant representative of a weight carries the same multiplicity.

    source
    theorem TauCeti.weightSpace_eq_bot_dominantWeightOf_iff {n : ℕ} {k : Type u} [CommRing k] {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (l : Fin n → ℤ) :
    weightSpace ρ ↑(dominantWeightOf l) = ⊥ ↔ weightSpace ρ l = ⊥

    A weight occurs exactly when its dominant representative does, so the weights of a representation are determined by the dominant ones.