ExampleConstruction: Literature-sourcedVerification: 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.

The projection from $B (\infty)$ to a highest weight crystal for ${s l}_{2}$

Example

Let $g = {s l}_{2}$ with $q_{1} = q$ as in Kashiwara strings in the three-dimensional ${s l}_{2}$ -module. Then $U_{q}^{-} = Q (q) [F_{1}]$ and the Kashiwara operators on the negative half act by ${\tilde{f}}_{1} (F_{1}^{(n)}) = F_{1}^{(n + 1)}$ and ${\tilde{e}}_{1} (F_{1}^{(n)}) = F_{1}^{(n - 1)}$ (with $F_{1}^{(- 1)} = 0$ ), so $L (\infty) = A_{0} -span {F_{1}^{(n)} : n \geq 0}, B (\infty) = {b_{n} : = F_{1}^{(n)} + q L (\infty) : n \geq 0} ≅ Z_{\geq 0},$ with ${\tilde{f}}_{1} b_{n} = b_{n + 1}$ , ${\tilde{e}}_{1} b_{n + 1} = b_{n}$ , ${\tilde{e}}_{1} b_{0} = 0$ , $wt (b_{n}) = - n α_{1} = - 2 n ω$ , $ε_{1} (b_{n}) = n$ , formal $φ_{1} (b_{n}) = - n$ and actual lowering length $ℓ_{1}^{-} (b_{n}) = \infty$ .

For $λ = m ω \in P^{+}$ ( $m \geq 0$ ) let $V (m ω) = L_{1} (m)$ have basis $v_{t} = F_{1}^{(t)} h_{m}$ ( $0 \leq t \leq m$ , $h_{m}$ the highest weight vector) as in Divided-power commutation and the simple $U_{q_{i}} ({s l}_{2})$ string modules(iii), and let $π_{m} = π_{m ω} : U_{q}^{-} \to V (m ω)$ , $P \mapsto P h_{m}$ . Then:

(a) $π_{m} (b_{n}) = 0$ for $n > m$ , and $π_{m}$ restricts to a bijection ${b_{0}, \dots, b_{m}} \tilde{\to} B (m ω) = {v_{0} + q L (m ω), \dots, v_{m} + q L (m ω)}$ ;

(b) ${\tilde{e}}_{1} π_{m} (b_{n}) = π_{m} ({\tilde{e}}_{1} b_{n})$ for $0 \leq n \leq m$ ; this raising compatibility is asserted only for surviving residues. It fails at the killed residue $b_{m + 1}$ , where the left side is $0$ and the right side is the nonzero bottom residue $π_{m} (b_{m})$ . Lowering compatibility holds for every $b_{n}$ , with both sides zero for $n \geq m$ .

(c) for $m \geq n$ the map $π_{m} : L (\infty)_{- n α_{1}} \to L (m ω)_{m ω - n α_{1}}$ is an isomorphism, and ${b \in B (\infty)_{- n α_{1}} : π_{m} (b) \neq 0} = {b_{n}}$ for $m \geq n$ ; these are the large-weight instances of Projection from $L (\infty)$ to $L (λ)$ and its compatibility with the Kashiwara operators.

Choice. The example's own rank-one computations are choice-free, but it cites the general projection lemma Projection from $L (\infty)$ to $L (λ)$ and its compatibility with the Kashiwara operators and The crystal basis $B (\infty)$ of the negative half, whose proofs inherit the axiom of choice from the grand loop; The Axiom of Choice is therefore declared as a dependency.

Facts & Assumptions

Given: The rank-one datum of ${s l}_{2}$ , the divided powers $F_{1}^{(n)}$ , the module $V (m ω) = L_{1} (m)$ with basis $v_{t} = F_{1}^{(t)} h_{m}$ , and the projection $π_{m}$ .

[F1]

