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.

Simple roots and fundamental weights of A_n

Example

For $A_{n}$ realized in the sum-zero subspace $E = {x \in R^{n + 1} : \sum_{i} x_{i} = 0}$ the simple roots are $α_{i} = e_{i} - e_{i + 1}$ , $1 \leq i \leq n$ , and the fundamental weights are $ω_{k} = e_{1} + \dots + e_{k} - \frac{k}{n + 1} \sum_{i = 1}^{n + 1} e_{i}, 1 \leq k \leq n .$

Facts & Assumptions

Given: The model $A_{n} = {ε_{i} - ε_{j} : i \neq j}$ in the sum-zero subspace of $R^{n + 1}$ , with simple roots $α_{i} = e_{i} - e_{i + 1}$ and the vectors $ω_{k}$ displayed.

[L1]

In this model $A_{n}$ is a reduced crystallographic root system with simple roots $α_{i} = e_{i} - e_{i + 1}$ (Classical root systems in coordinates, Existence of each classified root system).

[L2]

The coroot of $α$ is $α^{\lor} = 2 α / (α, α)$ and the fundamental weights are the vectors dual to the simple coroots, $(ω_{k}, α_{i}^{\lor}) = δ_{k i}$ (Fundamental weights, Coroot and dual root system).

Verification

technique · direct

1.1

$(α_{i}, α_{i}) = 2$ and $α_{i}^{\lor} = α_{i}$ , since $α_{i}$ has two nonzero coordinates equal to $\pm 1$ .

L1L2algebra

2.1

For every $i, k$ one has $(ω_{k}, α_{i}) = (ω_{k}, e_{i}) - (ω_{k}, e_{i + 1})$ ; the vector $ω_{k}$ has coordinates $1 - k / (n + 1)$ in positions $1, \dots, k$ and $- k / (n + 1)$ in positions $k + 1, \dots, n + 1$ , so the difference equals $1$ when $i = k$ and $0$ otherwise. Hence $(ω_{k}, α_{i}^{\lor}) = δ_{k i}$ and the displayed vectors are the fundamental weights of $A_{n}$ ; they form a basis of the weight lattice by [L2].

L2step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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

Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I, Lectures 19-24 (standard reference, not scraped)