LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Presentations and localization under base extension

Statement

Let $A \to C$ be a unital ring map. For any set of variables $(t_{i})$ and any ideal $I \subseteq A [t_{i}]$ , $(A [t_{i}] / I) \otimes_{A} C ≅ C [t_{i}] / I C [t_{i}] .$ Here the extended ideal is generated by the coefficient images of all elements of $I$ . For a multiplicative subset $M \subseteq A$ , $(M^{- 1} A) \otimes_{A} C ≅ {\overline{M}}^{- 1} C .$ These are ring isomorphisms; no flatness, finite-generation or nonzero-ring hypothesis is required.

Facts & Assumptions

Given: The objects, hypotheses and conventions in the statement above.

[F1]

Let $A, B, C$ be commutative $R$ -algebras. For every pair of $R$ -algebra homomorphisms $f : A \to C$ and $g : B \to C$ , there is a unique $R$ -algebra homomorphism $h : A \otimes_{R} B ⟶ C$ such that $h (a \otimes 1) = f (a)$ and $h (1 \otimes b) = g (b)$ . It is given by $h (a \otimes b) = f (a) g (b) .$ Thus $A \otimes_{R} B$ , with its two canonical maps, is the coproduct of $A$ and $B$ among commutative $R$ -algebras. (Universal mapping property of the tensor product of commutative algebras)

[F2]

Let $R$ be a commutative ring, $I ⊴ R$ an ideal, and $M$ an $R$ -module. There is a natural $R$ -module isomorphism $M \otimes_{R} (R / I) ≅ M / I M, m \otimes (r + I) ⟼ r m + I M .$ Both sides also carry the induced $R / I$ -module structure, and the isomorphism is $R / I$ -linear. For $I = 0$ it is the tensor-unit isomorphism, while for $I = R$ both sides are zero. ( $M \otimes_{R} R / I ≅ M / I M$ naturally)

[F3]

Let $R$ be a commutative ring, let $S \subseteq R$ be multiplicative, and let $M$ be a left $R$ -module. The map $Φ : (S^{- 1} R) \otimes_{R} M ⟶ S^{- 1} M, Φ ((a / s) \otimes m) = a m / s,$ is an isomorphism of $S^{- 1} R$ -modules. Its inverse is $Ψ : S^{- 1} M ⟶ (S^{- 1} R) \otimes_{R} M, Ψ (m / s) = (1 / s) \otimes m .$ (Localisation of modules is extension of scalars)

Proof

1.1

A ring map from $C [t_{i}]$ to a $C$ -algebra $R$ is exactly a choice of elements of $R$ for the variables. Equivalently it is an $A$ -algebra map $A [t_{i}] \to R$ together with the fixed map $C \to R$ . F1 therefore identifies $A [t_{i}] \otimes_{A} C$ with $C [t_{i}]$ , fixing coefficients and variables; empty variable sets are included.

givenF1

1.2

The module isomorphism in F3, after swapping tensor factors, sends $(a / m) \otimes c$ to $a c / \overline{m}$ and has inverse $c / \overline{m} \mapsto (1 / m) \otimes c$ . These formulas preserve multiplication and 1. They also apply when $0 \in \overline{M}$ , in which case both rings are zero, and when $M = {1}$ , in which case both are $C$ .

F3algebra

2.1

A map out of the quotient must kill each element of $I$ , which under the preceding identification means killing $I C [t_{i}]$ . This proves the quotient formula by the same universal property. The module quotient map in F2 is consistent with it: multiplication of pure tensors is sent to the product of their images, so it is a ring map. For $I = 0$ this is the polynomial formula and for $I = (1)$ it is the zero ring.

F1F2step 1.1

3.1

For instance, base change of $k [x, y, t] / (y^{2} - x^{3} - t x)$ along $k [t] \to k [u, v]$ , $t \mapsto u v$ , gives $k [x, y, u, v] / (y^{2} - x^{3} - u v x)$ ; along $t \mapsto 3$ it gives $k [x, y] / (y^{2} - x^{3} - 3 x)$ . Finitely many generators and relations remain finite. The substitution follows from the displayed maps and holds in every characteristic.

step 1.1step 2.1algebra∎

Depends on

Used by

Finite type under base change and products over a field Corollary
A reduced field spectrum becomes nonreduced Counterexample
An integral real scheme splits over the complex numbers Counterexample
A closed-immersion fibre is one residue point or empty Example
A real conic acquires complex points Example
An empty fibre from a zero tensor ring Example
Quadratic fibres over rational points and the generic point Example
The fibres of xy=t Example
The ideal of a polynomial graph Example
The self fibre product of the quadratic cover Example
Affine charts after extension of the ground field Lemma
Base change of immersions Lemma
Intersections of subschemes Lemma
Local finiteness conditions under base change Lemma
Points of a fibre product via residue-field tensors Lemma
Why geometric properties differ from ordinary ones Remark
Coordinate ring of an affine fibre Theorem

Dependency tree · two levels

15 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

Vakil 10.2.A, B, F (standard reference, not scraped)