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 values of a central character are algebraic integers
Statement
Let be a finite group, let be an irreducible complex character of , and let be a conjugacy class of . Then is an algebraic integer.
Facts & Assumptions
Given: A finite group , an irreducible complex character of , and a conjugacy class of .
The class sum acts on the irreducible representation affording as the scalar (Class sums act on an irreducible representation by central-character scalars).
An element is integral over exactly when it lies in a faithful module that is finitely generated over (Integrality and finite-module characterizations for one element).
Integral elements over a nonzero base ring form a subring (Integral elements over a nonzero base ring form a subring).
Proof
Let be the conjugacy classes of , and let be the -subring of generated by the class sums . If , then each coefficient counts pairs with , so . Hence the additive group of is contained in the free abelian group on the finitely many class sums, so is finitely generated as a -module.
The ring is a faithful -module over itself, and step 1.1 makes it finitely generated over . Therefore [F2] shows that each generator is integral over . Then [F3] implies that every element of is integral over .
Let be an irreducible representation affording . By [F1], the action of on sends each to a scalar , and is a ring homomorphism because the action of is by endomorphisms. If is monic with , then applying gives the monic equation . So is integral over , that is, an algebraic integer.
Depends on
Used by
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, Proposition 3.5.2 (standard reference, not scraped)
- Anupam Singh, Representation Theory of Finite Groups, Proposition 15.5 (standard reference, not scraped)