Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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 simple objects of O

Statement

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=h⊕n+. Write Q+=∑iZ≥0αi, μ≤λ when λ−μ∈Q+, and w⋅λ=w(λ+ρ)−ρ.

The simple objects of O are exactly the modules L(λ), λ∈h∗, and L(λ)≅L(μ) if and only if λ=μ. Simplicity here excludes zero.

Facts & Assumptions

Given: The setting above and the hypotheses in the statement.

[F1]

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=h⊕n+. Write Q+=∑iZ≥0αi, μ≤λ when λ−μ∈Q+, and w⋅λ=w(λ+ρ)−ρ. The category O is closed under submodules, quotients and finite direct sums and is an abelian category. If 0→A→E→B→0 is exact, A,B∈O, and E is h-semisimple, then E∈O. The middle-term weight hypothesis is essential. (Category O is abelian and extension closed among weight modules)

[F2]

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=h⊕n+. Write Q+=∑iZ≥0αi, μ≤λ when λ−μ∈Q+, and w⋅λ=w(λ+ρ)−ρ. Every nonzero M∈O contains a nonzero weight vector killed by n+. (A nonzero O-object has a highest-weight vector)

[F3]

For a g-module V, sending a homomorphism T:M(λ)→V to T(vλ) is a bijection onto the vectors v∈V of weight λ annihilated by n+. Here M(λ) is def-verma-module. The nonzero vectors in this target are precisely the highest-weight vectors of weight λ from def-highest-weight-vector-and-cyclic-highest-weight-module; the zero vector corresponds to the zero homomorphism. (The universal property of Verma modules)

[F4]

The proper submodule J(λ) which is the sum of all proper submodules is the unique maximal submodule of M(λ). The quotient L(λ):=M(λ)/J(λ) is simple and is its unique simple quotient. (A Verma module has a unique simple quotient)

[F5]

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=h⊕n+. Write Q+=∑iZ≥0αi, μ≤λ when λ−μ∈Q+, and w⋅λ=w(λ+ρ)−ρ. Every Verma module M(λ), every quotient of it, and every finite-dimensional h-semisimple g-module belongs to O. (Verma and finite-dimensional weight modules belong to O)

Proof

1.1F1F2F3F4

For a nonzero simple object S, closure under submodules means simplicity in O is the same as module simplicity. Choose a highest-weight vector of weight λ in S. The Verma universal property yields a nonzero map M(λ)→S, necessarily surjective. Its unique simple quotient identifies S with L(λ).

2.1F4F5step 1.1

Conversely L(λ) belongs to O and is simple as a module, hence as an object of this full subcategory. Its highest line survives the Verma quotient: killing that generator kills the whole quotient. Its other weights are below λ. These weight facts also follow directly from the induced Verma construction.

3.1algebrastep 2.1∎

An isomorphism L(λ)≅L(μ) preserves weights, so the two highest weights give λ≤μ and μ≤λ. The positive root cone is pointed, so λ=μ. Conversely equal labels give the same quotient up to its defining isomorphism.

Depends on

Used by

Dependency tree · two levels

14 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