LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

Frobenius reciprocity for class functions

Statement

Let $G$ be a finite group, let $H \leq G$ be a subgroup, let $θ \in c f (H)$ be a class function on $H$ , and let $ψ \in c f (G)$ be a class function on $G$ . Then

$⟨ {Ind}_{H}^{G} θ, ψ ⟩_{G} = ⟨ θ, {Res}_{H}^{G} ψ ⟩_{H} .$

Facts & Assumptions

Given: A finite group $G$ , a subgroup $H \leq G$ , a class function $θ$ on $H$ , a class function $ψ$ on $G$ , and the induced and restricted class functions ${Ind}_{H}^{G} θ$ and ${Res}_{H}^{G} ψ$ of Induced class functions and restricted class functions.

[F1]

Restriction of class functions is the restriction map $ψ \mapsto ψ ∣_{H}$ , induction is the $C$ -linear map $θ \mapsto {Ind}_{H}^{G} θ$ given by the Frobenius formula, and for an honest character $χ$ of $H$ the class function ${Ind}_{H}^{G} χ$ is the honest induced character (Induced class functions and restricted class functions).

[F2]

The irreducible complex characters $φ_{1}, \dots, φ_{s}$ of $H$ form an orthonormal basis of $c f (H)$ , and the irreducible complex characters $χ_{1}, \dots, χ_{r}$ of $G$ form an orthonormal basis of $c f (G)$ (The irreducible complex characters form an orthonormal basis of $c f (G)$ , An irreducible complex character).

[F3]

The inner product $⟨ α, β ⟩ = \frac{1}{∣ G ∣} \sum_{g \in G} α (g) \overline{β (g)}$ is linear in its first argument and conjugate-linear in its second, on $c f (G)$ as well as on $c f (H)$ (The standard inner product on $c f (G)$ ).

[F4]

For complex characters $χ$ of $H$ and $ψ^{'}$ of $G$ one has $⟨ {Ind}_{H}^{G} χ, ψ^{'} ⟩_{G} = ⟨ χ, {Res}_{H}^{G} ψ^{'} ⟩_{H}$ (Frobenius reciprocity for complex characters).

[F5]

A class function on a finite group is determined by its values on conjugacy classes, and the space of class functions is a complex vector space (Class functions and the complex vector space $c f (G)$ ).

Proof

technique · direct

1.1

Since the irreducible characters form orthonormal bases, there are unique complex numbers $a_{1}, \dots, a_{s}$ and $b_{1}, \dots, b_{r}$ with $θ = \sum_{i = 1}^{s} a_{i} φ_{i}$ and $ψ = \sum_{j = 1}^{r} b_{j} χ_{j}$ .

F2F5given

2.1

By the linearity of induction in [F1], ${Ind}_{H}^{G} θ = \sum_{i} a_{i} {Ind}_{H}^{G} φ_{i}$ , and the functions ${Ind}_{H}^{G} φ_{i}$ are the honest induced characters of the characters $φ_{i}$ ; likewise ${Res}_{H}^{G} ψ = \sum_{j} b_{j} {Res}_{H}^{G} χ_{j}$ .

F1step 1.1

3.1

The inner product is linear in the first argument and conjugate-linear in the second, by [F3] on $G$ and on $H$ respectively, so bilinearity and the expansions of step 2.1 give $⟨ {Ind}_{H}^{G} θ, ψ ⟩_{G} = \sum_{i, j} a_{i} \overline{b_{j}} ⟨ {Ind}_{H}^{G} φ_{i}, χ_{j} ⟩_{G}$ and $⟨ θ, {Res}_{H}^{G} ψ ⟩_{H} = \sum_{i, j} a_{i} \overline{b_{j}} ⟨ φ_{i}, {Res}_{H}^{G} χ_{j} ⟩_{H}$ .

F3step 2.1

3.2

For every pair of indices $i, j$ the honest-character reciprocity [F4] applies to the character $φ_{i}$ of $H$ and the character $χ_{j}$ of $G$ , giving $⟨ {Ind}_{H}^{G} φ_{i}, χ_{j} ⟩_{G} = ⟨ φ_{i}, {Res}_{H}^{G} χ_{j} ⟩_{H}$ ; by step 2.1 the left-hand side is the same as $⟨ {Ind}_{H}^{G} φ_{i}, χ_{j} ⟩_{G}$ computed with the induced class function.

F1F4step 2.1

4.1

Substituting the identities of step 3.2 into the two expansions of step 3.1 makes the sums equal term by term, so $⟨ {Ind}_{H}^{G} θ, ψ ⟩_{G} = ⟨ θ, {Res}_{H}^{G} ψ ⟩_{H}$ , as claimed. ∎

step 3.1step 3.2

Depends on

Used by

Frobenius character extension is irreducible Lemma

Dependency tree · two levels

20 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

Alex Bartel, Introduction to Representation Theory of Finite Groups, §6.1 (standard reference, not scraped)
Peter Webb, A Course in Finite Group Representation Theory, §4.3 (standard reference, not scraped)