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.

Dynkin duality of B_n and C_n

Example

For $n \geq 2$ , the $B_{n}$ and $C_{n}$ diagrams have the same underlying chain and opposite arrows on the unique double edge; transposing the Cartan matrix exchanges them.

Facts & Assumptions

Given: An integer $n \geq 2$ ; the simple roots of $B_{n}$ : $α_{1} = ε_{1} - ε_{2}, \dots, α_{n - 1} = ε_{n - 1} - ε_{n}, α_{n} = ε_{n}$ ; and of $C_{n}$ : $β_{1} = ε_{1} - ε_{2}, \dots, β_{n - 1} = ε_{n - 1} - ε_{n}, β_{n} = 2 ε_{n}$ .

[L1]

The Cartan matrix entry is $a_{i j} = 2 (α_{j}, α_{i}) / (α_{i}, α_{i})$ , and the diagram has $a_{i j} a_{j i}$ edges with the arrow toward the shorter root (Cartan matrix of a based root system, Dynkin diagram with edge multiplicity and arrow convention).

[L2]

Coroot duality transposes the Cartan matrix, and the dual system of $B_{n}$ is $C_{n}$ (Duality exchanges B and C).

Verification

technique · direct

1.1

For $B_{n}$ : $∣ α_{i} ∣^{2} = 2$ for $i < n$ and $∣ α_{n} ∣^{2} = 1$ ; $(α_{n - 1}, α_{n}) = - 1$ , so $a_{n - 1, n} = 2 (- 1) / 2 = - 1$ and $a_{n, n - 1} = 2 (- 1) / 1 = - 2$ ; all other off-diagonal entries of adjacent pairs are $- 1$ and the rest vanish. Thus the diagram is a chain with a double edge at the end, the arrow being governed by $∣ a_{n, n - 1} ∣ = 2 > ∣ a_{n - 1, n} ∣ = 1$ and pointing toward the shorter root $α_{n}$ .

L1algebra

1.2

For $C_{n}$ : $∣ β_{i} ∣^{2} = 2$ for $i < n$ and $∣ β_{n} ∣^{2} = 4$ ; $(β_{n - 1}, β_{n}) = - 2$ , so $a_{n - 1, n} = 2 (- 2) / 2 = - 2$ and $a_{n, n - 1} = 2 (- 2) / 4 = - 1$ ; the diagram is again a chain with a double edge exactly at the end, and the arrow now points toward the shorter root $β_{n - 1}$ .

L1algebra

2.1

The matrices of steps 1.1 and 1.2 are transposes of one another, which is exactly coroot duality by [L2]; so transposing the Cartan matrix exchanges $B_{n}$ and $C_{n}$ , reversing the arrow while keeping the chain and the double-edge position.

L2step 1.1step 1.2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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)