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.

Kashiwara strings in the three-dimensional ${s l}_{2}$ -module

Example

Let $g = {s l}_{2}$ , so $I = {1}$ , $a_{11} = 2$ , $d_{1} = 1$ , $q_{1} = q$ , $P = Z ω$ with $⟨ h_{1}, ω ⟩ = 1$ and $α_{1} = 2 ω$ . Let $V = L_{1} (2)$ be the three-dimensional simple $U_{q} ({s l}_{2})$ -module of Divided-power commutation and the simple $U_{q_{i}} ({s l}_{2})$ string modules(iii), with highest weight vector $v_{2} = w_{2}$ of weight $2 ω$ , and put $v_{1} : = F_{1} v_{2}$ and $v_{0} : = F_{1}^{(2)} v_{2} = \frac{1}{[2]_{1}} F_{1}^{2} v_{2}$ ; then $(v_{2}, v_{1}, v_{0})$ is a $Q (q)$ -basis of $V$ with weights $2 ω, 0, - 2 ω$ , and $F_{1} v_{2} = v_{1}$ , $F_{1} v_{1} = [2]_{1} v_{0}$ , $F_{1} v_{0} = 0$ .

(a) String decompositions. $v_{2} = v_{2}$ (the $n = 0$ component is $v_{2}$ ), $v_{1} = F_{1}^{(1)} v_{2}$ (component $u_{1} = v_{2}$ ), $v_{0} = F_{1}^{(2)} v_{2}$ (component $u_{2} = v_{2}$ ). Hence ${\tilde{e}}_{1} v_{2} = 0, {\tilde{e}}_{1} v_{1} = v_{2}, {\tilde{e}}_{1} v_{0} = v_{1}, {\tilde{f}}_{1} v_{2} = v_{1}, {\tilde{f}}_{1} v_{1} = v_{0}, {\tilde{f}}_{1} v_{0} = 0.$ In particular $F_{1} v_{1} = [2]_{1} v_{0} \neq 0$ while ${\tilde{f}}_{1} v_{1} = v_{0}$ , and $F_{1} v_{0} = 0$ while ${\tilde{f}}_{1} v_{0} = 0$ : the Kashiwara operator ${\tilde{f}}_{1}$ agrees with $F_{1}$ on $Ker E_{1} = Q (q) v_{2}$ but not on the interior of the string, and ${\tilde{e}}_{1}$ agrees with $E_{1}$ on lowest weight vectors.

(b) Crystal. $L (2 ω) = A_{0} v_{2} \oplus A_{0} v_{1} \oplus A_{0} v_{0}$ is a crystal lattice of $V$ , and $B (2 ω) = {b_{2}, b_{1}, b_{0}}$ with $b_{2} = v_{2} + q L (2 ω)$ , $b_{1} = v_{1} + q L (2 ω)$ , $b_{0} = v_{0} + q L (2 ω)$ is a crystal basis with crystal graph $b_{2} \overset{1}{\to} b_{1} \overset{1}{\to} b_{0}$ . The invariants are $wt (b_{2}) = 2 ω$ , $wt (b_{1}) = 0$ , $wt (b_{0}) = - 2 ω$ , $ε_{1} (b_{2}) = 0$ , $ε_{1} (b_{1}) = 1$ , $ε_{1} (b_{0}) = 2$ , $φ_{1} (b_{2}) = 2$ , $φ_{1} (b_{1}) = 1$ , $φ_{1} (b_{0}) = 0$ , and $φ_{1} (b) = ε_{1} (b) + ⟨ h_{1}, wt (b) ⟩$ holds for all three (for example $2 = 0 + ⟨ h_{1}, 2 ω ⟩$ and $0 = 2 + ⟨ h_{1}, - 2 ω ⟩$ ), in accordance with The crystal graph, $ε_{i}$ , $φ_{i}$ and the weight function.

