LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-23 (gpt-6-sol)

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.

An invariant polynomial is determined by its restriction to a Cartan subalgebra

Statement

Assume the Axiom of Choice. Let $g$ be a finite-dimensional complex semisimple Lie algebra and let $h \subseteq g$ be a Cartan subalgebra. If an adjoint-invariant polynomial on $g$ vanishes on $h$ , then it vanishes identically on $g$ . Equivalently, an invariant polynomial is determined by its restriction to $h$ .

Facts & Assumptions

Given: The Axiom of Choice, a finite-dimensional complex semisimple Lie algebra $g$ , a Cartan subalgebra $h$ in the nilpotent self-normalizing sense, and an infinitesimally adjoint-invariant polynomial function $f \in S (g)^{g}$ whose restriction to $h$ is zero. The Killing form identifies the notation $S (g)$ with polynomial functions on $g$ .

[A1]

AC is The Axiom of Choice; under it every such Cartan subalgebra is maximal toral by Cartan subalgebras are exactly maximal toral subalgebras.

[F1]

For a maximal toral Cartan, Finite semisimple Cartan, root and string structure gives $g = h \oplus ⨁_{α \in Φ} g_{α}$ , with finite $Φ$ , one-dimensional root spaces, and nilpotent $ad e_{α}$ for every root vector.

[F2]

A holomorphic map between equal-dimensional complex affine spaces with invertible differential maps a neighbourhood onto a nonempty open set (The holomorphic inverse function theorem in several complex variables).

Proof

technique · direct

1.1givenA1F1algebra

If $g = 0$ , the conclusion is immediate. Otherwise [A1, F1] give the displayed root decomposition. Choose a nonzero vector $e_{α} \in g_{α}$ for each of the finitely many roots and fix an order on $Φ$ . Since each root is a nonzero linear functional and $C$ is infinite, the finite product $\prod_{α \in Φ} α$ is a nonzero polynomial; choose $h_{0} \in h$ where it does not vanish.

2.1F1step 1.1algebra

For $t = (t_{α})_{α \in Φ}$ define the following polynomial map. [F1, step 1.1] $F (t, h) = (\prod_{α \in Φ}^{f i x e d o r d e r} \exp (t_{α} ad e_{α})) h, F : C^{∣ Φ ∣} \times h ⟶ g .$ Every exponential is a finite polynomial because its adjoint operator is nilpotent. It is an automorphism of the Lie algebra: the derivation identity implies $\exp (t D) [x, y] = [\exp (t D) x, \exp (t D) y]$ for $D = ad e_{α}$ , and its inverse is $\exp (- t D)$ . Thus $F$ is a polynomial map.

3.1F1F2step 1.1step 2.1algebra

The source and target of $F$ have the same dimension by [F1]. At $(0, h_{0})$ , its derivative has the following form. [F1, step 1.1, step 2.1] $d F_{(0, h_{0})} ((s_{α}), k) = k + \sum_{α \in Φ} s_{α} [e_{α}, h_{0}] = k - \sum_{α \in Φ} s_{α} α (h_{0}) e_{α} .$ Every $α (h_{0})$ is nonzero, and the root spaces are distinct one-dimensional summands, so this derivative is an isomorphism. By [F2], the image of $F$ contains a nonempty Euclidean open subset of $g$ .

4.1givenstep 2.1step 3.1algebra∎

Infinitesimal invariance means the derivative of $f$ along each curve $t \mapsto \exp (t ad e_{α}) x$ is zero at every point of that curve. Hence $f$ is constant along each such curve, and $f (F (t, h)) = f (h) = 0$ for all $(t, h)$ . By step 3.1 it vanishes on a nonempty Euclidean open subset of $g$ . A complex polynomial that vanishes on a nonempty open set is zero identically (successively apply the one-variable polynomial identity theorem in local coordinates). Thus $f = 0$ .

Depends on

Used by

Dependency tree · two levels

34 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

Pavel Etingof, Representations of Lie Groups (standard reference, not scraped)
Yiannis Sakellaridis, Verma Modules and the Category O (standard reference, not scraped)