$U_{q}^{-} = Q (q) [F_{1}]$ is the polynomial algebra on $F_{1}$ ; the skew derivation satisfies $e_{1}^{'} (F_{1}^{n}) = (1 + q^{- 2} + \dots + q^{- 2 (n - 1)}) F_{1}^{n - 1}$ with kernel the constants, so the divided monomials $F_{1}^{(n)}$ have the single string component $1$ at position $n$ ; hence $L (\infty) = A_{0} -span {F_{1}^{(n)} : n \geq 0}$ with ${\tilde{f}}_{1} (F_{1}^{(n)}) = F_{1}^{(n + 1)}$ and ${\tilde{e}}_{1} (F_{1}^{(n)}) = F_{1}^{(n - 1)}$ (Kashiwara's skew derivations $e_{i}^{'}$ and $e_{i}^{''}$ on the negative half, The $i$ -string decomposition of the negative half).

[F2]

$V (m ω) = L_{1} (m)$ has divided basis $v_{t} = F_{1}^{(t)} h_{m}$ with ${\tilde{e}}_{1} v_{t} = v_{t - 1}$ , ${\tilde{f}}_{1} v_{t} = v_{t + 1}$ for the string positions and endpoint zeros, and $L (m ω) = A_{0} v_{0} \oplus \dots \oplus A_{0} v_{m}$ with residue basis $B (m ω)$ (Divided-power commutation and the simple $U_{q_{i}} ({s l}_{2})$ string modules, part (iii), The Kashiwara operators ${\tilde{e}}_{i}$ and ${\tilde{f}}_{i}$ of an integrable module, The Kashiwara lattices $L (λ)$ and $L (\infty)$ and their generating sets).

[F3]

The projection lemma and the negative-half crystal theorem give, for general highest weights, the lattice projection, the surviving-residue bijection, the operator compatibilities on surviving residues, the residue basis of $L (\infty)$ and the infinite lowering length; their proofs inherit the axiom of choice, declared here (Projection from $L (\infty)$ to $L (λ)$ and its compatibility with the Kashiwara operators, The crystal basis $B (\infty)$ of the negative half, The Axiom of Choice).

[F4]

Invariants of a crystal: $ε_{1} (b) = \max {n : {\tilde{e}}_{1}^{n} b \neq 0}$ , $φ_{1} = ε_{1} + ⟨ h_{1}, w t ⟩$ formally on the negative half, $ℓ_{1}^{-} = \infty$ (The crystal graph, $ε_{i}$ , $φ_{i}$ and the weight function).

Verification

technique · direct

1.1F1F4

The negative-half crystal. By [F1], the divided monomials $F_{1}^{(n)}$ form a field basis of the polynomial algebra, and $L (\infty) = ⨁_{n \geq 0} A_{0} F_{1}^{(n)}$ . Reducing this free direct sum modulo $q$ shows that the residue classes $b_{n} = F_{1}^{(n)} + q L (\infty)$ ( $n \geq 0$ ) are nonzero and linearly independent modulo $q$ ; the operators act as ${\tilde{f}}_{1} b_{n} = b_{n + 1}$ and ${\tilde{e}}_{1} b_{n + 1} = b_{n}$ , ${\tilde{e}}_{1} b_{0} = 0$ . Hence $B (\infty) ≅ Z_{\geq 0}$ , with weights $w t (b_{n}) = - n α_{1} = - 2 n ω$ , $ε_{1} (b_{n}) = n$ , formal $φ_{1} (b_{n}) = n - 2 n = - n$ and $ℓ_{1}^{-} (b_{n}) = \infty$ .

2.1F2step 1.1

The module crystal. By [F2], $π_{m} (F_{1}^{(n)}) = v_{n}$ for $n \leq m$ and $0$ for $n > m$ ; so $π_{m} (b_{n}) = 0$ for $n > m$ and $π_{m} (b_{n}) = v_{n} + q L (m ω)$ for $0 \leq n \leq m$ . The classes $v_{0}, \dots, v_{m}$ are a $Q$ -basis of $L (m ω) / q L (m ω)$ , and the operator action on them is the string action, so the surviving residues map bijectively onto $B (m ω)$ ; this is (a).

3.1F2step 2.1

Raising compatibility and its failure. For $0 \leq n \leq m$ one has ${\tilde{e}}_{1} π_{m} (b_{n}) = {\tilde{e}}_{1} (v_{n} + q L (m ω)) = v_{n - 1}$ for $n \geq 1$ and $0$ for $n = 0$ , while $π_{m} ({\tilde{e}}_{1} b_{n}) = v_{n - 1}$ for $n \geq 1$ and $0$ for $n = 0$ ; hence the two sides agree for every surviving residue. At the killed residue $n = m + 1$ , the left side is ${\tilde{e}}_{1} π_{m} (b_{m + 1}) = {\tilde{e}}_{1} \cdot 0 = 0$ , while the right side is $π_{m} ({\tilde{e}}_{1} b_{m + 1}) = π_{m} (b_{m}) = v_{m} \neq 0$ modulo $q$ ; this is the stated boundary failure. Lowering: ${\tilde{f}}_{1} π_{m} (b_{n}) = v_{n + 1}$ for $n < m$ and $0$ for $n \geq m$ , while $π_{m} ({\tilde{f}}_{1} b_{n}) = v_{n + 1}$ for $n < m$ and $0$ for $n \geq m$ , so both sides agree for every $n$ .

4.1F2F3step 2.1

Isomorphism in fixed degree. In root degree $- n α_{1}$ the free $A_{0}$ -module $L (\infty)_{- n α_{1}}$ is the one-dimensional span of $F_{1}^{(n)}$ with residue $b_{n}$ , and $L (m ω)_{m ω - n α_{1}}$ is the one-dimensional span of $v_{n}$ with residue $v_{n} + q L (m ω)$ for $m \geq n$ ; the map $π_{m}$ sends $F_{1}^{(n)}$ to $v_{n}$ , an isomorphism on these one-dimensional free modules, and its surviving-residue set is ${b_{n}}$ when $m \geq n$ and empty otherwise. Together with step 3.1 this is the large-weight instance of the projection lemma.

5.1F3∎

Choice. The computations of steps 1.1 through 4.1 use only explicit monomials, divided powers and one-dimensional free modules, so they are choice-free; the axiom of choice is declared because the cited general suppliers [F3] inherit it from the grand loop.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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

Masaki Kashiwara, On crystal bases of the q-analogue of universal enveloping algebras, Duke Math. J. 63 (1991), no. 2, 465-516 (standard reference, not scraped)
Kyeonghoon Jeong, Seok-Jin Kang and Masaki Kashiwara, Crystal Bases for Quantum Generalized Kac-Moody Algebras, arXiv:math/0305390 (standard reference, not scraped)
Richard Borcherds, Mark Haiman, Theo Johnson-Freyd, Nicolai Reshetikhin and Vera Serganova, Berkeley Lectures on Lie Groups and Quantum Groups (book-length lecture notes, last updated 18 January 2024) (standard reference, not scraped)

The projection from B(∞)B(∞) to a highest weight crystal for sl2sl2​