CorollaryStatement: 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 resolution has length the number of positive roots

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $λ \in Λ^{+}$ and let $w_{0} \in W$ be the longest element. Then $ℓ (w_{0}) = ∣ Φ^{+} ∣$ and $∣ {w \in W : ℓ (w) = ∣ Φ^{+} ∣} ∣ = 1$ , the BGG complex $C_{∙} (λ)$ is concentrated in degrees $0 \leq k \leq ∣ Φ^{+} ∣$ , the top term is $C_{∣ Φ^{+} ∣} (λ) = M (w_{0} \circ λ) \neq 0$ , and all higher terms vanish. Consequently the resolution has length $∣ Φ^{+} ∣$ and the last nonzero degree of the complex is $∣ Φ^{+} ∣$ ; in particular the alternating sum of The Euler-character identity for a finite-dimensional simple module is finite and has $∣ W ∣$ terms.

Facts & Assumptions

Given: The Axiom of Choice, a dominant integral weight $λ \in Λ^{+}$ , the longest element $w_{0} \in W$ , and the BGG complex $C_{∙} (λ)$ .

[F1]

$w_{0} Φ^{+} = Φ^{-}$ , $w_{0}$ is the unique longest element, and $ℓ (w) = ∣ Inv (w) ∣$ for every $w$ , where $Inv (w) = {α \in Φ^{+} : w α \in Φ^{-}}$ ; hence $ℓ (w_{0}) = ∣ Φ^{+} ∣$ and $ℓ (w) \leq ∣ Φ^{+} ∣$ for every $w$ , with equality only for $w = w_{0}$ (Finite Weyl closed chambers and stabilizers, Finite Weyl strong exchange and deletion, Finite Weyl positive roots and simple reflections).

[F2]

$C_{k} (λ) = ⨁_{ℓ (w) = k} M (w \circ λ)$ for $0 \leq k \leq ∣ Φ^{+} ∣$ and $C_{k} (λ) = 0$ for $k > ∣ Φ^{+} ∣$ ; the summands are indexed by the elements of $W$ of length $k$ , and $C_{∣ Φ^{+} ∣} (λ) = M (w_{0} \circ λ)$ because $w_{0}$ is the unique element of maximal length (The Bruhat graph and the BGG Verma sum in degree k, Verma modules).

[F3]

$M (ψ) \neq 0$ for every weight $ψ$ : $M (ψ)$ has a nonzero highest weight vector $v_{ψ}$ and $u \mapsto u v_{ψ}$ is a vector-space isomorphism $U (n^{-}) \tilde{\to} M (ψ)$ (Verma modules, The PBW model of a Verma module).

[F4]

$0 \to C_{∣ Φ^{+} ∣} (λ) \to \dots \to C_{1} (λ) \to C_{0} (λ) \to L (λ) \to 0$ is exact; equivalently the unaugmented complex $C_{∙} (λ)$ has homology $L (λ)$ in degree $0$ and no homology in positive degrees (The BGG resolution of a finite-dimensional simple module).

[F5]

The Euler-character identity expresses $[L (λ)]$ as the finite alternating sum $\sum_{w \in W} (- 1)^{ℓ (w)} [M (w \circ λ)]$ , whose terms are indexed by the elements of $W$ (The Euler-character identity for a finite-dimensional simple module).

Proof

1.1F1

Since $w_{0} Φ^{+} = Φ^{-}$ , one has $Inv (w_{0}) = {α \in Φ^{+} : w_{0} α \in Φ^{-}} = Φ^{+}$ , so $ℓ (w_{0}) = ∣ Inv (w_{0}) ∣ = ∣ Φ^{+} ∣$ by [F1]. If $ℓ (w) = ∣ Φ^{+} ∣$ for some $w$ , then $Inv (w)$ is a subset of $Φ^{+}$ of full cardinality, hence equals $Φ^{+}$ , so $w$ sends every positive root to a negative root, $w Φ^{+} = Φ^{-}$ , and by uniqueness of $w_{0}$ in [F1] we get $w = w_{0}$ . Therefore $∣ {w \in W : ℓ (w) = ∣ Φ^{+} ∣} ∣ = 1$ and $ℓ (w_{0}) = ∣ Φ^{+} ∣$ and $∣ {w \in W : ℓ (w) = ∣ Φ^{+} ∣} ∣ = 1$ .

1.2F2F3

By [F2] the complex is concentrated in degrees $0, \dots, ∣ Φ^{+} ∣$ with $C_{k} (λ) = 0$ for $k > ∣ Φ^{+} ∣$ , and the top term is $C_{∣ Φ^{+} ∣} (λ) = M (w_{0} \circ λ)$ ; this is nonzero by [F3]. Hence the last nonzero degree of the complex is $∣ Φ^{+} ∣$ and the resolution of [F4] has length $∣ Φ^{+} ∣$ .

1.3F5

The alternating sum of [F5] is $\sum_{w \in W} (- 1)^{ℓ (w)} [M (w \circ λ)]$ : it is finite, and its terms are indexed by the $∣ W ∣$ elements of the Weyl group, so it has exactly $∣ W ∣$ terms.

2.1F4step 1.1step 1.2step 1.3∎

Combining: $ℓ (w_{0}) = ∣ Φ^{+} ∣$ and $∣ {w : ℓ (w) = ∣ Φ^{+} ∣} ∣ = 1$ by step 1.1; the complex is concentrated in degrees $0 \leq k \leq ∣ Φ^{+} ∣$ with top term $M (w_{0} \circ λ) \neq 0$ and all higher terms zero by step 1.2; the resolution has length $∣ Φ^{+} ∣$ , its highest nonzero degree is $∣ Φ^{+} ∣$ (homology is concentrated in degree $0$ by [F4]), and the alternating sum has $∣ W ∣$ terms by step 1.3.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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 ($\ell(w_0)=|\Phi^+|=\dim\mathfrak n^-$) (standard reference, not scraped)
N. Hemelsoet and R. Voorhaar, A computer algorithm for the BGG resolution, arXiv:1911.00871, Sec. 2.1, p. 3 (standard reference, not scraped)