ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge 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.

Translation between two regular integral blocks

Example

For $g = {s l}_{2}$ , label $W ≅ S_{2}$ by ${123, 213}$ (the subgroup of $S_{3}$ fixing $3$ ), and write a weight as its coordinate $l = λ (h)$ , so $ρ = 1$ , the dot action is $s \cdot l = - l - 2$ , and the dominant regular integral weights are $l = n \in Z_{\geq 0}$ with regular integral block $C_{n}$ on the labels ${n, - n - 2}$ . Then for $n = 0$ and $n = 1$ the two blocks $C_{0}$ and $C_{1}$ have identical multiplicity data: with $e = 123$ and $s = 213$ , $(P (e \cdot l) : Δ (e \cdot l)) = 1, (P (s \cdot l) : Δ (e \cdot l)) = 1, (P (s \cdot l) : Δ (s \cdot l)) = 1, (P (e \cdot l) : Δ (s \cdot l)) = 0,$ $[M (e \cdot l) : L (e \cdot l)] = [M (e \cdot l) : L (s \cdot l)] = [M (s \cdot l) : L (s \cdot l)] = 1, [M (s \cdot l) : L (e \cdot l)] = 0,$ for $l = 0$ and $l = 1$ , matching the Kazhdan–Lusztig values $P_{123, 123} = P_{123, 213} = P_{213, 213} = 1$ and $P_{213, 123} = 0$ of $S_{2}$ . In each block $P (e \cdot l) = Δ (e \cdot l)$ is the projective cover of $L (e \cdot l)$ and $P (s \cdot l)$ fits into the nonsplit sequence $0 \to Δ (e \cdot l) \to P (s \cdot l) \to Δ (s \cdot l) \to 0$ , while $Δ (s \cdot l) = L (s \cdot l)$ ; the character formula gives $c h L (e \cdot l) = c h M (e \cdot l) - c h M (s \cdot l)$ and $c h L (s \cdot l) = c h M (s \cdot l)$ , and for the dominant label $e$ the first identity telescopes to the Weyl character $e^{n} + e^{n - 2} + \dots + e^{- n}$ of the $(n + 1)$ -dimensional simple module. The actual equivalence $F = {pr}_{χ_{1}} (L (1) \otimes -) {incl}_{χ_{0}}$ , with inverse $G = {pr}_{χ_{0}} (L (1)^{*} \otimes -) {incl}_{χ_{1}}$ , sends the sequence $0 \to M_{- 2} \to M_{0} \to L_{0} \to 0$ of the principal block to $0 \to M_{- 3} \to M_{1} \to L_{1} \to 0$ .

Facts & Assumptions

Given: The Axiom of Choice (inherited from the projectivity and transport suppliers below), the Lie algebra ${s l}_{2}$ with Cartan element $h$ , positive root $α$ and $ρ = α / 2$ , weights written as coordinates $l = λ (h)$ ; for $n \in Z_{\geq 0}$ the block $C_{n}$ on the dot orbit ${n, - n - 2}$ , with labels $e = 123$ and $s = 213$ .

[F1]

Block conventions (The regular integral dot-orbit labelling convention, Central characters are dot-Weyl orbits): $Δ (w \cdot l) = M (w \cdot l)$ , $L (w \cdot l)$ , $P (w \cdot l)$ labelled by $W$ , the central character depends only on the dot orbit, and a Verma is killed by the projection to a block exactly when its weight is outside the orbit of that block.

[F2]

Verma modules and the PBW model (Verma modules, The PBW model of a Verma module): $M (l)$ is generated by the highest weight vector $v_{l}$ , and multiplication $u \mapsto u v_{l}$ identifies $U (n^{-})$ with $M (l)$ ; in particular the $v_{k} : = f^{k} v_{l}$ ( $k \geq 0$ ) form a basis and generate $M (l)$ .

[F3]

Antidominant Vermas are simple (Antidominant regular Verma modules are simple): if $⟨ l + ρ, α^{\lor} ⟩ < 0$ then $M (l)$ is simple.

[F4]

The maximal-label projectivity (A maximal-label Verma is projective in its truncation): in a finite downward-closed ideal of a linkage class, the Verma at a maximal weight is projective.

[F5]

Projective covers (Category O has enough projectives): every simple admits a projective cover, unique up to isomorphism and indecomposable, and every object is a quotient of a finite direct sum of covers.

[F6]

BGG reciprocity (BGG reciprocity): $(P (l) : Δ (l^{'})) = [M (l^{'}) : L (l)]$ for all weights, the left side being the Verma-flag multiplicity.

[F7]

