CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-30

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.

Every irreducible complex character occurs in the induction of an irreducible constituent of its restriction

Statement

Let $G$ be a finite group, let $H \leq G$ , and let $ψ$ be an irreducible complex character of $G$ . Then some irreducible constituent $φ$ of ${Res}_{H}^{G} ψ$ satisfies

⟨ {Ind}_{H}^{G} φ, ψ ⟩_{G} > 0.

Equivalently, $ψ$ occurs in the induced character ${Ind}_{H}^{G} φ$ .

Facts & Assumptions

Given: A finite group $G$ , a subgroup $H \leq G$ , and an irreducible complex character $ψ$ of $G$ .

[F1]

Over $C$ , every finite-dimensional representation of a finite group is completely reducible (If $char k ∤ ∣ G ∣$ , every finite-dimensional representation of $G$ is completely reducible).

[F2]

The multiplicity of an irreducible constituent is the corresponding character inner product (The multiplicity of an irreducible summand is a character inner product).

[F3]

Frobenius reciprocity gives $⟨ {Ind}_{H}^{G} φ, ψ ⟩_{G} = ⟨ φ, {Res}_{H}^{G} ψ ⟩_{H}$ (Frobenius reciprocity for complex characters).

Proof

technique · direct

1.1

Let $V$ be an irreducible representation of $G$ affording $ψ$ . Its restriction to $H$ is completely reducible by [F1], so ${Res}_{H}^{G} V ≅ ⨁_{i = 1}^{r} m_{i} W_{i}$ for irreducible $H$ -representations $W_{i}$ with characters $φ_{i}$ .

F1given

2.1

Because ${Res}_{H}^{G} V$ is nonzero, some multiplicity $m_{i}$ is positive. By [F2], this means $m_{i} = ⟨ φ_{i}, {Res}_{H}^{G} ψ ⟩_{H} > 0$ .

F2step 1.1choose

3.1

Applying [F3] to $φ = φ_{i}$ gives $⟨ {Ind}_{H}^{G} φ, ψ ⟩_{G} = ⟨ φ, {Res}_{H}^{G} ψ ⟩_{H} = m_{i} > 0$ .

F3step 2.1algebra

4.1

The strict positivity in step 3.1 means that $ψ$ occurs in the induced character ${Ind}_{H}^{G} φ$ , by the multiplicity interpretation of [F2].

F2step 3.1

5.1

The chosen irreducible constituent $φ : = φ_{i}$ therefore has the required property.

step 2.1step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

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

Peter Webb, A Course in Finite Group Representation Theory, Corollary 4.3.8 (standard reference, not scraped)
Anupam Singh, Representation Theory of Finite Groups, Chapter 19 (standard reference, not scraped)