ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Kostant cohomology for sl2

Example

Assume the Axiom of Choice, inherited from Kostant's theorem (The Axiom of Choice). Let $g = {s l}_{2} (C)$ , with Cartan subalgebra $h = C H$ , positive root $α$ , Weyl vector $ρ = α / 2$ , fundamental weight $ω = α / 2$ , and $λ = m ω$ with $m \in Z_{\geq 0}$ , so that $V = L (m ω)$ has dimension $m + 1$ and $n^{+} = C e_{α}$ . The Weyl group is ${1, s}$ with $s \cdot λ = s (λ + ρ) - ρ = - λ - 2 ρ = - (m + 2) ω$ . Kostant's theorem gives $H^{0} (n^{+}, V) = C_{m ω}, H^{1} (n^{+}, V) = C_{- (m + 2) ω}, H^{k} (n^{+}, V) = 0 (k \geq 2),$ with generators $v_{m ω}$ and $ε_{α} \otimes v_{s λ}$ , where $v_{s λ} \in V_{s λ}$ has weight $s λ = - m ω$ . This verifies the sign of the dot action, the $ρ$ -shift and the top degree in the smallest rank, and shows that the degree-one weight is $- (m + 2) ω$ , not $- m ω$ .

Verification

Given: The Axiom of Choice; $g = {s l}_{2} (C)$ with the usual basis $H, e, f$ and positive root $α$ , the Weyl group ${1, s}$ , a nonnegative integer $m$ , the module $V = L (m ω)$ of dimension $m + 1$ , and $n^{+} = C e_{α}$ .

[L1] $s ρ = - ρ$ , $s α = - α$ , and the dot action is $s \cdot λ = s (λ + ρ) - ρ$ (Root reflections and the Weyl group action, The Weyl vector rho for a chosen positive system, The special linear Lie algebra sl_2, The root sl_2 triple).

[L2] $H^{k} (n^{+}, V) = ⨁_{ℓ (w) = k} C_{w \cdot λ}$ for $k = 0, 1$ and $H^{k} = 0$ for $k \geq 2$ , since $∣ Φ^{+} ∣ = 1$ and the Weyl group has the two elements $1, s$ of lengths $0, 1$ (Kostant's nilradical cohomology theorem, Kostant cohomology in degrees zero and top, Length and longest Weyl-group element).

[L3] $V = L (m ω)$ is finite dimensional of dimension $m + 1$ , the weight $s λ = - m ω$ occurs in $V$ with multiplicity one, and in degree one the extremal cochain of The extremal weight cochain of a Weyl element is closed and unique is $γ_{s} = ε_{α} \otimes v_{s λ}$ (Finite-dimensional representations of sl_2, Weight and weight space).

1.1L1L2

$1 \cdot λ = 1 (λ + ρ) - ρ = λ = m ω$ , and by [L1] $s \cdot λ = s (λ + ρ) - ρ = - λ - 2 ρ = - m ω - α = - (m + 2) ω$ ; since $∣ Φ^{+} ∣ = 1$ and $ℓ (1) = 0$ , $ℓ (s) = 1$ , [L2] gives the displayed cohomology.

1.2L1L2L3

In degree one, the generator is $ε_{α} \otimes v_{s λ}$ : its exterior factor has weight $- α$ and $v_{s λ}$ has weight $s λ = - m ω$ , so the total weight $- α - m ω = - (m + 2) ω$ is the dot weight, confirming the $ρ$ -shift; the degree-zero generator is the highest vector $v_{m ω}$ .

2.1L2step 1.2∎

Counting: $\dim H^{0} = 1$ , $\dim H^{1} = 1$ , and $H^{k} = 0$ for $k \geq 2$ , matching the top degree $∣ Φ^{+} ∣ = 1$ ; the degree-one weight is $- (m + 2) ω = - m ω - α$ , strictly below $- m ω$ , so the exterior root shift cannot be dropped.

Depends on

Used by

Omitting the exterior root-weight shifts gives the wrong dot weight Counterexample
Whitehead vanishing does not apply to the nilpotent radical Counterexample

Dependency tree · two levels

68 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

Peter Woit, Lie Algebra Cohomology and the Borel–Weil–Bott Theorem (Math G4344, Spring 2012), printed pp.1–7 (standard reference, not scraped)
Faisal Al-Faisal, On the Representation Theory of Semisimple Lie Groups (University of Waterloo MMath thesis, 2010), §3.4 printed pp.73–77 (standard reference, not scraped)