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 crystal graph of the quantum symmetric square of the standard $A_{2}$ -module

Example

Use the type $A_{2}$ datum with $q_{1} = q_{2} = q$ , $α_{1} = 2 ω_{1} - ω_{2}$ , $α_{2} = - ω_{1} + 2 ω_{2}$ . Let $W$ have standard basis $e_{1}, e_{2}, e_{3}$ of labels $ω_{1}$ , $ω_{2} - ω_{1}$ , $- ω_{2}$ , with $E_{1} e_{2} = e_{1}$ , $F_{1} e_{1} = e_{2}$ , $E_{2} e_{3} = e_{2}$ , $F_{2} e_{2} = e_{3}$ and all other positive and negative actions zero. Use $Δ E = E \otimes K^{- 1} + 1 \otimes E$ , $Δ F = F \otimes 1 + K \otimes F$ . The quantum symmetric square is the highest submodule $V = U_{q} (e_{1} \otimes e_{1}) \subset W \otimes W$ , isomorphic to $V (2 ω_{1})$ , with six divided-normalized basis vectors $v_{11} = e_{1} \otimes e_{1}, v_{12} = e_{2} \otimes e_{1} + q e_{1} \otimes e_{2}, v_{22} = e_{2} \otimes e_{2},$ $v_{13} = e_{3} \otimes e_{1} + q e_{1} \otimes e_{3}, v_{23} = e_{3} \otimes e_{2} + q e_{2} \otimes e_{3}, v_{33} = e_{3} \otimes e_{3} .$ Their respective labels are $(2, 0), (0, 1), (- 2, 2), (1, - 1), (- 1, 0), (0, - 2)$ in the $ω$ -basis. Their spans specialize to the ordinary symmetric square at $q = 1$ .

The color- $1$ divided strings are $v_{11} \to v_{12} \to v_{22}$ , $v_{13} \to v_{23}$ and ${v_{33}}$ ; the color- $2$ strings are $v_{12} \to v_{13}$ , $v_{22} \to v_{23} \to v_{33}$ and ${v_{11}}$ . The $A_{0}$ -span of the six vectors is the recursively generated crystal lattice and their residue classes form its crystal basis, with precisely these six lowering edges. Their $(ε_{1}, φ_{1}, ε_{2}, φ_{2})$ are respectively $(0, 2, 0, 0)$ , $(1, 1, 0, 1)$ , $(2, 0, 0, 2)$ , $(0, 1, 1, 0)$ , $(1, 0, 1, 1)$ , $(0, 0, 2, 0)$ . All twelve $ε$ - $φ$ equalities $φ_{i} (b) = ε_{i} (b) + ⟨ h_{i}, w t (b) ⟩$ hold. No choice principle is used.

Facts & Assumptions

Given: The $A_{2}$ Cartan datum with $I = {1, 2}$ , $a_{i j} = 2$ for $i = j$ and $- 1$ otherwise, $d_{1} = d_{2} = 1$ , $q_{1} = q_{2} = q$ , fundamental labels $ω_{1}, ω_{2}$ with $⟨ h_{i}, ω_{j} ⟩ = δ_{i j}$ , and the tensor product $W \otimes W$ with the stated coproduct.

[F1]

The Drinfeld–Jimbo algebra of the datum has generators $E_{i}, F_{i}, K_{h}$ with the relations $K_{h} E_{i} K_{h}^{- 1} = q^{⟨ α_{i}, h ⟩} E_{i}$ , $K_{h} F_{i} K_{h}^{- 1} = q^{- ⟨ α_{i}, h ⟩} F_{i}$ and $E_{i} F_{j} - F_{j} E_{i} = δ_{i j} (K_{i} - K_{i}^{- 1}) / (q - q^{- 1})$ , together with the Serre relations (The Drinfeld-Jimbo quantized enveloping algebra by generators and relations, Symmetrizable Cartan data for quantum groups).

[F2]

The coproduct is an algebra map with $Δ E_{i} = E_{i} \otimes K_{i}^{- 1} + 1 \otimes E_{i}$ and $Δ F_{i} = F_{i} \otimes 1 + K_{i} \otimes F_{i}$ , so tensor products of modules are modules (The Drinfeld–Jimbo formulas define a Hopf algebra).

