Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Derivations form a Lie algebra and inner derivations an ideal

Statement

Der(g) is a Lie subalgebra of Endk(g) under the commutator. The map ad:gDer(g) is a Lie-algebra homomorphism, its image is an ideal, and ker(ad)=Z(g).

Facts & Assumptions

Given: A Lie algebra g over k.

[L1]

Derivations satisfy the Lie Leibniz law of Derivations of Lie algebras.

[L2]

The bracket of g is alternating and satisfies Jacobi (Lie algebras over a field).

[L3]

The center and ideal conditions are those of Lie subalgebras, ideals, and center.

Proof

technique · direct
1.1

Derivations form a linear subspace of Endk(g), because the Leibniz identity is linear in D. For derivations D,E, expansion of (DEED)[x,y] gives [(DEED)x,y]+[x,(DEED)y]: the two cross terms [Dx,Ey] and [Ex,Dy] occur once with each sign and cancel. Hence [D,E]=DEED is a derivation.

L1algebra
1.2

Jacobi rewritten as [x,[y,z]][y,[x,z]]=[[x,y],z] says [adx,ady]=ad[x,y]. It also says adx[y,z]=[adxy,z]+[y,adxz], so every adx is a derivation and ad is a Lie homomorphism.

L2algebra
2.1

The endomorphism commutator is bilinear and alternating, and its Jacobi identity follows by expanding the six triple composites. Therefore the closed linear subspace in step 1.1 is a Lie subalgebra.

step 1.1algebra
2.2

If D is any derivation, then for every y, [D,adx](y)=D[x,y][x,Dy]=[Dx,y]; hence [D,adx]=adDx. Thus the inner derivations form an ideal of Der(g).

L1step 1.2
3.1

Finally, xker(ad) exactly when [x,y]=0 for every y, which is exactly xZ(g) by [L3]. For an abelian algebra the inner ideal is zero; for the zero algebra all assertions remain valid.

L3algebra

Depends on

Used by

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