(c) Partial inverses. ${\tilde{e}}_{1} {\tilde{f}}_{1} = {id}_{V} - p_{b o t}$ and ${\tilde{f}}_{1} {\tilde{e}}_{1} = {id}_{V} - p_{0}$ , where $p_{0}$ is the projection $v_{2} \mapsto v_{2}$ , $v_{1}, v_{0} \mapsto 0$ onto $Ker E_{1}$ ; evaluated at $v_{2}$ this shows the failure at the top of the string: ${\tilde{f}}_{1} {\tilde{e}}_{1} v_{2} = 0 \neq v_{2}$ . No choice principle is used. Here $p_{b o t}$ projects onto $Q (q) v_{0}$ , so ${\tilde{e}}_{1} {\tilde{f}}_{1} v_{0} = 0 \neq v_{0}$ fails at the bottom as well as ${\tilde{f}}_{1} {\tilde{e}}_{1} v_{2} = 0 \neq v_{2}$ fails at the top.

Facts & Assumptions

Given: The datum of ${s l}_{2}$ , the module $V = L_{1} (2)$ with basis $v_{2}, v_{1}, v_{0}$ and the operators of The Kashiwara operators ${\tilde{e}}_{i}$ and ${\tilde{f}}_{i}$ of an integrable module.

[F1]

In $V = L_{1} (2)$ use descending weight labels $v_{2}$ (highest), $v_{1} : = F_{1} v_{2}$ and $v_{0} : = F_{1}^{(2)} v_{2}$ . Then $K_{1} v_{2} = q^{2} v_{2}$ , $K_{1} v_{1} = v_{1}$ , $K_{1} v_{0} = q^{- 2} v_{0}$ ; $F_{1} v_{2} = v_{1}$ , $F_{1} v_{1} = [2]_{1} v_{0}$ , $F_{1} v_{0} = 0$ ; and $E_{1} v_{2} = 0$ , $E_{1} v_{1} = [2]_{1} v_{2}$ , $E_{1} v_{0} = v_{1}$ . These are the supplier's divided-string formulas with its position index $t$ replaced by $2 - t$ (Divided-power commutation and the simple $U_{q_{i}} ({s l}_{2})$ string modules, part (iii)).

[F2]

A vector $u \in M_{λ}$ has a unique admissible string decomposition $u = \sum_{n} F_{1}^{(n)} u_{n}$ with $u_{n} \in H_{λ + n α_{1}} = \ker E_{1} \cap M_{λ + n α_{1}}$ ; the operators act by ${\tilde{e}}_{1} (\sum_{n} F_{1}^{(n)} u_{n}) = \sum_{n \geq 1} F_{1}^{(n - 1)} u_{n}$ and ${\tilde{f}}_{1} (\sum_{n} F_{1}^{(n)} u_{n}) = \sum_{n \geq 0} F_{1}^{(n + 1)} u_{n}$ (Uniqueness of the $i$ -string decomposition of an integrable module, The Kashiwara operators ${\tilde{e}}_{i}$ and ${\tilde{f}}_{i}$ of an integrable module).

[F3]

$\dim V_{μ} = 1$ for $μ = 2 ω, 0, - 2 ω$ and $E_{1} v_{2} = 0$ , $F_{1} v_{2} = v_{1}$ , $F_{1} v_{1} = [2]_{1} v_{0}$ with $[2]_{1} = q + q^{- 1} \neq 0$ (Crystal lattices, crystal bases and their crystals, [F1], The Kashiwara lattices $L (λ)$ and $L (\infty)$ and their generating sets).

Verification

technique · direct

1.1F1F2F3

The string components. $V_{2 ω} = Q (q) v_{2}$ with $E_{1} v_{2} = 0$ , so the decomposition of $v_{2}$ is $v_{2} = F_{1}^{(0)} v_{2}$ with top component $v_{2} \in H_{2 ω}$ . Since $v_{1} = F_{1} v_{2} = F_{1}^{(1)} v_{2}$ and $V_{0} = Q (q) v_{1}$ , the decomposition of $v_{1}$ is $v_{1} = F_{1}^{(1)} v_{2}$ with top component $v_{2} \in H_{2 ω}$ ; likewise $v_{0} = F_{1}^{(2)} v_{2}$ is the decomposition of $v_{0}$ with top component $v_{2} \in H_{2 ω}$ .

