QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Quantum Information / Representation Qit

Representation Qit

Exercise PLAN-109

intermediate · proof · test_public

primary source nl only. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

      Question

      Let G be a finite group and let the characters of its pairwise inequivalent complex irreducible representations W_1, ..., W_k be chi_1, ..., chi_k, orthonormal for the inner product (x, y) = (1/|G|) sum_{g} conj(x(g)) y(g); so (chi_i, chi_j) = delta_{ij}. Let (phi, V) be an arbitrary finite-dimensional complex representation with isotypical decomposition V ~ (+)_i W_i^{(+) n_i} (n_i the multiplicity of W_i). Prove that n_i = (chi_i, chi_V), where chi_V is the character of V. Then prove the two consequences: V is irreducible iff (chi_V, chi_V) = 1, and two representations are isomorphic iff they have equal characters.

      Hint: mathematical route

      Character orthonormality turns multiplicities into inner products n_i = (chi_i, chi_V), from which irreducibility (norm-squared one) and the isomorphism-iff-equal-characters criterion follow.

      1. Additivity of characters gives chi_V = sum_j n_j chi_j from V ~ (+)_j W_j^{(+)n_j}.
      2. Orthonormality (chi_i, chi_j) = delta_{ij} yields (chi_i, chi_V) = n_i.
      3. (chi_V, chi_V) = sum_i n_i^2, which equals 1 iff a single n_i = 1: V irreducible.
      4. Equal characters force equal multiplicities n_i = (chi_i, chi_V), hence the same decomposition and V ~ V'.
      Reference solution

      By additivity of the character under direct sums (chi_{A (+) B} = chi_A + chi_B, which follows from tr being additive on block-diagonal operators), the isotypical decomposition V ~ (+)_j W_j^{(+) n_j} gives chi_V = sum_j n_j chi_j. Taking the inner product with chi_i and using bilinearity (conjugate-linearity in the first slot but the n_j are real nonnegative integers) together with orthonormality, (chi_i, chi_V) = (chi_i, sum_j n_j chi_j) = sum_j n_j (chi_i, chi_j) = sum_j n_j delta_{ij} = n_i. This proves the multiplicity formula. Consequence 1: compute (chi_V, chi_V) = (sum_i n_i chi_i, sum_j n_j chi_j) = sum_{i,j} n_i n_j delta_{ij} = sum_i n_i^2. Since the n_i are nonnegative integers, sum_i n_i^2 = 1 holds iff exactly one n_i equals 1 and all others are 0, i.e. iff V is (isomorphic to) a single irreducible W_i; thus V is irreducible iff (chi_V, chi_V) = 1. Consequence 2: if V ~ V' then they have the same character (characters are isomorphism invariants, since conjugate representation matrices have equal trace). Conversely, the multiplicities n_i = (chi_i, chi_V) are determined entirely by chi_V; so if chi_V = chi_{V'} then n_i(V) = n_i(V') for all i, meaning V and V' have the same isotypical decomposition and hence V ~ V'. Therefore two representations are isomorphic iff their characters coincide.

      Assessment rubric
      1. Expands chi_V = sum_j n_j chi_j from additivity of characters over the isotypical decomposition (1 weight)
      2. Computes (chi_i, chi_V) = sum_j n_j delta_{ij} = n_i using orthonormality of the irreducible characters (1 weight)
      3. Derives (chi_V, chi_V) = sum_i n_i^2 and argues it equals 1 (n_i nonnegative integers) iff V is irreducible (1 weight)
      4. Proves V ~ V' iff chi_V = chi_{V'} by noting the multiplicities, hence the whole decomposition, are determined by the character (1 weight)

      Graph-grounded prerequisites

      These are support/source anchors, not an automatically extracted theorem-dependency proof.

      • Harmonic analysis (frozen curriculum anchor; see graph registry)
      • Matrix analysis (frozen curriculum anchor; see graph registry)

      Download the shared core registry

      Lean view and evidence boundary

      No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

      Read the Lean track and existing diagnostic warmups

      Sources and provenance

      Contract: 3663d152b195ac1be961f0e4865bee80da4352df02d91d6f38b57e182057593b

      Item digest: 940d170e2bda6414a28189165ce2bc37170ee0653d2cf788e54f04b40a60ecd5

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

      Authored support steps: 4. This is not measured graph distance or model difficulty.