ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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 polynomial differential representation and positive-characteristic nonfaithfulness

Statement

Let $k$ be any field and $n \geq 1$ . Multiplication by $t_{i}$ and partial differentiation $\partial_{i}$ define a unital left $A_{n} (k)$ -module structure on $k [t_{1}, \dots, t_{n}]$ . If $char (k) = p > 0$ , this representation is not faithful: $p_{i}^{p}$ is a nonzero element of $A_{n} (k)$ that acts by zero.

Facts & Assumptions

Given: A field $k$ , an integer $n \geq 1$ , and the polynomial ring $k [t_{1}, \dots, t_{n}]$ .

[F1]

The polynomial ring $R [x_{i} : i \in I]$ as finitely supported coefficient families on monomials: polynomial elements are finite $k$ -linear combinations of distinct monomials $t^{γ}$ .

[F2]

Polynomial Weyl algebra and its central parameter: $A_{n} (k) = T (E_{n}) / J_{n, 1}$ , where $E_{n}$ has basis $x_{i}, p_{i}$ and $J_{n, 1}$ is generated by the same-type commutators and $p_{i} x_{j} - x_{j} p_{i} - δ_{i j} 1$ .

[F3]

Polynomial Weyl algebra presentation and normal-ordered basis: the monomials $x^{α} p^{β}$ form a basis of $A_{n} (k)$ .

[F4]

Universal property of the tensor algebra: a linear assignment from the generators to a unital associative algebra extends to a unital algebra homomorphism from the tensor algebra.

[F5]

A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring: a ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring.

[F6]

Unital left and right modules over a ring; unqualified module means left module: a unital algebra homomorphism into endomorphisms defines a unital left module action by evaluation.

[F7]

The ideal generated by a subset and principal ideals: the ideal generated by a set is contained in every two-sided ideal containing that set.

Verification

1.1givenF1construct

On a monomial $t^{γ} = t_{1}^{γ_{1}} \dots t_{n}^{γ_{n}}$ define $X_{i} (t^{γ}) = t^{γ + e_{i}}$ , and define $D_{i} (t^{γ}) = γ_{i} t^{γ - e_{i}}$ when $γ_{i} > 0$ and $0$ when $γ_{i} = 0$ ; extend both maps $k$ -linearly using [F1].

2.1F1F2step 1.1algebra

The $X_{i}$ commute because multiplication in the polynomial ring commutes; for distinct $i, j$ , the $D_{i}$ commute because applying the two exponent-lowering maps multiplies by $γ_{i} γ_{j}$ in either order, and $D_{i}$ commutes with itself. For each $i, j$ , applying $D_{i} X_{j} - X_{j} D_{i}$ to $t^{γ}$ gives $δ_{i j} t^{γ}$ : when $i = j$ the coefficient difference is $(γ_{i} + 1) - γ_{i} = 1$ , and when $i \neq j$ the two terms agree. Hence the generator assignments satisfy [F2].

3.1F2F4F5F6F7step 2.1algebraconstruct

Pointwise addition and scalar multiplication and composition make ${End}_{k} (k [t_{1}, \dots, t_{n}])$ a unital associative $k$ -algebra: composition is associative, the identity map is its unit, and $k$ -bilinearity follows by evaluating on polynomials. Send each generator $x_{i}, p_{i}$ to $X_{i}, D_{i}$ . By [F4] this linear assignment extends to a unital algebra map from $T (E_{n})$ . Step 2.1 shows that it kills every defining relator in [F2]. Its kernel is a two-sided ideal because it is an algebra homomorphism, so it contains their generated ideal by [F7]. By [F5] it factors through the quotient $A_{n} (k)$ ; write $ρ$ for this factor, which is $k$ -linear because the quotient map is surjective. Evaluation $a \cdot f : = ρ (a) f$ gives a unital left module by [F6]. If $char (k) = p > 0$ , then for every monomial, $D_{i}^{p} (t^{γ}) = 0$ : it vanishes when $γ_{i} < p$ , and otherwise its coefficient is a product of $p$ consecutive integers, hence divisible by $p$ . Thus $D_{i}^{p} = 0$ .

4.1F3step 3.1algebra∎

By [F3], $p_{i}^{p}$ is a nonzero normal-ordered basis monomial in $A_{n} (k)$ , while step 3.1 shows that the representation sends it to zero. Therefore the representation is nonfaithful in positive characteristic.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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

François Dumas, Noncommutative Invariants, §2.1.1 (standard reference, not scraped)
Pavel Etingof, Lectures on Calogero-Moser Systems, Lecture 8 (standard reference, not scraped)