ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-09-01

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.

Completion need not be exact without a finiteness hypothesis

Example

Let $p$ be a prime integer, let

M : = ⨁_{n \geq 1} Z e_{n},

and define an endomorphism

f ⁣ : M \to M, f (e_{n}) = p^{n} e_{n} .

Then

0 \to M \overset{f}{\to} M \to coker (f) \to 0

is exact, but the induced map on $(p)$ -adic completions

\hat{f} ⁣ : \hat{M} \to \hat{M}

is not surjective. So completion is not exact without a finiteness hypothesis.

Facts & Assumptions

Given: A prime integer $p$ , the module $M = ⨁_{n \geq 1} Z e_{n}$ , and the map $f (e_{n}) = p^{n} e_{n}$ .

[L1]

The $(p)$ -adic completion of a module is the inverse limit of the quotients $M / p^{r} M$ (The $I$ -adic completion of a module).

[L2]

Exactness of completion on finite modules is a genuinely finite statement (Adic completion is exact on finite modules over a Noetherian ring).

Verification

technique · direct

1.1

The map $f$ is injective because, if $f ⁣ (\sum_{i = 1}^{N} a_{i} e_{i}) = \sum_{i = 1}^{N} a_{i} p^{i} e_{i} = 0,$ then every coefficient $a_{i} p^{i}$ is $0$ and hence every $a_{i}$ is $0$ . Therefore $0 \to M \overset{f}{\to} M \to coker (f) \to 0$ is exact.

givenalgebra

1.2

For each $N \geq 1$ , set $s_{N} : = \sum_{n = 1}^{N} p^{n} e_{n} \in M .$ If $N^{'} > N$ , then $s_{N^{'}} - s_{N} = \sum_{n = N + 1}^{N^{'}} p^{n} e_{n} \in p^{N + 1} M .$ For each $r \geq 1$ , define $x_{r}$ to be the class of $s_{N}$ modulo $p^{r} M$ for any $N \geq r$ . The displayed containment makes this independent of $N$ , and the classes $x_{r}$ are compatible under reduction. Hence $x = (x_{r})_{r}$ is an element of $\hat{M}$ by [L1].

L1construct

2.1

Suppose $x = \hat{f} (y)$ for some $y \in \hat{M}$ . Let $\overline{y}$ be the image of $y$ in $M / p M = ⨁_{n \geq 1} (Z / p Z) e_{n} .$ Because this is a direct sum, $\overline{y}$ has finite support. But for each $n \geq 1$ , comparing the $e_{n}$ -component modulo $p^{n + 1}$ shows that the $e_{n}$ -coefficient of $\overline{y}$ must be $1 \in Z / p Z$ , since $f$ multiplies the $e_{n}$ -coordinate by $p^{n}$ and $x$ has $e_{n}$ -coefficient $p^{n}$ modulo $p^{n + 1}$ . Thus $\overline{y}$ would have infinitely many nonzero coordinates, a contradiction. So $x \notin im (\hat{f})$ .

step 1.2algebra

3.1

Every partial sum $s_{N}$ from step 1.2 lies in $im (f)$ , so its image in $coker (f)$ is $0$ . Therefore the compatible family $x \in \hat{M}$ maps to $0$ in every quotient $coker (f) / p^{r} coker (f)$ , hence to $0$ in $\hat{coker (f)}$ . Step 2.1 showed that $x \notin im (\hat{f})$ , so the completed sequence fails exactness at the middle term. This is exactly the failure excluded by the finite-generation hypothesis in [L2].

L2step 1.2step 2.1∎

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 22.19 (standard reference, not scraped)