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 character extension construction

Statement

Let $G$ be a finite Frobenius group with complement $H$ . For a nontrivial irreducible complex character $φ$ of $H$ put $θ : = φ - φ (1) 1_{H}$ and $\tilde{φ} : = {Ind}_{H}^{G} θ + φ (1) 1_{G}$ , where $1_{H}$ and $1_{G}$ denote the constant function with value $1$ on $H$ and on $G$ . Then

$\tilde{φ} ∣_{H} = φ, \tilde{φ} (1) = φ (1), \tilde{φ} (g) = φ (1) for every g \in G lying in no conjugate of H .$

Facts & Assumptions

Given: A finite group $G$ with Frobenius complement ${1} < H < G$ , a nontrivial irreducible complex character $φ$ of $H$ , and the class functions $θ = φ - φ (1) 1_{H}$ and $\tilde{φ} = {Ind}_{H}^{G} θ + φ (1) 1_{G}$ .

[F1]

Induction ${Ind}_{}^{H}$ is $C$ -linear on class functions, is given on $g \in G$ by the Frobenius sum, and agrees with honest induction on honest characters; the constant functions $1_{H}$ and $1_{G}$ are the characters of the trivial one-dimensional representations, hence are characters (Induced class functions and restricted class functions, The trivial representation, the regular representation, and permutation representations from finite $G$ -sets).

[F2]

If $θ \in c f (H)$ satisfies $θ (1) = 0$ , then ${Res}_{H}^{G} {Ind}_{H}^{G} θ = θ$ (Zero at identity induction restriction for a frobenius complement).

[F3]

$φ$ is the character of an irreducible complex representation of $H$ , so $φ$ is a class function with $φ (1) = \dim V \geq 1$ ; the constant function $1_{H}$ is the character of the trivial one-dimensional representation, and $φ \neq 1_{H}$ (An irreducible complex character, For a complex character, $χ (1) = \dim V$ , $χ$ is a class function, and $∣ χ (g) ∣ \leq χ (1)$ with equality exactly at scalars, The trivial representation, the regular representation, and permutation representations from finite $G$ -sets).

[F4]

A virtual character of a finite group is an integral linear combination of irreducible complex characters; the class functions on a finite group form a complex vector space (Virtual characters and the character ring $R (G)$ of a finite group, Class functions and the complex vector space $c f (G)$ ).

Proof

technique · direct

1.1

The function $θ = φ - φ (1) 1_{H}$ is a class function on $H$ with $θ (1) = φ (1) - φ (1) \cdot 1 = 0$ ; it is a virtual character of $H$ , being the integral combination $φ - φ (1) 1_{H}$ of the irreducible character $φ$ and the trivial character $1_{H}$ .

F3F4givenalgebra

2.1

By the linearity of induction in [F1], ${Ind}_{H}^{G} θ = {Ind}_{H}^{G} φ - φ (1) {Ind}_{H}^{G} 1_{H}$ ; here ${Ind}_{H}^{G} φ$ and ${Ind}_{H}^{G} 1_{H}$ are honest characters of $G$ , since $φ$ and $1_{H}$ are characters of $H$ , so ${Ind}_{H}^{G} θ$ is a virtual character of $G$ , and so is $\tilde{φ} = {Ind}_{H}^{G} θ + φ (1) 1_{G}$ .

F1step 1.1

2.2

Since $θ (1) = 0$ , [F2] gives ${Res}_{H}^{G} {Ind}_{H}^{G} θ = θ$ , and therefore $\tilde{φ} ∣_{H} = θ + φ (1) 1_{H} = φ - φ (1) 1_{H} + φ (1) 1_{H} = φ$ .

F2step 1.1algebra

3.1

Evaluating the same identity at the identity gives ${Ind}_{H}^{G} θ (1) = θ (1) = 0$ and hence $\tilde{φ} (1) = 0 + φ (1) \cdot 1 = φ (1)$ .

F2step 2.2algebra

4.1

Let $g \in G$ lie in no conjugate of $H$ , that is $x^{- 1} g x \notin H$ for every $x \in G$ . Then every summand in the Frobenius sum for ${Ind}_{H}^{G} θ (g)$ is absent, so ${Ind}_{H}^{G} θ (g) = 0$ and $\tilde{φ} (g) = 0 + φ (1) \cdot 1 = φ (1)$ . ∎

F1givenalgebra

Depends on

Used by

Dependency tree · two levels

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