TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Translation to the wall on Verma, simple and projective objects

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $(λ, μ)$ be as in The facet tensor-weight exclusion lemma: $λ$ integral dot-antidominant and dot-regular, $μ$ integral dot-antidominant with $F_{μ}$ in the closure of the chamber $F_{λ}$ , $J = J (μ)$ , $W_{μ} = W_{J}$ . Let $ν$ be the unique dominant weight of $W (μ - λ)$ and let $T : = T_{λ}^{μ} = {pr}_{χ_{μ}} \circ (L (ν) \otimes -) \circ {incl}_{χ_{λ}} ⁣ : O_{λ} ⟶ O_{μ}, T^{'} : = T_{μ}^{λ},$ be the translation functors of Translation functors by tensoring and projection, which are exact and biadjoint (Translation functors are exact and biadjoint). Then:

(1) $T Δ (w \cdot λ) ≅ Δ (w \cdot μ)$ and $T \nabla (w \cdot λ) ≅ \nabla (w \cdot μ)$ for every $w \in W$ .

(2) $T L (w \cdot λ) ≅ L (w \cdot μ)$ if $w \in W^{J}$ , and $T L (w \cdot λ) = 0$ otherwise; equivalently $T L (w \cdot λ) \neq 0$ if and only if $w$ lies in the set $W^{J}$ of minimal representatives of the cosets $w W_{J}$ .

(3) (Big projective on the wall.) Let $Ξ_{μ} : = T_{- ρ}^{μ} L (- ρ)$ be the translate of the simple object of the most singular block. Then $Ξ_{μ}$ is projective and injective in $O_{μ}$ , it is the projective cover $P (1 \cdot μ)$ of $L (μ)$ , and $(Ξ_{μ} : Δ (w \cdot μ)) = 1$ for every distinct orbit label (equivalently for its representatives $w \in W^{J}$ ); consequently $(P (μ) : Δ (y \cdot μ)) = 1$ for every distinct label $y \in W^{J}$ and $[Δ (w \cdot μ) : L (μ)] = 1$ for all $w \in W$ .

Facts & Assumptions

Given: The facet data $(λ, μ)$ of The facet tensor-weight exclusion lemma with $J = J (μ)$ , $W_{μ} = W_{J}$ , the translating weight $ν$ and $E = L (ν)$ ; the functors $T = T_{λ}^{μ}$ , $T^{'} = T_{μ}^{λ}$ of Translation functors by tensoring and projection with $E^{*} = L (ν)^{*}$ ; write $λ_{∙} = λ + ρ$ , $μ_{∙} = μ + ρ$ .

[F1]

$T = {pr}_{χ_{μ}} \circ (E \otimes -) \circ {incl}_{χ_{λ}}$ and $T^{'} = {pr}_{χ_{λ}} \circ (E^{*} \otimes -) \circ {incl}_{χ_{μ}}$ ; inclusions and projections are exact, and $O$ is the direct sum of its central-character blocks (Translation functors by tensoring and projection, Generalized central-character decomposition of O, Central characters are dot-Weyl orbits).

[F2]

$T$ and $T^{'}$ are exact and each is both a left and a right adjoint of the other; they send projectives to projectives and injectives to injectives (Translation functors are exact and biadjoint).

[F3]

The unique-factor clause: for every $w \in W$ , the tensor $E \otimes Δ (w \cdot λ)$ has exactly one Verma factor with central character $χ_{μ}$ , namely $Δ (w \cdot μ)$ , of multiplicity one (The facet tensor-weight exclusion lemma).

[F4]

Tensoring with $E$ preserves finite Verma flags: $E \otimes Δ (η)$ has a finite Verma flag with factors $Δ (η + γ)$ , $γ$ running over the weights of $E$ with multiplicity $\dim E_{γ}$ ; the flag factors of $E \otimes X$ for Verma-filtered $X$ are computed by convolution (Finite-dimensional tensoring preserves Verma flags).

[F5]

The block $O_{μ}$ : $J (μ)$ indexes the vanishing simple coroot pairings of $μ_{∙}$ , $W_{J}$ is the dot stabilizer of $μ$ , the labels $w \cdot μ$ depend only on $w W_{J}$ , and $W^{J}$ is the set of minimal right coset representatives (The singular integral block and its dot stabilizer, Dot-Weyl facets and single-wall translation data).

[F6]

Restricted Chevalley duality: $D (M)_{η} = M_{η}^{*}$ with the $τ$ -twisted action; $D$ is an exact contravariant involution of $O$ , preserves weight-space dimensions, simple composition multiplicities and central-character blocks, and $D (L (η)) ≅ L (η)$ , $D (Δ (η)) = \nabla (η)$ (Restricted duality is exact and involutive on O, Standard and costandard objects). For finite-dimensional $E$ , the natural tensor-dual identification is $D (E) \otimes D (M) ≅ D (E \otimes M)$ , with the Chevalley-twisted dual $D (E)$ , not the ordinary dual $E^{*}$ .

[F8]

For a dominant integral weight $ν$ , every weight $γ$ of $L (ν)$ satisfies $∣ γ ∣ \leq ∣ ν ∣$ , with equality exactly when $γ \in W ν$ , and every weight of the orbit $W ν$ occurs in $L (ν)$ with multiplicity one (Weights of a finite-dimensional simple module lie in the norm ball).

[F7]

Each Verma has the unique simple head $L (η)$ (A Verma module has a unique simple quotient), whose dual is the simple socle of its costandard by [F6]. BGG data: a nonzero $g$ -homomorphism $M (η) \to M (ζ)$ exists if and only if $η ↑ ζ$ in the strong linkage order (The BGG criterion for homomorphisms between Verma modules), such a map is injective (A nonzero homomorphism between Verma modules is injective), BGG reciprocity $(P (η) : Δ (ζ)) = [Δ (ζ) : L (η)]$ holds with finitely many nonzero multiplicities (BGG reciprocity, Finite Verma flags and their multiplicities, Projectives in category O have finite Verma flags), and $Hom (Δ (η), \nabla (ζ))$ is $0$ or one-dimensional according as $η \neq ζ$ or $η = ζ$ (Standard-costandard Hom and Ext-one orthogonality). Every object of $O$ has finite length and finite-length objects decompose into indecomposables (The simple objects of O, Fitting decomposition in a finite-length abelian category, Projective covers in O are indecomposable and unique, Category O has enough projectives).

[F9]

Orbit and weight bounds: for dot-antidominant integral $η$ , applying Dominant integral weights are maxima of their Weyl orbits to $- η - ρ$ gives $w \cdot η \geq η$ for every $w$ . Verma weights lie in $η - Q^{+}$ and the highest-weight space is one dimensional (Weights of a Verma module lie below lambda). By the central-character and simple-label facts in [F1], [F7], every composition factor of $M (η)$ has its highest weight in $W \cdot η$ ; the two bounds force that weight to equal $η$ . Exactness of weight spaces and the one-dimensional top then force length one. Thus $M (η) = L (η)$ , including singular $η$ and $η = - ρ$ .

[F10]

Finite-Weyl root/length criterion (Finite Weyl strong exchange and deletion): $ℓ (w s_{j}) < ℓ (w)$ iff $w α_{j} < 0$ , and $ℓ (s_{i} v) > ℓ (v)$ iff $v^{- 1} α_{i} > 0$ . Positive roots of a parabolic subsystem are nonnegative combinations of its simple roots, so $w α_{j} > 0$ for all $j \in J$ implies $w Φ_{J}^{+} \subseteq Φ^{+}$ .

Proof

technique · direct: compute $T$ on standards by the unique surviving factor, transport to costandards by restricted duality, decide simple survival by the nonminimal Verma embedding, and manufacture the big projective from the most singular block

1.1F1F3F4algebra

Standards (first clause of (1)). By [F3], the tensor $E \otimes Δ (w \cdot λ)$ has a finite Verma flag by [F4] in which the unique factor with central character $χ_{μ}$ is $Δ (w \cdot μ)$ , once. The exact projection ${pr}_{χ_{μ}}$ applied to this flag kills every factor whose central character differs from $χ_{μ}$ and carries the remaining $Δ (w \cdot μ)$ isomorphically, so $T Δ (w \cdot λ) ≅ Δ (w \cdot μ)$ for every $w$ .

1.2F1F2F4F5F6F7F8F9F10algebra

The big projective (3). By [F9], $M (- ρ) = L (- ρ)$ . Its dot orbit is a singleton, so BGG reciprocity [F7] gives a one-factor Verma flag for $P (- ρ)$ , proving $P (- ρ) = L (- ρ)$ . Simple-preserving duality makes it injective too. Put $E_{0} = L (w_{0} μ_{∙})$ and $S = T_{- ρ}^{μ}$ , whose adjoint is $S^{'} = T_{μ}^{- ρ}$ ; the ordinary dual $E_{0}^{*}$ has highest weight $- μ_{∙}$ . By [F2], $Ξ_{μ} = S L (- ρ)$ is projective and injective. Tensoring $M (- ρ)$ with $E_{0}$ and projecting retains exactly the factors $Δ (- ρ + γ)$ with $γ \in W μ_{∙}$ , each once by [F4], [F8]. These are precisely the distinct standards $Δ (y \cdot μ)$ . Likewise, since $L (μ) = M (μ)$ by [F9], tensoring it with $E_{0}^{*}$ and projecting to $χ_{- ρ}$ retains only $Δ (- ρ)$ , once, from the extremal weight $- μ_{∙}$ . Thus $S^{'} L (μ) = L (- ρ)$ , and adjunction gives $\dim Hom (Ξ_{μ}, L (μ)) = 1$ . The resulting epimorphism splits off the projective cover $P (μ)$ : lift it through the cover, use essentiality to make the lift surjective, and split by projectivity. For every $y$ , there is an injection $M (μ) ↪ M (y \cdot μ)$ . Indeed induct on a reduced expression $y = s_{i} v$ : [F10] gives $v^{- 1} α_{i} > 0$ , so $⟨ v (μ_{∙}), α_{i}^{\lor} ⟩ \leq 0$ . If it is zero the weights coincide; otherwise the positive integral pairing at $s_{i} v \cdot μ$ supplies the one-step strong linkage and the injection $M (v \cdot μ) ↪ M (s_{i} v \cdot μ)$ by [F7]. Compose these injections. BGG then gives $(P (μ) : Δ (y \cdot μ)) \geq 1$ for every distinct label. The direct-summand complement of $P (μ)$ in $Ξ_{μ}$ is projective and has a Verma flag by [F7]. Additivity and the already computed one-per-label flag of $Ξ_{μ}$ force every flag multiplicity of the complement to vanish, so the complement is zero. Hence $Ξ_{μ} = P (μ)$ and all the displayed standard and composition multiplicities are one.

2.1F5F7F10step 1.1algebra

Nonminimal vanishing (second half of (2)). Suppose $w \notin W^{J}$ ; then there is a simple $s \in J$ with $ℓ (w s) < ℓ (w)$ , equivalently $w α_{s} < 0$ by [F10]. Then $w \cdot λ - w s \cdot λ = w (λ - s \cdot λ) = ⟨ λ_{∙}, α_{s}^{\lor} ⟩ w α_{s}$ with $⟨ λ_{∙}, α_{s}^{\lor} ⟩ < 0$ and $w α_{s} < 0$ , so $w \cdot λ - w s \cdot λ \in Q^{+} ∖ {0}$ : $w s \cdot λ$ is strictly below $w \cdot λ$ . Put $β = - w α_{s} \in Φ^{+}$ ; then $s_{β} w = w s$ and $⟨ w λ_{∙}, β^{\lor} ⟩ = - ⟨ λ_{∙}, α_{s}^{\lor} ⟩ \in Z_{> 0}$ . This is a one-step strong linkage, so [F7] gives a nonzero (hence injective) map $Δ (w s \cdot λ) \to Δ (w \cdot λ)$ by [F7]. Applying the exact functor $T$ and step 1.1 gives a map $Δ (w s \cdot μ) \to Δ (w \cdot μ)$ ; now $w s \cdot μ = w \cdot (s \cdot μ) = w \cdot μ$ because $s \in J$ fixes $μ$ [F5], so this is an injective endomorphism of the finite-length module $Δ (w \cdot μ)$ , hence an isomorphism. If $N$ is the cokernel of $Δ (w s \cdot λ) \to Δ (w \cdot λ)$ , exactness of $T$ gives $T N = 0$ ; since $L (w \cdot λ)$ is a quotient of $N$ (the kernel of $Δ (w \cdot λ) ↠ L (w \cdot λ)$ contains $Δ (w s \cdot λ)$ because the latter has no composition factor $L (w \cdot λ)$ , its weights being strictly below), $T L (w \cdot λ) = 0$ .

2.2F1F6step 1.1algebra

Costandards (second clause of (1)). The evaluation pairing gives $D (E \otimes M) ≅ D (E) \otimes D (M)$ naturally, and $D (E) ≅ E$ for the finite-dimensional simple $E$ by [F6]. Hence $E \otimes \nabla (w \cdot λ) = E \otimes D Δ (w \cdot λ) ≅ D (E \otimes Δ (w \cdot λ))$ . Since $D$ preserves central-character blocks and is exact, it commutes with the inclusion and projection defining the translation functor, so $T \nabla (w \cdot λ) = {pr}_{χ_{μ}} (E \otimes \nabla (w \cdot λ)) ≅ D ({pr}_{χ_{μ}} (E \otimes Δ (w \cdot λ))) ≅ D Δ (w \cdot μ) = \nabla (w \cdot μ)$ by step 1.1.

3.1F6F7step 1.1step 2.2algebra

A translated simple is simple or zero. For every $x \in W$ , apply exact $T$ to $Δ (x \cdot λ) ↠ L (x \cdot λ) ↪ \nabla (x \cdot λ)$ . Steps 1.1 and 2.2 give a surjection $Δ (x \cdot μ) ↠ T L (x \cdot λ)$ followed by an injection into $\nabla (x \cdot μ)$ . If the intermediate object is nonzero, the composite is nonzero; the one-dimensional standard-costandard Hom of [F7] makes its image the canonical simple $L (x \cdot μ)$ . The injection identifies the intermediate object with that image. Thus $T L (x \cdot λ)$ is either zero or $L (x \cdot μ)$ , without any unstated Bruhat support assertion.

4.1F5step 1.1step 2.1step 3.1algebra

Minimal survival. Let $w \in W^{J}$ and translate a composition series of $Δ (w \cdot λ)$ . Its image is $Δ (w \cdot μ)$ , whose head $L (w \cdot μ)$ occurs as a composition factor. By step 3.1 that factor is the image of some $L (x \cdot λ)$ with $x \cdot μ = w \cdot μ$ . Step 2.1 kills every nonminimal $x$ , and [F5] says that the coset $w W_{J}$ has exactly one minimal representative, namely $w$ . Thus $T L (w \cdot λ)$ is nonzero and equals $L (w \cdot μ)$ by step 3.1. Together with step 2.1 this proves (2).

5.1step 1.1step 2.1step 1.2step 2.2step 3.1step 4.1∎

Part (1) is steps 1.1 and 2.2; part (2) is steps 2.1 and 3.1 together with the simplicity statement of step 4.1; part (3) is step 1.2.

Remarks

Upper closure. The upper closure in Dot-Weyl facets and single-wall translation data preserves strictly positive pairings and allows a negative pairing to become zero. Consequently $F_{w \cdot μ} \subseteq F_{w \cdot λ}^{+}$ holds exactly when $w Φ_{J}^{+} \subseteq Φ^{+}$ : zeros at the translated walls are allowed precisely when the corresponding regular pairings were negative. This is equivalent to $w α_{j} > 0$ for all $j \in J$ , hence to $w \in W^{J}$ by [F10]. The criterion therefore agrees with (2). In ${s l}_{2}$ , $F_{0}^{+} = (- 1, \infty)$ excludes the wall $- 1$ , whereas $F_{- 2}^{+} = (- \infty, - 1]$ includes it, in agreement with $T L (0) = 0$ and $T L (- 2) = L (- 1)$ . This is Chen Definition 3.9, Theorem 3.12 and Example 3.16; ordinary closure must not be substituted for upper closure.

Only the big antidominant projective $Ξ_{μ} = P (μ)$ carries every distinct singular standard exactly once; other singular projectives need not contain all standards, so no universal lower bound $(P : Δ) \geq 1$ is asserted for arbitrary projectives.

Depends on

Used by

Dependency tree · two levels

92 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

Lin Chen, lecture notes (Spring 2024), Lecture 9: standard filtrations, BGG reciprocity and translation functors (complete 7-page lecture) (standard reference, not scraped)
James E. Humphreys, Representations of Semisimple Lie Algebras in the BGG Category O, AMS Graduate Studies in Mathematics 94 (standard reference, not scraped)