TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Every matrix over a PID has a Smith normal form

Statement

Every rectangular matrix over a PID is equivalent to a Smith diagonal matrix. Equivalently, for every $A \in M_{m \times n} (R)$ there are invertible $P, Q$ such that

$P A Q = diag (d_{1}, \dots, d_{r}, 0, \dots, 0), d_{1} ∣ \dots ∣ d_{r},$

with every $d_{i} \neq 0$ . This is an existence theorem over a PID and does not assert a Euclidean row-reduction algorithm.

Facts & Assumptions

Given: Matrix equivalence and Smith form as in Matrix equivalence and Smith normal form over a PID; a matrix as a homomorphism $φ : R^{n} \to R^{m}$ ; free modules are projective (Under the stated choice boundary, free modules are projective and hence flat); and the first isomorphism theorem identifies $R^{n} / \ker φ$ with $im φ$ (First isomorphism theorem for modules: $M / \ker f ≅ im f$ ).

[L1]

A submodule of a finite free PID module admits aligned bases with a divisibility chain (Simultaneous bases for a submodule of a finite free module over a PID).

[L2]

Given a section of a short exact sequence, the middle module is the direct sum of the kernel and the section image (The splitting lemma for short exact sequences of modules).

Proof

technique · constructive

1.1

Regard $A$ as $φ : R^{n} \to R^{m}$ and put $I = im φ$ . By [L1], both $I \leq R^{m}$ and $\ker φ \leq R^{n}$ are finite free; the sequence $0 \to \ker φ \to R^{n} \to I \to 0$ is exact.

givenL1

2.1

Apply [L1] to align $I$ in the codomain: choose a basis $e_{1}, \dots, e_{m}$ of $R^{m}$ such that $d_{1} e_{1}, \dots, d_{r} e_{r}$ is a basis of $I$ with $d_{1} ∣ \dots ∣ d_{r}$ .

step 1.1L1

2.2

Since $I$ is free and projective, the surjection $R^{n} \to I$ has a section. By [L2], $R^{n} = \ker φ \oplus s (I)$ . Place the lifted basis $s (d_{1} e_{1}), \dots, s (d_{r} e_{r})$ first and then a basis of the kernel to obtain a domain basis.

step 1.1L2givenchoose

3.1

In the bases from steps 2.1 and 2.2, $φ$ sends the lifted vector for $d_{i} e_{i}$ to $d_{i} e_{i}$ and kills the kernel basis, so its matrix is the displayed Smith diagonal. Empty matrices, the zero map, and all rank deficiencies give the appropriate empty or trailing-zero diagonal.

step 2.1step 2.2constructdischarge-construct∎

Depends on

Used by

Dependency tree · two levels

21 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

M. Brussel, Finitely Generated Modules over a PID, Theorem 2.1.2 (standard reference, not scraped)
K. Conrad, Modules over a PID, aligned-basis theorem (standard reference, not scraped)