Documentation

TauCeti.RepresentationTheory.ClassicalGroups.Weight.ExteriorPower

The weights of an exterior power of the standard representation #

The standard representation of GL n k is the internal direct sum of its weight spaces, the coordinate lines, with the i-th line carrying the weight Pi.single i 1 (TauCeti.isInternal_weightSpace_stdRep). This file computes the weight spaces of its exterior powers, the representations ⋀ᵈ(kⁿ).

A wedge e_{i₁} ∧ ⋯ ∧ e_{i_d} of standard basis vectors is again a weight vector: a diagonal matrix scales it by the product t_{i₁} ⋯ t_{i_d} of the corresponding entries. Its weight is therefore the 0/1 indicator of the d-element subset {i₁, …, i_d}, which is TauCeti.weightOfSubset below. Those wedges are Mathlib's basis Module.Basis.exteriorPower of ⋀ᵈ(kⁿ), indexed by Set.powersetCard (Fin n) d, and distinct subsets carry distinct weights, so — once distinct weights give distinct characters of the torus — the weight spaces are the coordinate lines of that basis: the weight-l space is the line spanned by the wedge of s if l is the indicator of s, and is zero otherwise. In particular every weight of ⋀ᵈ(kⁿ) has multiplicity one, and there are n.choose d of them.

So the weights of ⋀ᵈ(kⁿ) are exactly the sums Pi.single i₁ 1 + ⋯ + Pi.single i_d 1 of d distinct weights of the standard representation, each occurring once. For d = 0 the only weight is 0, and for d > n there is no weight at all, the exterior power being zero. For 1 ≤ d ≤ n the largest weight in the dominance order is (1, …, 1, 0, …, 0) with d ones, the d-th fundamental weight of GL n; identifying it as the highest weight of ⋀ᵈ(kⁿ) needs the highest-weight classification and is not done here.

Main definitions #

Main results #

Implementation notes #

Everything past the eigenvector computation is an instance of TauCeti.RepresentationTheory.ClassicalGroups.Weight.Basis, which reads the weight spaces of a representation off a basis of weight vectors; what is specific to the exterior power is the wedge basis, the subset labelling, and the injectivity of that labelling.

The subset weight is packaged as TauCeti.weightOfSubset, taking a bare Finset (Fin n) rather than an element of Set.powersetCard (Fin n) d: nothing in the definition or in its injectivity uses the cardinality, and the consumers below apply it to the underlying finset of a basis index. The cardinality reappears only in TauCeti.sum_weightOfSubset, which records that a weight of ⋀ᵈ(kⁿ) has total degree d.

As in TauCeti/RepresentationTheory/ClassicalGroups/Weight/Basic.lean, the statements that pin a weight space down, rather than merely exhibiting vectors in it, assume that the coefficients separate weights, in the sense that l ↦ weightChar k l is injective; TauCeti.weightChar_injective supplies that over an infinite field. Without it the statements are false: over 𝔽₂ the diagonal torus of GL n 𝔽₂ is trivial, so every weight space of every representation is everything.

The eigenvector computation itself is Module.Basis.map_exteriorPower_of_apply, the exterior-power analogue of Module.Basis.map_symmetricPower_of_apply; it is what TauCeti.char_extPowerRep_diagonal sums to get the elementary symmetric polynomial, and the weight-space statements here refine that character identity to the decomposition behind it.

References #

The weight of a subset #

source
def TauCeti.weightOfSubset {n : ℕ} (s : Finset (Fin n)) :
Fin n → ℤ

The weight of a subset s ⊆ Fin n: its 0/1 indicator. This is the weight carried by the wedge of the standard basis vectors indexed by s.

