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.
A2 coinvariant algebra and basic invariants
Example
Let act by permuting coordinates on , the reflection plane. Put and restricted to . Then The coinvariant algebra has basis , Hilbert series , and dimension .
Facts & Assumptions
Given: The displayed permutation action and restricted elementary symmetric polynomials.
A faithful finite reflection group has a polynomial invariant algebra and a free polynomial module of rank its order (Chevalley shephard todd for finite weyl groups).
Invariants, the positive invariant ideal, and Reynolds averaging use the conventions of Finite linear invariant and coinvariant polynomial algebras.
Verification
Each transposition fixes a line in and has eigenvalue on the vector that subtracts its two exchanged coordinates. These transpositions generate . The action is faithful: a permutation fixing all coordinate differences fixes their labels and hence is identity. Thus F1 applies to this two-dimensional reflection representation. Eliminate to identify its polynomial algebra with and obtain and .
We verify generation directly. Any invariant polynomial on the plane has a polynomial lift to ; average its six permuted lifts. By F2 its restriction is unchanged and the resulting lift is symmetric. A symmetric homogeneous polynomial in three variables is a polynomial in : use lexicographic order on its finitely many monomials of fixed total degree. A leading exponent triple satisfies , because swapping an out-of-order pair would produce a larger monomial with the same coefficient. The polynomial has leading monomial with coefficient one. Subtract its required multiple and repeat; lexicographic order strictly decreases within a finite set. Sum over the finitely many homogeneous parts. Restricting proves invariant generation by .
These generators are algebraically independent without an appeal to a degree table. Their Jacobian determinant in is , a nonzero polynomial. If a nonzero relation of least positive total degree existed, differentiating it twice, once in each coordinate, and multiplying by the adjugate Jacobian matrix would give that determinant times each evaluated partial derivative of is zero. The polynomial ring is a domain, so both evaluated derivatives vanish. In characteristic zero some partial derivative of a nonconstant is nonzero and has lower degree, a contradiction; a nonzero constant cannot be a relation. Thus the stated invariant polynomial algebra has basic degrees two and three.
By 2.1 and 3.1, the positive invariant ideal in F2 generates in . Put and . The identity gives . First quotient by : with , the remaining quotient is . Division by this monic polynomial in has unique remainder with . Existence follows by canceling the highest power of ; uniqueness follows because a nonzero multiple of a monic degree-two polynomial has degree at least two, even over . The unique representatives of elements of have degrees at most two in . Hence are independent and spanning, proving the asserted basis and Hilbert series by their degrees .
The quotient dimension is therefore , matching the free rank in F1, and the degree product is . The degree-zero class is nonzero, the top class is nonzero by unique remainder, and all degrees above three vanish. This is an explicit calculation on the nonzero two-dimensional plane; there is no limiting parameter or choice assumption.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
6 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)