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.

Dimension of the kernel modulo n-minus equals the next term (BGG 10.7)

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $λ \in Λ^{+}$ , let $k \geq 0$ , and assume that $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$ (vacuous for $k = 0$ ). Let $d_{k} ⁣ : C_{k} (λ) \to C_{k - 1} (λ)$ be the BGG differential of The BGG differential from signed Verma maps. Then $\ker d_{k} / n^{-} \ker d_{k}$ is finite-dimensional and

$\dim_{C} \ker d_{k} / n^{-} \ker d_{k} = \dim_{C} C_{k + 1} (λ) / n^{-} C_{k + 1} (λ) = ∣ W_{k + 1} ∣ .$

Facts & Assumptions

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

[F1]

$\ker d_{k}$ is an object of $O$ of finite length, and every object $M$ of $O$ has a finite-dimensional $b$ -stable $h$ -semisimple generating subspace $E$ with a $b$ -flag whose quotients are one dimensional and annihilated by $n^{+}$ ; hence $M = U (n^{-}) E$ and $M / n^{-} M$ is spanned by the classes of finitely many weight vectors, so it is finite-dimensional (Category O is abelian and extension closed among weight modules, Finite Borel-stable generators and weight flags, Every object of O has finite length, The classical BGG category O).

[F2]

$C_{k + 1} (λ) = ⨁_{ℓ (w) = k + 1} M (w \circ λ)$ , each $M (ψ) ≅ U (n^{-}) v_{ψ}$ is free over $U (n^{-})$ on its highest weight vector, and $M (ψ) / n^{-} M (ψ) = C {\overset{ˉ}{v}}_{ψ}$ is one-dimensional of weight $ψ$ ; the weights $w \circ λ$ are pairwise distinct, so $\dim_{C} C_{k + 1} (λ) / n^{-} C_{k + 1} (λ) = ∣ W_{k + 1} ∣$ (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).

[F3]

${Tor}_{k + 1}^{U (n^{-})} (C, Π_{λ}) ≅ C^{∣ W_{k + 1} ∣}$ , where $Π_{λ} = L (λ)$ (Tor with the trivial module is computed by the weak BGG resolution).

[F4]

Tor can be computed from a free (hence projective) resolution $\dots \to F_{2} \to F_{1} \to F_{0} \to Π_{λ} \to 0$ of the left module $Π_{λ}$ : ${Tor}_{n}^{U (n^{-})} (C, Π_{λ}) = H_{n} (F_{∙} / n^{-} F_{∙})$ , and the functor $C \otimes_{U (n^{-})} (-)$ is right exact; free modules and their finite direct sums are projective, so resolutions exist under the Axiom of Choice (Tor from a projective resolution of the left module, The balanced Tor bifunctor, Degree-zero Tor is the tensor product in either construction, The long exact Tor sequence in the left-module variable, Under the Axiom of Choice, every module admits a projective resolution).

[F5]

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

[F6]

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

[F7]

$\ker d_{0} = \ker π$ is the maximal submodule of $M (λ) = C_{0} (λ)$ , which does not contain the highest weight vector, and $C_{0} (λ) / n^{-} C_{0} (λ) = C {\overset{ˉ}{v}}_{λ}$ has weight $λ$ (A Verma module has a unique simple quotient, A proper Verma submodule misses the highest-weight line, The PBW model of a Verma module).

Proof

1.1F1F2

By [F1] the space $\ker d_{k} / n^{-} \ker d_{k}$ is finite-dimensional and is spanned by classes of weight vectors; choose weight vectors $v_{1}, \dots, v_{n} \in \ker d_{k}$ whose classes ${\overset{ˉ}{v}}_{1}, \dots, {\overset{ˉ}{v}}_{n}$ form a basis of $\ker d_{k} / n^{-} \ker d_{k}$ . By [F2] the space $C_{k + 1} (λ) / n^{-} C_{k + 1} (λ)$ has dimension $∣ W_{k + 1} ∣$ .

2.1F1F5step 1.1

