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.

Lie representations are U(g)-modules

Statement

Restriction along $ι_{g} : g \to U (g)$ and extension by the universal property give mutually inverse correspondences between representations of $g$ and unital left $U (g)$ -module structures whose restriction along $k \to U (g)$ is the given scalar action on $V$ . A linear map is an intertwiner on one side exactly when it is a module homomorphism on the other.

Facts & Assumptions

Given: A Lie algebra $g$ and a vector space $V$ over $k$ .

[L1]

A unital left $U (g)$ -module structure whose central $k$ -scalars act by the given scalar multiplication is equivalently a unital $k$ -algebra map $U (g) \to {End}_{k} (V)$ . Indeed, the module axioms give additivity, multiplicativity, and preservation of the unit, while the stated scalar compatibility gives $k$ -linearity; conversely such a map defines the required action (Unital left and right modules over a ring; unqualified module means left module).

[L2]

Lie maps from $g$ into a commutator algebra extend uniquely across $U (g)$ (Universal property of the enveloping algebra).

[L3]

Representations and intertwiners are as in Representations of Lie algebras and Subrepresentations, quotient representations, and intertwiners.

[L4]

By its quotient-tensor-algebra definition, every element of $U (g)$ is a finite linear combination of images of tensor words, including the empty word $1$ ; these images are products of elements $ι_{g} (x)$ . Universal enveloping algebra.

Proof

technique · direct

1.1L1L2L3

A representation $ρ : g \to {End}_{k} (V)_{L i e}$ extends uniquely by [L2] to a unital algebra map $\overline{ρ} : U (g) \to {End}_{k} (V)$ , hence to a unital left module structure by [L1].

1.2L1L2algebra

Conversely, a scalar-compatible unital module gives a $k$ -algebra map $α : U (g) \to {End}_{k} (V)$ . Its restriction $α ι_{g}$ preserves Lie brackets because both $ι_{g}$ and every algebra map preserve commutators, so it is a representation. Starting with $ρ$ recovers $ρ$ by $\overline{ρ} ι_{g} = ρ$ ; starting with $α$ recovers $α$ by uniqueness in [L2].

1.3L3L4algebra

Let $T : V \to W$ be linear. If $T$ intertwines the $g$ -actions, then it intertwines each $ρ (x)$ , each finite product of these operators, and finite linear combinations of the products. By [L4], these include the actions of every element of $U (g)$ ; the empty product acts as the identity on both modules. Thus $T$ is a module homomorphism. Conversely, restricting a module homomorphism to $ι_{g} (g)$ gives an intertwiner.

2.1step 1.1step 1.2step 1.3∎

The object and morphism correspondences in steps 1.1–1.3 are mutually inverse, proving the claimed equivalence without any PBW or injectivity assumption.

Lie representations are U(g)-modules

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources