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.

Translation permutes normal isotypical components

Statement

Let $G$ be finite, $N ⊴ G$ , and $V$ a finite-dimensional complex $G$ -module. For $θ \in Irr (N)$ let $V_{θ}$ be the sum of all simple $N$ -submodules of character $θ$ , with $V_{θ} = 0$ when that type does not occur. Then $g V_{θ} = V_{^{g} θ} (g \in G) .$ Every $N$ -submodule $U \subseteq V$ satisfies $U = ⨁_{θ occurring in V ∣_{N}} (U \cap V_{θ}) .$

Facts & Assumptions

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

[F1]

The left conjugate is $^{g} θ (n) = θ (g^{- 1} n g)$ and defines an action on $Irr (N)$ . (Inertia group and characters lying above a normal type).

[F2]

A finite-dimensional representation of a finite group over a field whose characteristic does not divide its order is completely reducible. (If $char k ∤ ∣ G ∣$ , every finite-dimensional representation of $G$ is completely reducible).

[F3]

A completely reducible module is the direct sum of its isotypical components, independently of a chosen simple decomposition. (The isotypic decomposition of a completely reducible representation is unique).

Proof

technique · direct

1.1

For a simple $N$ -submodule $S \subseteq V$ , its translate $g S$ is $N$ -stable since $n (g s) = g ((g^{- 1} n g) s)$ . The map $s \mapsto g s$ is an isomorphism from $^{g} S$ to $g S$ , so $g S$ is simple of the conjugate type.

F1givenalgebra

2.1

Translating each simple summand in the defining sum gives $g V_{θ} \subseteq V_{^{g} θ}$ . Applying the same argument to $g^{- 1}$ gives equality, also when a component is zero.

step 1.1algebra

3.1

By complete reducibility applied to $N$ over $C$ , both $V ∣_{N}$ and $U$ are direct sums of simple modules. Each simple summand of $U$ belongs to the ambient isotypical component of its own type. The ambient directness therefore gives the displayed intersection decomposition; for $U = 0$ or $V = 0$ it is the zero direct sum.

F2F3given∎

Depends on

Used by

Dependency tree · two levels

11 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

Tammo tom Dieck, Representation Theory — §4.2 pp.53–54 before Proposition 4.2.2; Losev Theorem 2.14(2) (standard reference, not scraped)
Ivan Losev, Representation Theory, Chapter 0. Basics, Theorem 2.14(2) and Proposition 2.17, pp.10–11 (standard reference, not scraped)