LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Constituent multiplicities are dimensions of simple modules over the endomorphism algebra

Statement

Let $A$ be a finite-dimensional semisimple $C$ -algebra, let $M$ be a finite-dimensional semisimple $A$ -module and put $E : = {End}_{A} (M)$ (Semisimple modules as direct sums of simple modules, The endomorphism ring ${End}_{R} (M)$ under addition and composition). Let $r \geq 0$ and let $V_{1}, \dots, V_{r}$ be pairwise non-isomorphic simple $A$ -modules with $M ≅ ⨁_{i = 1}^{r} V_{i}^{\oplus m_{i}}, m_{i} \geq 1.$ Then:

$E$ is a semisimple $C$ -algebra, and there is an isomorphism $E ≅ \prod_{i = 1}^{r} M_{m_{i}} (C)$ ; for $r = 0$ both sides are the zero algebra;
for every $i$ the space $S_{i} : = {Hom}_{A} (V_{i}, M)$ , a left $E$ -module by postcomposition, is a simple $E$ -module of dimension $m_{i}$ , and $i \mapsto S_{i}$ is a bijection from ${1, \dots, r}$ onto the set of isomorphism classes of simple $E$ -modules;
the multiplicity $m_{i}$ of $V_{i}$ in $M$ equals $\dim_{C} S_{i}$ ; consequently the constituents of $M$ are indexed by the isomorphism classes of simple $E$ -modules, and the constituent attached to a simple $E$ -module $S$ has multiplicity $\dim_{C} S$ . If $E^{'}$ is a semisimple algebra abstractly isomorphic to ${End}_{A} (M)$ , the indexing transports along any such isomorphism, dimension being preserved. No choice principle is used.

Facts & Assumptions

Given: A finite-dimensional semisimple $C$ -algebra $A$ , a finite-dimensional semisimple $A$ -module $M$ , the algebra $E = {End}_{A} (M)$ , pairwise non-isomorphic simple $A$ -modules $V_{1}, \dots, V_{r}$ and an isomorphism $M ≅ ⨁_{i} V_{i}^{\oplus m_{i}}$ .

[F1]

Schur's lemma for modules: a nonzero homomorphism between simple modules is an isomorphism, and the endomorphism ring of a simple module is a division ring (Schur's lemma for simple modules).

[F2]

A finitely generated semisimple module is an internal direct sum of finitely many simple submodules, so it has an isotypic decomposition into its non-isomorphic simple constituents (Semisimple modules as direct sums of simple modules, A finitely generated semisimple module is a finite direct sum of simple modules).

[F3]

Endomorphisms of a finite direct sum $⨁_{j} M_{j}$ correspond to matrices $(f_{i j})$ with entries $f_{i j} \in {Hom}_{A} (M_{j}, M_{i})$ , with composition given by matrix multiplication, and $E = {End}_{A} (M)$ is a unital ring under pointwise addition and composition (Endomorphisms of a finite direct sum are matrices of Hom-groups, Module endomorphisms form a ring under pointwise addition and composition).

[F4]

Over an algebraically closed field every endomorphism of a nonzero finite-dimensional vector space has an eigenvalue; $C$ is algebraically closed (Every endomorphism of a nonzero finite-dimensional vector space over an algebraically closed field has an eigenvalue, The complex numbers form an algebraic closure of $R$ ).

[F5]

Wedderburn-Artin: a nonzero unital ring is semisimple exactly when it is a product of finitely many matrix rings over division rings, and the simple left modules of such a product are the column modules of its factors, one class per factor (Wedderburn–Artin theorem for semisimple rings, Simple modules over a product of matrix rings over division rings).

Proof

technique · direct

1.1F1F2algebra

Write $M = ⨁_{i = 1}^{r} M_{i}$ with $M_{i} ≅ V_{i}^{\oplus m_{i}}$ for each $i$ , the isotypic decomposition supplied by [F2]. For $j \neq i$ Schur's lemma over $C$ gives ${Hom}_{A} (V_{j}, M_{i}) = 0$ , because a nonzero such map would be an isomorphism from the simple module $V_{j}$ onto a simple submodule of $M_{i}$ , which is a direct sum of copies of $V_{i}$ ; and ${Hom}_{A} (V_{i}, M_{i}) ≅ {Hom}_{A} (V_{i}, V_{i})^{m_{i}}$ because the finite direct sum $M_{i}$ is a biproduct, with the components read off by the inclusions and projections of the $m_{i}$ copies of $V_{i}$ . With $D_{i} : = {End}_{A} (V_{i})$ a division ring by [F1], this identifies ${Hom}_{A} (V_{i}, M)$ with $D_{i}^{m_{i}}$ as a $C$ -vector space.

