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.
Class functions and the complex vector space
Definition
Let be a finite group. A function is a class function when it is constant on every conjugacy class (The conjugacy class and centralizer of an element):
The set of all class functions is written
With pointwise addition and pointwise scalar multiplication , the set is a complex vector space (Vector space over a field): the axioms (V1)–(V5) are inherited from the field at every argument . Because is finite, the evaluation functions are complex-linear, and a class function is determined by its values on one representative of each conjugacy class.
Depends on
Used by
- Induced class functions and restricted class functions Definition
- The Frobenius characteristic map Definition
- The standard inner product on cf(G) Definition
- Virtual characters and the character ring R(G) of a finite group Definition
- Frobenius character extension construction Lemma
- Frobenius reciprocity for class functions Lemma
- Row orthogonality for additive characters of a finite abelian group Lemma
- The Frobenius characteristic is an isometry Lemma
- Zero at identity induction restriction for a frobenius complement Lemma
- For a complex character, χ(1)=dim V, χ is a class function, and |χ(g)|≤χ(1) with equality exactly at scalars Proposition
- Irreducible Brauer characters form a basis of the p-regular class functions Theorem
- The irreducible complex characters form an orthonormal basis of cf(G) Theorem
Dependency tree · two levels
9 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, Section 3.2 (standard reference, not scraped)
- Pavel Etingof et al., Introduction to Representation Theory, Section 3.5 (standard reference, not scraped)