Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Inverse limits preserve kernels

Statement

Let (fn) ⁣:(Mn,φn)→(Nn,ψn) be a morphism of inverse systems of R-modules. Then the kernel of the induced map lim←⁡Mn⟶lim←⁡Nn is canonically isomorphic to lim←⁡ker⁡(fn).

Consequently, if 0→An→Bn→Cn is an exact sequence of inverse systems, then 0→lim←⁡An→lim←⁡Bn→lim←⁡Cn is exact.

Facts & Assumptions

Given: A morphism of inverse systems (fn) ⁣:(Mn,φn)→(Nn,ψn).

[L1]

The inverse limit consists of the compatible elements in the product system (Inverse systems and inverse limits of modules).

[L2]

The kernel of a homomorphism is the submodule of elements mapping to 0 (Module homomorphism and isomorphism, kernel, image and cokernel).

[L3]

A map into an inverse limit is determined by its compatible coordinate maps (Universal property of an inverse limit of modules).

Proof

technique · direct
1.1L2given

For each n, let Kn:=ker⁡(fn). Compatibility of the squares ψn∘fn=fn−1∘φn shows that φn(Kn)⊆Kn−1, so the kernels form an inverse system.

1.2L1L2

An element (xn)∈lim←⁡Mn lies in the kernel of lim←⁡Mn→lim←⁡Nn exactly when fn(xn)=0 for every n. By [L2], that is equivalent to xn∈Kn for every n. Together with the compatibility condition from [L1], this says precisely that (xn)∈lim←⁡Kn.

2.1step 1.2

Thus the underlying subsets of ker⁡ ⁣(lim←⁡Mn→lim←⁡Nn)andlim←⁡ker⁡(fn) coincide inside ∏Mn, and the module structures also agree componentwise. Hence these two modules are canonically equal, in particular canonically isomorphic.

3.1step 2.1L3∎

For an exact sequence 0→An→Bn→Cn, exactness means An=ker⁡(Bn→Cn) for every n. Applying step 2.1 to the maps Bn→Cn gives ker⁡ ⁣(lim←⁡Bn→lim←⁡Cn)=lim←⁡An, which is exactly left exactness.

Depends on

Used by

Dependency tree · two levels

6 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