Alphabeta Math
PropositionStatement: Literature-sourcedProof: 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 and BGG characters give the same Weyl numerator

Statement

Assume the Axiom of Choice and let λ∈Λ+. Put D=∏α∈Φ+(1−e−α) and Nλ=∑w∈W(−1)ℓ(w)ew⋅λ. In the Grothendieck group of the linkage block Oλ, the BGG resolution gives [L(λ)]=∑w∈W(−1)ℓ(w)[M(w⋅λ)] by The BGG resolution of a finite-dimensional simple module. Applying its formal-character map and the Verma character formula The formal character of a Verma module gives ch⁡L(λ)=D−1Nλ. Separately, the spaces Hk(n+,L(λ)) are finite-dimensional h-modules, and Kostant's nilradical cohomology theorem gives ∑k≥0(−1)kch⁡hHk(n+,L(λ))=Nλ, as recorded in The Kostant Euler character recovers the Weyl numerator. Thus the character calculations identify the same finite Weyl numerator after clearing the Verma denominator in the BGG character formula. No equality between classes in different Grothendieck groups is asserted, and no spectral sequence is constructed.

Facts & Assumptions

Given: The Axiom of Choice; λ∈Λ+; the linkage block Oλ with its Grothendieck group and formal-character map; the finite sums D and Nλ.

[F1]

In the Grothendieck group of the linkage block, [L(λ)]=∑w(−1)ℓ(w)[M(w⋅λ)], and applying the character homomorphism with the Verma character ch⁡M(μ)=eμ∏α>0(1−e−α)−1 gives ch⁡L(λ)=∑w(−1)ℓ(w)ew⋅λD−1=D−1Nλ (The Euler-character identity for a finite-dimensional simple module, The BGG resolution of a finite-dimensional simple module, The Bruhat graph and the BGG Verma sum in degree k, The Grothendieck group and character of O, The formal character of a Verma module, The classical BGG category O, Verma and finite-dimensional weight modules belong to O).

[F2]

Independently of [F1], the Kostant decomposition computes the alternating sum of the finite-dimensional h-module characters of the nilradical cohomology: ∑k(−1)kch⁡Hk(n+,L(λ))=∑w(−1)ℓ(w)ew⋅λ=Nλ (The Kostant Euler character recovers the Weyl numerator, Kostant's nilradical cohomology theorem, Integral, dominant, and strictly dominant weights).

Proof

technique · compute the numerator twice, once from the BGG class and once from the cohomology decomposition, and compare after clearing the denominator
1.1F1

The BGG side: [F1] gives ch⁡L(λ)=D−1Nλ in the formal-character target of the category-O character map, where D=∏α>0(1−e−α) is the Verma denominator.

1.2F2

The cohomological side: by [F2] the alternating sum of the characters of the finite-dimensional h-modules Hk(n+,L(λ)) equals the same finite numerator Nλ, computed directly from the cohomology decomposition and using no Weyl-character input.

2.1F1F2step 1.1step 1.2∎

Clearing the common denominator D in step 1.1 and comparing with step 1.2 identifies the same finite sum Nλ: D⋅D−1Nλ=Nλ=∑k(−1)kch⁡Hk(n+,L(λ)). Both sides live in the common completed formal-character target after this clearing, and no equality of classes in different Grothendieck groups is used: the BGG class lives in K0(Oλ), while the cohomology spaces are finite-dimensional h-modules and their alternating character is computed there. No spectral sequence is constructed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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