TheoremStatement: Literature-sourcedProof: 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 basis $B (\infty)$ of the negative half

Statement

Let $L (\infty) \subseteq U_{q}^{-}$ and $B (\infty) \subseteq L (\infty) / q L (\infty)$ be the Kashiwara lattice and generating set of The Kashiwara lattices $L (λ)$ and $L (\infty)$ and their generating sets, with the Kashiwara operators ${\tilde{e}}_{i}, {\tilde{f}}_{i}$ on $U_{q}^{-}$ of The $i$ -string decomposition of the negative half(iii).

(i) $(L (\infty), B (\infty))$ is a crystal basis of $U_{q}^{-}$ in the sense of Crystal lattices, crystal bases and their crystals: $L (\infty)$ is a free $A_{0}$ -submodule with $U_{q}^{-} ≅ Q (q) \otimes_{A_{0}} L (\infty)$ , stable under ${\tilde{e}}_{i}$ and ${\tilde{f}}_{i}$ ; and $B (\infty)$ is a $Q$ -basis of $L (\infty) / q L (\infty)$ satisfying ${\tilde{e}}_{i} B (\infty) \subseteq B (\infty) \cup {0}$ , ${\tilde{f}}_{i} B (\infty) \subseteq B (\infty)$ , and ${\tilde{f}}_{i} b = b^{'}$ if and only if $b = {\tilde{e}}_{i} b^{'}$ for all $b, b^{'} \in B (\infty)$ .

(ii) The root-graded components are free: $L (\infty) = ⨁_{ν \in Q_{+}} L (\infty)_{- ν}$ and each $L (\infty)_{- ν}$ is a free $A_{0}$ -module of rank $# B (\infty)_{- ν} = \dim_{Q (q)} U_{q}^{-} [- ν]$ .

(iii) For every $λ \in P^{+}$ the projection $π_{λ} (P) = P v_{λ}$ maps $B (\infty)$ onto $B (λ) \cup {0}$ , and the compatibility statements of Projection from $L (\infty)$ to $L (λ)$ and its compatibility with the Kashiwara operators hold: $π_{λ} (L (\infty)_{- α}) = L (λ)_{λ - α}$ , ${b \in B (\infty)_{- α} : π_{λ} (b) \neq 0} ≅ B (λ)_{λ - α}$ , ${\tilde{f}}_{i} π_{λ} = π_{λ} {\tilde{f}}_{i}$ and ${\tilde{e}}_{i} π_{λ} (b) = π_{λ} ({\tilde{e}}_{i} b)$ whenever $π_{λ} (b) \neq 0$ .

(iv) The root-graded crystal has finite $ε_{i}$ on each element, formal $φ_{i} = ε_{i} + ⟨ h_{i}, w t ⟩$ , and actual lowering length $ℓ_{i}^{-} = \infty$ . Every ${\tilde{f}}_{i}$ -iterate is nonzero because ${\tilde{e}}_{i} {\tilde{f}}_{i} = i d$ holds on its lattice and residue. Thus it is the infinite lowering crystal of the unit, with the negative-half convention of the crystal-graph definition.

Choice. The axiom of choice is declared via The Axiom of Choice and enters only through the grand loop: the partial-inverse axiom in (i) uses clause J(r) of The grand loop: existence of the highest weight crystal bases, whose proof consumes the AC-dependent form comparison of the negative-half form. The freeness and rank statements are choice-free.

Facts & Assumptions

Given: The negative half $U_{q}^{-}$ with its root grading and operators, and the lattice $L (\infty)$ generated by the monomials ${\tilde{f}}_{i_{1}} \dots {\tilde{f}}_{i_{r}} 1$ .

[F1]

Structure of the lattice: $L (\infty) = ⨁_{ν \in Q_{+}} L (\infty)_{- ν}$ is generated by the lowering monomials, each component is finitely generated and torsionfree, and it is a free $A_{0}$ -module by the PID supplier (The Kashiwara lattices $L (λ)$ and $L (\infty)$ and their generating sets, Every finitely generated torsion-free module over a PID is free, The local ring $A_{0}$ of rational functions regular at $q = 0$ ).

[F2]

Grand loop clauses: H(r) ( ${\tilde{e}}_{i} L (\infty)_{- α} \subseteq L (\infty)$ ), I(r) ( ${\tilde{e}}_{i} B (\infty)_{- α} \subseteq B (\infty) \cup {0}$ ), J(r) (if ${\tilde{e}}_{i} b \neq 0$ then $b = {\tilde{f}}_{i} {\tilde{e}}_{i} b$ ), K(r) ( $B (\infty)_{- α}$ is a $Q$ -basis of $L (\infty)_{- α} / q L (\infty)_{- α}$ ), and the large-weight lattice isomorphism $π_{λ} : L (\infty)_{- α} \to L (λ)_{λ - α}$ for $λ$ large (The grand loop: existence of the highest weight crystal bases).

[F3]

On the negative half ${\tilde{e}}_{i} {\tilde{f}}_{i} = i d$ , ${\tilde{f}}_{i}$ is injective, ${\tilde{e}}_{i} u = 0$ if and only if $u \in \ker e_{i}^{'}$ , and ${\tilde{e}}_{i}$ lowers the root height by one (The $i$ -string decomposition of the negative half).

[F4]

Projection lemma: for every $α$ and $λ$ one has $π_{λ} (L (\infty)_{- α}) = L (λ)_{λ - α}$ , the surviving residue bijection, and the ${\tilde{e}}_{i}$ - and ${\tilde{f}}_{i}$ -compatibilities on surviving classes; clause (c) inherits the axiom of choice (Projection from $L (\infty)$ to $L (λ)$ and its compatibility with the Kashiwara operators, The Axiom of Choice).

[F5]

In module crystals the raising and lowering lengths are finite. The negative-half convention of the crystal graph is: finite $ε_{i}$ , formal $φ_{i} = ε_{i} + ⟨ h_{i}, w t ⟩$ and actual lowering length $ℓ_{i}^{-} = \infty$ (The crystal graph, $ε_{i}$ , $φ_{i}$ and the weight function).

Proof

technique · direct. Every assertion is read off from the grand loop and the projection lemma

1.1F1F2F3algebra

Freeness and scalar extension. Each component is finitely generated and torsionfree, hence free over the PID $A_{0}$ by [F1]. As in the grand-loop conclusion [F2], enumerate $A_{0}$ and the finite ordered word generators of each component and take the first finite tuple of their linear combinations that is a basis. These uniquely specified component bases unite to a basis of the graded direct sum without simultaneous choice. For field spanning, use the grand-loop field-spanning argument [F2]: if $x = \sum_{n} F_{i}^{(n)} x_{n}$ is homogeneous, then $F_{i} x = {\tilde{f}}_{i} (\sum_{n} [n + 1]_{i} F_{i}^{(n)} x_{n})$ , and the vector in parentheses has the same root degree as $x$ . Thus every positive-height component, being the sum of the $F_{i}$ -images of preceding components, is also spanned by their ${\tilde{f}}_{i}$ -images. Induction from $U_{q}^{-} [0] = Q (q) 1$ shows that the lowering words span each field component. The canonical map $Q (q) \otimes_{A_{0}} L (\infty)_{- α} \to U_{q}^{-} [- α]$ is therefore surjective. It is injective by clearing denominators: a finite tensor sum equals $d^{- 1} \otimes z$ for some $0 \neq d \in A_{0}$ and $z \in L (\infty)_{- α}$ , and its image $d^{- 1} z$ vanishes only when $z = 0$ . Taking graded direct sums gives the claimed scalar-extension isomorphism.

1.2F1F2F3

Stability and residue basis. Stability under ${\tilde{f}}_{i}$ holds by construction, since a ${\tilde{f}}_{i}$ -image of a lowering monomial is a lowering monomial; stability under ${\tilde{e}}_{i}$ is clause H(r). Clause K(r) says that $B (\infty)_{- α}$ is a $Q$ -basis of $L (\infty)_{- α} / q L (\infty)_{- α}$ , and clause I(r) gives ${\tilde{e}}_{i} B (\infty) \subseteq B (\infty) \cup {0}$ . For ${\tilde{f}}_{i}$ , the image of a monomial is a monomial and ${\tilde{e}}_{i} {\tilde{f}}_{i} = i d$ prevents it from vanishing modulo $q$ : if ${\tilde{f}}_{i} b \in q L (\infty)$ then $b = {\tilde{e}}_{i} {\tilde{f}}_{i} b \in q L (\infty)$ , contradicting $b \neq 0$ in the crystal limit.

1.3F2F3

The partial-inverse axiom. If ${\tilde{f}}_{i} b = b^{'}$ with $b, b^{'} \in B (\infty)$ , then applying ${\tilde{e}}_{i}$ and [F3] gives $b = {\tilde{e}}_{i} {\tilde{f}}_{i} b = {\tilde{e}}_{i} b^{'}$ . Conversely, if $b = {\tilde{e}}_{i} b^{'} \neq 0$ , then $b^{'} = {\tilde{f}}_{i} {\tilde{e}}_{i} b^{'}$ by clause J(r), so ${\tilde{f}}_{i} b = {\tilde{f}}_{i} {\tilde{e}}_{i} b^{'} = b^{'}$ by [F3]; hence ${\tilde{f}}_{i} b = b^{'}$ if and only if $b = {\tilde{e}}_{i} b^{'}$ , and this is the only place where the grand-loop clause J(r), and with it the inherited axiom of choice, is used.

2.1F4F5step 1.2

The projection statements. The lattice projection, surviving-residue bijection and operator compatibilities in (iii) are [F4]. To see that zero is also attained, fix $i \in I$ : by step 1.2 every ${\tilde{f}}_{i}^{n} 1$ has nonzero negative-half residue, while lowering compatibility projects it to ${\tilde{f}}_{i}^{n} v_{λ}$ . The latter is zero for sufficiently large $n$ because the module lowering length is finite by [F5]. Thus the image is exactly $B (λ) \cup {0}$ .

2.2F1F2step 1.1

The rank formula. By [F1] and clause K(r), the free rank of $L (\infty)_{- α}$ is $# B (\infty)_{- α}$ , and by step 1.1 the scalar extension is $U_{q}^{-} [- α]$ , so this number is also $\dim_{Q (q)} U_{q}^{-} [- α]$ ; this is (ii).

3.1F3F5step 1.2∎

The infinite chain. By [F3] the operator ${\tilde{f}}_{i}$ is injective on $U_{q}^{-}$ and ${\tilde{e}}_{i} {\tilde{f}}_{i} = i d$ , and by step 1.2 no iterate of a residue element vanishes; hence $ℓ_{i}^{-} = + \infty$ for every $b \in B (\infty)$ , while $ε_{i} (b) < \infty$ by the finite string structure of the negative half (the height bound). The formal $φ_{i} = ε_{i} + ⟨ h_{i}, w t ⟩$ is the convention of [F5] and is not the lowering-chain length.

Depends on

Used by

Dependency tree · two levels

44 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)
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)

The crystal basis B(∞)B(∞) of the negative half