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.

Upper and lower global bases are dual and crystal compatible

Statement

Let $M$ be $U^{-}$ or $V (λ)$ with the balanced triple and lower global basis of The lower global basis of $U_{q}^{-}$ and of a highest weight module, and let $M_{A}^{\lor}$ , $L_{0}^{\lor}$ , $L_{\infty}^{\lor}$ , $G^{u p}$ , $ψ^{\lor}$ and the upper Kashiwara operators be as in The upper (form-dual) global basis and the required perfectness of the integral pairing. Then, for every finite root or label component:

(i) the restricted graded integral dual $M_{A}^{\lor}$ has the actual $A$ -basis ${G^{u p} (b)}$ dual to ${G (b)}$ , and $B : (M_{A}^{\lor})_{μ} \times (M_{A})_{μ} \to A$ is perfect; globally the bases form direct sums, which is restricted graded perfectness and not an identification with the full product ${Hom}_{A} (M_{A}, A)$ ;

(ii) the dual charts are $L_{0}^{\lor} = ⨁_{b} A_{0} G^{u p} (b)$ and $L_{\infty}^{\lor} = ⨁_{b} A_{\infty} G^{u p} (b)$ , and their balanced $Z$ -intersection is $⨁_{b} Z G^{u p} (b)$ , so the dual triple is integrally balanced; at $0$ one has $L_{0}^{\lor} = L_{0}$ and the residue of $G^{u p} (b)$ is $b$ , while at infinity its residue is the dual of the lower infinity-chart class in the dual infinity chart;

(iii) the upper bar $ψ^{\lor}$ fixes each $G^{u p} (b)$ ;

(iv) the upper operators satisfy the exact mixed adjunctions $B ({\tilde{f}}_{i}^{l o w} u, v) = B (u, {\tilde{e}}_{i}^{u p} v)$ and $B ({\tilde{e}}_{i}^{l o w} u, v) = B (u, {\tilde{f}}_{i}^{u p} v)$ ; their reductions at $0$ equal the lower crystal operators and give the same crystal set $B$ ;

