Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Frobenius' formula for the character of an induced representation

Statement

Let G be a finite group, let H≤G, and let χ be the character of a finite-dimensional complex representation of H. Then for every g∈G,

Ind⁡HGχ(g)=1∣H∣∑x∈Gx−1gx∈Hχ(x−1gx).

Facts & Assumptions

Given: A finite group G, a subgroup H≤G, a finite-dimensional complex representation W of H with character χ, and an element g∈G.

[F1]

The induced character is the character of the induced representation Ind⁡HGW (The induced character Ind⁡HGχ of a complex character).

[F2]

A left transversal identifies Ind⁡HGW with a direct sum of one copy of W for each left coset of H in G (A left transversal identifies Ind⁡HGW with a direct sum of [G:H] copies of W).

[F3]

A complex character is constant on conjugacy classes, and χ(h)=tr⁡ρ(h) on its defining representation (For a complex character, χ(1)=dim⁡V, χ is a class function, and ∣χ(g)∣≤χ(1) with equality exactly at scalars).

[F4]

A finite sum is unchanged by reindexing a finite set bijectively (The sum ∑i∈Sai over a finite index set, and its product form).

Proof

technique · direct
1.1F2givenchoose

Choose a left transversal T for G/H. By [F2], Ind⁡HGW≅⨁t∈TWt, where each Wt is one copy of W indexed by the coset representative t.

2.1F1F2step 1.1algebra

For t∈T, write gt=t′h with t′∈T and h∈H. Under the identification of step 1.1, the action of g sends the t-summand to the t′-summand; if t′=t, so t−1gt=h∈H, then this action on Wt is exactly the action of h=t−1gt on W. Therefore the contribution of the t-summand to the trace is χ(t−1gt) when t−1gt∈H, and 0 otherwise.

3.1F1step 2.1algebra

The trace of g on the direct sum of step 1.1 is the sum of the traces on the summands fixed by the permutation it induces on T. Hence Ind⁡HGχ(g)=∑t∈T, t−1gt∈Hχ(t−1gt).

4.1F3step 3.1algebra

Fix t∈T with t−1gt∈H. The elements of the left coset tH are x=th with h∈H, and then x−1gx=h−1t−1gth. By [F3], the character value χ(x−1gx) is therefore the constant χ(t−1gt) on that whole coset, and every element of tH contributes to the displayed sum exactly when t−1gt∈H. So the total contribution of tH to ∑x−1gx∈Hχ(x−1gx) is ∣H∣χ(t−1gt).

5.1F4step 3.1step 4.1algebra∎

Summing the identity of step 4.1 over the distinct cosets indexed by T, and reindexing by the finite partition G=⨆t∈TtH, gives ∑x∈G, x−1gx∈Hχ(x−1gx)=∣H∣∑t∈T, t−1gt∈Hχ(t−1gt). By step 3.1 and [F4], dividing by ∣H∣ yields the stated Frobenius formula.

Depends on

Used by

Dependency tree · two levels

23 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