TheoremStatement: Literature-sourcedProof: 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 BGG resolution of a finite-dimensional simple module

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $λ \in Λ^{+}$ . The BGG complex $C_{∙} (λ)$ with differentials $d_{k}$ is a resolution of $L (λ)$ by Verma modules:

$0 \to C_{∣ Φ^{+} ∣} (λ) \to \dots \to C_{1} (λ) \to C_{0} (λ) \to L (λ) \to 0$

is exact. Equivalently, $coker d_{1} = L (λ)$ and $im d_{k + 1} = \ker d_{k}$ for all $k \geq 1$ .

Facts & Assumptions

Given: The Axiom of Choice, a dominant integral weight $λ \in Λ^{+}$ , the BGG complex $C_{∙} (λ)$ with differentials $d_{k} ⁣ : C_{k} (λ) \to C_{k - 1} (λ)$ and augmentation $d_{0} = π ⁣ : C_{0} (λ) = M (λ) ↠ L (λ)$ .

[F1]

$d_{k - 1} \circ d_{k} = 0$ for all $k \geq 2$ , and the augmented sequence is a complex; $d_{k + 1}$ therefore maps $C_{k + 1} (λ)$ into $\ker d_{k}$ for every $k \geq 0$ , and its restriction to $C_{k + 1} (λ)$ is a $U (n^{-})$ -linear map onto a submodule of $\ker d_{k}$ (The BGG differential squares to zero, The BGG differential from signed Verma maps).

[F2]

The complex is exact at $C_{0}$ : $im d_{1} = \ker d_{0} = \ker π$ and $coker d_{1} = L (λ)$ (The augmentation kernel is the sum of the simple-reflection Verma submodules).

[F3]

For every $j$ the module $C_{j} (λ) = ⨁_{ℓ (w) = j} M (w \circ λ)$ is an object of $O$ that is free over $U (n^{-})$ on the weight-vector generators $v_{w}$ (the highest weight vectors of the summands), and $C_{j} (λ) / n^{-} C_{j} (λ)$ has dimension $∣ W_{j} ∣$ ; $C_{j} (λ) = 0$ for $j > ∣ Φ^{+} ∣$ (The PBW model of a Verma module, The Bruhat graph and the BGG Verma sum in degree k, Positive coroot pairings of a dominant integral weight, The classical BGG category O).

[F4]

BGG 10.7 (Dimension of the kernel modulo n-minus equals the next term (BGG 10.7)): if $C_{∙} (λ)$ is exact in degrees $0, \dots, k - 1$ , then $\ker d_{k} / n^{-} \ker d_{k}$ is finite-dimensional of dimension $∣ W_{k + 1} ∣ = \dim C_{k + 1} (λ) / n^{-} C_{k + 1} (λ)$ .

[F5]

BGG 10.6 (The BGG differential induces an injection into kernel coinvariants (BGG 10.6)): if $C_{∙} (λ)$ is exact in degrees $0, \dots, k - 1$ , then ${\overset{ˉ}{d}}_{k + 1} ⁣ : C_{k + 1} (λ) / n^{-} C_{k + 1} (λ) \to \ker d_{k} / n^{-} \ker d_{k}$ is injective.

[F6]

BGG 10.5 (Surjectivity modulo n-minus for free weight-generated modules (BGG 10.5)): if $N \in O$ and $φ ⁣ : M \to N$ is a $U (n^{-})$ -linear map from a free $U (n^{-})$ -module $M$ on weight-vector generators with each $φ (v_{i})$ a weight vector, then $φ$ is surjective if and only if $\overset{ˉ}{φ}$ is surjective.

[F7]

$\ker d_{k}$ is an object of $O$ for every $k$ (a subobject of $C_{k} (λ) \in O$ ), and the differentials are $h$ -equivariant, so $d_{k + 1} (v_{w})$ is a weight vector of weight $w \circ λ$ for each generator $v_{w}$ of $C_{k + 1} (λ)$ (The classical BGG category O, The Bruhat graph and the BGG Verma sum in degree k).

