TheoremStatement: Literature-sourcedProof: 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 integrable quantum highest weight module exists and is unique

Statement

Let $λ \in P$ be a dominant integral label weight, put $m_{i} : = ⟨ λ, h_{i} ⟩ \geq 0$ , and let $M (λ)$ be the quantum Verma module with highest vector $v_{λ}$ (Quantum Verma modules $M (λ)$ , highest weight vectors, and the simple highest weight quotient $L (λ)$ , Kac moody integral and dominant integral weights).

(i) The quotient $\tilde{L} (λ) : = M (λ) / \sum_{i} U_{q} (g) F_{i}^{(m_{i} + 1)} v_{λ}$ is nonzero, has finite-dimensional label weights and support contained in $λ - Q_{+}$ , is integrable, and equals the canonical simple highest weight module $L (λ)$ , which is simple also as an ordinary (not assumed graded) $U_{q} (g)$ -module.

(ii) Universality. Every integrable cyclic highest weight module $V$ of highest weight $λ$ with highest vector $v \neq 0$ receives a $U_{q} (g)$ -module map $\tilde{L} (λ) \to V$ with ${\overset{ˉ}{v}}_{λ} \mapsto v$ , and this map is unique; every nonzero such $V$ is isomorphic to $L (λ)$ .

(iii) Its character equals the classical integrable highest weight character of the explicitly regularized realization of the datum. No global $Z [q, q^{- 1}]$ -freeness and no crystal or global basis is used.

Facts & Assumptions

Given: The dominant integral weight $λ$ , the Verma module and its highest vector, the quotient $\tilde{L} (λ)$ , and the integral form used by the deformation lemma.

[F1]

The Serre quotient lemma: $\tilde{L} (λ)$ is nonzero with nonzero top class ${\overset{ˉ}{v}}_{λ}$ , has finite-dimensional label weights and support in $λ - Q_{+}$ , is integrable, and every integrable cyclic highest weight module of highest weight $λ$ is a quotient of $\tilde{L} (λ)$ ; its proof does not use commutation of distinct adjacent-root divided powers (The dominant quantum Serre quotient is nonzero and integrable(i)-(iii)).

[F2]

The local deformation lemma: every nonzero graded quotient of $\tilde{L} (λ)$ with nonzero highest line has the classical simple character, and consequently $\tilde{L} (λ) ≅ L (λ)$ for the simple graded quotient $L (λ)$ of $M (λ)$ ; this uses the DVR $Q [q]_{(q - 1)}$ and no global freeness (Local q=1 deformation proves integrable highest weight universality(a),(b)).

[F3]

The Cartan projection lemma: the normalized homogeneous contravariant form on $M (λ)$ descends to $L (λ) = M (λ) / N (λ)$ with $N (λ)$ the largest proper graded submodule, and the maximum-height raising argument proves that $L (λ)$ has no proper nonzero ordinary submodule, i.e. it is simple as a $U_{q} (g)$ -module without a grading hypothesis (Cartan projection constructs the Verma contravariant form and identifies its radical).

[F4]

$M (λ)$ has the universal property that every highest weight module of weight $λ$ with highest vector $v$ receives a unique map $M (λ) \to V$ with $v_{λ} \mapsto v$ , and the map is surjective when $V$ is cyclic; the top label space of a highest weight module is one-dimensional (Quantum Verma modules $M (λ)$ , highest weight vectors, and the simple highest weight quotient $L (λ)$ , Quantum weight modules, weights in $P$ , and integrability).

Verification

technique · assemble the construction and universality from the Serre quotient, identify the quotient with the simple module by the local q=1 deformation, and transfer ordinary simplicity from the Cartan projection lemma

1.1F1F2algebra

Construction, support and integrability. The quotient $\tilde{L} (λ)$ of the statement is the quotient constructed in [F1] (the sum of the vectors $F_{i}^{(m_{i} + 1)} v_{λ}$ and their $U_{q}$ -translates is the displayed submodule); hence it is nonzero, has one-dimensional top label space with generator ${\overset{ˉ}{v}}_{λ} \neq 0$ , has finite-dimensional label weights, support contained in $λ - Q_{+}$ , and is integrable. This proves the first part of (i).

1.2F1F2algebra

Identification with the simple module and character. The simple graded quotient $L (λ)$ of $M (λ)$ is a nonzero graded quotient of $\tilde{L} (λ)$ with nonzero highest line: the image of ${\overset{ˉ}{v}}_{λ}$ generates it, and a nonzero highest vector of weight $λ$ cannot lie in the kernel, since the kernel is a graded submodule not containing the top label space. By [F2] both $\tilde{L} (λ)$ and $L (λ)$ have the classical simple character, so the surjection $\tilde{L} (λ) \to L (λ)$ is injective on every finite-dimensional label space, hence an isomorphism; $\tilde{L} (λ) ≅ L (λ)$ and the character statement (iii) follow.

1.3F2F3algebra

Ordinary simplicity. By [F3], $L (λ)$ has no proper nonzero ordinary submodule. Since $\tilde{L} (λ) ≅ L (λ)$ , the same holds for $\tilde{L} (λ)$ ; this completes (i).

2.1F1F2F3F4algebra∎

Universality. Let $V$ be an integrable cyclic highest weight module of highest weight $λ$ with highest vector $v \neq 0$ . By [F4] there is a unique $U_{q} (g)$ -module map $M (λ) \to V$ with $v_{λ} \mapsto v$ , and it is surjective because $v$ generates $V$ . By F1 the integrability of $V$ forces this map to kill the defining submodule of $\tilde{L} (λ)$ : namely the kernel contains each $F_{i}^{(m_{i} + 1)} v_{λ}$ , since the image $F_{i}^{(m_{i} + 1)} v$ must vanish (the minimal $t_{i}$ with $F_{i}^{t_{i}} v = 0$ equals $m_{i} + 1$ by the rank-one string computation used in [F1]); hence the map factors through $\tilde{L} (λ) \to V$ . This map is unique because it is determined on the cyclic vector, and it sends the class of $v_{λ}$ to $v$ . If $V \neq 0$ , then by step 1.3 the source $\tilde{L} (λ) ≅ L (λ)$ is simple, so the surjection is an isomorphism: $V ≅ L (λ)$ . This proves (ii).

Depends on

Used by

Dependency tree · two levels

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