LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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 character extension is irreducible

Statement

Let $G$ be a finite Frobenius group with complement $H$ and let $φ$ be a nontrivial irreducible complex character of $H$ . Then $\tilde{φ} = {Ind}_{H}^{G} θ + φ (1) 1_{G}$ with $θ = φ - φ (1) 1_{H}$ is an irreducible complex character of $G$ .

Facts & Assumptions

Given: A finite group $G$ with Frobenius complement ${1} < H < G$ , a nontrivial irreducible complex character $φ$ of $H$ , and the class function $\tilde{φ}$ of Frobenius character extension construction.

[F1]

Put $d = φ (1) \in N_{> 0}$ . The construction gives $\tilde{φ} = {Ind}_{H}^{G} (φ - d 1_{H}) + d 1_{G}$ , $\tilde{φ} ∣_{H} = φ$ and $\tilde{φ} (1) = d$ , hence ${Res}_{H}^{G} {Ind}_{H}^{G} θ = θ$ (Frobenius character extension construction). Induction of class functions is linear and sends honest characters to honest characters (Induced class functions and restricted class functions). Thus $\tilde{φ} = {Ind}_{H}^{G} φ - d {Ind}_{H}^{G} 1_{H} + d 1_{G}$ is an integral combination of honest characters. Each honest character has integral coefficients in the irreducible-character basis: its coefficient at $χ_{i}$ is its inner product with $χ_{i}$ , a dimension of an intertwiner space (The irreducible complex characters form an orthonormal basis of $c f (G)$ , The class-function inner product $⟨ χ_{V}, χ_{W} ⟩$ equals $\dim {Hom}_{G} (W, V)$ ). Consequently $\tilde{φ} = \sum_{i} n_{i} χ_{i}$ with $n_{i} \in Z$ , so it is a virtual character (Virtual characters and the character ring $R (G)$ of a finite group).

[F2]

For class functions $α$ on $H$ and $β$ on $G$ one has $⟨ {Ind}_{H}^{G} α, β ⟩_{G} = ⟨ α, {Res}_{H}^{G} β ⟩_{H}$ (Frobenius reciprocity for class functions).

[F3]

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

[F4]

Irreducible complex characters $ψ_{1}, ψ_{2}$ of a finite group satisfy $⟨ ψ_{1}, ψ_{2} ⟩ = δ_{12}$ ; the trivial character $1_{H}$ , being the character of the one-dimensional trivial representation, is irreducible with $⟨ 1_{H}, 1_{H} ⟩ = 1$ , and since $φ \neq 1_{H}$ the characters $φ$ and $1_{H}$ are distinct irreducibles, so $⟨ φ, 1_{H} ⟩ = 0$ and $⟨ φ, φ ⟩ = 1$ (The first orthogonality relation for irreducible complex characters, An irreducible complex character, The trivial representation, the regular representation, and permutation representations from finite $G$ -sets).

Proof

technique · direct

1.1

With $θ = φ - φ (1) 1_{H}$ one computes $⟨ θ, θ ⟩_{H} = ⟨ φ, φ ⟩ - 2 φ (1) ⟨ φ, 1_{H} ⟩ + φ (1)^{2} ⟨ 1_{H}, 1_{H} ⟩ = 1 + 0 + φ (1)^{2}$ , using the orthonormality data of [F4] and the linearity of the inner product in its first argument.

F3F4algebra

2.1

Similarly $⟨ θ, 1_{H} ⟩_{H} = ⟨ φ, 1_{H} ⟩ - φ (1) ⟨ 1_{H}, 1_{H} ⟩ = 0 - φ (1) = - φ (1)$ , and hence by [F2] $⟨ {Ind}_{H}^{G} θ, 1_{G} ⟩_{G} = ⟨ θ, {Res}_{H}^{G} 1_{G} ⟩_{H} = - φ (1)$ .

F2F4step 1.1algebra

2.2

By [F2] and the restriction identity of [F1], $⟨ {Ind}_{H}^{G} θ, {Ind}_{H}^{G} θ ⟩_{G} = ⟨ θ, {Res}_{H}^{G} {Ind}_{H}^{G} θ ⟩_{H} = ⟨ θ, θ ⟩_{H} = 1 + φ (1)^{2}$ .

F1F2step 1.1

3.1

Expanding $\tilde{φ} = {Ind}_{H}^{G} θ + φ (1) 1_{G}$ and using linearity in the first slot and conjugate-linearity in the second (the cross inner products are the equal real number $- d$ ) together with $⟨ 1_{G}, 1_{G} ⟩ = 1$ gives $⟨ \tilde{φ}, \tilde{φ} ⟩_{G} = ⟨ {Ind}_{H}^{G} θ, {Ind}_{H}^{G} θ ⟩_{G} + 2 φ (1) ⟨ {Ind}_{H}^{G} θ, 1_{G} ⟩_{G} + φ (1)^{2} ⟨ 1_{G}, 1_{G} ⟩_{G} = (1 + φ (1)^{2}) - 2 φ (1)^{2} + φ (1)^{2} = 1$ .

F3step 2.1step 2.2algebra

4.1

For the expansion $\tilde{φ} = \sum_{i} n_{i} χ_{i}$ of the virtual character $\tilde{φ}$ over the irreducible characters of $G$ in [F1], orthonormality [F4] gives $\sum_{i} n_{i}^{2} = ⟨ \tilde{φ}, \tilde{φ} ⟩_{G} = 1$ ; as the coefficients $n_{i}$ are integers, exactly one of them equals $\pm 1$ and all others are $0$ , so $\tilde{φ} = \pm χ$ for some irreducible character $χ$ of $G$ .

F1F4step 3.1algebra

5.1

Since $\tilde{φ} (1) = φ (1) \geq 1$ by [F1] while $χ (1) \geq 1$ and $(- χ) (1) < 0$ , the sign is positive, so $\tilde{φ} = χ$ is a genuine irreducible character of $G$ . ∎

F1step 4.1given

Depends on

Used by

Frobenius kernel is an intersection of character kernels Lemma

Dependency tree · two levels

37 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)