ExampleConstruction: Literature-sourcedVerification: 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 two projectives in the principal sl2 block

Example

Assume the Axiom of Choice (The Axiom of Choice).

The rank-one computation is done for a general regular block and then specialised. Let $g = {s l}_{2}$ with basis $e, f, h$ and coordinate $l = λ (h)$ on weights, so that $ρ = 1$ and the dot action of the reflection is $s \cdot l = - l - 2$ . For every $λ$ the Verma module $M (λ)$ has basis $v_{k} = f^{k} v_{0}$ , $k \geq 0$ , on which $h \cdot v_{k} = (λ (h) - 2 k) v_{k}$ , $f \cdot v_{k} = v_{k + 1}$ and $e \cdot v_{k} = k (λ (h) - k + 1) v_{k - 1}$ . Fix an integer $n \geq 0$ and take $λ (h) = n$ : the span $U$ of $v_{k}$ for $k \geq n + 1$ is a submodule isomorphic to $M (- n - 2) = L (- n - 2)$ , the quotient $M (n) / U$ is the simple module $L (n)$ , and $0 \to L (- n - 2) \to M (n) \to L (n) \to 0$ is nonsplit. The dot orbit of $n$ is ${n, - n - 2}$ with $- n - 2 \leq n$ , and $χ_{n} = χ_{- n - 2}$ ; thus $Δ (n) = M (n)$ and $Δ (- n - 2) = M (- n - 2) = L (- n - 2)$ are the two standards of the regular integral block $C_{n}$ of highest weight $n$ .

For every such $n$ , the projective covers are $P (n) = Δ (n)$ and $P (- n - 2)$ with the nonsplit sequence $0 ⟶ Δ (n) ⟶ P (- n - 2) ⟶ Δ (- n - 2) ⟶ 0.$ The latter has head and socle $L (- n - 2)$ and middle factor $L (n)$ .

For $n = 0$ this is the regular integral block $C$ of highest weight $0$ , whose simple labels are $0$ and $- 2$ with $- 2 \leq 0$ . Then $Δ (0) = M (0)$ is projective and is the projective cover $P (0)$ of the one-dimensional simple module $L (0) = C$ . The projective cover $P (- 2)$ of $L (- 2) = Δ (- 2)$ fits into the nonsplit short exact sequence $0 ⟶ Δ (0) ⟶ P (- 2) ⟶ Δ (- 2) ⟶ 0,$ its head and socle are $L (- 2)$ , and its middle composition factor is $L (0)$ . The Verma-flag multiplicities are $(P (0) : Δ (0)) = 1$ and $(P (- 2) : Δ (- 2)) = (P (- 2) : Δ (0)) = 1$ , matching BGG reciprocity with $[Δ (0) : L (0)] = [Δ (0) : L (- 2)] = [Δ (- 2) : L (- 2)] = 1$ and $[Δ (- 2) : L (0)] = 0$ .

Facts & Assumptions

Given: The Axiom of Choice, $g = {s l}_{2}$ with its standard basis, the coordinate $l = λ (h)$ on weights with $ρ = 1$ and dot action $s \cdot l = - l - 2$ , an integer $n \geq 0$ , the regular integral block $C_{n}$ with labels $n$ and $- n - 2$ , and its projective covers.

[F1]

For every weight $λ$ the Verma module $M (λ) = U ({s l}_{2}) \otimes_{U (b)} C_{λ}$ has basis $v_{k} = f^{k} v_{0}$ , $k \geq 0$ , with $h \cdot v_{k} = (λ (h) - 2 k) v_{k}$ , $f \cdot v_{k} = v_{k + 1}$ and $e \cdot v_{k} = k (λ (h) - k + 1) v_{k - 1}$ , by the PBW factorisation $U ({s l}_{2}) = U (C f) U (h \oplus C e)$ applied to the induced module (Verma modules, Poincaré–Birkhoff–Witt theorem, The special linear Lie algebra sl_2).

[F2]