2.1F1F2step 1.1

The six formulas. Reading the definitions off the decompositions of step 1.1: ${\tilde{e}}_{1} v_{2} = 0$ , ${\tilde{e}}_{1} v_{1} = F_{1}^{(0)} v_{2} = v_{2}$ , ${\tilde{e}}_{1} v_{0} = F_{1}^{(1)} v_{2} = v_{1}$ and ${\tilde{f}}_{1} v_{2} = F_{1}^{(1)} v_{2} = v_{1}$ , ${\tilde{f}}_{1} v_{1} = F_{1}^{(2)} v_{2} = v_{0}$ , ${\tilde{f}}_{1} v_{0} = F_{1}^{(3)} v_{2} = 0$ . In particular $F_{1} v_{1} = [2]_{1} v_{0}$ while ${\tilde{f}}_{1} v_{1} = v_{0}$ , and $E_{1} v_{0} = v_{1} = {\tilde{e}}_{1} v_{0}$ and $F_{1} v_{0} = 0 = {\tilde{f}}_{1} v_{0}$ show the bottom agreements; the interior difference is exactly the factor $[2]_{1} \neq 1$ .

3.1F1F3step 2.1

Lattice and residue basis. Since $v_{2}, v_{1}, v_{0}$ have distinct weights, $L (2 ω) = A_{0} v_{2} \oplus A_{0} v_{1} \oplus A_{0} v_{0}$ and it generates $V$ over $Q (q)$ ; step 2.1 shows that ${\tilde{e}}_{1}$ and ${\tilde{f}}_{1}$ preserve it, so it is a crystal lattice. The classes $b_{2}, b_{1}, b_{0}$ of the three basis vectors are $Q$ -independent in $L / q L$ because $L$ is free with those basis vectors and the crystal-limit map is an isomorphism, so they form a $Q$ -basis; the operator action of step 2.1 lies in ${b_{2}, b_{1}, b_{0}} \cup {0}$ , and the only nonzero arrows are $b_{2} \to b_{1}$ and $b_{1} \to b_{0}$ , whose inverses under ${\tilde{e}}_{1}$ hold, giving the partial-inverse axiom.

4.1step 3.1algebra

The invariants. From the chain $b_{2} \to b_{1} \to b_{0}$ the values $ε_{1} (b_{2}) = 0$ , $ε_{1} (b_{1}) = 1$ , $ε_{1} (b_{0}) = 2$ and $φ_{1} (b_{2}) = 2$ , $φ_{1} (b_{1}) = 1$ , $φ_{1} (b_{0}) = 0$ are immediate, and the weights are those of step 3.1; the equalities $φ_{1} (b) = ε_{1} (b) + ⟨ h_{1}, w t (b) ⟩$ read $2 = 0 + 2$ , $1 = 1 + 0$ , $0 = 2 - 2$ .

5.1step 2.1∎

Partial inverses. Evaluating step 2.1 gives ${\tilde{e}}_{1} {\tilde{f}}_{1} v_{2} = v_{2}$ , ${\tilde{e}}_{1} {\tilde{f}}_{1} v_{1} = v_{1}$ , ${\tilde{e}}_{1} {\tilde{f}}_{1} v_{0} = 0 = v_{0} - p_{b o t} v_{0}$ , and ${\tilde{f}}_{1} {\tilde{e}}_{1} v_{2} = 0 = v_{2} - p_{0} v_{2}$ , ${\tilde{f}}_{1} {\tilde{e}}_{1} v_{1} = v_{1} = v_{1} - p_{0} v_{1}$ , ${\tilde{f}}_{1} {\tilde{e}}_{1} v_{0} = v_{0} = v_{0} - p_{0} v_{0}$ ; by linearity these are the stated identities, and no choice is used because everything is computed on the three displayed vectors.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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)

Kashiwara strings in the three-dimensional sl2sl2​-module