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.

Quantum Verma and simple modules for sl2

Example

Use the standard rank-one datum $P = Z ω$ , $P^{\lor} = Z h$ , $α = 2 ω$ , $⟨ ω, h ⟩ = 1$ and $d_{1} = 1$ . Thus $U_{q} (g)$ is generated by $E, F, K^{\pm 1}$ with $q_{1} = q$ . For $m \in Z$ , put $λ = m ω$ and write $[t] = (q^{t} - q^{- t}) / (q - q^{- 1})$ .

The Verma module $M (m)$ has ordinary-power basis $u_{t} = F^{t} u_{0}$ , $t \geq 0$ , where $u_{0} = v_{λ}$ . Its actions are $K u_{t} = q^{m - 2 t} u_{t}, F u_{t} = u_{t + 1}, E u_{t} = [t] [m - t + 1] u_{t - 1} (t \geq 1), E u_{0} = 0.$ The divided-power basis $v_{t} = F^{(t)} u_{0} = u_{t} / [t]!$ instead satisfies $K v_{t} = q^{m - 2 t} v_{t}, F v_{t} = [t + 1] v_{t + 1}, E v_{t} = [m - t + 1] v_{t - 1} (t \geq 1), E v_{0} = 0.$

(a) For $m \geq 0$ , the submodule generated by $F^{m + 1} u_{0}$ is the tail spanned by $u_{t}$ , $t \geq m + 1$ . Its quotient $L (m)$ is simple of dimension $m + 1$ , with divided-power basis $v_{0}, \dots, v_{m}$ and the second set of actions, with $v_{- 1} = v_{m + 1} = 0$ . For $m = 0$ it is trivial.

(b) For $m = - 1$ , the raising coefficients in the divided-power basis are $[- t] = - [t] \neq 0$ for every $t \geq 1$ . Hence $M (- 1) = L (- 1)$ is irreducible, infinite-dimensional and not integrable. Its highest weight is integral and is not dominant.

(c) For every $m < 0$ , $m - t + 1 \neq 0$ at all $t \geq 1$ , so the same conclusions hold. Thus dominance in The integrable quantum highest weight module exists and is unique is essential.

Facts & Assumptions

Given: The rank-one Cartan datum, the Verma module $M (m) = U_{q}^{-} v_{0}$ with $U_{q}^{-} = Q (q) [F]$ , and the generators $E, F, K^{\pm 1}$ .

[F1]

$M (λ)$ is free of rank one over $U_{q}^{-}$ with basis $u_{t} = F^{t} u_{0}$ , has weights $λ - Q_{+} = {λ - t α_{1}} = {m - 2 t : t \geq 0}$ , and satisfies $K v_{0} = q^{m} v_{0}$ , $E v_{0} = 0$ , $K F = q^{- 2} F K$ (Quantum Verma modules $M (λ)$ , highest weight vectors, and the simple highest weight quotient $L (λ)$ , Quantum weight modules, weights in $P$ , and integrability).

[F2]

$E F^{t} = F^{t} E + F^{t - 1} \frac{1}{q - q^{- 1}} \sum_{s = 0}^{t - 1} (q^{- 2 s} K - q^{2 s} K^{- 1})$ for $t \geq 1$ , and $[m - t + 1] = \frac{q^{m - t + 1} - q^{- m + t - 1}}{q - q^{- 1}}$ (Divided-power commutation and the simple $U_{q_{i}} ({s l}_{2})$ string modules (ii), Quantum integers, factorials, Gaussian binomials and divided powers at $q_{i}$ ).

[F3]

$[j] = 0$ for an integer $j$ if and only if $j = 0$ , and $[j] \neq 0$ otherwise; more precisely $[- t] = - [t]$ for $t \geq 1$ (Quantum integers, factorials, Gaussian binomials and divided powers at $q_{i}$ ).

[F4]