A homomorphism out of a Verma module is determined by the image of its highest-weight vector, which may be any vector killed by $n^{+}$ of the prescribed weight; in particular a highest-weight vector of weight $μ$ in a module $V$ induces a unique $g$ -map $M (μ) \to V$ (The universal property of Verma modules, Verma modules).

[F3]

If $⟨ λ + ρ, α^{\lor} ⟩ < 0$ then $M (λ)$ is simple; here $⟨ (- n - 2) + 1, α^{\lor} ⟩ = - (n + 1) < 0$ , so $M (- n - 2) = L (- n - 2)$ (Antidominant regular Verma modules are simple).

[F4]

With $ρ = 1$ the dot action is $s \cdot l = - l - 2$ , so the dot orbit of $n$ is ${n, - n - 2}$ and $χ_{n} = χ_{- n - 2}$ ; and $- n - 2 \leq n$ because $n - (- n - 2) = (n + 1) α$ with $α$ the positive root, and $(n + 1) α \in Q^{+}$ (The classical BGG category O, Central characters are dot-Weyl orbits).

[F5]

The block $C_{n}$ is the full subcategory of objects all of whose simple composition factors are $L (n)$ and $L (- n - 2)$ ; the set ${n, - n - 2}$ is a finite downward-closed ideal of its linkage class in which $n$ is maximal and $- n - 2$ is minimal (Central-character summands refine into linkage blocks, Truncation at a finite downward-closed ideal of a linkage class).

[F6]

Since $n$ is maximal in the finite downward-closed ideal $C_{n}$ , the Verma module $Δ (n) = M (n)$ is projective in $O_{C_{n}}$ , and an object of $O_{C_{n}}$ projective there is projective in $O$ (A maximal-label Verma is projective in its truncation, Exact projections onto linkage blocks preserve projectives).

[F7]

Each simple $L (μ)$ has an indecomposable projective cover $P (μ)$ , unique up to isomorphism, with head $L (μ)$ ; conversely an indecomposable projective with head $L (μ)$ is a projective cover of $L (μ)$ (Category O has enough projectives, Projective covers in O are indecomposable and unique).

[F8]

Every projective is Verma-filtered, and BGG reciprocity gives $(P (λ) : Δ (μ)) = [Δ (μ) : L (λ)]$ ; two weights label composition factors of an indecomposable object only if they lie in one linkage block, hence in the same full dot orbit (Projectives in category O have finite Verma flags, BGG reciprocity, Central characters are dot-Weyl orbits, Central-character summands refine into linkage blocks).

Verification

technique · direct: derive the rank-one Verma submodule and quotient from the PBW model, then identify both projective covers for every $n\ge0$ and specialise to $n=0$

1.1F1F2F3

By the action of [F1], for $n \geq 0$ the subspace $U = \sum_{k \geq n + 1} C v_{k}$ is a submodule: it is $h$ - and $f$ -stable, and $e \cdot v_{k} = k (n - k + 1) v_{k - 1}$ lies in $U$ for $k \geq n + 2$ while $e \cdot v_{n + 1} = 0$ ; the vector $v_{n + 1}$ is a highest-weight vector of weight $- n - 2$ , so [F2] gives a nonzero map $M (- n - 2) \to U$ , which is surjective because the powers of $f$ on $v_{n + 1}$ span $U$ and injective because $M (- n - 2)$ is simple by [F3], hence an isomorphism; hence $U ≅ L (- n - 2)$ . The quotient $M (n) / U$ has basis the images $u_{0}, \dots, u_{n}$ of $v_{0}, \dots, v_{n}$ , on which $e \cdot u_{j} = j (n - j + 1) u_{j - 1} \neq 0$ for $1 \leq j \leq n$ ; any nonzero submodule contains some $u_{j}$ , and applying $e^{j}$ with all factors $j! (n - j + 1) \dots n$ nonzero gives $u_{0}$ , which generates the quotient, so $M (n) / U$ is simple of highest weight $n$ , that is $L (n)$ . A splitting of $0 \to L (- n - 2) \to M (n) \to L (n) \to 0$ would exhibit a submodule of $M (n)$ isomorphic to $L (n)$ , necessarily containing a nonzero vector of the weight- $n$ space $C v_{0}$ and hence, since $v_{0}$ generates the infinite-dimensional $M (n)$ , the whole of $M (n)$ ; so the sequence is nonsplit.

