ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedverified 2026-09-23 (gpt-6-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 regular integral sl2 block

Example

Assume the Axiom of Choice.

For $g = {s l}_{2}$ identify a highest weight with its value on $h$ , so $ρ = 1$ and $s \cdot λ = - λ - 2$ . For every integer $n \geq 0$ , the regular integral block has simple labels $n$ and $- n - 2$ . Its standards are $M (n)$ and $M (- n - 2) = L (- n - 2)$ , and

$0 ⟶ L (- n - 2) ⟶ M (n) ⟶ L (n) ⟶ 0$

is nonsplit. Its costandards are $\nabla (n)$ and $\nabla (- n - 2) = L (- n - 2)$ , with the nonsplit sequence $0 \to L (n) \to \nabla (n) \to L (- n - 2) \to 0$ . The linkage order is $- n - 2 < n$ .

Facts & Assumptions

Given: The Axiom of Choice (The Axiom of Choice), the setting above and the hypotheses in the example.

[F1]

The category $O$ is the categorical direct sum of its generalized central-character subcategories, and each object has only finitely many nonzero character components (Generalized central-character decomposition of O).

[F10]

Under the Axiom of Choice, $χ_{λ} = χ_{μ}$ if and only if $μ \in W \cdot λ$ (Central characters are dot-Weyl orbits).

[F11]

Under the Axiom of Choice, every object of $O$ has finite length (Every object of O has finite length), and its simple objects are exactly the distinct $L (η)$ (The simple objects of O).

[F2]

Fix a finite-dimensional complex semisimple Lie algebra $g$ , a Cartan subalgebra $h$ , and a positive Borel $b = h \oplus n^{+}$ . Write $Q^{+} = \sum_{i} Z_{\geq 0} α_{i}$ , $μ \leq λ$ when $λ - μ \in Q^{+}$ , and $w \cdot λ = w (λ + ρ) - ρ$ . Restricted Chevalley duality is an exact contravariant equivalence $D : O \to O^{o p}$ , with a natural isomorphism $D^{2} ≅ id$ . It preserves each weight-space dimension, the formal character, and every simple composition multiplicity. (Restricted duality is exact and involutive on O)

[F3]

Fix a finite-dimensional complex semisimple Lie algebra $g$ , a Cartan subalgebra $h$ , and a positive Borel $b = h \oplus n^{+}$ . Write $Q^{+} = \sum_{i} Z_{\geq 0} α_{i}$ , $μ \leq λ$ when $λ - μ \in Q^{+}$ , and $w \cdot λ = w (λ + ρ) - ρ$ . The costandard object $\nabla (λ)$ has a unique simple submodule, isomorphic to $L (λ)$ . Its socle, the sum of all simple submodules, is that submodule. (The simple socle of a costandard object)

[F4]

If $⟨ λ + ρ, α_{i}^{\lor} ⟩ \in Z_{> 0}$ , there is an embedding $M (s_{i} \cdot λ) ↪ M (λ)$ . (Simple-reflection embeddings of Verma modules)

[F5]

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)

[F6]

The standard ${s l}_{2}$ generators satisfy $[e, f] = h$ and $[h, f] = - 2 f$ (The special linear Lie algebra sl_2). The induced Verma highest vector satisfies $e v_{η} = 0$ and $h v_{η} = η v_{η}$ (Verma modules), and PBW makes $v_{k} = f^{k} v_{η}$ ( $k \geq 0$ ) a basis (The PBW model of a Verma module).

[F7]

The weights of $M (λ)$ are exactly $λ - β$ for $β \in Q^{+}$ ; every weight space is finite dimensional, and $M (λ)_{λ} = C v_{λ}$ . (Weights of a Verma module lie below lambda)

[F8]

For every highest weight $η$ , $D (L (η)) ≅ L (η)$ as $g$ -modules. (Restricted self-duality of simple highest-weight modules)

[F9]

The standard and costandard objects are $Δ (η) = M (η)$ and $\nabla (η) = D (M (η))$ . (Standard and costandard objects)