For $λ \in P^{+}$ the Serre quotient $M (λ) / \sum_{i} U_{q} (g) F_{i}^{λ (h_{i}) + 1} v_{λ}$ is the simple module $L (λ)$ and is universal among integrable cyclic highest weight modules of weight $λ$ (The integrable quantum highest weight module exists and is unique).

Verification

technique · read the rank-one Verma string from the commutation formula, split off the finite string when the highest weight is nonnegative, and prove irreducibility in the negative cases by the largest-index raising argument

1.1F1F2F3algebra

Basis and action. By [F1], the ordinary-power vectors $u_{t} = F^{t} u_{0}$ are a basis, with $K u_{t} = q^{m - 2 t} u_{t}$ and $F u_{t} = u_{t + 1}$ . Evaluating [F2] on $u_{0}$ gives $E u_{t} = (\sum_{s = 0}^{t - 1} (q^{m - 2 s} - q^{- m + 2 s}) / (q - q^{- 1})) u_{t - 1}$ . The geometric sums satisfy $\sum_{s = 0}^{t - 1} q^{- 2 s} = q^{- (t - 1)} [t]$ and $\sum_{s = 0}^{t - 1} q^{2 s} = q^{t - 1} [t]$ , so $E u_{t} = [t] [m - t + 1] u_{t - 1}$ . Dividing by $[t]!$ gives the displayed actions on $v_{t} = F^{(t)} u_{0}$ .

2.1step 1.1F1F3F4algebra

The dominant quotient. For $m \geq 0$ , $E u_{m + 1} = 0$ by step 1.1. The tail spanned by $u_{t}$ , $t \geq m + 1$ , is stable under $E, F, K^{\pm 1}$ by those formulas, and it is exactly the submodule generated by $u_{m + 1}$ because repeated $F$ generates every tail vector. Therefore its quotient has basis $v_{0}, \dots, v_{m}$ and the stated truncated divided-power actions. For a nonzero vector $x = \sum_{t = 0}^{T} c_{t} v_{t}$ with largest occupied index $T \leq m$ , $E^{T} x = c_{T} \prod_{j = 1}^{T} [m - j + 1] v_{0} \neq 0$ : lower-index terms are killed. Any submodule containing $x$ contains $v_{0}$ and then every $v_{t}$ , so the quotient is simple. The empty product covers $T = 0$ and $m = 0$ gives the trivial module.

2.2step 1.1F1F3algebra

The boundary $m = - 1$ . Here $E v_{t} = - [t] v_{t - 1}$ for $t \geq 1$ . For a nonzero finite sum $x = \sum_{t = 0}^{T} c_{t} v_{t}$ with $c_{T} \neq 0$ , $E^{T} x = c_{T} \prod_{j = 1}^{T} (- [j]) v_{0} \neq 0$ , including the empty product when $T = 0$ . A submodule containing $x$ therefore contains $v_{0}$ and every $v_{t}$ ; $M (- 1)$ is simple. It is infinite-dimensional by its basis, and $F^{t} u_{0} = u_{t} \neq 0$ for all $t$ , so it is not integrable. The label $- 1$ is integral and is not dominant.

3.1step 1.1step 2.1step 2.2F1F3F4algebra∎

For $m < 0$ , all scalars $[m - j + 1]$ , $j \geq 1$ , are nonzero. The same largest-index argument gives $E^{T} x = c_{T} \prod_{j = 1}^{T} [m - j + 1] v_{0} \neq 0$ for each nonzero finite sum. Thus $M (m) = L (m)$ is simple, infinite-dimensional and non-integrable, with integral non-dominant highest weight. The explicit dominant strings in step 2.1 and these negative cases prove all stated conclusions.

Depends on

Used by

Direct q=1 substitution in quantum denominators Counterexample
Specializing a quantum highest weight lattice at q=1 Example

Dependency tree · two levels

19 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)
Math 263C Quantum Groups (Stanford, 2022), lecture slides 'Lusztig's quantum group. Tilting modules. The Fusion Category in Action' (standard reference, not scraped)