The multiplicity of a simple module, as the dimension of a hom space #
Let A be an algebra over a field k and let S be a simple A-module, finite-dimensional over
k. If a module M is written as a finite direct sum of simple
modules, the number of summands isomorphic to S is the multiplicity of S in M. Written
that way the multiplicity refers to a chosen decomposition. Over an algebraically closed field
this file identifies it with the manifestly choice-free number
Module.finrank k (S →ₗ[A] M),
so that the multiplicity is an invariant of M and needs no decomposition to be defined.
The proof is Schur's lemma plus additivity. A hom space out of S into a finite product splits
as the product of the hom spaces into the factors, and each factor contributes 1 or 0
according as it is or is not isomorphic to S. Those two values are the dimension forms of
Schur's lemma, TauCeti.finrank_linearMap_eq_one_of_nonempty_linearEquiv and
TauCeti.finrank_linearMap_eq_zero_of_isEmpty_linearEquiv, proved in
TauCeti/RingTheory/Semisimple/Schur.lean alongside the transport of a hom space along an
isomorphism of its target, TauCeti.homCongrRight.
Over an arbitrary field, an isomorphic factor instead contributes
finrank k (Module.End A S). The corresponding scaled multiplicity formula is enough to recover
the number of factors, since this endomorphism algebra has positive dimension. Constituent
detection and hom-space reconstruction therefore need no algebraic closure. Multiplicity
invariance is proved over arbitrary rings by identifying the factor count with the
Jordan-Hölder multiplicity.
The hom-space dimension results are stated for a k-algebra A and A-modules that are
k-modules compatibly. For A = k[G], the hom space is the space of intertwiners. The
reconstruction result from simple-module classes needs only a semisimple ring, while
reconstruction from hom-space dimensions returns to the finite-dimensional k-algebra setting.
Main results #
TauCeti.finrank_linearMap_eq_natCard_of_linearEquiv_pi: the multiplicity theorem. IfM ≃ₗ[A] ∀ i, N iwith everyN isimple, thenfinrank k (S →ₗ[A] M)is the number of indicesiwithN i ≅ S.LinearEquiv.finrank_linearMap_eq_natCard_mul_finrank_end: over an arbitrary field, the same count is multiplied by the dimension of the division algebraEnd_A(S); the literal product form isTauCeti.finrank_linearMap_pi_eq_natCard_mul_finrank_end.TauCeti.jordanHolderMultiplicity_pi_eq_natCard: over any ring, the count of simple factors is the Jordan-Hölder multiplicity.TauCeti.natCard_eq_natCard_of_linearEquiv_pi: equivalent finite products of simple modules over any ring have equally many factors isomorphic toS; applied to two decompositions of one module, this says that the multiplicity is well defined.TauCeti.nonempty_linearEquiv_pi_of_natCard_eq: conversely, two finite products of simple modules are linearly equivalent when their numbers of factors in every simple-module class agree.TauCeti.nonempty_linearEquiv_of_finrank_linearMap_eq: finite modules over a finite-dimensional semisimple algebra are linearly equivalent when every simple left ideal has the same hom-space dimension into them.TauCeti.natCard_linearMap_eq_pow_jordanHolderMultiplicity: over any ring, maps from a finitely generated semisimple moduleMto a simple moduleSnumber#End(S) ^ [M : S].TauCeti.natCard_linearMap_pi_eq_prod_pow: maps fromMinto a finite product of simple modulesN inumber∏ i, #End(N i) ^ [M : N i].TauCeti.IsSemisimpleModule.nonempty_linearEquiv_of_jordanHolderMultiplicity_eq: over any ring, finitely generated semisimple modules with the same Jordan-Hölder multiplicities are isomorphic.TauCeti.IsSemisimpleModule.nonempty_linearEquiv_of_natCard_linearMap_mul_eq: over any ring, finite semisimple modulesMandNwith#Hom(M, N) · #Hom(N, M) = #End(M) · #End(N)are isomorphic.TauCeti.finrank_linearMap_pos_iff_exists_nonempty_linearEquiv: the multiplicity is positive exactly whenSoccurs among the factors, so the hom space detects the constituents.TauCeti.finrank_linearMap_eq_natCard_of_linearEquiv_pi_const: the isotypic case, whereMis a power ofSitself and the multiplicity is the number of copies.TauCeti.nonempty_linearEquiv_isotypicComponent: the isotypic component is the power of its type with exponent the multiplicity,isotypicComponent A M S ≃ₗ[A] Fin m → Sform = finrank k (S →ₗ[A] M), andTauCeti.finrank_isotypicComponent: consequentlydim (isotypicComponent A M S) = m · dim S.TauCeti.finrank_linearMap_pos_of_ne_bot: for a finite-dimensionalM, the hom space out of any nonzero submodule is positive-dimensional. This asks for neither simplicity nor an algebraically closed field, so it lives apart from the results above.
The isotypic component #
Mathlib's isotypicComponent A M S is the sum of the submodules of M isomorphic to S, and
IsIsotypicOfType.linearEquiv_fun writes it as a finite power of S once S is simple and M is
finite-dimensional. What the multiplicity theorem adds is the value of the exponent: every
A-linear map out of S lands in the isotypic component
(LinearMap.apply_mem_isotypicComponent), so TauCeti.linearMapIsotypicComponentEquiv identifies
their hom spaces out of S, and the count above identifies the exponent with
finrank k (S →ₗ[A] M). This is the decomposition-free description of the component that a
multiplicity computation needs.
Implementation notes #
The index set of a decomposition is counted with Nat.card of a subtype rather than with a
Finset.filter, so that no DecidablePred instance enters the statements; the proofs introduce
classical decidability and a Fintype structure locally.
The semisimple-ring reconstruction theorem counts factors by simpleModuleClass; the hom-space
reconstruction theorem converts those class fibres to the Nonempty (S ≃ₗ[A] N i) convention of
the multiplicity theorem using simpleModuleClass_eq_mk_iff.
Over an arbitrary ring, where simple modules need not embed in the ring, the factors of a
finitely generated semisimple module are instead taken to be quotients R ⧸ m by maximal left
ideals, and are matched up to isomorphism directly; maps out of such a module into a simple module
are counted with Nat.card, which needs no base field.
The dimension formulas assume simplicity of S and finite dimensionality over k. The
multiplicity theorem takes the decomposition of M as data; existence of a decomposition is the
separate semisimplicity input. The ring-general factor-count statements need neither a base field
nor simplicity of the module whose occurrences are counted.
References #
See C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §25, or J.-P. Serre, Linear Representations of Finite Groups, §2.
The multiplicity of a simple module in a finite direct sum #
The multiplicity formula over an arbitrary field. The dimension of the space of maps from
a simple module S into a finite product of simple modules is the number of factors isomorphic
to S, multiplied by the dimension of the division algebra End_A(S).
The multiplicity formula over an arbitrary field, for a module given with a finite
simple decomposition. Each copy of S contributes the dimension of End_A(S).
The multiplicity theorem for a product of simple modules. The dimension of the space of
A-linear maps from a simple module S into a finite product of simple modules counts the
factors isomorphic to S.
The multiplicity theorem. If M decomposes as a finite direct sum of simple modules
N i, then the dimension of the space of A-linear maps from a simple module S into M is
the number of factors isomorphic to S.
Only the right-hand side mentions the decomposition, so this is the statement that the
multiplicity of S in M is an invariant of M; see
TauCeti.natCard_eq_natCard_of_linearEquiv_pi.
A module with a finite decomposition into simple modules has a finite-dimensional space of maps from a finite-dimensional simple module into it.
A hom space detects a constituent. There is a nonzero A-linear map from the simple
module S into M exactly when S occurs among the simple factors of M.
Multiplicity invariance over arbitrary rings #
The Jordan-Hölder multiplicity in a finite product of simple modules counts the factors isomorphic to the given module.
Equivalent finite products of simple modules contain equally many copies of every module. This is Jordan-Hölder invariance over an arbitrary ring, without a choice of base field.
Reconstructing a finite sum from its multiplicities #
Finite sums of simple modules are determined by their multiplicities. If two finite families contain equally many modules in every simple-module isomorphism class, their products are linearly equivalent.
Semisimple modules over an arbitrary ring #
A finitely generated semisimple module is a finite product of quotients of the ring by maximal
left ideals. This is IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp with each simple summand
replaced by an isomorphic cyclic module, so that all the factors live in the universe of R.
Maps from a finite product of simple modules into a simple module S. Their number is
the number of endomorphisms of S, raised to the number of factors isomorphic to S: by Schur's
lemma a factor isomorphic to S contributes a copy of End_R(S), and any other factor
contributes only the zero map. No base field is involved, and the formula holds even when
End_R(S) is infinite, both sides then being 0 or 1 together.
Maps from a semisimple module into a simple module count its multiplicity. For a finitely
generated semisimple module M and a simple module S,
#Hom_R(M, S) = #End_R(S) ^ [M : S], where [M : S] is the Jordan-Hölder multiplicity. When
End_R(S) is finite with at least two elements, the number of maps therefore determines the
multiplicity.
Maps from a semisimple module into a finite product of simple modules. For a finitely
generated semisimple module M, #Hom_R(M, ∏ i, N i) = ∏ i, #End_R(N i) ^ [M : N i]: maps into a
product are families of maps into the factors, counted by
TauCeti.natCard_linearMap_eq_pow_jordanHolderMultiplicity.
Semisimple modules are determined by their Jordan-Hölder multiplicities, over an arbitrary
ring. Two finitely generated semisimple modules which contain every simple module equally often
are isomorphic. It suffices to test the simple modules in the universe of R, since every simple
module is isomorphic to a quotient of R.
Over a semisimple ring this is TauCeti.nonempty_linearEquiv_pi_of_natCard_eq, where the simple
modules are indexed by the simple left ideals of R; in general a simple module need not embed in
R, and the factors are matched by isomorphism directly.
Finite semisimple modules are determined by the numbers of maps between them, over an
arbitrary ring. Two finite semisimple modules M and N with
#Hom(M, N) · #Hom(N, M) = #End(M) · #End(N) are isomorphic.
Writing a_S and b_S for the multiplicities of a simple module S in M and N, and
q_S = #End(S) ≥ 2, the four numbers of maps are ∏ q_S ^ (a_S b_S), ∏ q_S ^ (b_S a_S),
∏ q_S ^ (a_S ^ 2) and ∏ q_S ^ (b_S ^ 2), so the hypothesis says ∏ q_S ^ ((a_S - b_S) ^ 2) = 1.
This form of the comparison applies when only maps between M and N themselves can be counted,
for instance when M and N are reductions of lattices whose hom modules are known.
Reconstructing finite modules from hom-space dimensions #
Finite modules over a semisimple algebra are determined by their simple multiplicities.
If every simple left ideal has hom spaces of the same dimension into M and P, then M and
P are linearly equivalent.
The isotypic case #
The multiplicity of S in a power of S. If M is a finite power of the simple module
S, the dimension of the space of A-linear maps S → M is the number of copies.
This is the form Clifford theory uses: an isotypic component of a restriction is a power of a single constituent, and its multiplicity is read off as a dimension.
The isotypic component #
The multiplicity of S in M is its multiplicity in the S-isotypic component, every
map out of S landing there.
The isotypic component is the power of its type with exponent the multiplicity. Mathlib's
IsIsotypicOfType.linearEquiv_fun writes the component as a finite power of S; what is proved
here is that the exponent is the multiplicity finrank k (S →ₗ[A] M), which is the form that
identifies it without reference to the decomposition.
The dimension of an isotypic component is the multiplicity times the dimension of its
type. This is the counted form of the isotypic decomposition: the S-isotypic component of M
is S^{⊕ m} with m the multiplicity finrank k (S →ₗ[A] M).
Positivity for an arbitrary nonzero submodule #
A nonzero submodule has a positive-dimensional hom space. The inclusion of a nonzero
A-submodule S of M is a nonzero element of S →ₗ[A] M, and that hom space is
finite-dimensional over k because S and M are. For a simple S over a splitting field this
is the statement that a constituent occurs with positive multiplicity.
A is a ring rather than a semiring because the finite-dimensionality of the hom space is
LinearMap.finiteDimensional', which needs one; over a semiring ↥S carries no AddCommGroup
instance and Module.Finite.linearMap does not apply.