Alphabeta MathHow 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 reciprocity for complex characters
Statement
Let be a finite group, let , let be a complex character of , and let be a complex character of . Then
Facts & Assumptions
Given: A finite group , a subgroup , a finite-dimensional complex representation of with character , and a finite-dimensional complex representation of with character .
The inner product of two complex characters equals the dimension of the intertwiner space between the corresponding representations (The class-function inner product equals ).
Induction is left adjoint to restriction: (Induction is left adjoint to restriction for finite-group modules over a commutative ring).
The character is the character of (The induced character of a complex character).
Proof
By [F3] and then [F1], .
By [F2], this dimension equals ; applying [F1] again on gives .
The expressions in steps 1.1 and 1.2 are equal, which is exactly the Frobenius reciprocity identity.
Depends on
Used by
- Cyclic fixed-space dimensions detect rational virtual characters Corollary
- Every irreducible complex character occurs in the induction of an irreducible constituent of its restriction Corollary
- M-groups are solvable (Taketa) Corollary
- Normal subgroup induction criterion Corollary
- Ramification indices account for the inertia quotient Corollary
- Frobenius reciprocity matches multiplicities in the two preceding S₃ inductions Example
- Restricting that degree-two S₃ character to the three-cycle subgroup gives the two nontrivial linear characters Example
- Branching rule for Specht modules: adding or removing boxes in distinct columns Lemma
- Frobenius character extension is irreducible Lemma
- Frobenius reciprocity for class functions Lemma
- Littlewood's identity - the internal product against an outer product Lemma
- Restriction to the two-block Young subgroup has LR multiplicities Lemma
- Induction and restriction satisfy the projection formula on character rings Proposition
- The restriction coproduct is Schur skewing Proposition
- Fixed-tabloid reconstruction of the character table (Fox–Mullineux) Theorem
- Mackey's irreducibility criterion for finite groups Theorem
Dependency tree · two levels
12 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, Corollary 4.3.8 (standard reference, not scraped)
- Anupam Singh, Representation Theory of Finite Groups, Chapter 19 (standard reference, not scraped)