Alphabeta MathHow 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.
Universal property of a polynomial ring on an arbitrary family of indeterminates
Statement
Let be commutative rings, let be a ring homomorphism, and let be a family in . There is a unique ring homomorphism
whose restriction to is and which satisfies for every .
Facts & Assumptions
Given: Commutative rings , a ring homomorphism , and a family in .
The finite convolution construction is a commutative ring containing (Finite convolution makes a commutative ring containing ).
A ring homomorphism preserves addition, multiplication, and the multiplicative identity (Ring homomorphism: additive, multiplicative, and required to send to ).
Finite sums may be reindexed and evaluated in either order over finite products (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).
Proof
For define , and for define ; both expressions are finite and the empty product is .
Pointwise addition gives , while and finite reindexing give .
The zero monomial gives , constants give , and the one-supported exponent family gives ; hence is the required ring homomorphism by [L2].
Any ring homomorphism with these values must send to and therefore, by finite additivity, must equal the formula in step 1.1.
Depends on
Used by
- A polynomial ring on a finite ordered family agrees canonically with the iterated polynomial-ring construction Corollary
- Quasi-separatedness in pushforward cannot be omitted Counterexample
- Algebraic independence in a field extension Definition
- An irreducible curve can have arbitrarily large tangent dimension Example
- Classical bilinear-form equations linearize to matrix spaces Example
- Dual numbers compute the tangent spaces of the general and special linear groups Example
- Dual-number vectors in affine space Example
- Fitting ideals of a diagonal two-by-two presentation Example
- The product of two parabolas: a block Jacobian and the direct-sum formula Example
- The tangent space of the parabola at a general point and the local parameter Example
- Three axes are not three coplanar lines Example
- A dominant map has a surjective differential on a dense source open Lemma
- A tangent direction is realized by a local smooth curve Lemma
- A transverse hyperplane slice is smooth at the chosen point Lemma
- Artin's ideal generated by f(x_f) for all monic nonconstant f∈ F[x] is proper Lemma
- Base change of standard smooth presentations Lemma
- Field extension preserves the graded pieces and the total length of a zero-dimensional projective quotient Lemma
- Polynomial diagonal differences form a regular sequence Lemma
- Polynomial differentials are free Lemma
- Standard smooth algebras are finitely presented and flat Lemma
- The Jacobian kernel computes the tangent space Theorem
Dependency tree · two levels
14 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)