Documentation

TauCeti.RepresentationTheory.ClassicalGroups.Weight.Combinatorics

The weight of a multiset #

A weight of the diagonal torus of GL n k is an integer vector l : Fin n → ℤ, and a multiset s over Fin n carries one: its multiplicity vector TauCeti.weightOfMultiset s, the vector whose i-th entry is the number of times i occurs in s. This file is the combinatorics of that vector — the part of the weight theory of the symmetric powers of the standard representation that mentions no representation.

There are three facts. A multiset over Fin n is recovered from its multiplicities, so the labelling is injective; the entries are nonnegative and sum to the cardinality; and conversely every nonnegative vector of total degree d is the multiplicity vector of an unordered d-tuple, which is Sym.equivNatSumOfFintype read in ℤ. Together they say that the multiplicity vectors of the elements of Sym (Fin n) d are exactly the exponent vectors of the degree-d monomials in n variables. Finally, the torus character of a multiset weight is the product of the entries the multiset lists, repetitions included, which is the scalar by which a diagonal matrix acts on the corresponding product of standard basis vectors.

The weight of the unordered tuple of an ordered tuple p : Fin d → Fin n — its content — is read off p directly: the multiplicity of j is the number of places at which p takes the value j, and TauCeti.sum_weightOfMultiset_ofFn counts the entries whose values lie in any finite set. Its initial-segment form compares two contents in the dominance order.

The subset counterpart, the 0/1 indicator TauCeti.weightOfSubset carried by a d-element subset, is in TauCeti.RepresentationTheory.ClassicalGroups.Weight.ExteriorPower beside its one consumer.

Main definitions #

Main results #

Implementation notes #

The weight takes a bare Multiset (Fin n) rather than an element of Sym (Fin n) d: nothing in the definition or in its injectivity uses the cardinality, and the consumers apply it to the underlying multiset of a basis index. The cardinality reappears only in TauCeti.sum_weightOfMultiset.

The vector itself is Multiset.toFinsupp read in ℤ, but it is spelled as a plain function rather than through that equivalence because a weight is a plain function Fin n → ℤ: routing it through a Finsupp coercion would leave every rewrite in the consuming files fighting the coercion for no gain.

source
def TauCeti.weightOfMultiset {n : ℕ} (s : Multiset (Fin n)) :
Fin n → ℤ

The weight of a multiset over Fin n: its multiplicity vector. This is the weight carried by the product of the standard basis vectors it lists.

Instances For
    source
    @[simp]
    theorem TauCeti.weightOfMultiset_apply {n : ℕ} (s : Multiset (Fin n)) (i : Fin n) :
    weightOfMultiset s i = ↑(Multiset.count i s)

    The defining formula for TauCeti.weightOfMultiset.

    source
    theorem TauCeti.weightOfMultiset_nonneg {n : ℕ} (s : Multiset (Fin n)) (i : Fin n) :
    0 ≤ weightOfMultiset s i

    Multiplicities are nonnegative, so the weights of a symmetric power are.

    source
    theorem TauCeti.weightOfMultiset_injective {n : ℕ} :
    Function.Injective weightOfMultiset

    A multiset is recovered from its weight, a multiset over Fin n being determined by its multiplicities.

    source
    theorem TauCeti.sum_weightOfMultiset {n : ℕ} (s : Multiset (Fin n)) :
    ∑ i : Fin n, weightOfMultiset s i = ↑s.card

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

    source
    theorem TauCeti.exists_sym_weightOfMultiset_eq_iff {n d : ℕ} (l : Fin n → ℤ) :
    (∃ (s : Sym (Fin n) d), weightOfMultiset ↑s = l) ↔ (∀ (i : Fin n), 0 ≤ l i) ∧ ∑ i : Fin n, l i = ↑d

    The weights of Symᵈ(kⁿ) are the exponent vectors of the degree-d monomials in n variables: an integer vector is the multiplicity vector of an unordered d-tuple over Fin n exactly when it is nonnegative and sums to d.

    The content of an ordered tuple #

    source
    theorem TauCeti.weightOfMultiset_ofFn_apply {n d : ℕ} (p : Fin d → Fin n) (j : Fin n) :
    weightOfMultiset (↑(Sym.ofFn p)) j = ↑{x : Fin d | p x = j}.card

    The multiplicity of j in the content of an ordered tuple is the number of places at which the tuple takes the value j.

    source
    theorem TauCeti.sum_weightOfMultiset_ofFn {n d : ℕ} (p : Fin d → Fin n) (S : Finset (Fin n)) :
    ∑ j ∈ S, weightOfMultiset (↑(Sym.ofFn p)) j = ↑{x : Fin d | p x ∈ S}.card

    The multiplicities of the values in S add up to the number of entries of the tuple whose values lie in S.

    source
    theorem TauCeti.sum_weightOfMultiset_ofFn_filter_val_lt {n d : ℕ} (p : Fin d → Fin n) (m : ℕ) :
    ∑ j : Fin n with ↑j < m, weightOfMultiset (↑(Sym.ofFn p)) j = ↑{x : Fin d | ↑(p x) < m}.card

    The partial sums of the content of an ordered tuple count its small values: the multiplicities of the values below m add up to the number of places at which the tuple takes such a value.

    This is the form in which the content of a tuple is compared with another in the dominance order.

    source
    @[simp]
    theorem TauCeti.weightChar_weightOfMultiset {k : Type u} [CommRing k] {n : ℕ} (s : Multiset (Fin n)) (t : Fin n → kˣ) :
    (weightChar k (weightOfMultiset s)) t = (Multiset.map t s).prod

    The torus character of a multiset weight is the product of the entries it lists.