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

The tensor crystal $B (1) \otimes B (1)$ for ${s l}_{2}$

Example

Let $g = {s l}_{2}$ , $I = {1}$ , with fundamental weight $λ_{1}$ and simple root $α_{1} = 2 λ_{1}$ . Let $V (1)$ be the two-dimensional simple integrable module with highest vector $v_{0}$ and crystal $B (1) = {v_{0}, v_{1}}$ , where $v_{1} = F_{1} v_{0}$ ; the $i$ -string is $v_{0} \overset{1}{\to} v_{1}$ with $w t (v_{0}) = λ_{1}$ , $w t (v_{1}) = - λ_{1}$ and $ε_{1} (v_{0}) = 0, φ_{1} (v_{0}) = 1, ε_{1} (v_{1}) = 1, φ_{1} (v_{1}) = 0$ (JKK Example 5.1(a) with $m = 1$ ).

Compute the tensor crystal $B (1) \otimes B (1)$ of The tensor product crystal $B_{1} \otimes B_{2}$ and its two-case convention with the two-case rule of The crystal basis of a tensor product and the two-case operator rule. Writing the four vertices as $v_{j} \otimes v_{k}$ with $j, k \in {0, 1}$ , the rule gives

${\tilde{f}}_{1} (v_{j} \otimes v_{k}) = {\begin{cases} v_{j + 1} \otimes v_{k}, & 1 - j > k, \\ v_{j} \otimes v_{k + 1}, & 1 - j \leq k, \end{cases} {\tilde{e}}_{1} (v_{j} \otimes v_{k}) = {\begin{cases} v_{j - 1} \otimes v_{k}, & 1 - j \geq k, \\ v_{j} \otimes v_{k - 1}, & 1 - j < k . \end{cases}$

Consequently: $v_{0} \otimes v_{0}$ is the unique highest vertex of weight $2 λ_{1}$ and generates the chain $v_{0} \otimes v_{0} \to v_{1} \otimes v_{0} \to v_{1} \otimes v_{1}$ ; the remaining vertex $v_{0} \otimes v_{1}$ has weight $0$ , is killed by ${\tilde{e}}_{1}$ and by ${\tilde{f}}_{1}$ , and forms a one-element component; and $ε_{1}, φ_{1}$ of the four vertices are $(0, 2), (1, 1), (2, 0), (0, 0)$ at $(0, 0), (1, 0), (1, 1), (0, 1)$ respectively. Hence $B (1) \otimes B (1) = B (2) ⊔ B (0)$ , matching the classical decomposition $V (1) \otimes V (1) = V (2) \oplus V (0)$ of dimensions $4 = 3 + 1$ ; here $B (2)$ is the three-element $1$ -chain of weights $2 λ_{1}, 0, - 2 λ_{1}$ and $B (0)$ the one-element crystal of weight $0$ .

Facts & Assumptions

Given: $g = {s l}_{2}$ with $I = {1}$ , $α_{1} = 2 λ_{1}$ , the two-element crystal $B (1) = {v_{0}, v_{1}}$ with the single arrow $v_{0} \overset{1}{\to} v_{1}$ , and the tensor product crystal $B (1) \otimes B (1)$ of The tensor product crystal $B_{1} \otimes B_{2}$ and its two-case convention with the operators of The crystal basis of a tensor product and the two-case operator rule.

[F1]

The rank-one crystal of dimension two (Divided-power commutation and the simple $U_{q_{i}} ({s l}_{2})$ string modules, with Quantum integers, factorials, Gaussian binomials and divided powers at $q_{i}$ ): the module $L_{1} (1)$ has basis $v_{0}, v_{1} = F_{1} v_{0}$ , with $K_{1} v_{t} = q_{1}^{1 - 2 t} v_{t}$ , so $w t (v_{0}) = λ_{1}$ , $w t (v_{1}) = - λ_{1}$ ; the crystal basis is ${v_{0}, v_{1}}$ and the operators shift the string, giving the arrow $v_{0} \overset{1}{\to} v_{1}$ with $ε_{1} (v_{0}) = 0$ , $φ_{1} (v_{0}) = 1$ , $ε_{1} (v_{1}) = 1$ , $φ_{1} (v_{1}) = 0$ .

[F2]

The two-case tensor rule (The tensor product crystal $B_{1} \otimes B_{2}$ and its two-case convention, The crystal basis of a tensor product and the two-case operator rule): ${\tilde{f}}_{1}$ acts on the first factor if and only if $φ_{1} (b_{1}) > ε_{1} (b_{2})$ and on the second otherwise, ${\tilde{e}}_{1}$ acts on the first factor if and only if $φ_{1} (b_{1}) \geq ε_{1} (b_{2})$ and on the second otherwise, with value $0$ when the chosen factor reaches the string end.

[F3]

The max formulas (The weight, $ε_{i}$ and $φ_{i}$ formulas for the tensor product crystal): $ε_{1} (b_{1} \otimes b_{2}) = \max (ε_{1} (b_{1}), ε_{1} (b_{2}) - ⟨ h_{1}, w t (b_{1}) ⟩)$ and $φ_{1} (b_{1} \otimes b_{2}) = \max (φ_{1} (b_{1}) + ⟨ h_{1}, w t (b_{2}) ⟩, φ_{1} (b_{2}))$ .

[F4]

Crystal graph conventions (The crystal graph, $ε_{i}$ , $φ_{i}$ and the weight function): each finite $i$ -string has $ε_{i} + φ_{i} + 1$ vertices, $φ_{i} (b) - ε_{i} (b) = ⟨ h_{i}, w t (b) ⟩$ , and $K_{1} v_{0} = q_{1} v_{0}$ gives $⟨ h_{1}, w t (v_{0}) ⟩ = 1$ , $⟨ h_{1}, w t (v_{1}) ⟩ = - 1$ .

[F5]

The canonical rank-one crystals (Divided-power commutation and the simple $U_{q_{i}} ({s l}_{2})$ string modules, The Kashiwara lattices $L (λ)$ and $L (\infty)$ and their generating sets, The Kashiwara operators ${\tilde{e}}_{i}$ and ${\tilde{f}}_{i}$ of an integrable module): $B (2)$ is the three-element one-colour chain of weights $2 λ_{1}, 0, - 2 λ_{1}$ , and $B (0)$ the one-element crystal of weight $0$ killed by both operators.

Verification

technique · direct

1.1givenF1

Read off the four residues and the values $ε_{1} (v_{0}) = 0, φ_{1} (v_{0}) = 1, ε_{1} (v_{1}) = 1, φ_{1} (v_{1}) = 0$ from the two-element chain $v_{0} \overset{1}{\to} v_{1}$ , which is the $m = 1$ case of the rank-one crystal basis of [F1].

2.1step 1.1F2

Apply the rule [F2] vertex by vertex: ${\tilde{f}}_{1} (v_{0} \otimes v_{0}) = v_{1} \otimes v_{0}$ since $1 > 0$ ; ${\tilde{f}}_{1} (v_{1} \otimes v_{0}) = v_{1} \otimes v_{1}$ since $0 \leq 0$ ; ${\tilde{f}}_{1} (v_{1} \otimes v_{1}) = 0$ since $0 \leq 1$ selects the second factor and ${\tilde{f}}_{1} v_{1} = 0$ ; ${\tilde{f}}_{1} (v_{0} \otimes v_{1}) = 0$ since $1 \leq 1$ selects the second factor and ${\tilde{f}}_{1} v_{1} = 0$ . This gives the two components stated, with the highest vertices $v_{0} \otimes v_{0}$ and $v_{0} \otimes v_{1}$ .

3.1step 2.1step 1.1F3F4

Compute $ε_{1}, φ_{1}$ by iterating the same rule and compare with the max formulas [F3], using $⟨ h_{1}, w t (v_{0}) ⟩ = 1$ and $⟨ h_{1}, w t (v_{1}) ⟩ = - 1$ from [F4]: at $v_{0} \otimes v_{0}$ , $ε_{1} = \max (0, 0 - 1) = 0$ and $φ_{1} = \max (φ_{1} (v_{0}) + ⟨ h_{1}, w t (v_{0}) ⟩, φ_{1} (v_{0})) = \max (1 + 1, 1) = 2$ ; at $v_{1} \otimes v_{0}$ , $ε_{1} = \max (1, 0 - (- 1)) = 1$ and $φ_{1} = \max (0 + 1, 1) = 1$ ; at $v_{1} \otimes v_{1}$ , $ε_{1} = \max (1, 1 - (- 1)) = 2$ and $φ_{1} = \max (0 - 1, 0) = 0$ ; at $v_{0} \otimes v_{1}$ , $ε_{1} = \max (0, 1 - 1) = 0$ and $φ_{1} = \max (1 - 1, 0) = 0$ .

4.1step 3.1step 2.1F4F5

Identify the components. The three-element chain has top weight $2 λ_{1}$ , middle weight $0$ , bottom weight $- 2 λ_{1}$ and one colour; a connected crystal with a unique highest vertex of weight $2 λ_{1}$ and $ε_{1} + φ_{1} + 1 = 3$ vertices in its only string is the rank-one crystal $B (2)$ of [F5] (the $m = 2$ case of the same rank-one description). The remaining vertex is killed by both operators and has weight $0$ , so it is $B (0)$ . This identifies the two components without invoking the general uniqueness theorem, so the example is choice-free.

5.1step 4.1F1F2algebra∎

Cross-check the module decomposition directly. Put $z = q_{1}$ , $t = v_{0} \otimes v_{0}$ and $s = v_{0} \otimes v_{1} - z v_{1} \otimes v_{0}$ . The coproduct convention underlying [F2] and the rank-one action of [F1] give $E_{1} t = 0$ , $F_{1} t = v_{1} \otimes v_{0} + z v_{0} \otimes v_{1}$ , $F_{1}^{(2)} t = v_{1} \otimes v_{1}$ , and $E_{1} s = F_{1} s = 0$ , $K_{1} s = s$ . The two weight-zero vectors $F_{1} t, s$ are independent because their coefficient determinant is $1 + z^{2} \neq 0$ . Hence the three-dimensional cyclic string of $t$ and the trivial line of $s$ sum directly to the four-dimensional tensor module; [F1] identifies them as $V (2)$ and $V (0)$ . This gives $4 = 3 + 1$ , and the corresponding classical two-dimensional tensor square has the same dimensions and highest weights.

Depends on

Used by

Dual crystals reverse arrows and weights: two small computations Example

Dependency tree · two levels

27 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

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)
Mark Shimozono, Crystals for Dummies (lecture notes, 28 August 2005) (standard reference, not scraped)

The tensor crystal B(1)⊗B(1)B(1)⊗B(1) for sl2sl2​