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.
The A2 regular integral-dominant Verma embedding poset
Example
Let be regular dominant integral in type . The six distinct weights are indexed by , and there is an embedding exactly when in Bruhat order. Thus the directed Hasse diagram runs from the longest element's Verma module down through the two length-two, two length-one, and identity vertices as inclusions into .
Facts & Assumptions
Given: Strong linkage The strong linkage order on weights the BGG criterion The BGG criterion for homomorphisms between Verma modules, Bruhat order The Bruhat order on by rank inequalities, and injectivity A nonzero homomorphism between Verma modules is injective.
Verification
Put . Regularity makes the dot orbit free, so its members are indexed by the six elements of . For and a positive root , is positive exactly when is positive; integrality makes every such positive value a positive integer.
Write , , and . The positive-reflection pairs are . The rank inequalities defining Bruhat order give precisely these reflection comparisons (all except are covers). Thus checking the three positive roots of shows that the reflections satisfying step 1.1 are exactly the pairs in Bruhat order. In particular every strong-linkage edge lies in Bruhat order, while every Bruhat cover is one of these positive-integral reflection edges. Taking transitive closures and applying the BGG criterion proves the nonzero-homomorphism equivalence; the cited injectivity lemma turns every such map into an embedding. This proves both directions of the stated embedding equivalence.
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, Representations of Lie Groups, §15 (standard reference, not scraped)