PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-05

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 algebra actions extend to unital actions of the enveloping algebra

Statement

Let $g$ be a complex Lie algebra, let $V$ be a complex vector space, and let $ρ ⁣ : g \to End (V)$ be a Lie algebra action. Then there is a unique unital algebra homomorphism

$\tilde{ρ} ⁣ : U (g) \to End (V)$

whose restriction to $g \subset U (g)$ is $ρ$ .

Facts & Assumptions

Given: A complex Lie algebra $g$ , a complex vector space $V$ , and a Lie algebra homomorphism $ρ ⁣ : g \to End (V)$ .

Proof

technique · direct

1.1

By the tensor-algebra universal property, $ρ$ extends uniquely to a unital algebra homomorphism $\hat{ρ} ⁣ : T (g) \to End (V)$ with $\hat{ρ} (x) = ρ (x)$ for $x \in g$ .

givenconstruct

1.2

For $x, y \in g$ , the Lie-homomorphism identity gives $\hat{ρ} (x \otimes y - y \otimes x - [x, y]) = ρ (x) ρ (y) - ρ (y) ρ (x) - ρ ([x, y]) = 0$ , so the defining ideal of The universal enveloping algebra as a tensor quotient lies in $\ker \hat{ρ}$ .

algebra

2.1

Therefore $\hat{ρ}$ descends uniquely through the quotient $T (g) ↠ U (g)$ from The universal enveloping algebra as a tensor quotient, producing the required unital algebra homomorphism $\tilde{ρ}$ .

step 1.1step 1.2∎

Depends on

The universal enveloping algebra as a tensor quotient

Used by

Central character of a Lie algebra module Definition

Dependency tree · one level

1 result within one dependency step 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

Pavel Etingof, Lie Groups and Lie Algebras I (standard reference, not scraped)