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.
Chevalley restriction for symmetric invariants
Statement
Assume the Axiom of Choice. Let be a finite-dimensional complex semisimple Lie algebra, let be any Cartan subalgebra in the nilpotent self-normalizing sense, and let be its Weyl group. Restriction to induces an algebra isomorphism
Facts & Assumptions
Given: The Axiom of Choice, a finite-dimensional complex semisimple Lie algebra , any Cartan subalgebra in the nilpotent self-normalizing sense, its Weyl group , and the restriction map .
The Axiom of Choice is The Axiom of Choice and is used in both the injectivity and extension suppliers.
Proof
Under [A1], the restriction map is injective by An invariant polynomial is determined by its restriction to a Cartan subalgebra.
Under [A1], the restriction map is surjective by Weyl-invariant polynomials on the Cartan extend to invariant polynomials on , which constructs an adjoint-invariant extension for every Weyl-invariant polynomial on this arbitrary Cartan .
Hence restriction is a bijective algebra homomorphism, so it is an algebra isomorphism.
Depends on
Used by
- The center of the enveloping algebra is polynomial on rank-many generators Corollary
- Adjoint isotypic modules have the zero-weight rank Lemma
- The central reduction of U(sl2) is simple away from the finite-dimensional central characters Lemma
- The nilpotent central fiber is reduced and integral Lemma
- Harish-Chandra isomorphism for the center Theorem
Dependency tree · two levels
12 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)
- Lin Chen, Geometric Representation Theory I, Lecture 5 (standard reference, not scraped)