Instances For
    source
    @[simp]
    theorem TauCeti.weightOfSubset_apply {n : ℕ} (s : Finset (Fin n)) (i : Fin n) :
    weightOfSubset s i = if i ∈ s then 1 else 0

    The defining formula for TauCeti.weightOfSubset.

    source
    theorem TauCeti.weightOfSubset_injective {n : ℕ} :
    Function.Injective weightOfSubset

    A subset is recovered from its weight, the support of the indicator being the subset.

    source
    theorem TauCeti.sum_weightOfSubset {n : ℕ} (s : Finset (Fin n)) :
    ∑ i : Fin n, weightOfSubset s i = ↑s.card

    The weight of a subset has total degree its cardinality: the weights of ⋀ᵈ(kⁿ) all lie in degree d.

    source
    @[simp]
    theorem TauCeti.weightChar_weightOfSubset {k : Type u} [CommRing k] {n : ℕ} (s : Finset (Fin n)) (t : Fin n → kˣ) :
    (weightChar k (weightOfSubset s)) t = ∏ i ∈ s, t i

    The torus character of a subset weight is the product of the entries it selects.

    The wedges of standard basis vectors are weight vectors #

    source
    theorem TauCeti.extPowerRep_diagGL_apply_basis {k : Type u} [CommRing k] {n d : ℕ} (t : Fin n → kˣ) (s : ↑(Set.powersetCard (Fin n) d)) :
    ((extPowerRep k n d) (diagGL t)) ((Module.Basis.exteriorPower d (Pi.basisFun k (Fin n))) s) = (∏ i ∈ ↑s, ↑(t i)) • (Module.Basis.exteriorPower d (Pi.basisFun k (Fin n))) s

    A wedge of standard basis vectors is an eigenvector of every diagonal matrix, with eigenvalue the product of the entries it selects.

    This is deliberately not a simp lemma: Representation.exteriorPower_apply already rewrites the left-hand side to exteriorPower.map d (stdRep k n (diagGL t)), so it is not in simp normal form.

    source
    theorem TauCeti.basis_mem_weightSpace_extPowerRep {k : Type u} [CommRing k] {n d : ℕ} (s : ↑(Set.powersetCard (Fin n) d)) :
    (Module.Basis.exteriorPower d (Pi.basisFun k (Fin n))) s ∈ weightSpace (extPowerRep k n d) (weightOfSubset ↑s)

    The wedge of the standard basis vectors indexed by s has weight the indicator of s.

    source
    theorem TauCeti.iSup_weightSpace_extPowerRep_eq_top {k : Type u} [CommRing k] {n d : ℕ} :
    ⨆ (l : Fin n → ℤ), weightSpace (extPowerRep k n d) l = ⊤

    The weight spaces of an exterior power of the standard representation span it: the wedge basis consists of weight vectors.

    The weight spaces are the lines of the wedge basis #

    Here the coefficients must separate weights, in the sense that l ↦ weightChar k l is injective; TauCeti.weightChar_injective supplies that over an infinite field.

    source
    theorem TauCeti.weightSpace_extPowerRep_eq_span {k : Type u} [CommRing k] [IsCancelMulZero k] {n d : ℕ} (hchar : Function.Injective (weightChar k)) (s : ↑(Set.powersetCard (Fin n) d)) :
    weightSpace (extPowerRep k n d) (weightOfSubset ↑s) = k ∙ (Module.Basis.exteriorPower d (Pi.basisFun k (Fin n))) s

    The weight spaces of an exterior power of the standard representation are the coordinate lines of the wedge basis: the weight-l space of ⋀ᵈ(kⁿ), for l the indicator of a d-element subset s, is the line spanned by the wedge of the standard basis vectors indexed by s.

    source
    theorem TauCeti.weightSpace_extPowerRep_eq_bot {k : Type u} [CommRing k] [IsCancelMulZero k] {n d : ℕ} (hchar : Function.Injective (weightChar k)) {l : Fin n → ℤ} (hl : ∀ (s : ↑(Set.powersetCard (Fin n) d)), l ≠ weightOfSubset ↑s) :
    weightSpace (extPowerRep k n d) l = ⊥

    Only the indicators are weights of an exterior power of the standard representation.

    source
    theorem TauCeti.weightSpace_extPowerRep_ne_bot_iff {k : Type u} [CommRing k] [IsCancelMulZero k] {n d : ℕ} [Nontrivial k] (hchar : Function.Injective (weightChar k)) (l : Fin n → ℤ) :
    weightSpace (extPowerRep k n d) l ≠ ⊥ ↔ ∃ (s : ↑(Set.powersetCard (Fin n) d)), l = weightOfSubset ↑s

    The weights of ⋀ᵈ(kⁿ) are exactly the indicators of the d-element subsets of Fin n, of which there are n.choose d.

    source
    theorem TauCeti.isInternal_weightSpace_extPowerRep {k : Type u} [Field k] {n d : ℕ} (hchar : Function.Injective (weightChar k)) :
    DirectSum.IsInternal fun (l : Fin n → ℤ) => weightSpace (extPowerRep k n d) l

    An exterior power of the standard representation is the internal direct sum of its weight spaces.

    source
    theorem TauCeti.finrank_weightSpace_extPowerRep {k : Type u} [Field k] {n d : ℕ} (hchar : Function.Injective (weightChar k)) (s : ↑(Set.powersetCard (Fin n) d)) :
    Module.finrank k ↥(weightSpace (extPowerRep k n d) (weightOfSubset ↑s)) = 1

    Every weight of ⋀ᵈ(kⁿ) has multiplicity one.