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.

Induction of an inertia constituent is irreducible

Statement

Let $G$ be finite, $N ⊴ G$ , $θ \in Irr (N)$ , and $I = I_{G} (θ)$ . If $W$ is an irreducible complex $I$ -module lying over $θ$ , then $W ∣_{N}$ is $θ$ -isotypical and $X = {Ind}_{I}^{G} W$ is irreducible. Its $θ$ -isotypical component is the identity-coset copy of $W$ , consisting of the covariant functions supported on $I$ .

Facts & Assumptions

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

[F1]

For an irreducible module of a finite group, restriction to a normal subgroup has one orbit of constituents. (Normal restriction has one orbit of constituents).

[F2]

An $N$ -submodule of a complex $G$ -module is the direct sum of its intersections with the normal isotypical components. (Translation permutes normal isotypical components).

[F3]

Evaluation on a finite left transversal identifies an induced function module with the direct sum of its coset-supported copies of the inducing space. (A left transversal identifies ${Ind}_{H}^{G} W$ with a direct sum of $[G : H]$ copies of $W$ ).

Proof

technique · direct

1.1

Apply the orbit result inside $I$ : every element of $I$ fixes $θ$ , so $W ∣_{N}$ is a positive number of copies of $θ$ .

F1given

2.1

Use a left transversal $T$ containing $1$ , and write $X = ⨁_{t \in T} X_{t}$ , where $X_{t}$ consists of functions supported on $t I$ . For $n \in N$ , covariance gives $(n f) (t) = f (n^{- 1} t) = f (t (t^{- 1} n^{- 1} t)) = (t^{- 1} n t) f (t)$ . Thus evaluation makes $X_{t}$ a module of type $^{t} θ$ . These types are distinct for distinct $t I$ , so the $X_{t}$ are exactly the normal isotypical components, and $X_{1} ≅ W$ as an $I$ -module.

F3step 1.1algebra

3.1

If $Y \subseteq X$ is a nonzero $G$ -submodule, the intersection decomposition gives $Y \cap X_{t} \neq 0$ for some $t$ . Left translation by $t^{- 1}$ carries $X_{t}$ onto $X_{1}$ and preserves $Y$ , so $Y \cap X_{1} \neq 0$ . This intersection is $I$ -stable, hence equals $X_{1}$ by irreducibility of $W$ . Translating back fills every $X_{t}$ , giving $Y = X$ . This includes $I = G$ (one block) and $I = N$ (induction of the chosen normal type).

F2step 2.1given∎

Depends on

Used by

Clifford correspondence Theorem

Dependency tree · two levels

12 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 — Theorem 4.2.4(1) pp.55–56; Späth Theorem 1.2 (standard reference, not scraped)