(v) for a divided module string $F_{i}^{(n)} v$ of top rank-one weight $a$ , with $d_{a, n} = q_{i}^{n (a - n)} {(\binom{a}{n})}_{i}$ , the upper operator ${\tilde{e}}_{i}^{u p}$ at position $n \geq 1$ multiplies the preceding divided position by $d_{a, n} / d_{a, n - 1} = q_{i}^{a - 2 n + 1} [a - n + 1]_{i} / [n]_{i}$ , and ${\tilde{f}}_{i}^{u p}$ at position $n < a$ multiplies the next by the reciprocal $d_{a, n} / d_{a, n + 1}$ ; for a half string with $e_{i}^{'} v = 0$ , with $d_{n} = q_{i}^{- n (n - 1) / 2} / [n]_{i}! = 1 / [n]_{q_{i}^{2}}!$ , the ratios are $1 / [n]_{q_{i}^{2}}$ and $[n + 1]_{q_{i}^{2}}$ . All admissible ratios are units congruent to $1$ in $A_{0}$ , so unweighted lower adjunction holds modulo $q$ but generally not exactly over $Q (q)$ . No equality of upper and lower integral bases, even in symmetric type, is implied.

Facts & Assumptions

Given: The lower global bases, charts and balancedness of the integral globalization theorem (Bar invariance, congruence and uniqueness of the lower global basis, The highest weight and negative half integral crystal triples are balanced); the upper definitions of The upper (form-dual) global basis and the required perfectness of the integral pairing; the norm and residue theory of Integral residues of the negative half: freeness, the crystal basis and the form characterization and Crystal lattice polarizations are perfect at $q = 0$ ; the bar and duality stability of The bar involution and the contravariant anti-involution preserve $U_{A}$ .

[F1]

Upper definitions (The upper (form-dual) global basis and the required perfectness of the integral pairing): on each finite component the form $B$ is nondegenerate over $Q (q)$ , and $G^{u p} (b)$ is the inverse-Gram dual of $G (b)$ ; $M_{A}^{\lor}$ , $L_{0}^{\lor}$ , $L_{\infty}^{\lor}$ are restricted direct sums, so only finite-dimensional linear algebra in each component is used.

[F2]

Lower basis and charts (Bar invariance, congruence and uniqueness of the lower global basis): $G (B)$ is an $A$ -basis of $M_{A}$ , an $A_{0}$ -basis of $L_{0}$ and an $A_{\infty}$ -basis of $L_{\infty}$ , with balanced intersection $⨁_{b} Z G (b)$ ; the global extension is a direct sum over finite weight components.

[F3]

Zero-chart polarization (Crystal lattice polarizations are perfect at $q = 0$ ): the pairing is $A_{0}$ -valued on $L_{0}$ , its crystal residues are orthonormal, and its Gram matrix in the lower global chart basis is the identity modulo $q$ . Consequently $L_{0}^{\lor} = L_{0}$ . The integral half-residue refinement is Integral residues of the negative half: freeness, the crystal basis and the form characterization; no $A_{0}$ -valuedness on the whole Laurent lattice is inferred.

[F4]

String inputs (Divided-power commutation and the simple $U_{q_{i}} ({s l}_{2})$ string modules, Kashiwara's skew derivations $e_{i}^{'}$ and $e_{i}^{''}$ on the negative half): admissible module strings have $E_{i} F_{i}^{(n)} v = [a - n + 1]_{i} F_{i}^{(n - 1)} v$ for $E_{i} v = 0$ , and $σ (F_{i}) = q_{i}^{- 1} K_{i} E_{i}$ (The contravariant form on an integrable highest weight module). In the half, $B (F_{i} x, y) = B (x, e_{i}^{'} y)$ and $e_{i}^{'} F_{i}^{(n)} v = q_{i}^{- (n - 1)} F_{i}^{(n - 1)} v$ for $e_{i}^{'} v = 0$ . Step 1.2 derives the string pairing factors and adjoint ratios from these identities.

[C1]

Choice: declared via The Axiom of Choice and used only through the grand loop and perfect-polarization suppliers of [F2] and [F3]; the dual-basis, chart and adjunction computations are choice-free.

Proof

technique · direct

1.1F1F2

The dual basis on each finite component. Fix a finite weight component with lower basis $g_{b} = G (b)$ . The Gram matrix $C = (B (g_{b}, g_{c}))$ is invertible over $Q (q)$ since $B$ is nondegenerate there, and we define $g_{b}^{u p}$ by $B (g_{b}, g_{c}^{u p}) = δ_{b c}$ , i.e. $g^{u p} = C^{- 1}$ in the dual basis. For arbitrary $x$ in the component, its coordinates in the dual family are exactly $B (g_{b}, x)$ . Hence $x \in M_{A}^{\lor}$ if and only if all those coordinates lie in $A$ , proving that the $g_{b}^{u p}$ form an $A$ -basis of the restricted dual and that the pairing is perfect on the component; the argument needs only that $C$ is field-invertible, not that $\det C$ is a unit of $A$ , and the global statement follows by restricted direct sum.

1.2F1F4algebra

String pairings and adjoints. On a module string of top weight $a$ , contravariance and $F_{i}^{(n)} = [n]_{i}^{- 1} F_{i} F_{i}^{(n - 1)}$ give $B (F_{i}^{(n)} v, F_{i}^{(n)} w) = q_{i}^{a - 2 n + 1} [a - n + 1]_{i} / [n]_{i}$ times the preceding-position pairing. Iteration from the top gives $d_{a, n} B (v, w)$ . Distinct rank-one highest weights give orthogonal strings: move enough $F_{i}$ factors across the pairing to apply more $E_{i}$ factors than the shorter position permits. Within one top space the arbitrary pairing $B (v, w)$ is retained; different top vectors are not presumed orthogonal. In the half the same argument with the $e_{i}^{'}$ adjunction gives $d_{n} B (v, w)$ and orthogonality of unequal string positions. Thus the adjoint of the lower raising-position shift sends position $n \geq 1$ to position $n - 1$ with factor $d_{a, n} / d_{a, n - 1}$ , and the adjoint of the reverse shift sends $n < a$ to $n + 1$ with factor $d_{a, n} / d_{a, n + 1}$ ; the half calculation gives its stated ratios. These prove the exact mixed adjunctions and (v).

2.1F1F2step 1.1

Dual charts and the balanced dual triple. The same coordinate criterion, applied over $A_{0}$ and $A_{\infty}$ , shows $L_{0}^{\lor} = ⨁_{b} A_{0} G^{u p} (b)$ and $L_{\infty}^{\lor} = ⨁_{b} A_{\infty} G^{u p} (b)$ ; the balanced $Z$ -intersection of the dual triple is $⨁_{b} (A \cap A_{0} \cap A_{\infty}) G^{u p} (b) = ⨁_{b} Z G^{u p} (b)$ , and the dual globalization map is the inverse of the same coordinate evaluation. This proves integral balancedness of the dual triple and its chart descriptions.

2.2F1F2F3step 1.1

Residues and the upper bar. Since $B (g_{b}, g_{c}) \equiv δ_{b c} m o d q$ by [F3], the inverse-Gram family satisfies $G^{u p} (b) \equiv b$ in the zero chart, and [F3]'s perfection gives $L_{0}^{\lor} = L_{0}$ ; at infinity the pairing with the lower chart basis defines the residue class of $G^{u p} (b)$ in the genuine dual infinity chart, which is the dual of the lower class and is not asserted to be congruent modulo $q^{- 1}$ in $L_{\infty}$ . Because $B (g_{b}, g_{b}) = 1$ modulo $q$ and the residue pairing is symmetric and orthonormal, the defining relation $B (ψ u, ψ^{\lor} v) = \overline{B (u, v)}$ gives $ψ^{\lor} G^{u p} (b) = G^{u p} (b)$ : expanding in the dual basis, the left side pairs against $g_{c}$ as $\overline{B (g_{c}, G^{u p} (b))} = δ_{b c}$ , the same values as $G^{u p} (b)$ itself. This proves (ii) and (iii).

2.3F3F4step 1.2

Positivity and crystal reduction. With the module scalars $d_{a, n} / d_{a, n - 1} = q_{i}^{a - 2 n + 1} [a - n + 1]_{i} / [n]_{i}$ for $1 \leq n \leq a$ and the half scalars $1 / [n]_{q_{i}^{2}}$ and $[n + 1]_{q_{i}^{2}}$ , every admissible ratio is a unit congruent to $1$ in $A_{0}$ ; therefore the upper operators preserve the zero chart, reduce modulo $q$ to the same partial-inverse moves on $B$ , and give the same crystal set $B$ . Since the ratios are generally not equal to $1$ over $Q (q)$ , unweighted adjunction holds only modulo $q$ , and no upper/lower basis equality follows.

3.1step 2.1step 2.2step 2.3C1∎

Conclusion. Step 1.1 and step 2.1 prove the dual basis, perfectness and dual charts; step 2.2 proves the residue statements and upper-bar invariance; steps 1.2 and 2.3 prove the exact mixed adjunctions, unit positivity and crystal compatibility. The Choice use is confined to [C1].

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

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)
Jonathan Brundan, Dual Canonical Bases and Kazhdan–Lusztig Polynomials, arXiv:math/0509700v2 (Transform. Groups 14 (2009), 535–558) (standard reference, not scraped)