LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

The Frobenius characteristic is an isometry

Statement

Extend the Hall form on $Λ$ $Q$ -bilinearly to $Λ_{Q}$ and then sesquilinearly to $Λ_{C} = C \otimes_{Q} Λ_{Q}$ , linear in the first argument and conjugate-linear in the second, so that $⟨ p_{ρ}, p_{σ} ⟩_{H} = δ_{ρ σ} z_{ρ}$ for all partitions $ρ, σ$ (Power sums are orthogonal for the Hall form, The Hall inner product on symmetric functions). For all $f, g \in c f (S_{n})$ ,

$⟨ ch (f), ch (g) ⟩_{H} = ⟨ f, g ⟩_{S_{n}} = \frac{1}{n!} \sum_{w \in S_{n}} f (w) \overline{g (w)} .$

Consequently $ch$ is injective on $c f (S_{n})$ , and $⟨ f, f ⟩_{S_{n}} = \sum_{ρ ⊢ n} ∣ f (ρ) ∣^{2} / z_{ρ} \geq 0$ with equality if and only if $f = 0$ .

Facts & Assumptions

Given: An integer $n \geq 0$ and class functions $f, g \in c f (S_{n})$ .

[F1]

$ch (f) = \sum_{ρ ⊢ n} f (ρ) p_{ρ} / z_{ρ} \in Λ_{C}^{n}$ , where $f (ρ)$ is the common value of $f$ on elements of cycle type $ρ$ and $z_{ρ} = \prod_{i} i^{m_{i} (ρ)} m_{i} (ρ)!$ (The Frobenius characteristic map).

[F2]

A class function is constant on conjugacy classes, and a class function is determined by its values on one representative of each conjugacy class; the space $c f (S_{n})$ carries pointwise addition and scalar multiplication (Class functions and the complex vector space $c f (G)$ ).

[F3]

The standard inner product on $c f (S_{n})$ is $⟨ φ, ψ ⟩_{S_{n}} = \frac{1}{n!} \sum_{w \in S_{n}} φ (w) \overline{ψ (w)}$ , linear in the first argument and conjugate-linear in the second, and it is positive definite (The standard inner product on $c f (G)$ ).

[F4]

The Hall form is the graded $Z$ -bilinear form on $Λ$ with $⟨ h_{λ}, m_{μ} ⟩_{H} = δ_{λ μ}$ ; its $Q$ -bilinear extension to $Λ_{Q}$ satisfies $⟨ p_{ρ}, p_{σ} ⟩_{H} = δ_{ρ σ} z_{ρ}$ for all partitions $ρ, σ$ (The Hall inner product on symmetric functions, Power sums are orthogonal for the Hall form).

[F5]

If $σ \in S_{n}$ has exactly $m_{i} (ρ)$ cycles of length $i$ , then its centralizer has order $z_{ρ} = \prod_{i} i^{m_{i} (ρ)} m_{i} (ρ)!$ (If $σ \in S_{n}$ has $c_{k}$ cycles of length $k$ , then $∣ C_{S_{n}} (σ) ∣ = \prod_{k = 1}^{n} k^{c_{k}} c_{k}!$ ).

[F6]

The conjugacy classes of $S_{n}$ are indexed by the cycle types $ρ ⊢ n$ , and for $w \in S_{n}$ the class of $w$ has cardinality $[S_{n} : C_{S_{n}} (w)] = n! / ∣ C_{S_{n}} (w) ∣$ (The conjugacy classes of $S_{n}$ are indexed by the tuples $(c_{1}, \dots, c_{n})$ with $\sum k c_{k} = n$ , $G / C_{G} (x) \to {Cl}_{G} (x)$ is a bijection, so $∣ {Cl}_{G} (x) ∣ = [G : C_{G} (x)]$ whenever these cardinalities are finite).

Proof

technique · direct

1.1F4

The $Q$ -bilinear extension of the Hall form to $Λ_{Q}$ extends to a sesquilinear form on $Λ_{C} = C \otimes_{Q} Λ_{Q}$ by $⟨ a \otimes x, b \otimes y ⟩_{H} : = a \overline{b} ⟨ x, y ⟩_{H}$ on decomposable tensors; it is well defined because the form is $Q$ -bilinear, it is linear in the first argument and conjugate-linear in the second, and on power sums it has $⟨ p_{ρ} / z_{ρ}, p_{σ} / z_{σ} ⟩_{H} = δ_{ρ σ} / z_{ρ}$ by [F4] and $z_{ρ} > 0$ .

1.2F2F3F5F6algebra

On the group side, grouping the defining sum of [F3] by conjugacy classes, which by [F6] are indexed by the cycle types $ρ ⊢ n$ and have cardinality $n! / z_{ρ}$ by [F5] and [F6], and using that $f, g$ are constant on classes by [F2], gives $⟨ f, g ⟩_{S_{n}} = \frac{1}{n!} \sum_{ρ ⊢ n} \frac{n!}{z_{ρ}} f (ρ) \overline{g (ρ)} = \sum_{ρ ⊢ n} f (ρ) \overline{g (ρ)} / z_{ρ}$ .

2.1F1F4step 1.1algebra

Expanding both characteristics in the basis ${p_{ρ} / z_{ρ} : ρ ⊢ n}$ of $Λ_{Q}^{n}$ via [F1] and using the sesquilinearity of step 1.1 and the values $⟨ p_{ρ} / z_{ρ}, p_{σ} / z_{σ} ⟩_{H} = δ_{ρ σ} / z_{ρ}$ , $⟨ ch (f), ch (g) ⟩_{H} = \sum_{ρ, σ} f (ρ) \overline{g (σ)} ⟨ p_{ρ} / z_{ρ}, p_{σ} / z_{σ} ⟩_{H} = \sum_{ρ ⊢ n} f (ρ) \overline{g (ρ)} / z_{ρ}$ .

3.1F3step 2.1step 1.2∎

Steps 2.1 and 1.2 prove the displayed isometry $⟨ ch (f), ch (g) ⟩_{H} = ⟨ f, g ⟩_{S_{n}}$ for all $f, g \in c f (S_{n})$ . Taking $g = f$ and using positive definiteness of the standard inner product [F3], $⟨ f, f ⟩_{S_{n}} = \sum_{ρ ⊢ n} ∣ f (ρ) ∣^{2} / z_{ρ} \geq 0$ , with equality exactly when $f (ρ) = 0$ for every $ρ$ , that is, when $f = 0$ ; hence if $ch (f) = 0$ then $⟨ f, f ⟩_{S_{n}} = ⟨ ch (f), ch (f) ⟩_{H} = 0$ and $f = 0$ , so $ch$ is injective on $c f (S_{n})$ .

Depends on

Used by

Sign twist corresponds to the omega involution Proposition
The Frobenius characteristic is an isometric graded ring isomorphism Theorem

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

I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Chapter I §7 (standard reference, not scraped)
Peter Webb, A Course in Finite Group Representation Theory, §3.2 (standard reference, not scraped)