[F3]

Every integrable cyclic highest weight module with nonzero highest vector of label $2 ω_{1}$ receives a surjective map from the simple module $V (2 ω_{1})$ , determined by that vector (The integrable quantum highest weight module exists and is unique).

[F4]

Kashiwara operators are defined through the string decomposition; on a $2$ -step string with first step coefficient $1$ and second step coefficient $[2]$ , the operator ${\tilde{f}}_{i}$ moves one position with coefficient $1$ and ${\tilde{e}}_{i}$ is its inverse on the string; at the endpoints it acts by $0$ (The Kashiwara operators ${\tilde{e}}_{i}$ and ${\tilde{f}}_{i}$ of an integrable module, Uniqueness of the $i$ -string decomposition of an integrable module, Divided-power commutation and the simple $U_{q_{i}} ({s l}_{2})$ string modules, part (iii)).

[F5]

For an integrable type-1 module with a crystal lattice $L$ and residue basis $B$ , $ε_{i} (b) = \max {n : {\tilde{e}}_{i}^{n} b \neq 0}$ , $φ_{i} (b) = \max {n : {\tilde{f}}_{i}^{n} b \neq 0}$ and $φ_{i} = ε_{i} + ⟨ h_{i}, w t ⟩$ (The crystal graph, $ε_{i}$ , $φ_{i}$ and the weight function, Crystal lattices, crystal bases and their crystals, The Kashiwara lattices $L (λ)$ and $L (\infty)$ and their generating sets).

Verification

technique · direct

1.1F1F2algebra

$W$ is a module. The assignments of the statement satisfy the defining relations of [F1] on the three basis vectors: the toral actions are the stated labels; $[E_{1}, F_{1}]$ equals $e_{1} \mapsto e_{1}$ , $e_{2} \mapsto - e_{2}$ , $e_{3} \mapsto 0$ , which is $(K_{1} - K_{1}^{- 1}) / (q - q^{- 1})$ ; $[E_{2}, F_{2}]$ equals $e_{1} \mapsto 0$ , $e_{2} \mapsto e_{2}$ , $e_{3} \mapsto - e_{3}$ , which is $(K_{2} - K_{2}^{- 1}) / (q - q^{- 1})$ ; the mixed commutators $[E_{1}, F_{2}]$ , $[E_{2}, F_{1}]$ vanish on all three basis vectors; and the Serre relations hold because $E_{i}^{2} = F_{i}^{2} = 0$ for $i = 1, 2$ and every word with three or more factors from ${E_{1}, E_{2}}$ (or from ${F_{1}, F_{2}}$ ) kills every basis vector.

1.2F2algebra

Action table. Computing $Δ E_{i}, Δ F_{i}$ on the six displayed vectors gives $F_{1} v_{11} = v_{12}$ , $F_{1} v_{12} = [2] v_{22}$ , $F_{1} v_{13} = v_{23}$ , $F_{2} v_{12} = v_{13}$ , $F_{2} v_{22} = v_{23}$ , $F_{2} v_{23} = [2] v_{33}$ and $E_{1} v_{12} = [2] v_{11}$ , $E_{1} v_{22} = v_{12}$ , $E_{1} v_{23} = v_{13}$ , $E_{2} v_{13} = v_{12}$ , $E_{2} v_{23} = [2] v_{22}$ , $E_{2} v_{33} = v_{23}$ , with all other positive and negative actions on the six vectors zero; for instance $Δ F_{1} (v_{13}) = F_{1} e_{3} \otimes e_{1} + K_{1} e_{3} \otimes F_{1} e_{1} + q F_{1} e_{1} \otimes e_{3} + q K_{1} e_{1} \otimes F_{1} e_{3} = v_{23}$ and $Δ E_{2} (v_{23}) = E_{2} e_{3} \otimes K_{2}^{- 1} e_{2} + q E_{2} e_{2} \otimes K_{2}^{- 1} e_{3} + q e_{2} \otimes E_{2} e_{3} = (q^{- 1} + q) v_{22}$ . Diagonal toral actions are the six labels of the statement.

