LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-08

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.

Algebraicity of the coordinates over the invariant field and non-vanishing of the invariant Jacobian

Statement

Assume the Axiom of Choice. Let $(W, S)$ be a Coxeter system of finite type, $n = ∣ S ∣ \geq 1$ , with $V_{C}$ , $A = S / I$ and a fixed basic family $f_{1}, \dots, f_{n} \in R = S^{W}$ of degrees $d_{i}$ , generating the ideal $I = S R_{+}$ , algebraically independent and generating $R$ , as in Basic degrees, exponents, and the graded coinvariant algebra of a finite Coxeter system; choose $C$ -coordinates $x_{1}, \dots, x_{n}$ on $V_{C}$ (Polynomial rings in finitely many commuting indeterminates by iteration) and let $\partial / \partial x_{j}$ and $J = (\partial f_{i} / \partial x_{j})_{1 \leq i, j \leq n}$ be the formal partial derivatives and the Jacobian matrix of Equation rows and coordinate columns in an affine Jacobian. Put $L : = C (x_{1}, \dots, x_{n})$ and $K : = C (f_{1}, \dots, f_{n}) \subseteq L$ (The field of fractions $Frac (D) = (D ∖ {0})^{- 1} D$ of an integral domain).

(1) Annihilating orbit polynomials. For each $j$ , the orbit polynomial $P_{j} (T) : = \prod_{w \in W} (T - w \cdot x_{j}) \in S [T]$ is monic of degree $∣ W ∣$ , its coefficients lie in $R = C [f_{1}, \dots, f_{n}] \subseteq K$ , and $P_{j} (x_{j}) = 0$ . Hence every $x_{j}$ is algebraic over $K$ in the sense of Algebraic and transcendental elements and algebraic extensions.

(2) Minimal polynomial and its derivative. For each $j$ let $m_{j} \in K [T]$ be the minimal polynomial of $x_{j}$ over $K$ (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element). Then $x_{j} \notin K$ ; $m_{j}$ is nonconstant; $m_{j}^{'} \neq 0$ ; and $m_{j}^{'} (x_{j}) \neq 0$ .

(3) Differential bridge. For each $j$ there exist $b_{1 j}, \dots, b_{n j} \in L$ such that, for every $k \in {1, \dots, n}$ , the identity $δ_{j k} = \sum_{i = 1}^{n} b_{i j} \frac{\partial f_{i}}{\partial x_{k}}$ holds in $L$ (with $δ_{j k}$ the Kronecker symbol; equivalently $i d = B \cdot J$ with $B = (b_{j i})$ over $L$ ). Consequently $J$ has rank $n$ over $L$ , and $J : = \det (\frac{\partial f_{i}}{\partial x_{j}}) \in S$ is a nonzero polynomial: the invariant Jacobian.

No étale-quotient, scheme-theoretic or transcendental Jacobian criterion is used.

Facts & Assumptions

Given: The Axiom of Choice, the finite type system $(W, S)$ with basic family $f_{1}, \dots, f_{n}$ , and coordinates $x_{1}, \dots, x_{n}$ on $V_{C}$ .

[F1]

The fixed family $f_{1}, \dots, f_{n}$ is a minimal family of homogeneous positive-degree invariants generating $I = S R_{+}$ , generates $R$ as a $C$ -algebra and is algebraically independent, so evaluation gives a graded $C$ -algebra isomorphism $C [y_{1}, \dots, y_{n}] \to R$ , $y_{i} \mapsto f_{i}$ , and every element of $R$ is a polynomial in the $f_{i}$ ; also $d_{i} \geq 2$ (Basic degrees, exponents, and the graded coinvariant algebra of a finite Coxeter system, Finite reflection invariant generators are algebraically independent, Chevalley shephard todd for finite weyl groups).

[F2]

$ρ_{C} : W \to G L (V_{C})$ is the complexified canonical representation with $\dim_{C} V_{C} = n$ , and $V_{C}^{W} = {0}$ ; more precisely every $W$ -fixed linear form on $V_{C}$ is zero (Complexifying a finite Coxeter reflection representation: faithfulness, complex reflections, and the hypotheses of the invariant-theory suppliers (1),(3), The canonical reflection homomorphism, roots, reflections, and the positive cone).

[F3]

