Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-07 rests on unproved material (inherited)
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.

Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Nonintegral sl2 central characters split into two simple blocks

Example

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 g=sl2 and λCZ, Oχλ has exactly two distinct singleton linkage blocks, with labels λ and λ2. Each block is equivalent to finite-dimensional complex vector spaces. In particular the central-character summand is semisimple but is not one indecomposable block.

Facts & Assumptions

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

[F1]

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 a linkage class C=Wλλ, let OC be the full subcategory of objects all of whose simple composition factors have labels in C. Then O=COC, and each nonzero OC is indecomposable as a categorical direct summand. These are precisely the blocks. Each OC lies in Oχλ; a central-character summand can contain several blocks. Independently, grouping weights by cosets of the root lattice Q gives a canonical coarser decomposition by weight cosets. (Central-character summands refine into linkage blocks)

[F2]

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(λ+ρ)ρ. Every short exact sequence 0M(λ)EpM(λ)0 in O splits. (Verma self-extensions in O split)

[F3]

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 M,NO, HomO(M,N) is finite dimensional. For every weight λ, EndO(L(λ))=Cid. (Finite-dimensional Hom spaces in O)

[F4]

M(λ) is simple if and only if λ+ρ,αZ>0 for every αΦ+. (The Verma irreducibility criterion from Shapovalov determinants)

[F5]

Let Z=Z(U(g)), let χ:ZC be a unital complex-algebra character, and put mχ=kerχ. For MO, the generalized central-character submodule is Mχ={vM:mχNv=0 for some N1}, and Oχ consists of the objects with M=Mχ. (Generalized central-character subcategories)

[F6]

The simple objects of O are exactly the modules L(μ), μh, and L(μ)L(ν) if and only if μ=ν. (The simple objects of O)

[F7]

If a cyclic highest-weight module has highest weight μ, then every zZ(U(g)) acts on it by the scalar pr(z)(μ)=χμ(z). (The Harish-Chandra projection computes the highest-weight scalar)

[F8]

The highest-weight central characters satisfy χμ=χλ if and only if μWλ. (Central characters are dot-Weyl orbits)

[F9]

Every object of O has a finite composition series and is both Noetherian and Artinian. The length of zero is zero. (Every object of O has finite length)

Verification

1.1

For sl2, the dot orbit of λ is exactly {λ,λ2}. Its two labels are nonintegral and distinct: equality would imply λ=1. By F8 they have the same central character. Conversely, if a simple object belongs to Oχλ, F6 writes it as L(μ). Its highest vector is killed by a power of every zχλ(z) by F5, while F7 says that z acts on it as χμ(z). Hence χμ=χλ, and F8 forces μ{λ,λ2}. Neither label has an integral root pairing, so each integral-reflection group is trivial. Both Vermas are simple by F4, and F1 therefore identifies exactly the two asserted singleton blocks.

F1F4F5F6F7F8
2.1

Fix one label η and put S=M(η)=L(η). Every object in this block has a finite composition series by F9, and all its factors are S by F1. Every extension of S by itself splits by F2. More generally an extension 0SrES0 splits: push out along each coordinate projection SrS, obtaining Ei=(ES)/{(a,ai):aSr}. Each has a retraction to its kernel S. Composing these retractions with EEi and collecting coordinates gives a retraction ESr, hence a splitting. The case r=0 is immediate.

F1F2F9algebrastep 1.1
3.1

Induction on a composition series now expresses every object as a finite direct sum of S. Since End(S)=C, maps between Sr and Ss are exactly complex matrices. Thus VSV (with trivial action on the finite-dimensional multiplicity space) and XHom(S,X) are inverse equivalences. Zero corresponds to the zero-dimensional vector space.

F3algebrastep 2.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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