Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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 full algebraic Verma dual is too large

Statement refuted

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=hn+. Write Q+=iZ0αi, μλ when λμQ+, and wλ=w(λ+ρ)ρ.

False claim: replacing the restricted sum in Chevalley duality by the full algebraic dual always gives an object of O.

For sl2 and any λC, the full Chevalley-twisted dual HomC(M(λ),C) is not h-semisimple and hence is not in O.

Facts & Assumptions

Given: The setting above and the hypotheses in the statement refuted.

[F1]

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=hn+. Write Q+=iZ0αi, μλ when λμQ+, and wλ=w(λ+ρ)ρ. For an h-semisimple module M with finite-dimensional weight spaces, its restricted Chevalley dual is D(M)=μhMμ,(xφ)(m)=φ(τ(x)m)(xU(g)). Here each functional is extended by zero on the other weight spaces and τ is the fixed anti-involution of def-chevalley-contravariant-form. In particular τ(h)=h and D(M)μ=Mμ. A map f:MN induces D(f):D(N)D(M) by precomposition. The action law follows from τ(xy)=τ(y)τ(x); a root vector of weight α sends Mμ to Mμ+α, so the restricted sum is stable. This is a complex-linear algebraic dual, with no conjugation. Ordinary Lie-module duality has a minus sign and reverses weights; twisting that dual by the Lie automorphism xτ(x) gives the convention used here. (Restricted Chevalley dual)

[F2]

For λh, the Verma module is the induced g-module M(λ):=U(g)U(b)Cλ, where U(g) is the quotient algebra of def-universal-enveloping-algebra-as-a-tensor-quotient and Cλ is def-one-dimensional-borel-module-of-weight-lambda. Write vλ:=1cλ. Thus M(λ) is the quotient of U(g) by the left ideal generated by x for xn+ and hλ(h) for hh; in particular, n+vλ=0 and hvλ=λ(h)vλ. (Verma modules)

[F3]

The weights of M(λ) are exactly λβ for βQ+; every weight space is finite dimensional, and M(λ)λ=Cvλ. (Weights of a Verma module lie below lambda)

Counterexample

1.1

The induced Verma model has basis vk=fkvλ for k0 and hvk=(λ2k)vk. Define φ(vk)=1 for all k and extend linearly. This is an algebraic functional because vectors of M(λ) are finite sums, although its nonzero weight coordinates are infinite. On the full twisted dual use the same formula (hφ)(v)=φ(hv) as for restricted duality.

F1F2F3construct
2.1

For every polynomial p, (p(h)φ)(vk)=p(λ2k). The values λ2k are pairwise distinct over C, so a polynomial annihilating φ has infinitely many distinct zeros and must be the zero polynomial. Thus the C[h]-orbit of φ is infinite dimensional. A vector in a direct sum of eigenspaces has only finitely many eigencomponents and is annihilated by the product of their linear eigenvalue polynomials. Therefore this full dual cannot be a weight module.

algebrastep 1.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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