2.1F2F3step 1.2

Cyclicity and dimension. The table gives $v_{12} = F_{1} v_{11}$ , $v_{22} = F_{1}^{(2)} v_{11}$ , $v_{13} = F_{2} v_{12}$ , $v_{23} = F_{1} v_{13} = F_{2} v_{22}$ and $v_{33} = F_{2}^{(2)} v_{22}$ , so all six vectors lie in the cyclic submodule of $v_{11}$ . Their distinct labels and nonzero tensor coordinates make them independent, and their span is stable under all generators by step 1.2. Hence this span equals the cyclic submodule and has dimension six. It is integrable, since each $E_{i}, F_{i}$ is nilpotent on the displayed finite strings, and $v_{11}$ is highest of label $2 ω_{1}$ . Universality [F3] gives a surjection $V (2 ω_{1}) \to V$ sending its top to $v_{11}$ ; its kernel is zero by simplicity. Thus $V ≅ V (2 ω_{1})$ and this computation establishes its dimension without a Weyl-dimension prerequisite.

3.1F4F5step 1.2step 2.1

The divided strings and the lattice. In the table of step 1.2 the first $F_{i}$ -step of each color- $i$ string has coefficient $1$ and the second has coefficient $[2]$ ; normalizing by $[1]! = 1$ and $[2]! = [2]$ gives the divided strings of the statement, so by [F4] the Kashiwara operators act with coefficient $1$ along them: ${\tilde{f}}_{1} v_{11} = v_{12}$ , ${\tilde{f}}_{1} v_{12} = v_{22}$ , ${\tilde{f}}_{1} v_{13} = v_{23}$ , ${\tilde{f}}_{2} v_{12} = v_{13}$ , ${\tilde{f}}_{2} v_{22} = v_{23}$ , ${\tilde{f}}_{2} v_{23} = v_{33}$ , and the corresponding inverse ${\tilde{e}}_{i}$ -actions, with all endpoints $0$ . Distinct labels give linear independence, so the $A_{0}$ -span $L$ of the six vectors is their free direct sum; it is stable under both operators and generated by the lowering words from $v_{11}$ , so it is the recursively generated crystal lattice, and its residue classes form a $Q$ -basis of $L / q L$ by the crystal-limit isomorphism.

4.1step 3.1

Edges and partial inverses. The only nonzero arrows of the residue basis are the six listed: two color- $1$ edges on the first and one on the second of the chains $v_{11} \to v_{12} \to v_{22}$ and $v_{13} \to v_{23}$ , and the color- $2$ edges $v_{12} \to v_{13}$ and $v_{22} \to v_{23} \to v_{33}$ , exactly as in the statement; every arrow is the inverse of the corresponding ${\tilde{e}}_{i}$ -step by step 3.1, so the partial-inverse axiom holds and no further edges occur.

5.1F5step 3.1step 4.1∎

The invariants. Reading the string positions from step 4.1 gives the table $(ε_{1}, φ_{1}, ε_{2}, φ_{2})$ : $(0, 2, 0, 0)$ at $v_{11}$ , $(1, 1, 0, 1)$ at $v_{12}$ , $(2, 0, 0, 2)$ at $v_{22}$ , $(0, 1, 1, 0)$ at $v_{13}$ , $(1, 0, 1, 1)$ at $v_{23}$ and $(0, 0, 2, 0)$ at $v_{33}$ . Comparing with the six labels of the statement, the twelve equalities $φ_{i} = ε_{i} + ⟨ h_{i}, w t ⟩$ are the identities $2 = 0 + 2$ , $0 = 0 + 0$ ; $1 = 1 + 0$ , $1 = 0 + 1$ ; $0 = 2 - 2$ , $2 = 0 + 2$ ; $1 = 0 + 1$ , $0 = 1 - 1$ ; $0 = 1 - 1$ , $1 = 1 + 0$ ; $0 = 0 + 0$ , $0 = 2 - 2$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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 crystal graph of the quantum symmetric square of the standard A2A2​-module