Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-30
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.

Mackey's irreducibility criterion for finite groups

Statement

Let G be a finite group, let H≤G, let χ be an irreducible complex character of H, and let S be representatives for H\G/H with 1∈S. Then Ind⁡HGχ is irreducible if and only if for every s∈S∖{1},

⟨Res⁡H∩sHs−1Hχ,Res⁡H∩sHs−1sHs−1 sχ⟩H∩sHs−1=0.

Facts & Assumptions

Given: A finite group G, a subgroup H≤G, an irreducible complex character χ of H, and representatives S for H\G/H with 1∈S.

[F1]

A complex character is irreducible if and only if its self-inner-product is 1 (A complex character is irreducible if and only if its self-inner-product is 1).

[F2]

Frobenius reciprocity gives ⟨Ind⁡HGχ,ψ⟩G=⟨χ,Res⁡HGψ⟩H (Frobenius reciprocity for complex characters).

[F3]

Mackey's formula expands Res⁡HGInd⁡HGχ as a sum over the double cosets in H\G/H (Mackey's double-coset formula for restricting an induced character).

Proof

technique · direct
1.1

Because χ is irreducible, [F1] gives ⟨χ,χ⟩H=1. Applying [F2] with ψ=Ind⁡HGχ gives ⟨Ind⁡HGχ,Ind⁡HGχ⟩G=⟨χ,Res⁡HGInd⁡HGχ⟩H.

F1F2given
2.1

Apply [F3] to the restriction on the right side of step 1.1. The term for the identity double coset H is exactly χ, so it contributes 1. Every other term is Ind⁡H∩sHs−1H(Res⁡H∩sHs−1sHs−1 sχ), whose inner product with χ is, by another use of [F2], precisely ⟨Res⁡H∩sHs−1Hχ,Res⁡H∩sHs−1sHs−1 sχ⟩H∩sHs−1.

F2F3step 1.1algebra
3.1

Therefore ⟨Ind⁡HGχ,Ind⁡HGχ⟩G=1+∑s∈S∖{1}⟨Res⁡H∩sHs−1Hχ,Res⁡H∩sHs−1sHs−1 sχ⟩H∩sHs−1. Each summand is a multiplicity and hence a nonnegative integer.

F2step 2.1algebra
4.1

The self-inner-product in step 3.1 equals 1 if and only if every nonidentity summand vanishes. By [F1], that is equivalent to Ind⁡HGχ being irreducible.

F1step 3.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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