LemmaStatement: 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.

Composition factors of the BGG kernel lie above the degree (BGG 10.6a)

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $λ \in Λ^{+}$ , let $k \geq 0$ , and let $d_{k} ⁣ : C_{k} (λ) \to C_{k - 1} (λ)$ be the BGG differential of The BGG differential from signed Verma maps (with $d_{0} = π$ the augmentation). Assume that the complex $C_{∙} (λ)$ is exact in degrees $0, \dots, k - 1$ , that is, $im d_{j + 1} = \ker d_{j}$ for $0 \leq j \leq k - 1$ ; this hypothesis is vacuous for $k = 0$ . If a simple module $L (μ)$ occurs in a composition series of $\ker d_{k}$ , then $μ = u \circ λ$ with $ℓ (u) \geq k + 1$ . Equivalently, no composition factor of $\ker d_{k}$ has the form $L (u \circ λ)$ with $ℓ (u) \leq k$ .

Facts & Assumptions

Given: The Axiom of Choice, a dominant integral weight $λ \in Λ^{+}$ , an integer $k \geq 0$ , the BGG complex $C_{∙} (λ)$ with differentials $d_{j}$ , and the hypothesis that $C_{∙} (λ)$ is exact in degrees $0, \dots, k - 1$ .

[F1]

The weak BGG resolution: $0 \to B_{∣ Φ^{+} ∣} (λ) \to \dots \to B_{1} (λ) \to B_{0} (λ) \to Π_{λ} \to 0$ is an exact complex of objects of $O$ and $Typ B_{i} (λ) = {w \circ λ : ℓ (w) = i}$ with each weight occurring once (Weak BGG resolution, Type of a module with a Verma filtration).

[F2]

$C_{i} (λ) = ⨁_{ℓ (w) = i} M (w \circ λ)$ is a direct sum of Verma modules and $B_{i} (λ)$ is Verma-filtered with type ${w \circ λ : ℓ (w) = i}$ , so the multiset of Jordan-Holder factors is $JH C_{i} = ⨆_{ℓ (w) = i} JH M (w \circ λ) = JH B_{i}$ : the factors of a direct sum and of a filtration are the multiset unions of the factors of the pieces, and the factors of $M (w \circ λ)$ are independent of the filtration (The BGG differential from signed Verma maps, The Bruhat graph and the BGG Verma sum in degree k, Composition series and composition factors of an object).

[F3]

If a simple module $L (μ)$ occurs in a composition series of $M (w \circ λ)$ , then $μ = u \circ λ$ with $u \geq w$ in Bruhat order, so $ℓ (u) \geq ℓ (w)$ ; every composition factor of $C_{i} (λ)$ therefore has the form $L (u \circ λ)$ with $ℓ (u) \geq i$ (Jordan-Holder factors of Verma modules dominate the head (BGG 8.12)).

[F4]

For a short exact sequence $0 \to A \to B \to C \to 0$ of objects of $O$ the multisets satisfy $JH B = JH A ⊎ JH C$ ; hence equalities of two of the multisets force the equality of the third, and $JH A \subseteq JH B$ for a subobject $A \subseteq B$ . Objects of $O$ have finite length and $O$ is abelian (Category O is abelian and extension closed among weight modules, Every object of O has finite length, Composition series and composition factors of an object).

[F5]

The complex $B_{∙} (λ)$ is exact at every degree (it is a resolution), while $C_{∙} (λ)$ is a complex; by hypothesis it is exact at degrees $0, \dots, k - 1$ (Weak BGG resolution, The BGG differential from signed Verma maps, Chain complex in an abelian category).

Proof

1.1F2F4F5

The comparison chain. We prove $JH \ker d_{i} = JH \ker d_{i}^{B}$ for all $0 \leq i \leq k$ by induction on $i$ . Base $i = 0$ : the augmentation $Π_{λ} = B_{0} (λ) / \ker d_{0}^{B} = C_{0} (λ) / \ker d_{0}$ is the same simple module, so $JH (B_{0} / \ker d_{0}^{B}) = JH (C_{0} / \ker d_{0})$ , and [F2] gives $JH B_{0} = JH C_{0}$ ; by the additivity of [F4] applied to $0 \to \ker d_{0}^{B} \to B_{0} \to B_{0} / \ker d_{0}^{B} \to 0$ and to the same sequence for $C_{0}$ , the equality of the middle and quotient multisets gives $JH \ker d_{0}^{B} = JH \ker d_{0}$ .

2.1F2F4F5step 1.1F1

Induction step. Let $1 \leq i \leq k$ and assume $JH \ker d_{i - 1}^{B} = JH \ker d_{i - 1}$ . By exactness of $B_{∙}$ at $i - 1$ we have $im d_{i}^{B} = \ker d_{i - 1}^{B}$ , and by the hypothesis of the statement (which covers $i - 1 \leq k - 1$ ) we have $im d_{i} = \ker d_{i - 1}$ ; hence $JH im d_{i}^{B} = JH im d_{i}$ . The first isomorphism theorem applied in the abelian category gives $im d_{i}^{B} ≅ B_{i} / \ker d_{i}^{B}$ and $im d_{i} ≅ C_{i} / \ker d_{i}$ , so $JH (B_{i} / \ker d_{i}^{B}) = JH (C_{i} / \ker d_{i})$ . Since $JH B_{i} = JH C_{i}$ by [F2], additivity [F4] applied to the two short exact sequences $0 \to \ker d_{i}^{B} \to B_{i} \to B_{i} / \ker d_{i}^{B} \to 0$ and $0 \to \ker d_{i} \to C_{i} \to C_{i} / \ker d_{i} \to 0$ yields $JH \ker d_{i}^{B} = JH \ker d_{i}$ .

3.1F4F5step 1.1step 2.1

At $i = k$ , the comparison gives $JH \ker d_{k} = JH \ker d_{k}^{B}$ . Exactness gives $\ker d_{k}^{B} = im d_{k + 1}^{B}$ . Applying [F4] to $0 \to \ker d_{k + 1}^{B} \to B_{k + 1} \to im d_{k + 1}^{B} \to 0$ yields $JH \ker d_{k} = JH im d_{k + 1}^{B} \subseteq JH B_{k + 1}$ .

4.1F2F3step 3.1

By [F2] $JH B_{k + 1} = ⨆_{ℓ (w) = k + 1} JH M (w \circ λ)$ , and by [F3] every simple factor in this union is $L (u \circ λ)$ with $ℓ (u) \geq k + 1$ . Hence every composition factor of $\ker d_{k}$ is of the form $L (u \circ λ)$ with $ℓ (u) \geq k + 1$ , which proves the main assertion.

5.1F3step 4.1∎

For the equivalent formulation, note first that $\ker d_{k} \subseteq C_{k} (λ)$ , so every factor of $\ker d_{k}$ is a factor of $C_{k} (λ)$ and hence, by [F3], of the form $L (u \circ λ)$ with $ℓ (u) \geq k$ . Given step 4.1, the condition "no factor of $\ker d_{k}$ has the form $L (u \circ λ)$ with $ℓ (u) \leq k$ " is therefore equivalent to the main assertion.

Depends on

Used by

The BGG differential induces an injection into kernel coinvariants (BGG 10.6) Lemma

Dependency tree · two levels

59 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.2.2 (BGG Lemma 10.6a), pp. 22-25 (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. 9 and Sec. 10, pp. 349-354 (standard reference, not scraped)