Alphabeta Math
CorollaryStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-09-05
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.

Cyclic fixed-space dimensions detect rational virtual characters

Statement

For each cyclic subgroup C≤G, define

mC(x):=⟨Res⁡CGx,1C⟩C(x∈RQ(G)).

Then the family (mC(x))(C), indexed by conjugacy classes of cyclic subgroups of G, determines x uniquely. In particular, the map

RQ(G)⟶∏(C)Q,x⟼(mC(x))(C)

is injective. For an honest Q-representation V, one has mC(χV)=dim⁡VC.

Facts & Assumptions

Given: A finite group G, an element x∈RQ(G), and a cyclic subgroup C≤G.

[F1]

The standard inner product on class functions is Hermitian, with linearity in the first argument and conjugate-linearity in the second, and it is positive definite. On rational-valued class functions its restriction is symmetric and Q-bilinear (The standard inner product on cf(G)).

[F2]

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

[F3]

For an honest finite-dimensional complex representation V, ⟨Res⁡CGχV,1C⟩C=dim⁡VC (The averaging operator projects onto the fixed subspace, The fixed subspace VG of a representation).

[F4]

For a finite cyclic group D, the generator-indicator class function ηD is an integral linear combination of permutation characters induced from subgroups of D (The generator-indicator class function of a cyclic group is obtained by Mobius inversion).

[F5]

Induction is transitive along subgroup chains (Induction is transitive along subgroup chains).

[F6]

Frobenius' formula computes induced character values (Frobenius' formula for the character of an induced representation).

[F7]

Every element of RQ(G) is a rational linear combination of characters induced from cyclic subgroups (Artin induction for rational characters).

Proof

technique · direct
1.1givenalgebra

Let C≤G be cyclic, and let y∈RQ(C). By The rational representation ring RQ(G) and rational-valued class functions, y is an integral linear combination of characters of finite-dimensional Q-representations of C, so it is enough to prove the next claim for one such character and then extend by linearity. Let ρ:C→GL⁡(V) be a finite-dimensional Q-representation with character y, let D≤C, and let d,d′ be generators of D. Then d′=du for some integer u coprime to ∣D∣. Because d∣D∣=1, the matrix ρ(d) has rational entries and satisfies ρ(d)∣D∣=I, so over C it is diagonalizable with eigenvalues among the ∣D∣-th roots of unity. Because the characteristic polynomial of ρ(d) lies in Q[t], those eigenvalues occur with multiplicities stable under the Galois automorphism ζ↦ζu of the cyclotomic field. Thus the multisets of eigenvalues of ρ(d) and ρ(d′)=ρ(d)u agree, so y(d′)=tr⁡ρ(d′)=tr⁡ρ(d)=y(d). Therefore every y∈RQ(C) is constant on the set of generators of each subgroup of C. The rational representation ring RQ(G) and rational-valued class functions

2.1step 1.1givenchooseconstruct

For each subgroup D≤C, choose a generator dD of D when D≠1 and put d1=e. Writing bD:=y(dD)∈Q, step 1.1 gives ∣C∣y=∑D≤CbD η~D, where η~D(c)=∣C∣ when ⟨c⟩=D and η~D(c)=0 otherwise.

3.1F4F5F6step 2.1algebra

For each D≤C, one has η~D=Ind⁡DCηD. Indeed, if c∈C generates D, then c∈D and C is abelian, so [F6] gives Ind⁡DCηD(c)=∣C∣; if ⟨c⟩≠D, then either c∉D or c does not generate D, and the induced value is 0. Using [F4] inside D and [F5] to induce further to C, each η~D is therefore an integral linear combination of the permutation characters UEC:=Ind⁡EC1E with E≤D. Thus every y∈RQ(C) is a rational linear combination of the UEC.

4.1F1F2step 3.1givenalgebra

Suppose now that mD(x)=0 for every cyclic subgroup D≤G. Let C≤G be cyclic. For each subgroup E≤C, the class functions Res⁡CGx and UEC are rational-valued, so [F1] makes their inner product symmetric. Using that symmetry and then Frobenius reciprocity [F2], we get ⟨Res⁡CGx,UEC⟩C=⟨UEC,Res⁡CGx⟩C=⟨1E,Res⁡EGx⟩E=⟨Res⁡EGx,1E⟩E=mE(x)=0.

5.1F1F2step 3.1step 4.1algebra

By step 3.1, every y∈RQ(C) is a rational linear combination of the class functions UEC, and both Res⁡CGx and y are rational-valued by The rational representation ring RQ(G) and rational-valued class functions. Thus the Q-bilinearity of [F1] on rational-valued class functions combines with step 4.1 to give ⟨Res⁡CGx,y⟩C=0 for every y∈RQ(C). Applying [F2] again, we get ⟨Ind⁡CGy,x⟩G=0 for every cyclic subgroup C≤G and every y∈RQ(C).

6.1F1F7step 5.1algebra

By [F7], the rational virtual character x is itself a rational linear combination of the induced characters Ind⁡CGy from step 5.1. Linearity of [F1] in the first argument and step 5.1 therefore give ⟨x,x⟩G=0. The positive definiteness in [F1] forces x=0. Therefore the map x↦(mC(x))(C) is injective.

7.1F3step 6.1∎

For an honest Q-representation V, the equality mC(χV)=dim⁡VC is exactly [F3].

Depends on

Used by

Dependency tree · two levels

30 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