Verification

1.1F6inductionalgebra

For any highest weight $η$ , the PBW basis in [F6] and $[h, f] = - 2 f$ give $h v_{k} = (η - 2 k) v_{k}$ . Also $e v_{0} = 0$ , and $[e, f] = h$ gives the induction step $e v_{k + 1} = f (e v_{k}) + h v_{k}$ . If $e v_{k} = k (η - k + 1) v_{k - 1}$ , this step yields $e v_{k + 1} = [k (η - k + 1) + η - 2 k] v_{k} = (k + 1) (η - k) v_{k}$ . Therefore $e v_{k} = k (η - k + 1) v_{k - 1}$ for all $k \geq 1$ .

2.1F6F10F11step 1.1

The integral pairing is $n + 1 > 0$ , and the two distinct dot-orbit labels are $n$ and $- n - 2$ . Under Choice, [F10] says that $L (n)$ and $L (- n - 2)$ are exactly the simple labels in the central-character summand $O_{χ_{n}}$ : by [F11] every simple is a highest-weight $L (η)$ and hence has the scalar character $χ_{η}$ . For $η = - n - 2$ , every coefficient $k (η - k + 1) = - k (n + k + 1)$ from step 1.1 is nonzero when $k \geq 1$ . A nonzero submodule of $M (η)$ contains a nonzero weight vector, hence some basis vector $v_{k}$ ; repeated application of $e$ reaches $v_{0}$ , which generates the entire Verma module. Thus $M (- n - 2) = L (- n - 2)$ directly.

3.1F4F6F7step 1.1step 2.1

Write $v_{k} = f^{k} v_{n}$ in $M (n)$ . The action derived in step 1.1 gives $h v_{k} = (n - 2 k) v_{k}$ and $e v_{k} = k (n - k + 1) v_{k - 1}$ for $k \geq 1$ , with $e v_{0} = 0$ . The weight spaces are one dimensional. The singular vector $v_{n + 1}$ generates the embedded $M (- n - 2)$ , which is also the embedding supplied by F4.

4.1F5algebrastep 1.1step 3.1

The quotient has basis $v_{0}, \dots, v_{n}$ . A nonzero submodule contains a weight vector, and applying $e$ repeatedly reaches $v_{0}$ , since $k (n - k + 1) \neq 0$ for $1 \leq k \leq n$ by step 1.1. Applying $f$ then generates the whole quotient. It is simple, hence is $L (n)$ . A split sequence would make $M (n)$ a sum of two proper submodules, contrary to its unique maximal submodule. For $n = 0$ the quotient consists just of $v_{0}$ and the same argument holds.

5.1F2F3F8F9step 2.1step 4.1

By F8, exact duality fixes both simples; it reverses the sequence, and F9 identifies the middle term as $\nabla (n)$ , giving the displayed costandard sequence. If it split, its dual would split the original. The costandard socle is $L (n)$ by F3. Since $M (- n - 2) = L (- n - 2)$ , F8 and F9 also give $\nabla (- n - 2) = L (- n - 2)$ .

6.1F1F5F11step 2.1step 4.1∎

By [F1], $O_{χ_{n}}$ is a categorical direct summand. It has exactly the two simple labels from step 2.1. If this summand decomposed into two nonzero categorical summands, finite length [F11] would place a simple in each; the two labels would therefore lie in different summands. Then $M (n)$ , which has both as factors by steps 3.1 and 4.1, would split as a direct sum of two nonzero submodules, contradicting the unique-maximal-submodule property [F5]. Hence $O_{χ_{n}}$ is indecomposable and is the asserted regular integral block. The integral Weyl group is the full order-two Weyl group, giving the stated linkage order $- n - 2 < n$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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

Chen, Lecture 8 §3 Example 3.17, p.6 (standard reference, not scraped)
Chen, Lecture 2 §2 Example 2.16 and Exercise 2.17, p.4 (standard reference, not scraped)