ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-16

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.

Tensoring the injection $k [x] \overset{\cdot x}{\to} k [x]$ with $k [x] / (x)$ gives the zero map

Example

Let $k$ be a field and set $A : = k [x]$ . Multiplication by $x$ is an injection $μ_{x} : A \to A$ , but after tensoring with $A / (x)$ the induced map

$μ_{x} \otimes 1 : A \otimes_{A} A / (x) ⟶ A \otimes_{A} A / (x)$

is the zero map between nonzero modules.

Facts & Assumptions

Given: A field $k$ , the polynomial ring $A = k [x]$ , and the principal ideal $(x)$ .

[L1]

Polynomials are finitely supported coefficient families; in particular $x$ is nonzero and $1 \notin (x)$ (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L2]

A polynomial ring over an integral domain is an integral domain (A polynomial ring over an integral domain is an integral domain).

[L3]

The tensor-unit isomorphism sends $a \otimes \overline{b}$ to $a \overline{b}$ , and $A \otimes_{A} A / (x) ≅ A / (x)$ (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ , $M \otimes_{R} R / I ≅ M / I M$ naturally).

Verification

technique · direct

1.1givenL1L2algebra

A field is an integral domain, so [L2] makes $A$ an integral domain. Since $x \neq 0$ by [L1], $x a = x b$ implies $x (a - b) = 0$ and hence $a = b$ ; therefore $μ_{x}$ is injective.

1.2givenL3

Under [L3], the tensor map sends the class $\overline{a}$ to $\overline{x a} = 0$ because $x \in (x)$ . Thus $μ_{x} \otimes 1$ is the zero map.

2.1step 1.1step 1.2L1∎

The module $A / (x)$ is nonzero because $1 \notin (x)$ by [L1]. Hence step 1.2 is a zero map on a nonzero module and is not injective, despite step 1.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

Christopher Dennis, Week 4 (standard reference, not scraped)

Tensoring the injection k[x]→⋅xk[x]k[x]⋅x​k[x] with k[x]/(x)k[x]/(x) gives the zero map