PropositionStatement: 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 differential squares to zero

Statement

Assume the Axiom of Choice (The Axiom of Choice). With the maps $d_{k}$ of The BGG differential from signed Verma maps, $d_{k - 1} \circ d_{k} = 0$ for all $k \geq 2$ ; with $d_{0}$ included the augmented sequence is a complex of $g$ -modules

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

Facts & Assumptions

Given: The Axiom of Choice, a dominant integral weight $λ \in Λ^{+}$ , the degree- $k$ Verma sums $C_{k} (λ) = ⨁_{ℓ (w) = k} M (w \circ λ)$ with $g$ -homomorphisms $d_{k} ⁣ : C_{k} (λ) \to C_{k - 1} (λ)$ for $k \geq 1$ and $d_{0} = π ⁣ : M (λ) ↠ L (λ)$ .

[F1]

$d_{k}$ is the morphism whose $(w, w^{'})$ -component is $ε (w, w^{'}) ι_{w \to w^{'}}$ when $w ⊳ w^{'}$ and $0$ otherwise, where $ι_{w \to w^{'}} ⁣ : M (w \circ λ) ↪ M (w^{'} \circ λ)$ is the canonical cover embedding; $C_{k} (λ) = 0$ for $k > ∣ Φ^{+} ∣$ . Composition of morphisms of direct sums multiplies matrices of components: for $ℓ (w_{1}) = k$ and $ℓ (w_{4}) = k - 2$ the $(w_{1}, w_{4})$ -component of $d_{k - 1} \circ d_{k}$ is $\sum_{ℓ (w_{2}) = k - 1} (d_{k - 1})_{w_{2}, w_{4}} \circ (d_{k})_{w_{1}, w_{2}}$ (The BGG differential from signed Verma maps, The Bruhat graph and the BGG Verma sum in degree k).

[F2]

Each $ι_{w \to w^{'}}$ is injective with image a proper submodule of $M (w^{'} \circ λ)$ , and for a length-two saturated path $w_{1} ⊳ m ⊳ w_{4}$ the composite $ι_{m \to w_{4}} \circ ι_{w_{1} \to m}$ is the canonical inclusion of $M (w_{1} \circ λ)$ into $M (w_{4} \circ λ)$ , independent of the middle element $m$ (Bruhat covers give canonical Verma embeddings, and composites are inclusions).

[F3]

If $w_{4} < w_{1}$ and $ℓ (w_{1}) = ℓ (w_{4}) + 2$ , then there are exactly two elements $m_{1} \neq m_{2}$ with $w_{1} ⊳ m_{i} ⊳ w_{4}$ , and $[w_{4}, w_{1}] = {w_{4}, m_{1}, m_{2}, w_{1}}$ (Bruhat intervals of rank two are diamonds).

[F4]

On every square the four signs multiply to $- 1$ ; equivalently the two saturated paths of a rank-two interval carry opposite total signs: $ε (w_{1}, m_{1}) ε (m_{1}, w_{4}) = - ε (w_{1}, m_{2}) ε (m_{2}, w_{4})$ (Compatible signs exist on the Bruhat graph).

[F5]

The kernel of $π ⁣ : M (λ) ↠ L (λ)$ is the unique maximal submodule $J (λ)$ of $M (λ)$ , the sum of all proper submodules; in particular every proper submodule of $M (λ)$ is contained in $\ker π$ (A Verma module has a unique simple quotient).

[F6]

$C_{k} (λ) = 0$ for $k > ∣ Φ^{+} ∣$ , so $d_{k} = 0$ for $k > ∣ Φ^{+} ∣ + 1$ (The Bruhat graph and the BGG Verma sum in degree k).

Proof

1.1F1

Fix $k \geq 2$ , $w_{1}$ of length $k$ and $w_{4}$ of length $k - 2$ . By [F1] the $(w_{1}, w_{4})$ -component of $d_{k - 1} \circ d_{k}$ is $\sum_{ℓ (w_{2}) = k - 1} ε (w_{1}, w_{2}) ε (w_{2}, w_{4}) ι_{w_{2} \to w_{4}} \circ ι_{w_{1} \to w_{2}}$ , where a term is present only when $w_{1} ⊳ w_{2} ⊳ w_{4}$ and is zero otherwise, because $(d_{k})_{w_{1}, w_{2}} = 0$ unless $w_{1} ⊳ w_{2}$ and $(d_{k - 1})_{w_{2}, w_{4}} = 0$ unless $w_{2} ⊳ w_{4}$ .

1.2F1F2F5

The case $k = 1$ : $d_{0} \circ d_{1} = π \circ d_{1}$ . Each summand of $C_{1} (λ)$ maps under $d_{1}$ into $M (λ)$ through a scalar multiple of a cover embedding $ι_{s_{i} \to e}$ whose image is a proper submodule of $M (λ)$ , hence is contained in $J (λ) = \ker π$ by [F5]; therefore $π \circ d_{1} = 0$ .

2.1F3step 1.1

If no $w_{2}$ with $w_{1} ⊳ w_{2} ⊳ w_{4}$ exists, every term of step 1.1 vanishes and the component is $0$ . If such a $w_{2}$ exists, then $w_{4} < w_{1}$ with $ℓ (w_{1}) = ℓ (w_{4}) + 2$ , so by [F3] the only two candidates are $m_{1}, m_{2}$ and the component equals $ε (w_{1}, m_{1}) ε (m_{1}, w_{4}) ι_{m_{1} \to w_{4}} \circ ι_{w_{1} \to m_{1}} + ε (w_{1}, m_{2}) ε (m_{2}, w_{4}) ι_{m_{2} \to w_{4}} \circ ι_{w_{1} \to m_{2}}$ .

3.1F2F4step 2.1

In the situation of the second case of step 2.1, the two composites are equal: both are the canonical inclusion $M (w_{1} \circ λ) ↪ M (w_{4} \circ λ)$ by [F2]. The two coefficients are opposite by [F4]. Hence the component is $(ε (w_{1}, m_{1}) ε (m_{1}, w_{4}) + ε (w_{1}, m_{2}) ε (m_{2}, w_{4})) ι = 0$ , where $ι$ denotes the common composite.

4.1F6step 3.1step 1.2

The cases outside $2 \leq k \leq ∣ Φ^{+} ∣ + 1$ : for $k > ∣ Φ^{+} ∣ + 1$ one has $C_{k} (λ) = 0$ and $d_{k} = 0$ by [F6]; for $k < 0$ there is no differential. In all ranges the components of $d_{k - 1} \circ d_{k}$ that lie in the ranges where a factor is zero vanish, and the remaining components are those treated in steps 3.1 and 1.2.

5.1step 3.1step 1.2step 4.1∎

All components of $d_{k - 1} \circ d_{k}$ vanish for every $k \geq 1$ : for $k \geq 2$ by steps 1.1, 2.1 and 3.1 with [F6], for $k = 1$ by step 1.2. Hence $d_{k - 1} \circ d_{k} = 0$ for all $k \geq 2$ , and with $d_{0}$ included the augmented sequence $0 \to C_{∣ Φ^{+} ∣} (λ) \to \dots \to C_{1} (λ) \to C_{0} (λ) \to L (λ) \to 0$ is a complex of $g$ -modules, i.e. a chain complex in $O$ (Chain complex in an abelian category).

Depends on

Used by

Dependency tree · two levels

27 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. 4.1 Step 1, p. 14 (standard reference, not scraped)
N. Hemelsoet and R. Voorhaar, A computer algorithm for the BGG resolution, arXiv:1911.00871, Sec. 2.2 (solving $d^2=0$ square-wise), pp. 4-5 (standard reference, not scraped)