ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

Localisation need not commute with infinite products

Example

Fix a prime number $p$ , let $S = {p^{n} : n \in N}$ , and let

P = \prod_{n \geq 0} Z .

Then the natural map

S^{- 1} P ⟶ \prod_{n \geq 0} S^{- 1} Z = \prod_{n \geq 0} Z [1 / p]

is not surjective. So localisation need not commute with infinite products.

Facts & Assumptions

Given: A prime number $p$ , the multiplicative set $S = {p^{n} : n \in N}$ , and the product module $P = \prod_{n \geq 0} Z$ .

[L1]

Localisation commutes with arbitrary direct sums, but no corresponding product statement has been proved (Localisation commutes with quotient modules and arbitrary direct sums).

[L2]

An element of a localisation $S^{- 1} P$ has one common denominator for all coordinates, because it is represented by a single fraction $x / s$ (Localisation of a module at a multiplicative subset).

Verification

technique · direct

1.1

The family $y = (1, 1 / p, 1 / p^{2}, \dots)$ is an element of $\prod_{n \geq 0} Z [1 / p]$ .

given

1.2

Suppose $y$ came from an element of $S^{- 1} P$ . By [L2], it would have the form $(a_{0}, a_{1}, \dots) / p^{r}$ for some fixed $r \geq 0$ and integers $a_{n}$ . Then the $n$ th coordinate equation $a_{n} / p^{r} = 1 / p^{n}$ would force $a_{n} = p^{r - n}$ in $Z$ for every $n > r$ , impossible.

L2algebra

2.1

Therefore the displayed map is not surjective, so localisation does not commute with this infinite product. The contrast with [L1] is exactly the point of the example.

L1step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise 12.27 (standard reference, not scraped)