2.1F1F4F5F6F7step 1.1

The dot orbit is ${n, - n - 2}$ by [F4]. By [F5] and [F6], $Δ (n)$ is projective in its block. The Verma module is indecomposable, since its one-dimensional highest line lies in one summand and generates the whole module. Its unique simple quotient is $L (n)$ by step 1.1, so [F7] identifies $Δ (n)$ with $P (n)$ . Its one-factor flag gives $(P (n) : Δ (n)) = 1$ and $(P (n) : Δ (- n - 2)) = 0$ .

2.2F5F7F8step 1.1

By [F7] and [F8], the indecomposable cover $P (- n - 2)$ is Verma-filtered with multiplicities $[Δ (μ) : L (- n - 2)]$ . Step 1.1 gives these multiplicities as one for $μ = n, - n - 2$ . No other label contributes: all Verma factors of a module in $C_{n}$ lie in $C_{n}$ , whose only simple labels are $n, - n - 2$ , by [F5]. Thus the flag has exactly the factors $Δ (n)$ and $Δ (- n - 2)$ , once each.

3.1F7step 2.2

The bottom flag factor cannot be $Δ (- n - 2)$ , since the resulting quotient $Δ (n)$ would give the simple quotient $L (n)$ , contradicting the unique head $L (- n - 2)$ of $P (- n - 2)$ . Hence the flag is the exact sequence $0 \to Δ (n) \to P (- n - 2) \to Δ (- n - 2) \to 0$ . It is nonsplit, since a splitting decomposes the cover into two nonzero summands.

4.1F7step 1.1step 2.2step 3.1

The socle of $Δ (n)$ is $L (- n - 2)$ : it contains that simple submodule by step 1.1, and a simple submodule not contained there would map isomorphically to $L (n)$ and split that nonsplit sequence. Likewise, any simple submodule of $P (- n - 2)$ outside $Δ (n)$ would map isomorphically to its quotient $L (- n - 2)$ and split step 3.1. Thus $P (- n - 2)$ has socle $L (- n - 2)$ , head $L (- n - 2)$ , and middle composition factor $L (n)$ , since its three factors come from the flag and step 1.1.

5.1F8step 1.1step 2.1step 2.2step 4.1∎

Taking $n = 0$ gives $P (0) = Δ (0)$ and the nonsplit sequence $0 \to Δ (0) \to P (- 2) \to Δ (- 2) \to 0$ , with head and socle $L (- 2)$ and middle factor $L (0)$ . The flag entries are $(P (0) : Δ (0)) = 1$ , $(P (0) : Δ (- 2)) = 0$ , and $(P (- 2) : Δ (0)) = (P (- 2) : Δ (- 2)) = 1$ ; the standard composition entries are $[Δ (0) : L (0)] = [Δ (0) : L (- 2)] = [Δ (- 2) : L (- 2)] = 1$ and $[Δ (- 2) : L (0)] = 0$ . They agree with BGG reciprocity by [F8].

Depends on

Used by

A projective Verma flag need not split Counterexample
A Verma module need not be projective in its block Counterexample
Verma filtrations are not closed under quotients Counterexample
The same Verma in two ambient categories Example
The sl2 reciprocity matrices Example
Translation through the sl2 wall Example

Dependency tree · two levels

68 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

Pavel Etingof, Representations of Lie Groups (18.757, Fall 2023), Proposition 16.4 and Example 20.8 (standard reference, not scraped)
Lin Chen, lecture notes (Spring 2024), Lecture 9, Theorem 2.2 and Example 3.16 (standard reference, not scraped)