Alphabeta Math
CorollaryStatement: 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.

The Euler-character identity for a finite-dimensional simple module

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let λ∈Λ+. In the Grothendieck group of the linkage block of λ (The Grothendieck group and character of O, Simple and standard bases of K0(O)) the finite alternating sum of Verma classes equals the class of the simple module:

[L(λ)]=∑w∈W(−1)ℓ(w)[M(w∘λ)].

Equivalently, applying the character homomorphism and the Verma character ch⁡M(μ)=eμ∏α∈Φ+(1−e−α)−1 (The formal character of a Verma module),

ch⁡L(λ)=∑w∈W(−1)ℓ(w)ew∘λ∏α∈Φ+(1−e−α)−1,

the Weyl numerator identity in the form needed by the Weyl character formula. Proof: an exact finite complex has vanishing alternating sum of classes.

Facts & Assumptions

Given: The Axiom of Choice, a dominant integral weight λ∈Λ+, the BGG resolution of L(λ), and the Grothendieck group of the linkage block of λ with its character homomorphism.

[F1]

0→C∣Φ+∣(λ)→⋯→C1(λ)→C0(λ)→L(λ)→0 is an exact sequence in O, and Ci(λ)=⨁ℓ(w)=iM(w∘λ) (The BGG resolution of a finite-dimensional simple module, The Bruhat graph and the BGG Verma sum in degree k).

[F2]

The Grothendieck group K(O) is the abelian group with generators the classes of objects and relations [B]=[A]+[C] for every short exact sequence 0→A→B→C→0; consequently an exact sequence 0→An→⋯→A0→B→0 gives [B]=∑i=0n(−1)i[Ai], and [A⊕B]=[A]+[B]. The classes of the simple modules [L(μ)] and of the Verma modules [M(μ)] each form a basis of K(O) (The Grothendieck group and character of O, Simple and standard bases of K0(O)).

[F3]

The formal character ch⁡ is additive on exact sequences and hence defines a homomorphism from K(O) to the group of formal characters; ch⁡M(μ)=eμ∏α∈Φ+(1−e−α)−1 (The formal character of a Verma module, The Grothendieck group and character of O).

[F4]

All M(w∘λ) and L(λ) lie in the linkage block of λ; the block decomposition splits O into a direct sum of subcategories, and the corresponding projection of Grothendieck groups is additive on classes. Hence an identity between classes of objects of the block that holds in K(O) holds in the Grothendieck group of the block (Central-character summands refine into linkage blocks, The Grothendieck group and character of O).

Proof

1.1F1F2F4

The resolution of [F1] is a finite exact sequence 0→C∣Φ+∣(λ)→⋯→C0(λ)→L(λ)→0. By the additivity of [F2] applied successively to its short exact sequences, [L(λ)]=∑i=0∣Φ+∣(−1)i[Ci(λ)]; by the direct-sum rule and [F1], [Ci(λ)]=∑ℓ(w)=i[M(w∘λ)]. Substituting gives [L(λ)]=∑w∈W(−1)ℓ(w)[M(w∘λ)]. All the modules involved lie in the linkage block of λ, so by [F4] this identity holds in the Grothendieck group of that block.

2.1F3step 1.1

Applying the character homomorphism of [F3] to the identity of step 1.1 and using the Verma character gives ch⁡L(λ)=∑w∈W(−1)ℓ(w)ch⁡M(w∘λ)=∑w∈W(−1)ℓ(w)ew∘λ∏α∈Φ+(1−e−α)−1, the common factor ∏α∈Φ+(1−e−α)−1 being independent of w.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 are exactly the two asserted identities: the alternating sum of Verma classes in the Grothendieck group of the linkage block, and the Weyl numerator form of the character identity.

Depends on

Used by

Dependency tree · two levels

43 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