The packaged isotypic decomposition M ≅ ⨁ L(λ)^{m λ} #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically
closed field of characteristic zero, let H be a Cartan subalgebra and b a base of its root
system. Weyl's theorem decomposes a finite-dimensional L-module M into irreducible Lie
submodules, and LieModule.isotypicMultiplicity counts how many of them lie in a given
isomorphism class, independently of the decomposition. This file assembles the two into the single
statement a consumer wants:
M ≃ₗ⁅K,L⁆ ⨁ (λ, k), L(λ),
the sum being over pairs of a dominant integral weight λ and a counter k in
Fin (m λ), where m λ is the multiplicity of L(λ) in M
(TauCeti.nonempty_lieModuleEquiv_directSum_irreducibleQuotient). Only finitely many
multiplicities are nonzero, so all but finitely many summands are indexed by the empty type.
The companion statement LieModule.nonempty_lieModuleEquiv_isotypicComponent of
TauCeti/Algebra/Lie/UniversalEnveloping/Multiplicity.lean decomposes one isotypic component as a
power S^{⊕ m} of a single irreducible. It is not what proves the theorem below, since nothing
so far exhibits M as the direct sum of its isotypic components; the decomposition into
irreducibles is regrouped directly instead.
The argument #
Each irreducible summand N i of a decomposition of M carries a highest weight vector of a
dominant integral weight c i, and two irreducible modules with highest weight vectors of the same
weight are equivalent, so N i ≃ L(c i)
(TauCeti.exists_isDominantIntegral_nonempty_lieModuleEquiv_irreducibleQuotient). Regrouping the
decomposition by the label c is DirectSum.nonempty_lieModuleEquiv_sigma_of_isInternal, and what
it asks for is that the fibre of c over λ have exactly m λ elements. That is
TauCeti.natCard_eq_isotypicMultiplicity_irreducibleQuotient, and it splits in two.
L(λ) is irreducible, and finite-dimensional because λ is dominant integral, so
LieModule.isotypicMultiplicity_eq_ncard_of_isInternal counts the summands equivalent to it; those
are exactly the summands labelled λ, by the classification of the irreducible highest weight
modules.
The decomposition read on characters #
Formal characters are additive over an internal decomposition
(TauCeti.formalCharacter_eq_sum_of_isInternal), so the same regrouping turns the decomposition
into the character identity ch M = ∑_λ m_λ · ch L(λ), the form in which "decompose M into
irreducibles" becomes a computation. The formal character is defined only for a
finite-dimensional module, and L(λ) is finite-dimensional at every dominant integral λ
(TauCeti.finiteDimensional_irreducibleQuotient_of_isDominantIntegral); at a non-dominant λ it
is infinite-dimensional
(TauCeti.finiteDimensional_iff_isDominantIntegral_of_isHighestWeightVector). So the sum does not
run over all of Module.Dual K H: TauCeti.irreducibleFormalCharacter names the character of
L(λ) as a function of a weight bundled with its dominance, and the sum runs over that subtype.
TauCeti.irreducibleFormalCharacter_def unfolds it wherever the finite-dimensionality instance is
already at hand, so the definition itself never needs unfolding.
That character is never zero (TauCeti.irreducibleFormalCharacter_ne_zero), L(λ) being
irreducible, so the character API is not vacuous.
Restricting the sum to the dominant integral weights loses nothing:
TauCeti.isotypicMultiplicity_irreducibleQuotient_eq_zero_of_not_isDominantIntegral says that
L(λ) for a non-dominant λ has multiplicity zero in every finite-dimensional module, so every
multiplicity the sum omits is zero.
Main definitions #
TauCeti.irreducibleFormalCharacter: the formal character ofL(λ), at a dominant integralλ.
Main results #
TauCeti.natCard_eq_isotypicMultiplicity_irreducibleQuotient: the summands of a decomposition labelled by a dominant integralλare counted by the multiplicity ofL(λ).TauCeti.nonempty_lieModuleEquiv_directSum_irreducibleQuotient: the packaged isotypic decompositionM ≃ ⨁_λ L(λ)^{m λ}.TauCeti.isotypicMultiplicity_irreducibleQuotient_eq_zero_of_not_isDominantIntegral:L(λ)of a non-dominant weightλhas multiplicity zero in every finite-dimensional module.TauCeti.irreducibleFormalCharacter_ne_zero: the character ofL(lam)is nonzero.TauCeti.formalCharacter_eq_finsum_isotypicMultiplicity_smul: the character of a finite-dimensional module is the multiplicity-weighted sum of the irreducible characters.
References #
This is the packaged-decomposition item of the milestone "isotypic components and multiplicities,
through the enveloping-algebra dictionary" in the Layer 6 decomposition toolkit of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §6.3 (complete reducibility) and §§20.3, 21.2 (the classification of the finite-dimensional irreducible modules).
The multiplicity counts the summands with a given label #
The multiplicity of L(lam) counts the summands labelled lam. For a finite
decomposition of M into irreducible Lie submodules, each labelled by a weight whose L it is a
copy of, and for a dominant integral weight lam, the number of indices carrying the label lam
is the multiplicity of L(lam) in M.
The packaged decomposition #
The packaged isotypic decomposition. A finite-dimensional module over a
Killing-semisimple Lie algebra in characteristic zero over an algebraically closed field is the
direct sum of the modules L(lam), indexed by a dominant integral weight lam together with a
counter running over the multiplicity of L(lam) in the module.
Only finitely many multiplicities are nonzero, so all but finitely many of the summands are
indexed by Fin 0.
The character of the irreducible module of a dominant integral weight #
The formal character of the highest weight module L(lam) of a dominant integral weight
lam, which TauCeti.finiteDimensional_irreducibleQuotient_of_isDominantIntegral makes
finite-dimensional. The weight is bundled with its dominance so that the character is a function of
a single argument, and can therefore index a sum. It is nonzero
(TauCeti.irreducibleFormalCharacter_ne_zero).
Equations
- TauCeti.irreducibleFormalCharacter b lam = TauCeti.formalCharacter K (↥H) (TauCeti.irreducibleQuotient b ↑lam)
Instances For
The character of L(lam) is the formal character of L(lam). With the
finite-dimensionality instance in hand, TauCeti.irreducibleFormalCharacter needs no unfolding.
The character of L(lam) is nonzero. The character records the dimension of L(lam),
which is nonzero, L(lam) being irreducible.
The multiplicity-weighted sum of irreducible characters #
L(lam) of a non-dominant weight has multiplicity zero in every finite-dimensional
module. A nonzero multiplicity gives a nonzero morphism out of L(lam), which is irreducible
(TauCeti.isIrreducible_irreducibleQuotient); that morphism is then injective, so it would make
L(lam) finite-dimensional, hence lam dominant integral.
The character of a finite-dimensional module is the multiplicity-weighted sum of the
irreducible characters. A decomposition into irreducibles labels each summand by the dominant
integral weight whose L(lam) it is a copy of; characters are additive over the decomposition, and
the summands carrying a given label are counted by the multiplicity of L(lam)
(TauCeti.natCard_eq_isotypicMultiplicity_irreducibleQuotient).