Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08
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 generic quantum halves form a Drinfeld–Jimbo crossed double

Statement

Fix a finite symmetrizable Cartan datum over k=Q(q), with qi=qdi and Ki=Kdihi. Let A+ and A− be the independently presented k-algebras on ei and fi, respectively, modulo their separate symmetric quantum Serre relations, and let C=k[P∨] have basis Kh, h∈P∨. Then the vector space D=A−⊗kC⊗kA+ carries a unique associative unital algebra structure in which a−⊗Kh⊗a+ equals the product of the three embedded factors, the factors retain their algebra structures, and Khei=qαi(h)eiKh,Khfi=q−αi(h)fiKh,[ei,fj]=δijKi−Ki−1qi−qi−1. This is the Drinfeld–Jimbo crossed double. Its normal-factor multiplication map to the presented algebra Uq(g) of The Drinfeld-Jimbo quantized enveloping algebra by generators and relations is an algebra isomorphism, whose inverse sends Ei,Fi,Kh to the indicated factor generators. Thus all three abstract factor maps are injective; their images are the subalgebras of Positive, negative and toral quantum subalgebras and their root gradings.

In the presentation U~ obtained by omitting both Serre families, the halves T± are free, the toral factor is C, and multiplication identifies U~=T−⊗C⊗T+. Every Serre element satisfies [Fk,Sij+]=[Ek,Sij−]=0. Writing I±⊴T± for the separate Serre ideals, the full Serre ideal of U~ is exactly I−⊗C⊗T++T−⊗C⊗I+. No nonsingularity of the Cartan matrix and no choice principle is required.

Facts & Assumptions

Given: A finite symmetrizable Cartan datum and its Drinfeld–Jimbo presentation.

[F1]

The toral, toral-action and mixed relations give the Serre-free presentation; adding the separate Serre sums gives Uq(g), and assignments satisfying these relations extend uniquely (The Drinfeld-Jimbo quantized enveloping algebra by generators and relations, Universal property of the tensor algebra, A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring).

[F2]

The integral weight characters are additive, qi=qdi, and qjaji=qiaij by symmetrizability (Symmetrizable Cartan data for quantum groups).

[F3]

For t=qi, the symmetric Gaussian coefficients satisfy CN,r[N−r]i=CN,r+1[r+1]i and ∑s=0N(−1)sCN,st±(N−1)s=0 for N≥1. The first identity is factorial cancellation and the second follows from the Gauss formula and its inverse-parameter substitution (Quantum integers, factorials, Gaussian binomials and divided powers at qi, The quantum Pascal recurrences, the Gauss product formula and Gaussian integrality).

[F4]

Tensoring quotient maps is surjective and has kernel the sum of the factor kernels, by repeated right exactness (Tensoring is right exact).

[F5]

The positive, negative and toral subalgebras are the generated images of the corresponding presentation generators (Positive, negative and toral quantum subalgebras and their root gradings).

Proof

1.1F1F2construct

Put ci=(Ki−Ki−1)/(qi−qi−1). In the free Serre-free presentation reduce EiFj to FjEi+δijci, EiKh to q−αi(h)KhEi, KhFj to q−αj(h)FjKh, KhKg to Kh+g, and K0 to 1. For each monomial use the lexicographic triple consisting of the number of E/F letters, the number of inverted type pairs for F<K<E, and the number of toral letters. Every resulting term decreases this triple: the mixed correction decreases the first coordinate, the other mixed or crossing terms decrease inversions, and toral merging or deletion decreases inversions or the final coordinate. Each rule has finitely many outputs, so the finitely branching reduction tree terminates; an infinite tree of arbitrarily deep descendants would give an infinite decreasing path by choosing its first such child at each stage. The irreducible words are precisely Fi1⋯FiaKhEj1⋯Ejb, with K0 interpreted as the empty toral factor.

1.2F1F2F3algebra

Fix i≠j, set t=qi, a=aij, N=1−a, and Cs=(Ns)i, so Sij+=∑s(−1)sCsEiN−sEjEis. Expanding the commutator in each position and moving toral factors to the right gives [Fi,Eim]=−[m]iEim−1(tm−1Ki−t−(m−1)Ki−1)/(t−t−1) for m≥1: the two geometric sums are ∑r=0m−1t±2r=t±(m−1)[m]i. For k≠i,j, the commutator [Fk,Sij+] is zero because every letter commutes with Fk. For k=j, only the Ej contributes, and moving Kj past the last s copies of Ei gives [Fj,Sij+]=−EiNqj−qj−1((∑s(−1)sCstas)Kj−(∑s(−1)sCst−as)Kj−1)=0. The crossing uses qjaji=ta from [F2], and both sums vanish by [F3] because a=1−N.

