TheoremStatement: Literature-sourcedProof: 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.

Projectives in category O have finite Verma flags

Statement

Assume the Axiom of Choice (The Axiom of Choice). Every projective object of $O$ has a finite Verma flag (Finite Verma flags and their multiplicities).

More precisely, each projective cover $P (μ)$ produced by Category O has enough projectives is a direct summand of the projective object ${pr}_{C} (E \otimes M (λ))$ of Finite-dimensional tensoring reaches every simple of a linkage class, which is a direct summand of $E \otimes M (λ)$ ; a general projective object has finite length, hence is a finite direct sum of indecomposable projectives, each of which is a projective cover of its simple head.

Facts & Assumptions

Given: The Axiom of Choice, the projective covers $P (μ) ↠ L (μ)$ produced by the enough-projectives theorem, and an arbitrary projective object $P \in O$ .

[F1]

The cover $P (μ)$ is (isomorphic to) a direct summand of the projective object ${pr}_{C} (E \otimes M (λ))$ of Finite-dimensional tensoring reaches every simple of a linkage class, and ${pr}_{C} (E \otimes M (λ))$ is a direct summand of $E \otimes M (λ)$ in the block decomposition (Finite-dimensional tensoring reaches every simple of a linkage class, Category O has enough projectives, Projective covers in O are indecomposable and unique).

[F2]

$E \otimes M (λ)$ is Verma-filtered, and every direct summand of a Verma-filtered object of $O$ is Verma-filtered (Finite-dimensional tensoring preserves Verma flags, Direct summands of Verma-filtered objects are Verma-filtered).

[F3]

Every object of $O$ has finite length and is a finite direct sum of indecomposable objects; an indecomposable projective is a projective cover of its simple head (Every object of O has finite length, Fitting decomposition in a finite-length abelian category, Projective covers in O are indecomposable and unique).

Proof

technique · direct: each projective cover is a direct summand of a tensored Verma, and a general projective splits into finitely many such covers

1.1F1given

By [F1] each $P (μ)$ is a direct summand of ${pr}_{C} (E \otimes M (λ))$ , which is in turn a direct summand of $E \otimes M (λ)$ .

2.1F2step 1.1

By [F2] the object $E \otimes M (λ)$ is Verma-filtered; both ${pr}_{C} (E \otimes M (λ))$ and its direct summand $P (μ)$ are direct summands of a Verma-filtered object and hence Verma-filtered by [F2]. So every projective cover $P (μ)$ has a finite Verma flag.

3.1F3step 2.1∎

Let $P \in O$ be projective. By [F3] it has finite length and decomposes as a finite direct sum $P = P_{1} \oplus \dots \oplus P_{n}$ of indecomposables; each $P_{i}$ is projective and indecomposable, hence a projective cover of its simple head $L (μ_{i})$ by [F3], hence isomorphic to $P (μ_{i})$ by uniqueness of projective covers, so each $P_{i}$ is Verma-filtered by step 2.1. A finite direct sum of Verma-filtered objects is Verma-filtered, by concatenating the flags along the summands; hence $P$ has a finite Verma flag.

Remarks

The statement of this theorem is only the existence of a finite flag; the sharper restriction on the labels occurring in a flag of $P (λ)$ is proved in The triangular restriction on projective Verma flags, after BGG reciprocity, so that the proof here does not assume reciprocity.

Depends on

Used by

Injectives have costandard filtrations Corollary
The triangular restriction on projective Verma flags Corollary
A projective Verma flag need not split Counterexample
A Verma module need not be projective in its block Counterexample
The two projectives in the principal sl2 block Example
BGG reciprocity Theorem

Dependency tree · two levels

47 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

Lin Chen, lecture notes (Spring 2024), Lecture 9, Theorem 1.4 and its proof (standard reference, not scraped)
Pavel Etingof, Representations of Lie Groups (18.757, Fall 2023), Sec. 20.2 (standard reference, not scraped)