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.

Weak BGG resolution of the trivial module

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $B_{k}$ be the standard induced complex of The standard induced resolution of the trivial module and let $B_{k}^{χ_{0}}$ denote its generalised central-character component at the central character $χ_{0}$ of $M (0)$ . Then $0 \to B_{∣ Φ^{+} ∣}^{χ_{0}} \to \dots \to B_{1}^{χ_{0}} \to B_{0}^{χ_{0}} \to C \to 0$ is a resolution of the trivial module by objects of $O$ , and $Typ B_{k}^{χ_{0}} = {w \circ 0 : ℓ (w) = k}$ , each weight occurring once.

Facts & Assumptions

Given: The Axiom of Choice, the standard induced complex $(B_{∙}, d_{∙})$ with augmentation $B_{0} \to C$ of The standard induced resolution of the trivial module, and the central character $χ_{0}$ of $M (0)$ .

[F1]

$(B_{∙}, d_{∙})$ is a complex of objects of $O$ with $B_{k} ≅ U (n^{-}) \otimes Λ^{k} (n^{-})$ , and $0 \to B_{∣ Φ^{+} ∣} \to \dots \to B_{0} \to C \to 0$ is exact (The standard induced resolution of the trivial module, The standard induced complex is a resolution of the trivial module).

[F2]

The induced module $U (g) \otimes_{U (b)} N$ for a finite-dimensional $h$ -semisimple $b$ -module $N$ is Verma-filtered with type $Wt N$ (Induced modules from finite-dimensional B-modules have type their weights). Since $g / b ≅ n^{-}$ has weights $Φ^{-} = - Φ^{+}$ , the exterior power $Λ^{k} (g / b)$ has weight multiset $Wt Λ^{k} (g / b) = {- \sum_{α \in S} α : S \subseteq Φ^{+}, ∣ S ∣ = k}$ , so $Typ B_{k} = {- \sum_{α \in S} α : ∣ S ∣ = k}$ .

[F3]

The central-character projection $(-)_{χ_{0}}$ is an exact functor on $O$ and sends a Verma-filtered module $M$ to a Verma-filtered module with $Typ M_{χ_{0}} = {ψ \in Typ M : χ_{ψ} = χ_{0}}$ (Generalized central-character decomposition of O, Generalized central-character summands, Central-character cuts of a typed module are typed by the matching weights).

[F4]

$χ_{ψ} = χ_{0}$ if and only if $ψ = w \circ 0$ for some $w \in W$ ; the weights $w \circ 0$ are pairwise distinct and $w \circ 0 = - \sum_{α \in Π_{w}} α$ with $Π_{w} = {α \in Φ^{+} : w^{- 1} α \in Φ^{-}}$ , $# Π_{w} = ℓ (w)$ ; if $S \subseteq Φ^{+}$ has $\sum_{α \in S} α = \sum_{α \in Π_{w}} α$ then $S = Π_{w}$ (Central characters are dot-Weyl orbits, Weight subsets with equal root sums are unique, Positive coroot pairings of a dominant integral weight).

[F5]

The trivial module $C$ has central character $χ_{0}$ , so $C_{χ_{0}} = C$ (Generalized central-character subcategories, Central-character cuts of a typed module are typed by the matching weights).

Proof

1.1F1F3F5

The projection functor is exact by [F3], so applying it to the exact complex of [F1] and to its augmentation gives an exact complex $0 \to B_{∣ Φ^{+} ∣}^{χ_{0}} \to \dots \to B_{1}^{χ_{0}} \to B_{0}^{χ_{0}} \to C_{χ_{0}} \to 0$ ; by [F5] this is a resolution of $C$ by the objects $B_{k}^{χ_{0}}$ of $O$ .

1.2F2F3F4

By [F2] the type of $B_{k}$ is the multiset ${- \sum_{α \in S} α : S \subseteq Φ^{+}, ∣ S ∣ = k}$ . Cutting by $χ_{0}$ and using [F3], the type of $B_{k}^{χ_{0}}$ consists of those sums $- \sum_{α \in S} α$ with $χ_{- \sum_{S} α} = χ_{0}$ ; by [F4] this is equivalent to $- \sum_{α \in S} α = w \circ 0$ for some $w \in W$ .

2.1F4step 1.2

For every $w \in W$ of length $k$ the subset $Π_{w}$ has $k$ elements and $w \circ 0 = - \sum_{α \in Π_{w}} α$ by [F4], so $w \circ 0$ occurs in $Typ B_{k}^{χ_{0}}$ . Conversely, if $S \subseteq Φ^{+}$ has $k$ elements and $- \sum_{α \in S} α = w \circ 0 = - \sum_{α \in Π_{w}} α$ , then $\sum_{S} α = \sum_{Π_{w}} α$ and the uniqueness statement of [F4] gives $S = Π_{w}$ , so the sum is the one attached to $w$ ; in particular $k = ∣ S ∣ = # Π_{w} = ℓ (w)$ . Distinct $w$ give distinct weights $w \circ 0$ and distinct subsets $Π_{w}$ by [F4], so the correspondence $w \leftrightarrow Π_{w}$ is a bijection between the elements of length $k$ and the surviving $k$ -element subsets. Hence $Typ B_{k}^{χ_{0}} = {w \circ 0 : ℓ (w) = k}$ with each weight occurring once.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 together give the asserted resolution and its type.

Depends on

Used by

Weak BGG resolution Theorem

Dependency tree · two levels

40 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. 5.2, pp. 33-34 (standard reference, not scraped)
J. van Ekeren, Topics in representation theory (IMPA 2024), Sec. 29, pp. 123-124 (standard reference, not scraped)