TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Universal property of an inverse limit of modules

Statement

Let $M_{1} \overset{φ_{2}}{\leftarrow} M_{2} \overset{φ_{3}}{\leftarrow} M_{3} \overset{}{\leftarrow} \dots$ be an inverse system of $R$ -modules. For every $R$ -module $N$ , giving an $R$ -linear map $f ⁣ : N \to \underset{\leftarrow}{l i m} M_{n}$ is equivalent to giving a family of $R$ -linear maps $f_{n} ⁣ : N \to M_{n}$ such that $φ_{n} \circ f_{n} = f_{n - 1} (n \geq 2) .$

Equivalently, the projections $π_{n} ⁣ : \underset{\leftarrow}{l i m} M_{n} \to M_{n}$ form a terminal compatible cone.

Facts & Assumptions

Given: An inverse system $(M_{n}, φ_{n})$ of $R$ -modules and an $R$ -module $N$ .

[L1]

The inverse limit is the compatible-element submodule of the product $\underset{\leftarrow}{l i m} M_{n} = {(x_{n}) \in \prod M_{n} : φ_{n} (x_{n}) = x_{n - 1} for n \geq 2}$ with projections to the coordinates (Inverse systems and inverse limits of modules).

Proof

technique · direct

1.1

If $f ⁣ : N \to \underset{\leftarrow}{l i m} M_{n}$ is $R$ -linear, define $f_{n} : = π_{n} \circ f ⁣ : N \to M_{n} .$ For each $x \in N$ , the element $f (x)$ lies in the compatible submodule from [L1], so its coordinates satisfy $φ_{n} (f_{n} (x)) = f_{n - 1} (x)$ for every $n \geq 2$ . Thus the family $(f_{n})$ is compatible.

L1given

1.2

Conversely, let $(f_{n})$ be a compatible family and define $f (x) : = (f_{n} (x))_{n \geq 1} \in \prod M_{n} .$ Compatibility says $φ_{n} (f_{n} (x)) = f_{n - 1} (x)$ for every $n \geq 2$ , so $f (x)$ actually lies in $\underset{\leftarrow}{l i m} M_{n}$ . Since products and coordinate maps are $R$ -linear, $f$ is $R$ -linear.

L1givenconstruct

2.1

The two constructions are inverse to each other: starting from $f$ and then taking coordinates recovers each $f_{n}$ , while starting from $(f_{n})$ and then forming $f$ gives the unique map whose $n$ th coordinate is $f_{n}$ .

step 1.1step 1.2

3.1

Therefore maps $N \to \underset{\leftarrow}{l i m} M_{n}$ are in bijection with compatible families $(f_{n})$ , which is exactly the terminal-cone universal property.

step 2.1∎

Depends on

Inverse systems and inverse limits of modules

Used by

Equivalent adic filtrations have canonically isomorphic completions Example
Inverse limits preserve kernels Theorem
Kernel and universal property of adic completion Theorem

Dependency tree · one level

1 result within one dependency step 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., §22.5 (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, Proposition 9.5 (standard reference, not scraped)
The Stacks Project, Section 10.87 (standard reference, not scraped)