Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29
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.

Characters add on direct sums, multiply on tensor products, and conjugate on duals

Statement

Let G be a finite group and let V and W be finite-dimensional complex representations of G. Then, for every g∈G:

  1. χV⊕W(g)=χV(g)+χW(g);
  2. χV⊗W(g)=χV(g) χW(g);
  3. χV∗(g)=χV(g)‾.

Facts & Assumptions

Given: Finite-dimensional complex representations V, W of a finite group G, and an element g∈G.

[F2]

The dual action is (g⋅f)(v)=f(g−1⋅v) (The dual or contragredient complex representation).

[F3]

The tensor-product action is g⋅(v⊗w)=(g⋅v)⊗(g⋅w) (The tensor product of two complex representations).

[A1]

In a basis made of a basis of V followed by a basis of W, the matrix of the direct-sum action on V⊕W is block diagonal with the two action matrices on its diagonal, so its trace is the sum of the two block traces.

[A2]

Trace is linear, in particular additive, on the space of square matrices (Trace is a linear functional on Mn(F)).

[A3]

A basis of V and a basis of W give the basis (vi⊗wj)i,j of the tensor product (The elementary tensors of two bases form the product basis of the tensor product).

Proof

technique · direct
1.1F1A1A2given

Writing the direct-sum action in the concatenated basis of [A1], its trace is the sum of the traces of the two diagonal blocks, so χV⊕W(g)=tr⁡(ρV(g)⊕ρW(g))=tr⁡ρV(g)+tr⁡ρW(g)=χV(g)+χW(g) by [F1]. This is claim 1.

1.2F3A3given

By [F3] and [A3], the matrix of the tensor-product action in the basis (vi⊗wj) has entry ρV(g)ii′ ρW(g)jj′ at the position (i,j)↦(i′,j′), because g⋅(vi′⊗wj′)=∑i,jρV(g)ii′vi⊗ρW(g)jj′wj.

1.3F2given

With dual bases (vi) of V and (vi∗) of V∗, the matrix of the dual action of [F2] is the transpose of the matrix of ρV(g−1): writing g−1⋅vj=∑iρV(g−1)ijvi gives (g⋅vi∗)(vj)=vi∗(g−1⋅vj)=ρV(g−1)ij.

2.1F1step 1.2algebra

Its trace is the sum of its diagonal entries: ∑i,jρV(g)iiρW(g)jj=(∑iρV(g)ii)(∑jρW(g)jj). By [F1] the two factors are χV(g) and χW(g), so χV⊗W(g)=χV(g)χW(g), which is claim 2.

3.1F1A4step 1.3algebra∎

A matrix and its transpose have the same diagonal entries, hence the same trace, so χV∗(g)=tr⁡ρV(g−1)=χV(g−1). By [A4], χV(g−1)=χV(g)‾, which is claim 3.

Depends on

Used by

Dependency tree · two levels

23 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