Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge 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.

A Verma module need not be projective in its block

Statement refuted

Every Verma module lying in an integral block of O is projective in that block; in particular, in the regular integral block with labels m and −m−2 both Verma modules Δ(m) and Δ(−m−2) are projective.

Facts & Assumptions

Given: The Axiom of Choice, g=sl2, an integer m≥0, and the regular integral block Cm with labels m and −m−2, ordered by −m−2≤m.

[F1]

For every n≥0 the regular integral block Cn has simple labels n and −n−2 with −n−2<n, standards Δ(n)=M(n) and Δ(−n−2)=M(−n−2)=L(−n−2), and nonsplit sequence 0→L(−n−2)→M(n)→L(n)→0; this is the rank-one computation of the parent example, applied here with n=m (The two projectives in the principal sl2 block, Antidominant regular Verma modules are simple).

[F2]

Since m is maximal in the finite downward-closed ideal Cm of its linkage class, M(m) is projective in OCm and in O (A maximal-label Verma is projective in its truncation, Dominant integral weights are maxima of their Weyl orbits, Truncation at a finite downward-closed ideal of a linkage class).

[F3]

The projective cover P(−m−2) of L(−m−2) exists, is indecomposable with head L(−m−2), is Verma-filtered, and BGG reciprocity gives (P(−m−2):Δ(μ))=[Δ(μ):L(−m−2)]; composition factors of standards from other linkage classes are disjoint from the block Cm (Category O has enough projectives, Projective covers in O are indecomposable and unique, Projectives in category O have finite Verma flags, BGG reciprocity, Central-character summands refine into linkage blocks).

Counterexample

Assume the Axiom of Choice (The Axiom of Choice).

Proof technique: direct: the maximal label is projective, the minimal label is the head of a nonsplit two-step cover.

1.1F1F2

By [F2] the maximal-label Verma Δ(m)=M(m) is projective in OCm (and in O). By [F1] the other Verma is simple, Δ(−m−2)=M(−m−2)=L(−m−2), and the composition factors of M(m) are L(−m−2) and L(m), each with multiplicity one.

1.2F1F3

By [F3] the cover P(−m−2) is Verma-filtered and BGG reciprocity gives (P(−m−2):Δ(μ))=[Δ(μ):L(−m−2)], which is 1 for μ=−m−2 and μ=m by [F1] and 0 for all other μ because L(−m−2) lies in the block Cm and other linkage classes contribute no composition factors to it. Hence every Verma flag of P(−m−2) has exactly the two factors Δ(m) and Δ(−m−2), each once.

2.1F3step 1.2

In such a flag the bottom factor cannot be Δ(−m−2): then P(−m−2) would have Δ(m)=M(m) as a quotient, and composing with M(m)↠L(m) would exhibit L(m) as a simple quotient, contradicting that P(−m−2) has the unique simple quotient L(−m−2) with m≠−m−2. So there is a subobject Δ(m)⊆P(−m−2) with quotient Δ(−m−2), giving the short exact sequence 0→Δ(m)→P(−m−2)→Δ(−m−2)→0; it is nonsplit because projective covers are indecomposable by [F3].

3.1step 1.1step 2.1∎

The Verma Δ(−m−2) is not projective in the block Cm: if it were, the epimorphism P(−m−2)↠Δ(−m−2) would split, contradicting the nonsplitness of step 2.1. Since Δ(m) is projective by step 1.1, projectivity indeed depends on the position of the highest weight in the linkage poset, refuting the statement.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

58 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