TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-14

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.

Lower and upper central series characterize nilpotence

Statement

A Lie algebra $g$ is nilpotent if and only if its upper central series reaches $g$ : equivalently, for some $c \geq 0$ ,

$γ_{c + 1} (g) = 0 ⟺ Z_{c} (g) = g .$

Facts & Assumptions

Given: A Lie algebra $g$ and an integer $c \geq 0$ .

[L1]

The lower central series satisfies $γ_{1} = g$ and $γ_{r + 1} = [g, γ_{r}]$ (Lower central series and nilpotent Lie algebras).

[L2]

The upper central series satisfies $Z_{0} = 0$ and $x \in Z_{r + 1}$ exactly when $[g, x] \subseteq Z_{r}$ (Upper central series of a Lie algebra).

[L3]

The quotient-center formulation of $Z_{r + 1} / Z_{r}$ uses the quotient Lie bracket (Quotient Lie algebras).

Proof

technique · direct

1.1

Assume $γ_{c + 1} = 0$ . We prove $γ_{c + 1 - r} \subseteq Z_{r}$ for $0 \leq r \leq c$ . At $r = 0$ this is the assumed containment in $Z_{0} = 0$ . If it holds at $r$ , then $x \in γ_{c - r}$ implies $[g, x] \subseteq γ_{c + 1 - r} \subseteq Z_{r}$ , so [L2] gives $x \in Z_{r + 1}$ . At $r = c$ we obtain $g = γ_{1} \subseteq Z_{c}$ , hence equality.

givenL1L2L3algebra

2.1

Conversely assume $Z_{c} = g$ . Starting from $γ_{1} = g = Z_{c}$ , induction gives $γ_{r + 1} \subseteq Z_{c - r}$ for $0 \leq r \leq c$ : if $γ_{r + 1} \subseteq Z_{c - r}$ , then [L1] and [L2] give $γ_{r + 2} = [g, γ_{r + 1}] \subseteq Z_{c - r - 1}$ . At $r = c$ this yields $γ_{c + 1} \subseteq Z_{0} = 0$ , so $g$ is nilpotent. The argument also covers $c = 0$ , when both conditions say $g = 0$ .

givenL1L2step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Milne, Lie Algebras, Proposition 2.5 (standard reference, not scraped)