ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Standard and dual representations of ${s l}_{n}$

Example

Assume the Axiom of Choice. Let $n \geq 2$ , $g = {s l}_{n} (C) = {A \in M_{n} (C) : tr A = 0}$ (Classical complex matrix Lie algebras), let $h$ be the diagonal traceless matrices, let $ε_{1}, \dots, ε_{n} \in h^{*}$ be the coordinate functionals $ε_{i} (H) = H_{i i}$ , and let the positive system be the roots $ε_{i} - ε_{j}$ with $i < j$ , with base $α_{j} = ε_{j} - ε_{j + 1}$ (Root systems of the classical complex Lie algebras). Then the standard module $C^{n}$ with its natural action is irreducible of highest weight $ω_{1} = ε_{1}$ , and its dual is irreducible of highest weight $ω_{n - 1} = - ε_{n}$ (Fundamental weights).

Facts & Assumptions

Given: The Axiom of Choice, such $g$ , its diagonal Cartan $h$ , the matrix units $E_{i j}$ , the coordinate functionals $ε_{i}$ , the positive system ${ε_{i} - ε_{j} : i < j}$ with simple roots $α_{j} = ε_{j} - ε_{j + 1}$ , the Killing form $B$ (Killing form), the standard module $V = C^{n}$ with basis $e_{1}, \dots, e_{n}$ , and its dual $V^{*}$ with dual basis $e_{1}^{*}, \dots, e_{n}^{*}$ .

[A1]

The Axiom of Choice is assumed; among the facts used below, it enters through the highest-weight classification in [L4]. The explicit classical root calculation [L1] has no choice hypothesis (The Axiom of Choice).

[L1]

The roots of $g$ with respect to $h$ are the functionals $ε_{i} - ε_{j}$ , $i \neq j$ , with root spaces $C E_{i j}$ ; each is one-dimensional and the root set is a reduced crystallographic Euclidean root system of type $A_{n - 1}$ (Root systems of the classical complex Lie algebras).

[L2]

For $α = ε_{i} - ε_{j}$ the coroot is $h_{α} = E_{i i} - E_{j j}$ : on diagonal traceless $X = diag (x_{1}, \dots, x_{n})$ one has $B (X, X) = tr ({ad}_{X}^{2}) = \sum_{i \neq j} (x_{i} - x_{j})^{2} = 2 n tr (X^{2})$ , so $B (E_{i i} - E_{j j}, H) = 2 n tr ((E_{i i} - E_{j j}) H) = 2 n (H_{i i} - H_{j j})$ and the normalisation $h_{α} = 2 H_{α} / α (H_{α})$ gives $h_{α} = E_{i i} - E_{j j}$ (Coroot of a Lie-algebra root).

[L3]

The fundamental weights are the functionals dual to the simple coroots: $ω_{k} (h_{α_{j}}) = δ_{k j}$ , and the simple coroots form a basis of $h$ (Fundamental weights, The roots form a reduced crystallographic Euclidean root system).

[L4]

A nonzero weight vector killed by all positive root vectors is a highest-weight vector of the module it generates; every finite-dimensional irreducible module has a unique highest weight (Highest-weight vectors and modules, Weight and weight space, Highest-weight classification).

[L5]

For $n \geq 2$ , the Killing form of ${s l}_{n} (C)$ is the nondegenerate form $B (X, Y) = 2 n tr (X Y)$ (Classical simple Lie algebras and their Killing forms); hence this finite-dimensional characteristic-zero Lie algebra is semisimple by Cartan's semisimplicity criterion. This supplies the semisimplicity hypothesis of [L2]--[L4].

Verification

technique · direct

1.1L1L5given

The action on $V$ is $H \cdot e_{i} = H_{i i} e_{i}$ and $E_{i j} \cdot e_{l} = δ_{j l} e_{i}$ ; hence the weights of $V$ are $ε_{1}, \dots, ε_{n}$ , each with one-dimensional weight space, and $e_{1}$ is killed by every positive root vector $E_{i j}$ with $i < j$ , since $j > i \geq 1$ forces $j \neq 1$ .

1.2given

$V$ is irreducible: if $0 \neq v = \sum_{i} v_{i} e_{i}$ and $v_{l} \neq 0$ , then $E_{i l} \cdot v = v_{l} e_{i}$ for every $i \neq l$ . Choose one such $i$ (possible since $n \geq 2$ ); applying $E_{l i}$ to the resulting $e_{i}$ gives $e_{l}$ . All matrix units used are off-diagonal and belong to ${s l}_{n}$ . Hence every basis vector belongs to the submodule generated by $v$ , which equals $V$ .

1.3given

For the dual module the action is $(X \cdot φ) (v) = - φ (X \cdot v)$ , so the weights of $V^{*}$ are $- ε_{1}, \dots, - ε_{n}$ on the dual basis vectors $e_{i}^{*}$ ; the vector $e_{n}^{*}$ is killed by every positive root vector: $(E_{i j} \cdot e_{n}^{*}) (v) = - e_{n}^{*} (E_{i j} v) = - e_{n}^{*} (v_{j} e_{i}) = - v_{j} δ_{i n} = 0$ because $i < j \leq n$ gives $i \neq n$ .

2.1A1L2L3L4step 1.1step 1.2

By [L2] and [L3], $ε_{1} (h_{α_{j}}) = ε_{1} (E_{j j} - E_{j + 1, j + 1}) = δ_{1 j} = ω_{1} (h_{α_{j}})$ for every $j$ , and the simple coroots span $h$ ; hence $ε_{1} = ω_{1}$ , so $V$ is irreducible with highest weight $ω_{1}$ by steps 1.1, 1.2 and [L4].

2.2givenstep 1.2

$V^{*}$ is irreducible: if $0 \neq W \subseteq V^{*}$ is a submodule, then its annihilator $W^{⊥} \subseteq V$ is a submodule: for $v \in W^{⊥}$ and $φ \in W$ , $φ (X v) = - (X φ) (v) = 0$ . Its dimension is $\dim W^{⊥} = n - \dim W < n$ , hence $W^{⊥} = 0$ by step 1.2 and $W = V^{*}$ .

3.1A1L2L3L4step 1.3step 2.2∎

Finally $- ε_{n} (h_{α_{j}}) = - (E_{j j} - E_{j + 1, j + 1})_{n n} = δ_{j, n - 1} = ω_{n - 1} (h_{α_{j}})$ for every $j$ , so $- ε_{n} = ω_{n - 1}$ by [L3]; hence $V^{*}$ is irreducible of highest weight $ω_{n - 1}$ by steps 1.3, 2.2 and [L4].

Depends on

Used by

Exterior powers and fundamental weights of slₙ Example
Symmetric powers as highest-weight modules Example
The eight-dimensional adjoint representation of sl3 Example

Dependency tree · two levels

59 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)
Alexander Kirillov Jr., An Introduction to Lie Groups and Lie Algebras (standard reference, not scraped)

Standard and dual representations of slnsln​