Alphabeta Math
PropositionStatement: 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.

Lie representations as actions before enveloping

Statement

A representation of g on V is equivalently a k-bilinear action (x,v)xv satisfying

[x,y]v=x(yv)y(xv).

In general this action does not, by itself, canonically make g into an associative unital ring over which V is a module.

Facts & Assumptions

Given: A Lie algebra g and a vector space V over the same field k.

[L1]

A representation is a linear map ρ:gEndk(V) preserving the Lie bracket (Representations of Lie algebras).

[L2]

A left module over a ring requires an associative multiplication and a unit action as in Unital left and right modules over a ring; unqualified module means left module.

Proof

technique · direct
1.1

From a representation ρ, set xv=ρ(x)v. Linearity of ρ and of each ρ(x) makes the action bilinear, and bracket preservation expands to [x,y]v=x(yv)y(xv).

L1algebra
1.2

Conversely, a bilinear action defines a linear map ρ(x)(v)=xv into Endk(V). The displayed identity says exactly that ρ([x,y])=ρ(x)ρ(y)ρ(y)ρ(x), so ρ is a representation.

L1algebra
2.1

The equivalence is therefore exact, but [L2] does not apply directly from the Lie-algebra data in general. The bracket need not be associative; if it is the zero bracket on a nonzero abelian Lie algebra, that multiplication has no unit. There is a genuine exceptional case: if g=0 and V=0, the zero bracket makes g the permitted unital zero ring, and its unique action on V is a unital module action. This exception does not give a general ring structure for Lie representations. The canonical associative-module formulation for arbitrary g,V uses U(g).

step 1.1step 1.2L2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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