CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-sol)audited 2026-09-27

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.

An arbitrary algebra map does not make differentials a base change

Statement refuted

False claim: for every ring map $B \to C$ over a base ring $A$ the canonical map $C \otimes_{B} Ω_{B / A} \to Ω_{C / A}$ of (Localization, base change and functoriality of differentials) is an isomorphism. With $A = k$ a field, $B = k [x]$ and $C = k$ the map $x \mapsto 0$ , the source is the one-dimensional $k$ -vector space $k \otimes_{k [x]} Ω_{k [x] / k} ≅ k \cdot d x$ , while the target is $Ω_{k / k} = 0$ ; the canonical map is the zero map, so it is neither injective nor an isomorphism.

Facts & Assumptions

Given: A field $k$ , the $k$ -algebras $B = k [x]$ and $C = k$ with the $k$ -algebra map $ε ⁣ : k [x] \to k$ sending $x$ to $0$ .

[F1]

Universal algebraic differentials and A-derivations: for a ring map $A \to B$ , $Ω_{B / A}$ is the $B$ -module generated by the symbols $d b$ subject to additivity, the Leibniz rule, and $d a = 0$ for $a$ in the image of $A$ ; when $A = B$ the base elements are all elements of the ring, so all generators vanish.

[F2]

Differentials of a polynomial quotient and the Jacobian cokernel: for $A = k$ and $P = k [x]$ the module $Ω_{P / k}$ is free with basis $d x$ , so $Ω_{k [x] / k} ≅ k [x]$ as a $k [x]$ -module and $d x \neq 0$ .

[F3]

Localization, base change and functoriality of differentials: for an arbitrary $A$ -algebra map $B \to C$ there is a canonical $C$ -linear map $C \otimes_{B} Ω_{B / A} \to Ω_{C / A}$ , and for a general algebra map it is neither asserted injective nor asserted an isomorphism.

[F4]

Tensoring is right exact: tensoring is right exact and $(B / I) \otimes_{B} C ≅ C / I C$ ; in particular $k \otimes_{k [x]} k [x] ≅ k$ for the quotient $k = k [x] / (x)$ .

Counterexample

1.1

The source. By [F2] the module $Ω_{k [x] / k} = k [x] \cdot d x$ is free of rank one, so $k \otimes_{k [x]} Ω_{k [x] / k} ≅ k \otimes_{k [x]} k [x] ≅ k$ by [F4], a one-dimensional $k$ -vector space with basis $1 \otimes d x$ ; in particular $1 \otimes d x \neq 0$ .

F2F4algebra

2.1

The target and the map. The map $ε$ exhibits $k$ as a $k$ -algebra over itself, so every element of $k$ lies in the image of the base ring and [F1] gives $Ω_{k / k} = 0$ . The canonical map of [F3] sends $1 \otimes d x$ to $d ε (x) = d 0 = 0$ , hence is the zero map from a one-dimensional space to the zero space: not injective, and not an isomorphism. The hypothesis of a general algebra map in the base-change statement is therefore essential.

F1F3step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

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

Stacks Algebra 10.131.8 and 10.131.12 (standard reference, not scraped)
Vakil §22.2.3, p.575 (standard reference, not scraped)