ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Symmetric powers as highest-weight modules

Example

Assume the Axiom of Choice. Let $g = {s l}_{n} (C)$ with its diagonal Cartan $h$ , coordinate functionals $ε_{i}$ and upper-triangular positive system as in Standard and dual representations of sl_n. For every $m \geq 1$ the symmetric power ${Sym}^{m} (C^{n})$ is an irreducible module of highest weight $m ω_{1}$ .

Facts & Assumptions

Given: The Axiom of Choice, such $g, h$ , the standard module $V = C^{n}$ with basis $e_{1}, \dots, e_{n}$ , and $W = {Sym}^{m} (V)$ , identified with the homogeneous polynomials of degree $m$ in the variables $x_{1}, \dots, x_{n}$ on which $E_{i j} \cdot x_{l} = δ_{j l} x_{i}$ and $H \cdot x_{l} = H_{l l} x_{l}$ .

[A1]

The Axiom of Choice is assumed; it enters through the root-space and highest-weight theory used below (The Axiom of Choice).

[L1]

The monomials $x_{1}^{a_{1}} \dots x_{n}^{a_{n}}$ with $a_{1} + \dots + a_{n} = m$ form a basis of $W$ , their weights $\sum_{i} a_{i} ε_{i}$ are pairwise distinct, and $ε_{1} = ω_{1}$ (Standard and dual representations of sl_n, Weight and weight space).

[L2]

For a finite set of pairwise distinct weights and one of them, there is an element of $U (h)$ acting as the projection onto the corresponding weight component, because $U (h)$ is the polynomial algebra on $h^{*}$ and polynomials separate finitely many distinct points (Poincaré–Birkhoff–Witt theorem).

[L3]

A nonzero module generated by a highest weight vector of weight $λ$ with one-dimensional top weight space is irreducible exactly when every nonzero submodule contains the whole monomial basis; a nonzero submodule of an irreducible module is the whole module (Irreducible, completely reducible, and faithful representations, Highest-weight vectors and modules).

Verification

technique · direct

1.1

The vector $x_{1}^{m}$ is a highest weight vector: $H \cdot x_{1}^{m} = m H_{11} x_{1}^{m}$ , so its weight is $m ε_{1} = m ω_{1}$ ; and $E_{i j} \cdot x_{1} = 0$ for $i < j$ because $j \neq 1$ , so $E_{i j} \cdot x_{1}^{m} = 0$ for every positive root vector.

L1givenA1

1.2

Let $0 \neq U \subseteq W$ be a submodule; writing a nonzero element as a sum of distinct-weight monomials, [L2] produces an element of $U (h)$ that projects onto one of them, so $U$ contains a monomial $x_{1}^{a_{1}} \dots x_{n}^{a_{n}}$ with $a_{j} > 0$ for some $j > 1$ unless it already contains $x_{1}^{m}$ .

L1L2

2.1

From any monomial $x_{1}^{a_{1}} \dots x_{n}^{a_{n}}$ with $a_{j} > 0$ , $j > 1$ , applying $E_{1 j}$ exactly $a_{j}$ times replaces all $x_{j}$ -factors by $x_{1}$ -factors with nonzero coefficient $a_{j}!$ , and repeating for $j = 2, \dots, n$ reaches a nonzero multiple of $x_{1}^{m}$ ; hence $x_{1}^{m} \in U$ by step 1.2.

givenstep 1.2

2.2

Conversely, from $x_{1}^{m}$ the operators $E_{l 1}$ with $l > 1$ replace $x_{1}$ -factors by $x_{l}$ -factors, and applying them $a_{l}$ times successively for $l = 2, \dots, n$ produces a nonzero multiple of $x_{1}^{a_{1}} \dots x_{n}^{a_{n}}$ ; hence $U$ contains the whole monomial basis and $U = W$ .

givenstep 1.2

3.1

Therefore every nonzero submodule of $W$ is $W$ , so $W$ is irreducible, and by step 1.1 its highest weight is $m ω_{1} =$ the weight of $x_{1}^{m}$ ; this proves the assertion.

L3step 1.1step 2.1step 2.2∎

Depends on

Used by

The full weight lattice need not integrate through a central quotient Counterexample

Dependency tree · two levels

35 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

Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)