ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-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.

The associated variety of a finite-dimensional simple annihilator is the origin

Example

Let $g$ be a finite-dimensional complex semisimple Lie algebra and let $L (λ)$ be a finite-dimensional simple $U (g)$ -module, with $λ$ dominant integral. Then $I (λ) = {Ann}_{U (g)} L (λ)$ has finite codimension in $U (g)$ , and its associated variety is the origin:

$V (I (λ)) = {0} \subseteq g^{*} .$ Indeed, with $d = \dim_{C} L (λ)$ , Cayley-Hamilton shows that for every $y \in g$ the power $y^{d}$ is the symbol of an element of $I (λ)$ , so $gr I (λ)$ contains the $d$ -th powers of all of $g$ . Over $C$ , the polarization identity shows that these pure $d$ -th powers span $S^{d} (g)$ : for $y_{1}, \dots, y_{d} \in g$ , $d! y_{1} \dots y_{d} = \sum_{J \subseteq {1, \dots, d}} (- 1)^{d - ∣ J ∣} {(\sum_{j \in J} y_{j})}^{d} .$ Since $gr I (λ)$ is an ideal in $S (g)$ , it contains every $S^{k} (g)$ for $k \geq d$ . Its zero set is therefore ${0}$ ; equivalently, every point $ξ$ in it satisfies $ξ (y)^{d} = 0$ for all $y \in g$ . The finite-dimensionality of $L (λ)$ is essential here. Infinite-dimensional (Verma-type) annihilators behave differently: their associated varieties need not be ${0}$ , and on this page no positive-dimensionality statement about them is asserted.

Facts & Assumptions

Given: A finite-dimensional complex semisimple Lie algebra $g$ , a dominant integral weight $λ$ , and the finite-dimensional simple module $L (λ)$ with $d : = \dim_{C} L (λ) \geq 1$ .

[F1]

$I (λ)$ is the kernel of the unital algebra homomorphism $U (g) \to {End}_{C} (L (λ))$ given by the action, so it is a proper two-sided ideal and $U (g) / I (λ)$ embeds into the finite-dimensional algebra ${End}_{C} (L (λ))$ (The annihilator of a module over an enveloping algebra, Finite-dimensional simple modules are classified by dominant highest weights).

[F2]

Cayley-Hamilton: for every endomorphism $T$ of the finite-dimensional space $L (λ)$ , the characteristic polynomial $χ_{T}$ satisfies $χ_{T} (T) = 0$ ; it is monic of degree $d$ (Cayley-Hamilton: every finite-dimensional endomorphism satisfies its characteristic polynomial, $χ_{T} (T) = 0$ , Polynomial evaluation at an endomorphism: $p (T) = \sum_{k} a_{k} T^{k}$ ).

[F3]

The symbol of an element $p (y) = y^{d} + (terms of degree < d)$ of the PBW filtration is $y^{d} \in S^{d} (g)$ ; symbols multiply, and $V (I)$ is the zero locus of $gr I$ in $g^{*}$ with $g^{*}$ in duality with the degree-one symbols (The associated graded variety of a two-sided ideal, The PBW filtration by tensor degree on the enveloping algebra, PBW gives an ordered monomial basis for the enveloping algebra, Classical affine zero loci form the Zariski closed sets).

Verification

technique · direct

1.1F1given

The action map $U (g) \to {End}_{C} (L (λ))$ has kernel $I (λ)$ by definition, so $U (g) / I (λ)$ is isomorphic to a subalgebra of the finite-dimensional algebra ${End}_{C} (L (λ))$ ; hence $I (λ)$ has finite codimension in $U (g)$ . It is proper because $1$ acts as the identity on the nonzero module $L (λ)$ .

1.2F2F3algebra

Fix $y \in g$ and let $χ_{y}$ be the characteristic polynomial of the operator by which $y$ acts on $L (λ)$ ; by [F2] it is monic of degree $d$ and $χ_{y} (y)$ acts as $0$ on $L (λ)$ , that is, $χ_{y} (y) \in I (λ)$ . Writing $χ_{y} (y) = y^{d} + (terms of PBW degree < d)$ , its symbol in the associated graded is $y^{d}$ by [F3]; hence $y^{d} \in (gr I (λ))_{d} \subseteq S^{d} (g)$ .

2.1step 1.2F1F3algebra∎

Let $ξ \in V (I (λ))$ . By step 1.2 and the definition of the associated variety, $0 = ξ (y^{d}) = ξ (y)^{d}$ for every $y \in g$ , so $ξ (y) = 0$ for every $y \in g$ and hence $ξ = 0$ ; thus $V (I (λ)) \subseteq {0}$ . Conversely, $I (λ)$ is a proper ideal, so $I (λ) \cap C \cdot 1 = 0$ and $gr I (λ)$ has no nonzero degree-zero element; every $f \in gr I (λ)$ therefore has zero constant term and satisfies $f (0) = 0$ , so $0 \in V (I (λ))$ . Hence $V (I (λ)) = {0}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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

D. Barbasch, Cells in Weyl groups and primitive ideals (AIM workshop notes, 2006) (standard reference, not scraped)
D. A. Vogan, The orbit method and primitive ideals for semisimple Lie algebras (CMS Conf. Proc. 1986) (standard reference, not scraped)