LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Isotypical evaluation and multiplicity subspaces

Statement

Let $N$ be a finite group, let $S$ be an irreducible complex $N$ -module with character $θ$ , and let $U$ be a finite-dimensional $θ$ -isotypical $N$ -module, allowing $U = 0$ . Put $M = {Hom}_{N} (S, U)$ and give $M$ the trivial $N$ -action. Evaluation is an $N$ -isomorphism $E_{U} : S \otimes_{C} M ⟶ U, s \otimes f ⟼ f (s) .$ Every $N$ -submodule $U_{0} \subseteq U$ is $E_{U} (S \otimes M_{0})$ for a unique subspace $M_{0} \subseteq M$ , namely $M_{0} = {Hom}_{N} (S, U_{0})$ viewed inside $M$ by inclusion. If $U^{'}$ is another such module and $M^{'} = {Hom}_{N} (S, U^{'})$ , then every $N$ -map $U \to U^{'}$ is uniquely $E_{U^{'}} (1_{S} \otimes a) E_{U}^{- 1}$ for a linear map $a : M \to M^{'}$ . These identifications preserve composition.

Facts & Assumptions

Given: The groups, modules, characters, and hypotheses in the statement. All representations here are finite-dimensional complex left representations.

[F1]

Finite-dimensional complex representations of a finite group are completely reducible. (If $char k ∤ ∣ G ∣$ , every finite-dimensional representation of $G$ is completely reducible).

[F2]

Every endomorphism of an irreducible representation over an algebraically closed field is scalar. (Over an algebraically closed field, every endomorphism of an irreducible representation is scalar).

[F3]

The tensor representation has diagonal action on elementary tensors; in particular, when the second factor is trivial, $n (s \otimes m) = (n s) \otimes m$ . (The tensor product of two complex representations).

[F4]

A balanced map on a right and a left module induces a unique homomorphism from their tensor product, with the specified values on elementary tensors. (Universal property of the tensor product for balanced maps into abelian groups).

Proof

technique · direct

1.1

The map $(s, f) \mapsto f (s)$ is complex bilinear, so the tensor universal property defines evaluation. It is complex linear since this is true on elementary tensors, and it is $N$ -linear because $f (n s) = n f (s)$ and $N$ acts trivially on the second factor.

F3F4given

2.1

Complete reducibility and the isotypical hypothesis give $U ≅ S^{\oplus m}$ for some integer $m \geq 0$ . Fix inclusions $j_{1}, \dots, j_{m} : S \to U$ from such a decomposition. Each component of an $N$ -map $S \to U$ is a scalar endomorphism of $S$ , so the $j_{a}$ form a basis of $M$ . Evaluation sends $s \otimes j_{a}$ to $j_{a} (s)$ and is therefore an isomorphism. When $m = 0$ , both spaces and this map are zero.

F1F2step 1.1

3.1

If $U_{0} \subseteq U$ is an $N$ -submodule, it is completely reducible. Every simple summand $R$ of $U_{0}$ is isomorphic to $S$ : some coordinate projection $R \to S$ is nonzero, and its kernel and image are submodules, forcing an isomorphism. Apply step 2.1 to $U_{0}$ . Inclusion of its Hom space into $M$ intertwines the two evaluation maps on every elementary tensor, hence gives equality of actual subspaces $U_{0} = E_{U} (S \otimes M_{0})$ , with $M_{0} = {Hom}_{N} (S, U_{0})$ .

F1step 2.1algebra

4.1

For any subspace $M_{0} \subseteq M$ , the space $E_{U} (S \otimes M_{0})$ is $N$ -stable. The natural map $M_{0} \to {Hom}_{N} (S, E_{U} (S \otimes M_{0}))$ , sending $m$ to $(s \mapsto E_{U} (s \otimes m))$ , is an isomorphism by the scalar-coordinate calculation of step 2.1, and agrees with inclusion into $M$ . Thus recovery of $M_{0}$ is exact and unique, including $M_{0} = 0$ and $M_{0} = M$ .

F3step 2.1step 3.1

5.1

Choose simple decompositions of $U$ and $U^{'}$ . An $N$ -map between them is a matrix whose entries are endomorphisms of $S$ , hence scalars. Those scalar matrices are exactly the linear maps $a : M \to M^{'}$ . This proves the map assertion and uniqueness, also if either multiplicity space is zero. Composition satisfies $(1_{S} \otimes b) (1_{S} \otimes a) = 1_{S} \otimes (b a)$ on elementary tensors, proving compatibility.

F2step 2.1algebra∎

Depends on

Used by

Gallagher correspondence for an extendible type Theorem

Dependency tree · two levels

16 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

Ivan Losev, Representation Theory, Chapter 0. Basics — §2.3 Theorem 2.14, Corollary 2.16 and Proposition 2.17 pp.10–11 (standard reference, not scraped)