2.1F1F4step 1.1algebra

Each $D_{i}$ is a finite-dimensional $C$ -division algebra: it is a $C$ -algebra because $A$ is one and the action is $C$ -linear, and it is finite-dimensional because $V_{i}$ is a quotient of the finite-dimensional algebra $A$ , hence finite-dimensional over $C$ . For $0 \neq T \in D_{i}$ the left multiplication $L_{T} : D_{i} \to D_{i}$ is a $C$ -linear endomorphism of a nonzero finite-dimensional $C$ -space, so it has an eigenvalue $λ$ by [F4]; then $T - λ$ is not invertible, so $T = λ$ and $T \in C$ ; hence $D_{i} = C$ . In particular $\dim_{C} {Hom}_{A} (V_{i}, M) = m_{i}$ by step 1.1.

3.1F3F5step 1.1step 2.1algebra

The matrix description of endomorphisms of the finite direct sum $M = ⨁_{i} M_{i}$ from [F3], together with the vanishing ${Hom}_{A} (V_{j}, M_{i}) = 0$ for $j \neq i$ of step 1.1, gives a $C$ -algebra isomorphism $E ≅ \prod_{i = 1}^{r} {End}_{A} (M_{i})$ ; applying the matrix description again inside each isotypic block, and $D_{i} = C$ from step 2.1, gives ${End}_{A} (M_{i}) ≅ M_{m_{i}} ({End}_{A} (V_{i})) = M_{m_{i}} (C)$ , so $E ≅ \prod_{i} M_{m_{i}} (C)$ . If $r = 0$ then $M = 0$ , $E = 0$ is semisimple by the definition of Semisimple modules as direct sums of simple modules read for the zero ring, and the statement is the empty product; if $r \geq 1$ then $E \neq 0$ and Wedderburn-Artin [F5] applied to the product of matrix rings over the division rings $C$ shows that $E$ is semisimple. This proves assertion (1).

4.1F5step 1.1step 2.1step 3.1algebra

The space $S_{i} = {Hom}_{A} (V_{i}, M)$ is a left $E$ -module by postcomposition $(e \cdot f) (v) = e (f (v))$ , since a composite of $A$ -linear maps is $A$ -linear, and by step 1.1 it is $C$ -linearly isomorphic to ${End}_{A} (V_{i})^{m_{i}} = C^{m_{i}}$ . Under the isomorphism $E ≅ \prod_{i} M_{m_{i}} (C)$ of step 3.1 and this identification, an endomorphism $e = (e^{(1)}, \dots, e^{(r)})$ acts on the $i$ -th component of $M$ through the matrix $e^{(i)}$ acting on $C^{m_{i}}$ by matrix multiplication; hence $S_{i}$ is precisely the natural column module $C^{m_{i}}$ of the $i$ -th matrix factor of $E$ , a simple $E$ -module, and by [F5] these column modules represent all isomorphism classes of simple $E$ -modules, one per factor. Therefore $i \mapsto S_{i}$ is a bijection onto those classes and $\dim_{C} S_{i} = m_{i}$ : assertions (2) and (3).

5.1step 3.1step 4.1∎

Assertion (1) is step 3.1, and assertions (2) and (3) are step 4.1 together with the identification $\dim_{C} {Hom}_{A} (V_{i}, M) = m_{i}$ of step 2.1; this proves everything asserted for $E = {End}_{A} (M)$ . If $E^{'}$ is semisimple and $φ : E^{'} \to E$ is an algebra isomorphism, the map $S \mapsto S$ with $E^{'}$ -action $e^{'} \cdot f : = φ (e^{'}) \cdot f$ identifies the simple $E^{'}$ -modules with the simple $E$ -modules and preserves dimensions, so the indexing and multiplicities transport along $φ$ ; the same argument applies to any abstract isomorphism onto ${End}_{A} (M)$ . Every step used only finite-dimensional $C$ -linear algebra, the cited structure theorems and explicit component projections, so no choice principle is used.

Depends on

Used by

Dependency tree · two levels

32 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jay Taylor, Finite Reductive Groups - Theorem 5.21 and the paragraph after (1.7) of Curtis, printed pp. 45-46 (standard reference, not scraped)
Olivier Dudas and Jean Michel, Lectures on Finite Reductive Groups and Their Representations - Proposition 10.8 and its proof (parametrisation of a Harish-Chandra series by irreducible representations of the endomorphism algebra), printed pp. 43-44 (standard reference, not scraped)
Ivan Losev, Lecture 8: Representations of GL_n(F_q) - Section 2.1 (simple summands of a module with semisimple endomorphism algebra), PDF pp. 3-4 (standard reference, not scraped)