Proof

1.1F2base

Base of the induction. Exactness at $C_{0}$ is [F2]: $im d_{1} = \ker d_{0}$ and $coker d_{1} = L (λ)$ .

1.2F3ih

Induction statement. We prove by induction on $k \geq 1$ that $im d_{k + 1} = \ker d_{k}$ ; note that exactness at $C_{1}, \dots, C_{k}$ for the unaugmented complex means $im d_{j + 1} = \ker d_{j}$ for $1 \leq j \leq k$ . The induction hypothesis available at stage $k$ is that $C_{∙} (λ)$ is exact in degrees $0, \dots, k - 1$ . For $k > ∣ Φ^{+} ∣$ the modules $C_{k} (λ)$ vanish by [F3], so it suffices to run the induction for $1 \leq k \leq ∣ Φ^{+} ∣$ ; at $k = ∣ Φ^{+} ∣$ the statement $im d_{∣ Φ^{+} ∣ + 1} = \ker d_{∣ Φ^{+} ∣}$ says that $d_{∣ Φ^{+} ∣}$ is injective.

2.1F4step 1.2ih

Dimensions agree. Assume exactness in degrees $0, \dots, k - 1$ . By [F4] applied at degree $k$ , the two spaces $\ker d_{k} / n^{-} \ker d_{k}$ and $C_{k + 1} (λ) / n^{-} C_{k + 1} (λ)$ are finite-dimensional of the same dimension $∣ W_{k + 1} ∣$ .

3.1F5step 2.1ih

The reduced map is an isomorphism. Under the same hypothesis, ${\overset{ˉ}{d}}_{k + 1}$ is injective by [F5], and it is a linear map between the two finite-dimensional spaces of step 2.1 of equal dimension; hence ${\overset{ˉ}{d}}_{k + 1}$ is bijective.

4.1F3F6F7step 3.1

Upgrading to surjectivity. The module $C_{k + 1} (λ)$ is free over $U (n^{-})$ on its weight-vector generators $v_{w}$ by [F3], and $\ker d_{k} \in O$ by [F7]; the restriction $φ ⁣ : C_{k + 1} (λ) \to \ker d_{k}$ of $d_{k + 1}$ is $U (n^{-})$ -linear (indeed $g$ -linear) with $φ (v_{w})$ a weight vector for every generator by [F7], and $\overset{ˉ}{φ} = {\overset{ˉ}{d}}_{k + 1}$ is surjective by step 3.1. By [F6] the map $φ$ is surjective, i.e. $im d_{k + 1} = \ker d_{k}$ : exactness at $C_{k}$ .

5.1F1F3step 1.1step 4.1discharge-induction: induction on the degree $k$∎

The base of the induction is step 1.1, and step 4.1 passes from exactness in degrees $0, \dots, k - 1$ to exactness at degree $k$ , for every $1 \leq k \leq ∣ Φ^{+} ∣$ . Hence $0 \to C_{∣ Φ^{+} ∣} (λ) \to \dots \to C_{1} (λ) \to C_{0} (λ) \to L (λ) \to 0$ is exact and the two equivalent formulations hold.

Depends on

Used by

The BGG resolution has length the number of positive roots Corollary
The Euler-character identity for a finite-dimensional simple module Corollary
The A2 BGG resolution with six Verma summands Example
The BGG resolution for sl2 Example

Dependency tree · two levels

53 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

Fan Zhou, The classical and the functorial BGG resolutions (Columbia thesis 2021), Part I Sec. 3.2 and Sec. 4.1 (Theorem BGG and its proof), pp. 11 and 14-18 (standard reference, not scraped)
A. Rocha-Caridi, Splitting criteria for modules induced from a subalgebra of a semisimple Lie algebra, Trans. AMS 262 (1980), Sec. 10, Corollary 10.6, pp. 355-356 (standard reference, not scraped)
N. Hemelsoet and R. Voorhaar, A computer algorithm for the BGG resolution, arXiv:1911.00871, Theorems 2.5 and 2.6, p. 5 (standard reference, not scraped)