The action $(g \cdot f) (v) = f (ρ_{C} (g)^{- 1} v)$ makes $S = C [V_{C}]$ a graded algebra on which $W$ acts by graded algebra automorphisms, with invariant algebra $R = S^{W}$ , positive-degree part $R_{+}$ and $I = S R_{+}$ ; the degree-one part of $S$ is $V_{C}^{*}$ and the restricted action is the dual action, so a degree-one element of $S$ is $W$ -fixed exactly when it is an invariant linear form (Finite linear invariant and coinvariant polynomial algebras, Reflection basic invariants form a regular sequence).

[F4]

$S = C [x_{1}, \dots, x_{n}]$ is the iterated polynomial ring over $C$ , monomials form a basis, and $S$ is a domain with fraction field $L = C (x_{1}, \dots, x_{n})$ ; the subfield generated by $f_{1}, \dots, f_{n}$ is $K = C (f_{1}, \dots, f_{n}) = Frac (R)$ (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution, Polynomial rings in finitely many commuting indeterminates by iteration, The field of fractions $Frac (D) = (D ∖ {0})^{- 1} D$ of an integral domain). Over a field, a positive-sized square matrix is invertible exactly when its determinant is nonzero (A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit); hence $\det (λ I - M) = 0$ exactly when $λ$ is an eigenvalue.

[F5]

