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.
Finite linear invariant and coinvariant polynomial algebras
Definition
Let be a finite-dimensional complex vector space and finite. Write for its polynomial algebra. Concretely, after a finite choice of linear coordinates , this is the iterated polynomial ring of The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution, with finite monomial sums, total degree and substitution of linear forms. Under a change of coordinates, the two invertible linear substitutions are inverse algebra homomorphisms, so the construction is independent of that choice.
Define . Substitution respects sums and products, preserves total degree, and , so this is an action by graded algebra automorphisms. Let The invariant polynomial algebra is ; the coinvariant algebra is the graded quotient . The notation means finite sums of products with and . Because the action is graded, homogeneous parts of an invariant are invariant. Thus is an ideal of , is a homogeneous ideal of , and the quotient grading is well-defined.
The Reynolds operator is . The group is nonempty and is invertible in . Left multiplication permutes its finite elements, so every is invariant. For invariant all summands equal , hence and . For , termwise. It is therefore a graded -linear projection onto .
The polynomial-function notation is faithful over : a univariate nonzero degree- polynomial has at most roots by repeated division by , and induction on the number of variables, viewing the last variable's coefficients as polynomials in the others, shows that a polynomial vanishing everywhere is zero. Thus the substitution formulas can be checked either formally or on points.
If , then , is the trivial subgroup, and the coinvariant algebra is . If in positive dimension, and , so again . Constants survive in every case because has positive degree. All averages and coordinate choices are finite; no AC is used.
Depends on
Used by
- Weyl discriminant and reflecting hyperplane arrangement Definition
- A2 coinvariant algebra and basic invariants Example
- Finite linear group invariant polynomials separate orbits Lemma
- Finite reflection invariant generators are algebraically independent Lemma
- Local Chevalley restriction for Kostant freeness Lemma
- Weyl anti invariants are divisible by the discriminant Lemma
- Weyl coinvariant hilbert series has order w dimension Lemma
Dependency tree · two levels
3 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, §§11–13; local proof and exact reading limits in the group report (standard reference, not scraped)