The multiplicity of an irreducible Lie module #
LieModule.isotypicMultiplicity R L M S is the finrank of the space S →ₗ⁅R,L⁆ M of morphisms
from a Lie module S to a Lie module M. This file proves that when S is finite-dimensional and
irreducible over an algebraically closed field, this number counts
the summands equivalent to S in any finite decomposition of M into irreducible Lie
submodules, and is therefore independent of which such decomposition is chosen: it is the
multiplicity of S in M.
The argument #
The morphism space is additive over a direct sum in its target: a morphism S →ₗ⁅R,L⁆ ⨁ i, Pᵢ
is the same thing as a family of morphisms S →ₗ⁅R,L⁆ Pᵢ, one for each i, which is
TauCeti.LieModule.lieModuleHomDirectSumEquiv of TauCeti/Algebra/Lie/DirectSum.lean.
Transporting along DirectSum.lieModuleEquivOfIsInternal of
TauCeti/Algebra/Lie/Submodule/DirectSum.lean turns that into additivity over an internal
decomposition of M by Lie submodules.
The per-summand contribution is Schur's lemma in the dimension form of
TauCeti/Algebra/Lie/Schur.lean: for irreducible S and Nᵢ over an algebraically closed field,
dim_K (S →ₗ⁅K,L⁆ Nᵢ) is 1 when Nᵢ ≃ S and 0 otherwise. Summing over the finite index type
gives the count. Since the left-hand side never mentions the decomposition, two finite
decompositions of the same module have the same number of summands equivalent to S; this is the
uniqueness statement that makes "the multiplicity of S in M" well defined.
Nothing here needs complete reducibility: the counting theorem is stated for a finite decomposition
it is handed. Complete reducibility is what produces such a decomposition, through
TauCeti.exists_isInternal_isIrreducible of TauCeti/Algebra/Lie/Submodule/Decomposition.lean,
which a consumer combines with the counting theorem below.
Implementation notes #
The multiplicity joins the Lie isotypy interface of TauCeti/Algebra/Lie/Isotypic.lean
(LieModule.isotypicComponent, LieModule.IsIsotypicOfType), and like that interface it is stated
without the universal enveloping algebra: this layer depends only on Lie submodules and Lie-module
morphisms. The comparison with the ring-level multiplicity theory of
TauCeti/RingTheory/Semisimple/Multiplicity.lean is therefore made where the rest of the
enveloping-algebra dictionary lives,
LieModule.isotypicMultiplicity_eq_natCard_of_linearEquiv_pi of
TauCeti/Algebra/Lie/UniversalEnveloping/Multiplicity.lean, exactly as
TauCeti/Algebra/Lie/UniversalEnveloping/Isotypic.lean does for the isotypic component.
Main definitions #
LieModule.isotypicMultiplicity: the finrank ofS →ₗ⁅R,L⁆ M, which the theorems below identify with the multiplicity under their field, irreducibility, and decomposition hypotheses.
Main results #
LieModule.isotypicMultiplicity_eq_sum_of_isInternal: the multiplicity is additive over a finite decomposition ofMinto Lie submodules.LieModule.isotypicMultiplicity_eq_zero_of_subsingleton: the zero module occurs with multiplicity zero.LieModule.isotypicMultiplicity_eq_zero_of_subsingleton_codomain: everything occurs in the zero module with multiplicity zero.LieModule.isotypicMultiplicity_self: an irreducible module occurs in itself with multiplicity one.LieModule.isotypicMultiplicity_eq_of_lieModuleEquivandLieModule.isotypicMultiplicity_eq_of_lieModuleEquiv_type: the multiplicity depends only on the equivalence classes ofMand ofS.LieModule.isotypicMultiplicity_eq_ncard_of_isInternal: the multiplicity counts the summands equivalent toSin a finite decomposition ofMinto irreducibles.LieModule.ncard_setOf_nonempty_lieModuleEquiv_eq: the count is independent of which finite decomposition is taken.
Roadmap #
This is the isotypicMultiplicity target of the decomposition toolkit in Layer 6 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, together with the additivity of
the morphism space over a direct-sum decomposition that TauCeti/Algebra/Lie/Schur.lean names as
the missing ingredient of the multiplicity theorem. The multiplicity is stated for an arbitrary
irreducible S rather than for the irreducible quotient L(λ), which the roadmap's own signature
uses; the L(λ)-indexed form is this statement with S instantiated. The finrank of the isotypic
component, dim (LieModule.isotypicComponent S M) = isotypicMultiplicity · dim S, is the next item
of that milestone, "Isotypic components and multiplicities, through the enveloping-algebra
dictionary"; it is proved through the dictionary, as
LieModule.finrank_isotypicComponent of
TauCeti/Algebra/Lie/UniversalEnveloping/Multiplicity.lean. The packaged decomposition
M ≃ ⨁_λ L(λ)^{⊕ m_λ} that closes the milestone is
TauCeti.nonempty_lieModuleEquiv_directSum_irreducibleQuotient of
TauCeti/Algebra/Lie/HighestWeight/Decomposition.lean, which counts the summands of a
decomposition with the theorems below. The toolkit's remaining milestone, the tensor
multiplicities with the minuscule Pieri rule, is untouched here.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §6.
The multiplicity of an irreducible module #
The finrank of the space of morphisms S →ₗ⁅R,L⁆ M. For an irreducible,
finite-dimensional S over an algebraically closed field this is the multiplicity of S in M:
the number of summands equivalent to S in any finite decomposition of M into
irreducibles (LieModule.isotypicMultiplicity_eq_ncard_of_isInternal), and stating it as the
finrank of a morphism space is what makes it manifestly independent of the decomposition. In the
generality of the definition it is not itself a multiplicity: for a finite-dimensional irreducible
S over a field and a finite irreducible direct-sum decomposition of M, it is the multiplicity
times dim End_L(S), a factor that Schur's lemma makes 1 over an algebraically closed field.
Equations
- LieModule.isotypicMultiplicity R L M S = Module.finrank R (S →ₗ⁅R,L⁆ M)
Instances For
The multiplicity is the finrank of the morphism space. The definition is not exposed, so this is how it is unfolded.
The zero module has multiplicity zero: the only morphism out of it is the zero morphism.
Everything occurs in the zero module with multiplicity zero: the only morphism into it is the zero morphism.
The multiplicity depends only on the two equivalence classes #
The multiplicity only depends on the equivalence class of the ambient module. Postcomposition with an equivalence identifies the two morphism spaces.
The multiplicity only depends on the equivalence class of the module being counted. Precomposition with an equivalence identifies the two morphism spaces. This is what lets the multiplicity be read for an irreducible determined only up to equivalence, such as an irreducible highest-weight quotient.
The multiplicity as a count of summands #
Multiplicity is additive over an internal decomposition of its ambient module.
An irreducible module occurs in itself with multiplicity one.
The multiplicity counts the summands equivalent to S. For a finite decomposition of a
module into irreducible Lie submodules over an algebraically closed field, the
multiplicity of a finite-dimensional irreducible S is the number of indices whose summand is
equivalent to S: Schur's lemma makes each such summand contribute 1 to the morphism space and
every other summand contribute 0.
The number of summands equivalent to a given irreducible does not depend on which finite decomposition is taken. Both counts compute the same multiplicity, which is defined without reference to any decomposition.