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.
Characters add on direct sums, multiply on tensor products, and conjugate on duals
Statement
Let be a finite group and let and be finite-dimensional complex representations of . Then, for every :
- ;
- ;
- .
Facts & Assumptions
Given: Finite-dimensional complex representations , of a finite group , and an element .
The character is (The character of a finite-dimensional complex representation).
The dual action is (The dual or contragredient complex representation).
The tensor-product action is (The tensor product of two complex representations).
In a basis made of a basis of followed by a basis of , the matrix of the direct-sum action on is block diagonal with the two action matrices on its diagonal, so its trace is the sum of the two block traces.
Trace is linear, in particular additive, on the space of square matrices (Trace is a linear functional on ).
A basis of and a basis of give the basis of the tensor product (The elementary tensors of two bases form the product basis of the tensor product).
For a complex character, (For a complex character, , is a class function, and with equality exactly at scalars).
Proof
Writing the direct-sum action in the concatenated basis of [A1], its trace is the sum of the traces of the two diagonal blocks, so by [F1]. This is claim 1.
By [F3] and [A3], the matrix of the tensor-product action in the basis has entry at the position , because .
With dual bases of and of , the matrix of the dual action of [F2] is the transpose of the matrix of : writing gives .
Its trace is the sum of its diagonal entries: . By [F1] the two factors are and , so , which is claim 2.
A matrix and its transpose have the same diagonal entries, hence the same trace, so . By [A4], , which is claim 3.
Depends on
- The character $\chi_V(g)=\operatorname{tr}(\rho_V(g))$ of a finite-dimensional complex representation
- The dual or contragredient complex representation
- The tensor product of two complex representations
- For a complex character, $\chi(1)=\dim V$, $\chi$ is a class function, and $|\chi(g)|\le\chi(1)$ with equality exactly at scalars
- Trace is a linear functional on $M_n(F)$
- The elementary tensors of two bases form the product basis of the tensor product
Used by
- A complex character is irreducible if and only if its self-inner-product is 1 Corollary
- The multiplicity of an irreducible summand is a character inner product Corollary
- The regular character gives a second proof of the sum-of-squares formula Corollary
- Outer induction is not the Kronecker product Counterexample
- The outer induction product of symmetric-group characters Definition
- The restriction coproduct on the graded symmetric-group character ring Definition
- Virtual characters and the character ring R(G) of a finite group Definition
- The character table of S₄ and the normal subgroups it reveals Example
- The restriction coproduct of the character χ^(3,1) of S₄ Example
- The square of the two-dimensional S₃ character decomposes as 1+sgn+χ₂ Example
- The standard representation of Sₙ has character equal to the number of fixed points minus 1 Example
- Induction commutes with an external tensor factor Lemma
- The character ring of a direct product is the tensor product of the factor character rings Lemma
- Induction and restriction satisfy the projection formula on character rings Proposition
- Sign twist corresponds to the omega involution Proposition
- Character formula over a nonsplitting field Theorem
- Clifford restriction formula Theorem
- Gallagher correspondence for an extendible type Theorem
- The characteristic of a Specht character is a Schur function Theorem
- The class-function inner product ⟨χ_V,χ_W⟩ equals dimHom_G(W,V) Theorem
- The Frobenius characteristic is an isometric graded ring isomorphism Theorem
- The little group method for a semidirect product with abelian kernel Theorem
- The outer Littlewood–Richardson rule Theorem
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
- Peter Webb, A Course in Finite Group Representation Theory, Proposition 3.1.3 (standard reference, not scraped)
- Pavel Etingof et al., Introduction to Representation Theory, Section 3.4 (standard reference, not scraped)