Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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 Grothendieck group and character of O

Definition

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=hn+. Write Q+=iZ0αi, μλ when λμQ+, and wλ=w(λ+ρ)ρ.

For the abelian category Category O is abelian and extension closed among weight modules, define K0(O) as the free abelian group on isomorphism classes [M], modulo [B]=[A]+[C] for every short exact sequence 0ABC0. A set of representatives suffices: every finitely generated U(g)-module is a quotient of some U(g)n, and those quotients form a set up to isomorphism.

Define the formal character by chM=μ(dimMμ)eμ. By The support description of category O with finite generation, its integer coefficients are finite and supported in finitely many downward cones. Let R be the group of all such integer coefficient families, with pointwise addition. It is a ring with eμeν=eμ+ν: at a fixed resulting weight, in any pair of cones the equation β+γ=η with β,γQ+ has finitely many solutions, since every simple-root coefficient is bounded. Taking weight spaces is exact, so character gives a well-defined homomorphism K0(O)R. The zero object's class and character are zero.

Depends on

Used by

Dependency tree · two levels

9 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