LemmaStatement: 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 balanced-triple linear algebra over $P^{1}$

Statement

Let $V$ be finite-dimensional over $Q (q)$ , let $M \subset V$ be an $A = Z [q, q^{- 1}]$ -submodule spanning $V$ , and let $L_{0}, L_{\infty}$ be full free $A_{0}$ - and $A_{\infty}$ -lattices in $V$ . Write $E = M \cap L_{0} \cap L_{\infty}$ and use the balanced-triple language of Balanced triples over the two charts of $P^{1}$ and the globalization map.

(1) If the canonical $Z$ -linear map $E \to (M \cap L_{0}) / (M \cap q L_{0})$ is an isomorphism, then $M \cap L_{0} ≅ Z [q] \otimes_{Z} E, M \cap L_{\infty} ≅ Z [q^{- 1}] \otimes_{Z} E, M ≅ A \otimes_{Z} E,$ and the infinity residue map $E \to (M \cap L_{\infty}) / (M \cap q^{- 1} L_{\infty})$ is also an isomorphism; moreover $A_{0} \otimes_{Z} E ≅ L_{0}$ and $A_{\infty} \otimes_{Z} E ≅ L_{\infty}$ under the maps induced by inclusions. If $E$ has a finite $Z$ -basis, these are actual free bases of $M, L_{0}, L_{\infty}$ over $A, A_{0}, A_{\infty}$ . No containment $M \subset L_{0} \cap L_{\infty}$ and no freeness of $M / E$ is assumed.

(2) If a $Z$ -module $F$ maps into $M \cap L_{0} \cap L_{\infty}$ , generates $M$ over $A$ , and maps injectively into both rational residues $L_{0} / q L_{0}$ and $L_{\infty} / q^{- 1} L_{\infty}$ , then $F ≅ E ≅ (M \cap L_{0}) / (M \cap q L_{0})$ .

(3) More generally, let $N \subset M$ be an $A$ -submodule whose integral intersection $E_{N} = N \cap L_{0} \cap L_{\infty}$ satisfies $N ≅ A \otimes_{Z} E_{N}$ . If a $Z$ -module $F$ maps to $M \cap (L_{0} + N) \cap (L_{\infty} + N)$ , generates $M$ modulo $N$ over $A$ , and maps injectively into $(L_{0} + Q N) / (q L_{0} + Q N)$ and $(L_{\infty} + Q N) / (q^{- 1} L_{\infty} + Q N)$ , then $M$ is balanced. The sequence $0 \to (N \cap L_{0}) / (N \cap q L_{0}) \to (M \cap L_{0}) / (M \cap q L_{0}) \to (L_{0} + Q N) / (q L_{0} + Q N)$ is exact, and its last image is the image of $F$ . If $F$ and $E_{N}$ are finite free $Z$ -modules, then so is $E_{M} = M \cap L_{0} \cap L_{\infty}$ , and $M$ is free over $A$ .

These are the integral forms of Kashiwara's chart lemmas, in the notation of Balanced triples over the two charts of $P^{1}$ and the globalization map; their rational base extension gives the usual $A_{0} / A_{\infty}$ criterion, and no containment of charts or freeness of $M$ is assumed anywhere.

Facts & Assumptions

Given: A finite-dimensional $Q (q)$ -space $V$ , an $A$ -submodule $M \subseteq V$ spanning $V$ , full free chart lattices $L_{0}, L_{\infty}$ over $A_{0}, A_{\infty}$ , and the balanced-triple data of Balanced triples over the two charts of $P^{1}$ and the globalization map.

[F1]

Balanced-triple data (Balanced triples over the two charts of $P^{1}$ and the globalization map): $E = M \cap L_{0} \cap L_{\infty}$ ; the canonical maps $E \to (M \cap L_{0}) / (M \cap q L_{0})$ and $E \to (M \cap L_{\infty}) / (M \cap q^{- 1} L_{\infty})$ ; the rings $A = Z [q, q^{- 1}]$ , $A_{0}$ with uniformizer $q$ and residue field $Q$ , and $A_{\infty}$ with uniformizer $q^{- 1}$ and residue field $Q$ ; $L_{0}$ and $L_{\infty}$ are free and generate $V$ .

[F2]

Chart calculus: a free $A_{0}$ -lattice in a finite-dimensional $Q (q)$ -space spans it over $Q (q)$ , so every vector has finite vanishing/pole order, and $q L_{0} \subseteq L_{0}$ , $q^{- 1} L_{\infty} \subseteq L_{\infty}$ .

[A1]

The hypothesis used only in part (1): the canonical map $E \to (M \cap L_{0}) / (M \cap q L_{0})$ is an isomorphism.

Proof

technique · direct, using finite pole orders and the two residue injections

1.1A1F1F2algebra

Since $q^{\pm 1} M = M$ , we have $M \cap q L_{0} = q (M \cap L_{0})$ , and similarly at infinity. Under [A1], $E \cap q L_{0} = 0$ . For $x \in M \cap L_{0}$ surjectivity gives $x = e + q x_{1}$ with $e \in E$ and $x_{1} \in M \cap L_{0}$ . If also $x \in q^{n} L_{\infty}$ with $n \geq 1$ , then $e \in q^{n} L_{\infty}$ and $x_{1} \in q^{n - 1} L_{\infty}$ . Induction, starting with $M \cap L_{0} \cap L_{\infty} = E$ , therefore gives $M \cap L_{0} \cap q^{n} L_{\infty} = \sum_{k = 0}^{n} q^{k} E$ . The sum is direct: in a vanishing sum its constant coefficient belongs to $E \cap q L_{0} = 0$ , and division by $q$ removes successive coefficients.

1.2F1algebra

