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 BGG resolution for sl2

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $g = {s l}_{2}$ with $W = {1, s}$ , positive root $α$ , $ρ = α / 2$ and $λ = m ω$ with $m \geq 0$ dominant integral. Then $s \circ λ = - λ - 2 ρ = - (m + 2) ω$ and the BGG resolution of The BGG resolution of a finite-dimensional simple module reads

$0 \to M (- (m + 2) ω) \to M (m ω) \to L (m ω) \to 0,$

with the injection the canonical embedding of the Verma submodule generated by the singular vector $f^{m + 1} v_{λ}$ and the surjection the canonical projection. Both end degrees are computed: $∣ Φ^{+} ∣ = 1$ , $w_{0} = s$ , $C_{0} = M (λ)$ , $C_{1} = M (s \circ λ)$ .

Facts & Assumptions

Given: The Axiom of Choice, $g = {s l}_{2}$ with its standard positive root $α$ and $ρ = α / 2 = ω$ , the Weyl group $W = {1, s}$ , a dominant integral weight $λ = m ω$ with $m \geq 0$ , and the BGG complex $C_{∙} (λ)$ .

[F1]

$∣ Φ^{+} ∣ = 1$ , $α = 2 ω$ , $s (ω) = - ω$ and $w_{0} = s$ ; for $λ = m ω$ one has $λ + ρ = (m + 1) ω$ and $s \circ λ = s (λ + ρ) - ρ = - (m + 1) ω - ω = - (m + 2) ω = - λ - 2 ρ$ (Finite Weyl root system, lattice and chamber conventions, The Weyl vector rho for a chosen positive system, The Bruhat graph and the BGG Verma sum in degree k).

[F2]

$C_{0} (λ) = M (λ)$ , $C_{1} (λ) = M (s \circ λ)$ , and $C_{k} (λ) = 0$ for $k \geq 2$ ; the only arrow is the cover $s ⊳ e$ , the first differential is $d_{1} = ε (s, e) ι_{s \to e}$ with $ε (s, e) = \pm 1$ , and $d_{0} = π ⁣ : M (λ) ↠ L (λ)$ (The Bruhat graph and the BGG Verma sum in degree k, The BGG differential from signed Verma maps).

[F3]

The canonical embedding $ι_{s \to e} ⁣ : M (s \circ λ) ↪ M (λ)$ is a nonzero $g$ -homomorphism, injective with image the submodule generated by the singular vector $f^{⟨ λ + ρ, α^{\lor} ⟩} v_{λ} = f^{m + 1} v_{λ}$ of weight $s \circ λ$ ; it is the canonical submodule $M (s \circ λ) \subseteq M (λ)$ and every element of the one-dimensional space ${Hom}_{g} (M (s \circ λ), M (λ))$ is a scalar multiple of it (The simple-root singular vector in a Verma module, Dominant integral dot translates embed canonically in the Verma module, Bruhat covers give canonical Verma embeddings, and composites are inclusions, Simple-reflection embeddings of Verma modules).

[F4]

For $λ \in Λ^{+}$ the full augmented sequence is exact: $im d_{1} = \ker d_{0} = \ker π$ , $coker d_{1} = L (λ)$ , and here $\ker d_{1} = 0$ because $C_{2} (λ) = 0$ and $d_{1}$ is injective (The BGG resolution of a finite-dimensional simple module, The augmentation kernel is the sum of the simple-reflection Verma submodules).

[F5]

The irreducible ${s l}_{2}$ -module with highest weight $m ω$ has dimension $m + 1$ (Finite-dimensional representations of sl_2); the weight $- (m + 2) ω$ satisfies $⟨ - (m + 2) ω + ρ, α^{\lor} ⟩ = - (m + 1) < 0$ , so $M (- (m + 2) ω)$ is simple (Antidominant regular Verma modules are simple).

Verification

1.1F1F2

The terms: by [F1] and [F2], $C_{0} = M (m ω)$ and $C_{1} = M (s \circ m ω) = M (- (m + 2) ω)$ , and $C_{k} = 0$ for $k \geq 2$ ; hence the complex is concentrated in degrees $0$ and $1$ , and the sequence displayed in the Example is the BGG complex with $d_{0} = π$ .

1.2F3F5

The injection: by [F3] the map $d_{1}$ is, up to the sign $\pm 1$ , the canonical embedding $M (- (m + 2) ω) ↪ M (m ω)$ with image the Verma submodule generated by $f^{m + 1} v_{λ}$ , and it is injective; its source is even a simple Verma module by [F5], but simplicity is not needed for the injection.

1.3F4F5

Exactness at $C_{0}$ : by [F4], $im d_{1} = \ker π = \ker d_{0}$ and $coker d_{1} = L (m ω)$ ; equivalently the middle quotient $M (m ω) / M (- (m + 2) ω) ≅ L (m ω)$ is the standard finite-dimensional quotient of dimension $m + 1$ by [F5].

2.1step 1.2

Exactness at $C_{1}$ : $\ker d_{1} = 0 = im d_{2}$ , since $C_{2} = 0$ and $d_{1}$ is injective by step 1.2; this is the injectivity of a nonzero Verma map.

3.1step 1.1step 1.3step 2.1∎

Combining the computed end degrees of step 1.1, the identification of the injection in step 1.2, and the exactness in steps 1.3 and 2.1, the BGG resolution of $L (m ω)$ is exactly $0 \to M (- (m + 2) ω) \to M (m ω) \to L (m ω) \to 0$ with the stated maps, and $∣ Φ^{+} ∣ = 1$ is the length of the resolution.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

63 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, p. 11 (rank-one case) (standard reference, not scraped)
P. Etingof, Lie Groups and Lie Algebras II (18.755), Sec. 25 and Sec. 25.4, pp. 134-138 (Verma modules and the U(n-) model) (standard reference, not scraped)