Factors of a Verma (Jordan-Holder factors of Verma modules dominate the head (BGG 8.12)): if $L (l^{'})$ occurs in a composition series of $M (w \cdot l)$ for dominant integral $l$ , then $l^{'} = u \cdot l$ with $u \geq w$ , and $L (w \cdot l)$ occurs exactly once.

[F8]

Translation functors and their transport (Translation functors by tensoring and projection, Translation identifies the regular integral blocks): for dominant regular integral weights the functors $T_{λ}^{μ} = {pr}_{χ_{μ}} (E \otimes -) {incl}_{χ_{λ}}$ and $T_{μ}^{λ} = {pr}_{χ_{λ}} (E^{*} \otimes -) {incl}_{χ_{μ}}$ (with $E$ the finite-dimensional simple whose highest weight is the unique dominant member of $W (μ - λ)$ ) are inverse exact equivalences carrying $Δ (w \cdot λ) \mapsto Δ (w \cdot μ)$ , $L (w \cdot λ) \mapsto L (w \cdot μ)$ and $P (w \cdot λ) \mapsto P (w \cdot μ)$ .

[F9]

Finite-dimensional tensoring preserves Verma flags (Finite-dimensional tensoring preserves Verma flags): $E \otimes Δ (μ^{'})$ has a finite Verma flag with factors $Δ (μ^{'} + η)$ , the factor occurring $\dim E_{η}$ times.

[F10]

Kazhdan–Lusztig data (Kazhdan–Lusztig polynomials in the classical $q$ -normalization, The Kazhdan–Lusztig character formula in regular integral category O): for $S_{2}$ the three comparable-pair polynomials are $P_{e, e} = P_{e, s} = P_{s, s} = 1$ and $P_{s, e} = 0$ ; hence the inverse coefficient matrix at $v = 1$ is $(q_{x, w}^{'} (1)) = (\begin{array}{cc} 1 & - 1 \\ 0 & 1 \end{array})$ , and in each block $c h L (e \cdot l) = c h M (e \cdot l) - c h M (s \cdot l)$ , $c h L (s \cdot l) = c h M (s \cdot l)$ .

[F11]

The Weyl character formula (The Weyl character formula): for dominant integral $l$ the finite-dimensional simple $L (l)$ has character $A (l + ρ) A (ρ)^{- 1}$ , which for ${s l}_{2}$ is the finite geometric sum $e^{l} + e^{l - 2} + \dots + e^{- l}$ .

Verification

technique · direct

1.1F1algebra

The two blocks. With $ρ = 1$ the dot action on coordinates is $s \cdot l = s (l + 1) - 1 = - l - 2$ , so the orbit of $n$ is ${n, - n - 2}$ ; a weight $l$ is dominant regular integral exactly when $l \in Z_{\geq 0}$ , and then $- n - 2 < n$ in the dominance order. Hence $C_{n}$ is a regular integral block with the two labels $e = 123 \mapsto n$ and $s = 213 \mapsto - n - 2$ ; for $n = 0$ and $n = 1$ the abstract labelled data are the same, which is what makes the two blocks directly comparable.

1.2F2algebra

The PBW computation. Fix $n \geq 0$ and put $v_{k} : = f^{k} v_{n}$ , a basis of $M (n)$ by [F2]; the highest weight vector $v_{0}$ generates $M (n)$ and spans the $n$ -weight space, which is one-dimensional. From the ${s l}_{2}$ relations $[h, f] = - 2 f$ , $[e, f] = h$ one computes $h \cdot v_{k} = (n - 2 k) v_{k}$ , $f \cdot v_{k} = v_{k + 1}$ , and, by induction on $k$ from $e \cdot v_{0} = 0$ , $e \cdot v_{k} = k (n - k + 1) v_{k - 1}$ . If $M (n) = A \oplus B$ with $v_{0} = a + b$ , then $a$ and $b$ lie in the one-dimensional weight space $M (n)_{n} = C v_{0}$ ; if $b \neq 0$ then $b$ is a nonzero multiple of $v_{0}$ , so $v_{0} \in B$ and $M (n) = U (g) v_{0} \subseteq B$ , while if $b = 0$ then $v_{0} = a \in A$ and $M (n) \subseteq A$ ; either way one of the summands is zero. So $M (n)$ is indecomposable.

2.1F2F3step 1.2

The submodule $W$ . Let $W : = span {v_{k} : k \geq n + 1}$ . By step 1.2 it is stable under $f$ and $h$ ; and $e \cdot v_{n + 1} = (n + 1) (n - (n + 1) + 1) v_{n} = 0$ , while for $k \geq n + 2$ one has $e \cdot v_{k} = k (n - k + 1) v_{k - 1}$ with $k - 1 \geq n + 1$ , so $e$ maps $W$ into $W$ . Hence $W$ is a nonzero submodule. Its highest weight vector $v_{n + 1}$ has weight $n - 2 (n + 1) = - n - 2$ and is killed by $e$ ; the linear map $M (- n - 2) \to W$ sending the basis element $f^{k} v_{- n - 2}$ of the PBW model of $M (- n - 2)$ to $v_{n + 1 + k}$ is a $g$ -module isomorphism by the action formulas of step 1.2 (both sides have the same $h$ -eigenvalues and the same $e, f$ -action). Since $- n - 2 + 1 = - n - 1 < 0$ , the Verma $M (- n - 2)$ is simple by [F3], so $W ≅ M (- n - 2) = L (- n - 2)$ .

2.2F10F11step 1.2

Characters. By step 1.2 the weight multiplicities of $M (n)$ are $1$ in each weight $n - 2 k$ , $k \geq 0$ , so $c h M (n) = \sum_{k \geq 0} e^{n - 2 k}$ and $c h M (- n - 2) = \sum_{k \geq 0} e^{- n - 2 - 2 k}$ ; the character formula of [F10] therefore gives $c h L (n) = c h M (n) - c h M (- n - 2) = \sum_{k = 0}^{n} e^{n - 2 k} = e^{n} + e^{n - 2} + \dots + e^{- n}$ , in agreement with the Weyl character of the finite-dimensional simple $L (n)$ by [F11], and $c h L (- n - 2) = c h M (- n - 2)$ .

3.1F2F7step 1.2step 2.1

The quotient is $L (n)$ . By step 1.2 the images of $v_{0}, \dots, v_{n}$ form a basis of $Q : = M (n) / W$ , with weights $n, n - 2, \dots, - n$ , each occurring once; in particular $Q$ is finite-dimensional and nonzero with a one-dimensional $n$ -weight space. By [F7] every composition factor of $M (n)$ is $L (n)$ or $L (- n - 2)$ , and $L (n)$ occurs exactly once. The simple $L (- n - 2) = M (- n - 2)$ is infinite-dimensional, because the PBW basis ${f^{k} v_{- n - 2} : k \geq 0}$ of $M (- n - 2)$ is infinite by [F2]; hence no composition factor of the finite-dimensional module $Q$ is $L (- n - 2)$ , and the only remaining factor is $L (n)$ , occurring once. Therefore $Q ≅ L (n)$ , and $M (n)$ has exactly the two composition factors $L (n)$ and $L (- n - 2)$ , each once.

4.1F4F5F6step 1.2step 2.1step 3.1

The projective structure. The block $C_{n} = {n, - n - 2}$ is a finite downward-closed ideal with maximum $n$ ; by [F4] the Verma $Δ (n) = M (n)$ is projective in the block. Every submodule is a sum of weight spaces: polynomial interpolation in $h$ extracts the finitely many weight components of any vector. If a submodule contains $v_{k}$ for $0 \leq k \leq n$ , then $e^{k} v_{k}$ is a nonzero multiple of $v_{0}$ by step 1.2, and the submodule is all of $M (n)$ . Thus every proper submodule lies in $W = span {v_{k} : k \geq n + 1}$ , whose quotient is $L (n)$ by step 3.1; $W$ , rather than all lower weight spaces, is the unique maximal submodule. A submodule mapping onto $L (n)$ contains a weight- $n$ vector and hence $v_{0}$ , so $M (n) ↠ L (n)$ is essential. By uniqueness of projective covers [F5], $P (n) = P (e \cdot l)$ is isomorphic to $Δ (n)$ and is the projective cover of $L (n)$ . For the other label apply BGG reciprocity [F6]: $(P (- n - 2) : Δ (n)) = [M (n) : L (- n - 2)] = 1$ and $(P (- n - 2) : Δ (- n - 2)) = [M (- n - 2) : L (- n - 2)] = 1$ by steps 2.1 and 3.1, while all other flag multiplicities vanish since the block has only these two labels. So $P (s \cdot l) = P (- n - 2)$ has a flag with the two factors $Δ (n)$ and $Δ (- n - 2)$ , each once. If its quotient factor were $Δ (n)$ , projectivity of $Δ (n)$ would split that two-step flag, contradicting the indecomposability of $P (- n - 2)$ in [F5]. Hence the submodule factor is $Δ (n)$ and the quotient factor is $Δ (- n - 2)$ , giving the short exact sequence $0 \to Δ (n) \to P (- n - 2) \to Δ (- n - 2) \to 0$ . This sequence is nonsplit: a splitting would exhibit $P (- n - 2) ≅ Δ (n) \oplus Δ (- n - 2)$ as a direct sum of two nonzero objects, contradicting the indecomposability of projective covers in [F5]. Finally $Δ (- n - 2) = M (- n - 2) = L (- n - 2)$ by step 2.1.

5.1F10step 2.1step 3.1step 4.1

The multiplicity data for $n = 0, 1$ . The four flag multiplicities of the Example are those just computed and do not depend on $n$ : $(P (e \cdot l) : Δ (e \cdot l)) = 1$ , $(P (s \cdot l) : Δ (e \cdot l)) = 1$ , $(P (s \cdot l) : Δ (s \cdot l)) = 1$ , $(P (e \cdot l) : Δ (s \cdot l)) = 0$ (the last because $P (n) ≅ Δ (n)$ has only the factor $Δ (n)$ ). The composition multiplicities are likewise independent of $n$ : $[M (n) : L (n)] = [M (n) : L (- n - 2)] = [M (- n - 2) : L (- n - 2)] = 1$ and $[M (- n - 2) : L (n)] = 0$ by steps 2.1 and 3.1, since $M (- n - 2) = L (- n - 2)$ is simple and its highest weight differs from $n$ . For $n = 0, 1$ these are exactly the displayed matrices; they match $P_{e, e} = P_{e, s} = P_{s, s} = 1$ , $P_{s, e} = 0$ by [F10], as asserted by the multiplicity theorem on the A page.

5.2F1F5F8F9step 1.2step 2.1step 3.1step 4.1

The transported sequence. Take the principal block $n = 0$ and the target $n = 1$ , both dominant regular integral, and note that for $λ = 0$ , $μ = 1$ the difference $μ - λ = 1$ has dominant member $ν = 1$ ; here $E = L (1)$ is the two-dimensional simple with weights $+ 1, - 1$ , each once, and $E^{*} ≅ E$ . By [F9] the tensor $E \otimes M (0)$ has Verma flag factors $M (1)$ and $M (- 1)$ , and $E \otimes M (- 2)$ has factors $M (- 1)$ and $M (- 3)$ . The projections to the blocks $χ_{1}$ and $χ_{0}$ keep exactly the factors lying in the respective dot orbits ${1, - 3}$ and ${0, - 2}$ by [F1]: hence $F (M (0)) = {pr}_{χ_{1}} (E \otimes M (0)) ≅ M (1)$ and $F (M (- 2)) ≅ M (- 3)$ , while $G (M (1)) = {pr}_{χ_{0}} (E \otimes M (1)) ≅ M (0)$ from the factors $M (2), M (0)$ and $G (M (- 3)) ≅ M (- 2)$ from the factors $M (- 2), M (- 4)$ . By the transport theorem [F8] $F (L (0)) = L (1)$ , $G (L (1)) = L (0)$ , $F (P (0)) = P (1)$ , $F (P (- 2)) = P (- 3)$ and conversely. Since $F$ is exact, applying it to the nonsplit sequence $0 \to M (- 2) \to M (0) \to L (0) \to 0$ of the principal block produces the exact sequence $0 \to F (M (- 2)) \to F (M (0)) \to F (L (0)) \to 0$ , that is $0 \to M (- 3) \to M (1) \to L (1) \to 0$ in the block $C_{1}$ ; it is nonsplit because an exact inverse equivalence $G$ would carry a splitting of its image back to a splitting of the original sequence. The original middle module is $M (0) = P (0)$ , not $P (- 2)$ ; it is indecomposable by step 1.2, and its submodule $M (- 2)$ and quotient $L (0)$ are both nonzero by steps 2.1 and 3.1, so such a splitting is impossible.

6.1step 4.1step 5.1step 2.2step 5.2∎

The claims of the Example are therefore all verified: the two blocks $C_{0}$ and $C_{1}$ share the displayed multiplicity matrices (steps 4.1 and 5.1), the projective cover $P (e \cdot l)$ equals $Δ (e \cdot l)$ and $P (s \cdot l)$ carries the nonsplit two-step sequence with $Δ (s \cdot l) = L (s \cdot l)$ (step 4.1), the character identities telescope to the Weyl character of the $(n + 1)$ -dimensional simple (step 2.2), and the actual inverse equivalences $F$ and $G$ transport the principal-block Verma sequence to $0 \to M_{- 3} \to M_{1} \to L_{1} \to 0$ (step 5.2). The two blocks use different weight series; only the labels and the combinatorial data agree.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

94 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)
Lin Chen, lecture notes (Spring 2024), Lecture 9: standard filtrations, BGG reciprocity and translation functors (complete 7-page lecture) (standard reference, not scraped)