TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-29

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.

The first orthogonality relation for irreducible complex characters

Statement

Let $G$ be a finite group and let $χ_{1}, \dots, χ_{r}$ be the irreducible complex characters of $G$ , one from each equivalence class. Then

$⟨ χ_{i}, χ_{j} ⟩ = δ_{i j} (1 \leq i, j \leq r) .$

Facts & Assumptions

Given: A finite group $G$ , and irreducible complex representations $V_{1}, \dots, V_{r}$ of $G$ with characters $χ_{1}, \dots, χ_{r}$ , one from each equivalence class.

[F1]

Irreducible characters are the characters of irreducible representations (An irreducible complex character).

[F2]

The inner product computes intertwiner dimension: $⟨ χ_{i}, χ_{j} ⟩ = \dim {Hom}_{G} (V_{j}, V_{i})$ (The class-function inner product $⟨ χ_{V}, χ_{W} ⟩$ equals $\dim {Hom}_{G} (W, V)$ ).

[F3]

Every nonzero intertwiner between irreducible representations is an isomorphism, and in particular ${End}_{G} (V_{i})$ is a division ring (Schur's lemma for irreducible representations: a nonzero intertwiner is an isomorphism, and ${End}_{G} (V)$ is a division ring).

[F4]

Over the algebraically closed field $C$ , every intertwiner $V_{i} \to V_{i}$ is a scalar operator (Over an algebraically closed field, every endomorphism of an irreducible representation is scalar).

Proof

technique · direct

1.1

For $i \neq j$ the representations $V_{i}$ and $V_{j}$ are inequivalent, because one representative was chosen from each class. If $T \in {Hom}_{G} (V_{j}, V_{i})$ were nonzero, [F3] would make $T$ an isomorphism, contradicting inequivalence; hence ${Hom}_{G} (V_{j}, V_{i}) = 0$ .

F3given

1.2

For $i = j$ , [F4] says every element of ${Hom}_{G} (V_{i}, V_{i}) = {End}_{G} (V_{i})$ is a scalar multiple of the identity. The identity operator is nonzero, so the scalars $λ {id}_{V_{i}}$ form a one-dimensional complex line. Hence $\dim {Hom}_{G} (V_{i}, V_{i}) = 1$ .

F4given

2.1

By [F2], $⟨ χ_{i}, χ_{j} ⟩ = \dim {Hom}_{G} (V_{j}, V_{i})$ ; steps 1.1 and 1.2 give this dimension to be $0$ when $i \neq j$ and $1$ when $i = j$ . This is exactly $⟨ χ_{i}, χ_{j} ⟩ = δ_{i j}$ .

F1F2step 1.1step 1.2algebra∎

Depends on

Used by

The multiplicity of an irreducible summand is a character inner product Corollary
The character table of a finite cyclic group over ℂ Example
The character table of A₄ Example
The character table of Dih(C₄) Example
The character table of Q₈ Example
The character table of S₃ Example
The irreducible complex characters form an orthonormal basis of cf(G) Theorem

Dependency tree · two levels

15 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, Theorem 3.2.3 (standard reference, not scraped)
Pavel Etingof et al., Introduction to Representation Theory, Theorem 3.8 (standard reference, not scraped)