Let $D : = U (n^{-}) g_{1} \oplus \dots \oplus U (n^{-}) g_{n}$ be free on generators $g_{i}$ , and let $δ ⁣ : D \to \ker d_{k}$ be the $U (n^{-})$ -linear map with $δ (g_{i}) = v_{i}$ . Its reduction $\overset{ˉ}{δ} ⁣ : D / n^{-} D \to \ker d_{k} / n^{-} \ker d_{k}$ sends the basis ${\overset{ˉ}{g}}_{i}$ to the basis ${\overset{ˉ}{v}}_{i}$ , so it is an isomorphism, in particular surjective; the images $δ (g_{i}) = v_{i}$ are weight vectors, so [F5] applied to $M = D$ , $N = \ker d_{k}$ gives that $δ$ is surjective. Hence $im δ = \ker d_{k}$ , and the augmented sequence $D \to C_{k} (λ) \to C_{k - 1} (λ) \to \dots \to C_{0} (λ) \to Π_{λ} \to 0$ is exact: at $D \to C_{k}$ by surjectivity onto $\ker d_{k}$ , at $C_{j}$ for $0 \leq j \leq k - 1$ by the exactness hypothesis, at $C_{k}$ because $im δ = \ker d_{k}$ , and at $Π_{λ}$ because the augmentation is surjective.

3.1F2F4step 2.1

Every $C_{j} (λ)$ is free over $U (n^{-})$ by [F2], and $D$ is free; choose a free $U (n^{-})$ -module $D_{2}$ with a surjection $D_{2} ↠ \ker δ$ and continue inductively to obtain a free resolution $\dots \to D_{2} \to D \to C_{k} (λ) \to \dots \to C_{0} (λ) \to Π_{λ} \to 0$ of $Π_{λ}$ .

4.1F6F7step 2.1step 3.1

We compute the two maps that enter ${Tor}_{k + 1}$ . First, applying the right exact functor $C \otimes_{U (n^{-})} (-)$ to the exact sequence $D_{2} \to D \overset{δ}{\to} \ker d_{k} \to 0$ from step 3.1 gives an exact sequence $D_{2} / n^{-} D_{2} \to D / n^{-} D \to \ker d_{k} / n^{-} \ker d_{k} \to 0$ whose second map is the isomorphism $\overset{ˉ}{δ}$ ; hence the first map is zero. Second, if $k \geq 1$ , applying the functor to the exact sequence $D \overset{δ}{\to} C_{k} (λ) \overset{d_{k}}{\to} \ker d_{k - 1} \to 0$ (exact by step 2.1 and the hypothesis at $k - 1$ ) gives an exact sequence $D / n^{-} D \to C_{k} (λ) / n^{-} C_{k} (λ) \overset{{\overset{ˉ}{d}}_{k}}{\to} \ker d_{k - 1} / n^{-} \ker d_{k - 1} \to 0$ ; the composite is zero because $d_{k} δ = 0$ , and ${\overset{ˉ}{d}}_{k}$ is injective by [F6] with $j = k - 1$ (using exactness in degrees $0, \dots, k - 2$ , which the hypothesis provides), so the first map is zero. If $k = 0$ , the map $D / n^{-} D \to C_{0} (λ) / n^{-} C_{0} (λ)$ is zero because $δ (D) \subseteq \ker d_{0}$ , every weight of $\ker d_{0}$ is different from $λ$ by [F7], and $C_{0} (λ) / n^{-} C_{0} (λ)$ is one-dimensional of weight $λ$ .

5.1F4step 4.1

By the resolution of step 3.1 and [F4], ${Tor}_{k + 1}^{U (n^{-})} (C, Π_{λ})$ is the homology at degree $k + 1$ of the complex $\dots \to D_{2} / n^{-} D_{2} \to D / n^{-} D \to C_{k} (λ) / n^{-} C_{k} (λ) \to \dots$ , namely $\ker (D / n^{-} D \to C_{k} (λ) / n^{-} C_{k} (λ)) / im (D_{2} / n^{-} D_{2} \to D / n^{-} D)$ . Both maps vanish by step 4.1, so this homology equals $D / n^{-} D$ , which is isomorphic to $\ker d_{k} / n^{-} \ker d_{k}$ via $\overset{ˉ}{δ}$ .

6.1F1F2F3step 1.1step 5.1∎

Combining steps 1.1, 5.1 and [F3]: $\dim_{C} \ker d_{k} / n^{-} \ker d_{k} = \dim_{C} {Tor}_{k + 1}^{U (n^{-})} (C, Π_{λ}) = ∣ W_{k + 1} ∣$ , which equals $\dim_{C} C_{k + 1} (λ) / n^{-} C_{k + 1} (λ)$ by step 1.1. This proves both equalities.

Depends on

Used by

The BGG resolution of a finite-dimensional simple module Theorem

Dependency tree · two levels

67 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.3 (BGG Lemma 10.7), pp. 26-29 (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, Lemma 10.5 and Corollary 10.6, pp. 354-356 (standard reference, not scraped)