TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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 convolution makes $R [x_{i} : i \in I]$ a commutative ring containing $R$

Statement

For every commutative ring $R$ and set $I$ , the addition and convolution of The polynomial ring $R [x_{i} : i \in I]$ as finitely supported coefficient families on monomials make $R [x_{i} : i \in I]$ a commutative ring. The constant map $R \to R [x_{i} : i \in I]$ is an injective ring homomorphism. If $I = \emptyset$ , it is an isomorphism.

Facts & Assumptions

Given: A commutative ring $R$ , a set $I$ , and finitely supported coefficient families $c, d, e : M (I) \to R$ .

[L1]

Finite sums may be reindexed by bijections, split over disjoint unions, and evaluated in either order over a finite product (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[L2]

A ring homomorphism preserves addition, multiplication, and the multiplicative identity (Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ ).

[L3]

The coefficient families, pointwise addition, convolution, and constants are those of The polynomial ring $R [x_{i} : i \in I]$ as finitely supported coefficient families on monomials.

[L4]

For the empty index set, the monomial set consists only of the zero monomial (Monomials on an index set as finitely supported exponent families).

Proof

technique · direct

1.1L3

For a fixed $u \in M (I)$ , only pairs $(a, b) \in supp (c) \times supp (d)$ with $a + b = u$ contribute to $(c d)_{u}$ , so the coefficient sum is finite; moreover $supp (c d)$ is contained in the finite image of $supp (c) \times supp (d)$ under $(a, b) \mapsto a + b$ . Thus convolution is a finitely supported coefficient family.

1.2L3algebra

Pointwise addition makes the coefficient families an abelian group, with the zero family as identity and pointwise negatives.

1.3L1L3

Reindexing $(a, b)$ by $(b, a)$ proves $c d = d c$ , and reindexing triples together with finite Fubini proves $(c d) e = c (d e)$ coefficient by coefficient.

1.4L1L3

Splitting a finite sum proves $c (d + e) = c d + c e$ , while the coefficient family supported at the zero monomial with value $1_{R}$ is a multiplicative identity.

1.5L2L3algebra

The constant map preserves addition, multiplication, and $1$ by the convolution formula, so it is a ring homomorphism by [L2]; its zero-monomial coefficient recovers the original scalar, hence it is injective.

2.1L3L4∎

When $I = \emptyset$ , [L4] gives only the zero monomial, so every coefficient family is constant and the constant embedding is surjective.

Depends on

Used by

Quasi-separatedness in pushforward cannot be omitted Counterexample
Algebraic independence in a field extension Definition
Universal property of a polynomial ring on an arbitrary family of indeterminates Theorem

Cited to discharge well-definedness by The polynomial ring R[xᵢ:i∈ I] as finitely supported coefficient families on monomials.

Dependency tree · two levels

18 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

U. Thiel, Commutative Algebra, Section 1.4 (standard reference, not scraped)

Finite convolution makes R[xi:i∈I]R[xi​:i∈I] a commutative ring containing RR