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.

O is not closed under arbitrary tensor products

Statement refuted

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=h⊕n+. Write Q+=∑iZ≥0αi, μ≤λ when λ−μ∈Q+, and w⋅λ=w(λ+ρ)−ρ.

False claim: the tensor product of two objects of O always belongs to O.

For sl2, X=M(0)⊗M(0) with diagonal action has support −2Z≥0, weight multiplicities dim⁡X−2k=k+1, and locally nilpotent e action, but is not finitely generated over U(g).

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=h⊕n+. Write Q+=∑iZ≥0αi, μ≤λ when λ−μ∈Q+, and w⋅λ=w(λ+ρ)−ρ. The BGG category O is the full subcategory of left U(g)-modules M satisfying all three conditions: M is finitely generated; M=⨁μ∈h∗Mμ where Mμ={v:hv=μ(h)v for all h∈h}; and U(n+)v is finite dimensional for each v∈M. Its morphisms are all g-linear maps. The zero module is included, generated by the empty set. The enveloping and triangular conventions are those of thm-pbw-ordered-monomial-basis-for-the-enveloping-algebra and thm-triangular-decomposition-from-a-chosen-positive-root-system. (The classical BGG category O)

[F2]

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=h⊕n+. Write Q+=∑iZ≥0αi, μ≤λ when λ−μ∈Q+, and w⋅λ=w(λ+ρ)−ρ. Every M∈O is a quotient of a module with a finite Verma flag. Consequently it has a finite filtration whose nonzero factors are quotients of Verma modules, and is finitely generated over U(n−). The empty filtration is allowed for zero. No truncation hypothesis is needed, and a Verma flag of M itself is not asserted. (Finite filtrations by highest-weight quotients)

[F3]

Let x1,…,xr be an ordered basis of a finite-dimensional complex Lie algebra g. Then the monomials x1a1x2a2⋯xrar(ai∈N0) form a basis of U(g). In particular, multiplication identifies gr⁡U(g) with the symmetric algebra S(g) on the symbols of the xi. (PBW gives an ordered monomial basis for the enveloping algebra)

Counterexample

1.1F3algebra

The Verma PBW bases identify X with C[x,y], where xiyj corresponds to fiv0⊗fjv0. Its h-weight is −2(i+j), so its weight multiplicities are k+1. The diagonal f acts by multiplication by x+y. Each tensor of two basis vectors is killed by a high enough power of the diagonal e: expanding (e⊗1+1⊗e)N, every term vanishes once N>i+j. Hence e acts locally nilpotently on X.

2.1F1F2step 1.1

If X were finitely generated over U(g), its weight decomposition and local e-finiteness would put it in O. F2 then implies it is finitely generated over U(n−)=C[f], hence over C[x+y] in the displayed model.

3.1algebrastep 2.1∎

But C[x,y]/(x+y)C[x,y]≅C[x] is infinite dimensional over C. A module generated by r<∞ elements over C[x+y] has quotient by x+y generated by their r images over C, so that quotient has dimension at most r. This proves that X is not finitely generated and therefore is not in O, although each factor is cyclic with locally nilpotent e and is a weight module.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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