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.
Minimal realizations exist and are unique up to isomorphism
Statement
Every finite GCM has a minimal complex realization. Any two are isomorphic preserving all indexed roots and coroots. The dimension is the smallest possible dimension with both families independent.
Facts & Assumptions
Given: A GCM of size , rank , and the row convention .
The indexed roots and coroots must each be independent. (Realization of a generalized cartan matrix).
Proof
Let have basis , and define by . Choose a complement of by finite elimination. On put , and . The map is onto, so its coordinate functionals are independent; the are independent and have the prescribed evaluations. Moreover .
In any realization with independent roots, , , is onto. Its restriction to has rank , so . This proves the lower bound. At equality, , because .
For two minimal realizations choose the same complement of the common row image in . Lift a basis of to each using surjectivity of . The resulting linear sections give : an intersection vector has image both in and in the row image, hence zero; injectivity of on then kills it. Dimensions give spanning. The map , is invertible and commutes with , so preserves every . All selections are finite Gaussian elimination.
Sources
Source comparison: Kleshchev, Proposition 1.2.4, pp.11–12; independent row-image construction replaces a principal-minor assumption.
Depends on
Used by
- Contragredient lie algebra before the maximal ideal quotient Definition
- The affine a1 gcm has singular rank one realization data Example
- Nonsingular indecomposable Kac–Moody algebras are simple Lemma
Cited to discharge well-definedness by Realization of a generalized cartan matrix.
Dependency tree · two levels
2 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.