Algebraic elements and minimal polynomials: if $0 \neq P \in K [T]$ with $P (x_{j}) = 0$ then $x_{j}$ is algebraic over $K$ ; the minimal polynomial $m_{j}$ is the unique monic irreducible element generating $\ker ({ev}_{x_{j}}) = (m_{j})$ , and $f (x_{j}) = 0$ holds exactly when $m_{j} ∣ f$ (Algebraic and transcendental elements and algebraic extensions, The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[F6]

The formal partial derivatives $\partial_{x_{k}}$ are defined on monomials by the Leibniz monomial rule and extended $C$ -linearly, and the univariate formal derivative satisfies $(f + g)^{'} = f^{'} + g^{'}$ , $(c f)^{'} = c f^{'}$ , the product rule, $(T^{a})^{'} = a T^{a - 1}$ and the degree bound $\deg f^{'} \leq \deg f - 1$ when $f^{'} \neq 0$ (Equation rows and coordinate columns in an affine Jacobian, The formal derivative of a polynomial, Linearity, power rule, Leibniz rule and the degree bound for the formal derivative).

[F7]

The Axiom of Choice is used only to have an $n$ -element basic family as in [F1] (The Axiom of Choice).

Proof

1.1F1F3F4F5

Fix $j$ and form $P_{j} (T) = \prod_{w \in W} (T - w \cdot x_{j}) \in S [T]$ . For $g \in W$ one has $g \cdot (w \cdot x_{j}) = (g w) \cdot x_{j}$ (the action is a left action), so $g$ permutes the linear factors and hence fixes $P_{j}$ ; as $W$ acts by graded algebra automorphisms [F3], each coefficient of $P_{j}$ lies in $R = S^{W}$ . By [F1] $R = C [f_{1}, \dots, f_{n}]$ , so all coefficients lie in $K$ . The polynomial is monic of degree $∣ W ∣$ , being a product of $∣ W ∣$ monic linear factors, and $P_{j} (x_{j}) = 0$ because the factor with $w = 1$ is $T - x_{j}$ . Hence $x_{j}$ is algebraic over $K$ in the sense of [F5].

1.2F6

The operators $\partial_{x_{k}}$ are $C$ -linear on $S$ and satisfy the product rule on monomials by the Leibniz monomial rule, hence on all polynomials by bilinearity; by induction the power rule $\partial_{x_{k}} (x_{j}^{a}) = a x_{j}^{a - 1} δ_{j k}$ holds for all $a \geq 1$ , while $\partial_{x_{k}} 1 = 0$ . Consequently, for every polynomial $γ \in C [y_{1}, \dots, y_{n}]$ and all $g_{1}, \dots, g_{n} \in S$ , the chain rule $\partial_{x_{k}} (γ (g_{1}, \dots, g_{n})) = \sum_{i = 1}^{n} (\partial_{y_{i}} γ) (g_{1}, \dots, g_{n}) \partial_{x_{k}} g_{i}$ holds: expanding $γ = \sum_{α} c_{α} y^{α}$ , the product rule gives $\partial_{x_{k}} (g^{α}) = \sum_{i} α_{i} g^{α - e_{i}} \partial_{x_{k}} g_{i}$ , which is the displayed identity because $\partial_{y_{i}} γ = \sum_{α} c_{α} α_{i} y^{α - e_{i}}$ .

2.1F2F3F5F6step 1.1

Suppose $x_{j} \in K$ . Since $W$ acts on $S$ by algebra automorphisms it acts on the fraction field $L$ by $g \cdot (a / b) = (g \cdot a) / (g \cdot b)$ , and this action fixes $K$ pointwise because the $f_{i}$ are invariant; hence $g \cdot x_{j} = x_{j}$ for every $g$ . But $x_{j} \in V_{C}^{*}$ is a degree-one element of $S$ [F3], so by [F2] the only $W$ -fixed linear form is $0$ , while $x_{j}$ is a coordinate function and $x_{j} \neq 0$ : contradiction. So $x_{j} \notin K$ ; the minimal polynomial $m_{j}$ of $x_{j}$ over $K$ [F5] is therefore nonconstant. Its derivative is nonzero: the top coefficient of $m_{j}$ is nonzero and the degree is $\geq 1$ , so in characteristic zero the coefficient $\deg (m_{j}) \cdot c_{\deg}$ of $m_{j}^{'}$ is nonzero, and $\deg m_{j}^{'} < \deg m_{j}$ by [F6]. If $m_{j}^{'} (x_{j}) = 0$ , then the nonzero polynomial $m_{j}^{'} \in K [T]$ of degree $< \deg m_{j}$ would have $x_{j}$ as a root, contradicting the minimality of $m_{j}$ [F5]; hence $m_{j}^{'} (x_{j}) \neq 0$ in $L$ .

3.1F1F4F6F7step 1.1step 1.2step 2.1∎

Fix $j$ and write $m_{j} (T) = \sum_{a = 0}^{r} c_{a} T^{a}$ with $c_{a} \in K$ . Since $K = Frac (R)$ [F4], choose $0 \neq B \in R$ with $β_{a} : = B c_{a} \in R$ for all $a$ , and put $M_{j} (T) : = \sum_{a} β_{a} T^{a} \in R [T]$ . Then $M_{j} (x_{j}) = B m_{j} (x_{j}) = 0$ and $M_{j}^{'} (T) = B m_{j}^{'} (T)$ , so $M_{j}^{'} (x_{j}) = B m_{j}^{'} (x_{j}) \neq 0$ in $L$ by 2.1. Differentiate the polynomial identity $M_{j} (x_{j}) = \sum_{a} β_{a} x_{j}^{a} = 0$ with respect to $x_{k}$ using the product and power rules of 1.2: $0 = \sum_{a} (\partial_{x_{k}} β_{a}) x_{j}^{a} + M_{j}^{'} (x_{j}) \partial_{x_{k}} x_{j} = \sum_{a} (\partial_{x_{k}} β_{a}) x_{j}^{a} + M_{j}^{'} (x_{j}) δ_{j k},$ hence $δ_{j k} = - (\sum_{a} (\partial_{x_{k}} β_{a}) x_{j}^{a}) / M_{j}^{'} (x_{j})$ in $L$ . Each $β_{a} \in R = C [f_{1}, \dots, f_{n}]$ is $β_{a} = γ_{a} (f_{1}, \dots, f_{n})$ for a polynomial $γ_{a} \in C [y_{1}, \dots, y_{n}]$ [F1], so the chain rule of 1.2 gives $\partial_{x_{k}} β_{a} = \sum_{i} (\partial_{y_{i}} γ_{a}) (f_{1}, \dots, f_{n}) \partial_{x_{k}} f_{i}$ . Substituting, $δ_{j k} = \sum_{i = 1}^{n} b_{i j} \partial_{x_{k}} f_{i}, b_{i j} : = - \frac{\sum_{a} (\partial_{y_{i}} γ_{a}) (f_{1}, \dots, f_{n}) x_{j}^{a}}{M_{j}^{'} (x_{j})} \in L,$ for all $j, k$ ; equivalently $B J = i d$ for the matrix $B = (b_{j i})$ . Hence $J$ is invertible over the field $L$ , so it has rank $n$ over $L$ , its determinant is nonzero in $L$ , and since $S$ is a domain with fraction field $L$ [F4] the polynomial $J = \det J \in S$ is nonzero. For $n = 0$ there is no assertion to make; the only choice principle used is the AC entering the existence of the basic family [F7], and no étale-quotient, scheme-theoretic or transcendental Jacobian criterion is invoked.

Depends on

Used by

Dependency tree · two levels

66 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 (MIT 18.757 course notes, 162-page PDF) (standard reference, not scraped)
Josh Swanson, On eigenvalues of representations of reflection groups and wreath products (University of Washington CAT seminar notes, 7-page PDF) (standard reference, not scraped)