2.1F1F2step 1.1algebra

The overlapping reductions are KhKgKl, EiKhKg, KhKgFj, and EiKhFj, together with deletion of K0 against an adjacent crossing or toral product. The first three give respectively Kh+g+l, q−αi(h+g)Kh+gEi, and q−αj(h+g)FjKh+g along both routes. In the fourth, the two routes give the common term q−αi(h)−αj(h)FjKhEi and corrections δijq−αi(h)Khci and δijq−αj(h)ciKh; they agree since the toral elements commute and i=j whenever the correction is present. The zero-index cases and a toral sum h+g=0 agree by character additivity and αi(0)=0. There is no overlapping pair of EF rules, since its shared letter would have to be both E and F. Disjoint reductions commute by distributivity. Inducting on the decreasing triple in step 1.1, these joined first reductions therefore have the same final normal form in every word context. The linear normal-form map kills each relation multiplied on the left and right by arbitrary words, while every word minus its normal form lies in the relation ideal. It consequently induces inverse linear maps between U~ and the freely based normal-word space. This proves the full Serre-free tensor decomposition, including injectivity on arbitrary finite sums.

2.2F1F2F3step 1.2algebra

For k=i, expand in the left and right Ei blocks using step 1.2. The left-block term with s=r and right-block term with s=r+1 both have positive word EiN−1−rEjEir. In the left-block term, the exponent after moving Ki to the right is N−r−1+a+2r=r, since N−1+a=0; the inverse toral exponent is −r. The right-block term has those same exponents. Thus [Fi,Sij+]=−1t−t−1∑r=0N−1(−1)r(Cr[N−r]i−Cr+1[r+1]i)EiN−1−rEjEir(trKi−t−rKi−1)=0. The coefficient identity is [F3], including both endpoints. The assignment ω(Ei)=Fi, ω(Fi)=Ei, ω(Kh)=K−h is an involutive algebra map of the Serre-free presentation: toral actions reverse their signs, and both the mixed commutator and ci change sign. Applying it proves [Ek,Sij−]=0. Toral conjugation of either Serre generator is scalar, since its color degree is homogeneous.

3.1F1F2step 2.1step 1.2step 2.2algebra

In the normal-word space put X=I−CT++T−CI+. It contains the Serre generators and is a two-sided ideal. Same-side multiplication and toral multiplication preserve its two summands, using homogeneous toral conjugation. For the remaining crossed multiplications, expanding [Fk,w] for a positive word w yields positive-word/toral terms, and expanding [Ek,w] for a negative word yields negative-word/toral terms, by the mixed relation. If w=uSij+v, the Leibniz rule gives [Fk,w]=[Fk,u]Sij+v+uSij+[Fk,v] because the middle commutator vanishes by steps 1.2 and 2.2. Moving the resulting toral factors past the homogeneous Serre sum preserves its ideal. Hence [Fk,I+]⊆CI+, and similarly [Ek,I−]⊆I−C. When moving a crossed generator through an arbitrary normal product, these inclusions show that every term still belongs to X; multiplication in the other half only multiplies the existing ideal factor. This checks closure under all Ek,Fk,Kh on both sides. Conversely each summand of X lies in the ambient two-sided Serre ideal, by its definition. Therefore X equals that ideal, with the exact tensor-factor description claimed.

4.1F1F4F5step 1.1step 2.1step 3.1algebra∎

By [F4], the tensor quotient (T−/I−)⊗C⊗(T+/I+) is the quotient of T−⊗C⊗T+ by precisely X. Steps 2.1 and 3.1 therefore identify it linearly with U~/X=Uq(g), proving genuine tensor injectivity. Transport the associative quotient multiplication to this tensor space to define D. Its factor products, normal-factor products and cross-relations are as stated, and the factor embeddings are injective because 1 survives both homogeneous positive-height Serre ideals. Conversely any multiplication with those properties is determined by repeatedly using the crossing rules to rewrite a product of two normal tensors; these rules terminate by step 1.1. Thus the algebra structure is unique. Its generator map to Uq(g) and its inverse respect the defining relations by [F1] and the factor Serre relations, so are mutually inverse algebra homomorphisms. Their factor images are exactly [F5]. This proves all assertions.

Depends on

Used by

Dependency tree · two levels

38 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