Alphabeta Math
ExampleConstruction: AI-adaptedVerification: 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.

Degree-one Kostant classes correspond to simple reflections

Example

In the setting of Kostant's nilradical cohomology theorem, H1(n+,V)=⨁i=1rCsi⋅λ, one line for each simple reflection si, generated by the classes of the extremal cochains γsi of The extremal weight cochain of a Weyl element is closed and unique. This identifies the common simple-reflection indexing of degree-one Kostant cohomology and the first term ⨁iM(si⋅λ) of the BGG resolution, without identifying the cohomology lines with the Verma modules, and shows that distinct simple roots give distinct weights, because λ+ρ is regular.

Verification

Given: The setting of Kostant's nilradical cohomology theorem, with simple reflections s1,…,sr attached to a base Δ={α1,…,αr} of Φ+.

[L1] Hk(n+,V)≅⨁ℓ(w)=kCw⋅λ as h-modules, and consequently H1(n+,V)=⨁ℓ(w)=1Cw⋅λ (Kostant's nilradical cohomology theorem).

[L2] An element of W has length 1 exactly when it is a simple reflection: the length is the minimum number of simple reflections in an expression, so ℓ(w)=1 means w=si for some i, and conversely each si has ℓ(si)=1 with inversion set {αi} (Length and longest Weyl-group element, Finite Weyl positive roots and simple reflections, Simple roots form a signed integral basis, Root reflections and the Weyl group action).

[L3] The classes of the extremal cochains are nonzero and the cochain space in the extremal weight is one-dimensional: Cℓ(w)(n+,V)w⋅λ=Cγw and [γw]≠0 (The extremal weight cochain of a Weyl element is closed and unique).

[L4] Distinct simple roots give distinct reflections and distinct dot weights: si≠sj for i≠j, and λ+ρ has trivial stabilizer, so si⋅λ=sj⋅λ forces si=sj (Positive coroot pairings of a dominant integral weight, Integral, dominant, and strictly dominant weights).

[L5] The degree-one term of the BGG complex is C1(λ)=⨁ℓ(w)=1M(w⋅λ)=⨁i=1rM(si⋅λ) (The Bruhat graph and the BGG Verma sum in degree k, The classical BGG category O).

1.1L1L2L3

By [L1] and [L2], H1(n+,V)=⨁ℓ(w)=1Cw⋅λ=⨁i=1rCsi⋅λ, and each summand is generated by the class of γsi by [L3].

2.1L4L5step 1.1∎

By [L4] the weights si⋅λ are pairwise distinct, so the displayed sum is direct with one line per simple reflection; and by [L5] the same index set labels the first BGG term, giving H1(n+,V)≅⨁i=1rCsi⋅λ against C1(λ)=⨁iM(si⋅λ) as h-module statements.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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