Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

Kac moody relation module embeds in verma modules and obeys the casimir constraint

Statement

For symmetrizable A, the adjoint relation module r−/[r−,r−] embeds as a g-module in ⨁iMA(−αi). Each r± is generated as an ideal of n~± by its homogeneous spaces of degrees ±α, where α∈Q+∖({0}∪Π) and (α,α)=2(ρ,α).

Facts & Assumptions

Given: The maximal ideal r=r−⊕r+ and the standard form with rho(h_i)=1.

[F1]

The quotient kernel and augmentation intersection are known. (Enveloping quotient kernels and augmentation intersections).

[F2]

Objects of O are generated under the negative algebra by primitive vectors. (Bounded above kac moody weight modules are generated by primitive vectors).

[F3]

The Casimir acts on a highest module by the highest-weight scalar. (Generalized kac moody casimir is central and scalar on highest weight modules).

[F4]

The universal negative half is free. (Contragredient algebra has a triangular decomposition).

[F5]

Both Verma modules have PBW freeness and the highest-vector universal property. (Kac moody verma module).

Proof

1.1F4F5given

Put T=U(n~−), the free associative algebra on the fi by F4 and its free-Lie construction. In M~(0)=Tv~, the augmentation subspace T0v~ is a submodule: its quotient is the trivial one-dimensional module. The vectors fiv~ are highest of weight −αi, because ejfiv~=δijhiv~=0. The last-letter decomposition T0=⨁iTfi and F5 therefore identify this submodule with ⨁iM~(−αi), not merely a quotient.

2.1F5step 1.1

Let V=U(g)⊗U(g~)(T0v~). Associativity of balanced tensor products (the maps a⊗(b⊗1)↦ab⊗1 and its reverse) and F5 identify V=⨁iMA(−αi). Define ℓ(a)=1⊗av~ for a∈r−. For x∈g~, xv~∈T0v~, since the quotient in step 1.1 is trivial. Therefore ℓ([x,a])=1⊗xav~−1⊗axv~=π(x)⊗av~−π(a)⊗xv~=π(x)ℓ(a). In particular commutators in r− are killed. The two ideals r+ and r− commute because their bracket lies in their zero intersection. Hence the source modulo its self-commutator carries the adjoint g-action, and ℓ factors through a module map on it.

3.1F1F5step 1.1step 2.1

Write a=∑iuifi using its unique associative last-letter coefficients. The degree-one part of r− is zero, since the simple fi survive, so all ui∈T0. In the PBW identifications, ℓ(a)=(π(ui)v−αi)i. By F5, this is zero exactly when each π(ui)=0. F1 gives ui∈r−T, so a∈r−T0, and F1 then gives a∈r−∩r−T0=[r−,r−]. The reverse kernel inclusion was proved in step 2.1. Thus the module map is injective. These are associative coefficients, not adjoint coefficients.

4.1F2F3F5step 3.1

Each summand MA(−αi) has Casimir scalar (αi,αi)−2(ρ,αi)=2di−2di=0 by F3. Hence Ω=0 on the embedded relation module and each of its subquotients; the pointwise formula respects submodules. The relation module belongs to O, being a submodule of a finite sum of the Verma modules of F5. A primitive vector of weight −α has a nonzero highest image in a quotient. F3 applied to that image gives 0=(α,α)−2(ρ,α). Its degree is neither zero nor simple, as r− has neither component. F2 proves generation of the abelianized relation module by these degrees.

5.1step 4.1∎

Let K be the ideal of n~− generated by all the indicated full homogeneous spaces of r−. Step 4.1 says r−=K+[r−,r−]. If the positively regraded Lie algebra L=r−/K were nonzero, choose its least positive height m. Every nonzero bracket in L has height at least 2m, so Lm cannot lie in [L,L]. This contradicts L=[L,L]. Thus K=r−. The sign-changing involution gives the positive assertion with the identical equation on α.

Sources

Source comparison: Kleshchev, Proposition 9.3.4, pp.124–125; corrected associative last-letter coefficients and augmentation proof.

Depends on

Used by

Dependency tree · two levels

12 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