For (2), identify $F$ with its image, since its residue map is injective. In any finite Laurent sum $x = \sum_{k} q^{k} f_{k}$ with $f_{k} \in F$ , the least exponent cannot be negative when $x \in L_{0}$ : multiplying by its inverse power gives a constant coefficient in $F \cap q L_{0} = 0$ . Removing that coefficient repeatedly proves $M \cap L_{0} = Z [q] F$ . The mirror argument at infinity gives $M \cap L_{\infty} = Z [q^{- 1}] F$ . These expressions are unique by the same residue injections, so the simultaneous intersection is $F$ , and its integral residue map is an isomorphism. This proves (2); only the integral residue, rather than the entire rational residue, is identified with $F$ .

2.1step 1.1F2algebra

Every vector has finite infinity-pole order, so step 1.1 gives $M \cap L_{0} = Z [q] \otimes_{Z} E$ . Clearing a vector's zero-pole order by a power of $q$ gives $M = A E ≅ A \otimes_{Z} E$ . Also $E \cap q^{- 1} L_{\infty} = 0$ : if $e$ lies there, then $q e \in E \cap q L_{0} = 0$ . In a Laurent expansion of $x \in M \cap L_{\infty}$ , a largest positive exponent $n$ would give, after multiplication by $q^{- n}$ , a nonzero coefficient in $E \cap q^{- 1} L_{\infty}$ ; hence no such exponent occurs. Thus $M \cap L_{\infty} = Z [q^{- 1}] \otimes_{Z} E$ , with infinity residue $E$ .

2.2F1step 1.2algebra

For (3), the assumed canonical isomorphism $A \otimes E_{N} \to N$ forces $E_{N}$ to inject into both chart residues. Indeed, if $e \in E_{N} \cap q L_{0}$ , then $q^{- 1} e \in E_{N}$ as well, contradicting Laurent independence unless $e = 0$ ; the mirror argument handles infinity. Apply (2) to $N$ in its field span, with the induced lattices, to obtain its balancedness and $N = (N \cap L_{0}) + (N \cap L_{\infty})$ . If $x = l_{0} + n_{0} = l_{\infty} + n_{\infty}$ lies in $M \cap (L_{0} + N) \cap (L_{\infty} + N)$ , write $n_{0} - n_{\infty} = a + b$ with $a \in N \cap L_{0}$ and $b \in N \cap L_{\infty}$ . Then $x - (n_{0} - a) = l_{0} + a = l_{\infty} - b$ is a simultaneous lift. Thus this intersection is $N + E_{M}$ .

3.1step 1.1step 2.1F1algebra

The injection $E \to L_{0} / q L_{0}$ extends injectively over $Q$ , by clearing integer denominators. A rational basis $e_{1}, \dots, e_{t}$ of $Q E$ has field-independent images: a rational-function dependence, after clearing denominators, would be a polynomial dependence, contradicting step 1.1. Since $M = A E$ spans $V$ , this family is a field basis of $V$ , so $t = \dim V$ . Its residues are a rational basis of $L_{0} / q L_{0}$ ; expressing the $e_{j}$ in a free chart basis yields a square matrix invertible modulo $q$ , hence with determinant a unit in $A_{0}$ . Its adjugate gives $L_{0} = A_{0} E$ and the asserted tensor isomorphism. The same argument uses the infinity injection in step 2.1 to give $L_{\infty} = A_{\infty} E$ . This proves (1), including its finite-free conclusions.

3.2step 1.2step 2.2algebra

First restrict to a finitely generated subgroup $F^{'} \subseteq F$ and $M^{'} = N + A φ (F^{'})$ . The quotient-residue injection makes $F^{'}$ torsionfree, hence a finite free abelian group. Modify the images of a finite basis of $F^{'}$ by elements of $N$ , using step 2.2, to obtain simultaneous lifts. Together with $E_{N}$ they generate $M^{'}$ . Their direct sum injects into $L_{0} / q L_{0}$ : a vanishing residue first has zero $F^{'}$ coordinate by the injection into $(L_{0} + Q N) / (q L_{0} + Q N)$ , and then has zero $E_{N}$ coordinate by step 2.2. The infinity proof is identical. Criterion (2) now gives $E_{M^{'}} ≅ E_{N} \oplus F^{'}$ and balancedness of $M^{'}$ .

4.1step 3.1step 3.2algebra∎

Every element of $M$ belongs to some such $M^{'}$ , because its expression modulo $N$ uses finitely many images of $F$ . The preceding balancedness proves injectivity and surjectivity of the residue map for $M$ element by element. Its residue decompositions also prove the stated exact sequence: the kernel of the quotient-residue map is precisely the residue of $N$ , and its image is precisely the image of $F$ . When $F$ and $E_{N}$ are finite free, take $F^{'} = F$ in step 3.2; then $E_{M} ≅ E_{N} \oplus F$ is finite free and (1) makes $M$ free over $A$ . This proves (3) and completes the lemma.

Source note

Kashiwara, On crystal bases (1991), Lemmas 7.1.1–7.1.2, printed pp. 509–512, supply the integral chart and relative criteria. Here $Q N$ means the rational span $Q \otimes_{Z} N$ inside $V$ , as in that source. The proof uses bounded pole orders; it never assumes that an infinity lattice is $q$ -stable or that a $Z [q]$ -intersection is an $A_{0}$ -submodule.

Depends on

Balanced triples over the two charts of $\mathbb P^1$ and the globalization map

Used by

Dependency tree · two levels

2 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)
Kyeonghoon Jeong, Seok-Jin Kang and Masaki Kashiwara, Crystal Bases for Quantum Generalized Kac-Moody Algebras, arXiv:math/0305390 (standard reference, not scraped)

The balanced-triple linear algebra over P1P1