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.

Integral triangular decomposition and freeness of the Lusztig form

Statement

Assume the Axiom of Choice, inherited through the crystal/global-basis and generic/classical PBW-rank suppliers. Let $U_{A}$ be the Lusztig divided-power integral form of The Lusztig divided-power integral form $U_{A}$ , with its parts $U_{A}^{-}, U_{A}^{0}, U_{A}^{+}$ over $A = Z [q, q^{- 1}]$ . Then:

(i) multiplication $U_{A}^{-} \otimes_{A} U_{A}^{0} \otimes_{A} U_{A}^{+} \to U_{A}$ is an isomorphism;

(ii) the two divided-power halves are free $A$ -modules with finite free root components of the classical PBW ranks;

(iii) the unmodified torus has the $A$ -basis $K_{c} \prod_{i} K_{i}^{δ_{i}} T_{i, 0, t_{i}}$ with $δ_{i} \in {0, 1}$ and $c$ running over a system of representatives of $P^{\lor} / \sum_{i} Z (d_{i} h_{i})$ ; hence $U_{A}$ is free, and the degree- $β$ component is $⨁_{α - γ = β} U_{A}^{-} [- γ] \otimes_{A} U_{A}^{0} \otimes_{A} U_{A}^{+} [α]$ ;

(iv) unique coefficients refer to products of chosen basis elements, not to arbitrary sums of simple tensors.

Facts & Assumptions

Given: The divided-power form $U_{A} \subseteq U_{q} (g)$ with its half and toral parts, the skew derivations of the halves, and the toral elements $K_{h}, T_{i, c, t}$ of The Lusztig divided-power integral form $U_{A}$ .

[F1]

Divided-power identities (Divided-power multiplication, toral binomials and the $E_{i}^{(a)} F_{i}^{(b)}$ reordering identity): $E^{(a)} E^{(b)} = {(\binom{a + b}{a})}_{i} E^{(a + b)}$ and $F^{(a)} F^{(b)} = {(\binom{a + b}{a})}_{i} F^{(a + b)}$ ; the toral binomials reorder past $E_{i}, F_{i}$ by index shifts; and every element of $U_{A}$ is a finite $A$ -linear combination of products $b_{-} u b_{+}$ with $b_{-} \in U_{A}^{-}$ , $u \in U_{A}^{0}$ , $b_{+} \in U_{A}^{+}$ , i.e. multiplication from the tensor product is surjective.

[F2]

Integral negative-half basis (The highest weight and negative half integral crystal triples are balanced, Bar invariance, congruence and uniqueness of the lower global basis): the lower global basis $G_{\infty} (B (\infty))$ is an $A$ -basis of $U_{A}^{-}$ , and each finite root component $U_{A}^{-} [- γ]$ is a free $A$ -module of rank $\dim_{Q (q)} U_{q}^{-} [- γ]$ . The positive half is carried to the negative half by the algebra isomorphism $ι : E_{i} \mapsto F_{i}$ of The Drinfeld pairing between the positive and negative quantum halves, so $U_{A}^{+}$ is free with finite free root components as well.

[F3]

Unmodified integral torus (The unmodified integral torus has a quantum-binomial basis, The quantum Pascal recurrences, the Gauss product formula and Gaussian integrality): the displayed family $K_{c} \prod_{i} K_{i}^{δ_{i}} T_{i, 0, t_{i}}$ is an $A$ -basis of $U_{A}^{0}$ , with Gaussian-integral coefficients and Laurent-extremal independence.

[F4]

Field triangular decomposition (Triangular decomposition of a quantized enveloping algebra, and the Drinfeld–Jimbo decomposition display (1.7) of Jeong–Kang–Kashiwara, §1, printed p. 6): the natural map $U_{q}^{-} \otimes_{Q (q)} U_{q}^{0} \otimes_{Q (q)} U_{q}^{+} \to U_{q} (g)$ is an isomorphism of $Q (q)$ -vector spaces, with homogeneous components of the stated shape.

[F5]

Classical PBW ranks (Generic quantum Serre halves have classical PBW ranks and a nondegenerate Hopf pairing): the field dimension of each homogeneous component of the generic quantum half equals the classical PBW rank $\dim_{C} U (n^{\pm}) [\pm α]$ ; this identification carries that theorem's stated Choice hypothesis, in addition to the inherited crystal/global-basis use of [F2].

[C1]

Choice: the Axiom of Choice is inherited through the crystal/global-basis suppliers of [F2] and the rank supplier [F5], as declared in The Axiom of Choice; the explicit tensor, localization and toral-basis computations add no choice use.

Proof

technique · direct

1.1F2F3

Freeness of the factors. By [F2] the negative half is a direct sum of free $A$ -modules $U_{A}^{-} [- γ]$ of finite rank; by the transport $ι$ the same holds for $U_{A}^{+}$ ; and by [F3] the unmodified torus $U_{A}^{0}$ has the displayed $A$ -basis. Each factor is therefore a free $A$ -module, and the half factors have finite free root components; the toral degree-zero component can have infinite rank.

1.2F1

Surjectivity of the multiplication map. The spanning statement of [F1] says that every element of $U_{A}$ is a finite $A$ -linear combination of products $b_{-} u b_{+}$ ; grouping the factors according to root degree exhibits $U_{A}$ as the image of $U_{A}^{-} \otimes_{A} U_{A}^{0} \otimes_{A} U_{A}^{+} \to U_{A}$ , so the map is surjective.

2.1F4step 1.1step 1.2

Injectivity by field decomposition and torsion-freeness. Extending scalars along $A ↪ Q (q)$ gives the field multiplication map, which is an isomorphism by [F4]. If $x$ lay in the kernel of the integral map, its image in $U_{q}^{-} \otimes U_{q}^{0} \otimes U_{q}^{+}$ would lie in the kernel of the field isomorphism after extension and hence would be $0$ ; but the source is a free, hence torsion-free, $A$ -module, so the natural map from it to its $Q (q)$ -extension is injective, forcing $x = 0$ . Thus the multiplication map is an isomorphism, proving (i).

3.1F3step 2.1

Toral basis, freeness and the homogeneous form. Statement (iii) is the combination of the toral basis [F3] with the factorization of step 2.1; since a tensor product of free modules is free, $U_{A}$ is free, and restricting the isomorphism to homogeneous components gives the displayed degree- $β$ decomposition, with $U_{A}^{0}$ contributing only degree $0$ . Unique coefficients are those of the products of the chosen basis elements of the three factors, not of arbitrary sums of simple tensors, because the isomorphism is one of $A$ -modules with the displayed direct-sum decomposition.

4.1F2F5step 3.1C1∎

Ranks and conclusion. The ranks of the half components are their field dimensions by [F2]; by [F5], applied with its stated Choice hypothesis [C1], those dimensions equal the classical PBW ranks, proving (ii). Steps 1.1–3.1 prove (i), (iii) and (iv); no torsionfree-to-free conversion over the non-PID ring $A$ and no modified dot- $U$ basis was used, since freeness came from explicit bases.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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 Mathematical Journal 63 (1991), 465–516 (standard reference, not scraped)
George Lusztig, Introduction to Quantum Groups (Progress in Mathematics 110, Birkhauser, 1993; second printing 1994; author-hosted scan) (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)
Kyeonghoon Jeong, Seok-Jin Kang and Masaki Kashiwara, Crystal Bases for Quantum Generalized Kac-Moody Algebras, arXiv:math/0305390 (standard reference, not scraped)