TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Simultaneous bases for a submodule of a finite free module over a PID

Statement

Let $R$ be a PID, let $M$ be free of finite rank $n$ , and let $N \leq M$ . For a submodule $N$ of a finite free PID module, aligned bases have nonzero factors $a_{1} ∣ \dots ∣ a_{r}$ . More precisely, there is a basis $e_{1}, \dots, e_{n}$ of $M$ and nonzero elements $a_{1} ∣ \dots ∣ a_{r}$ such that there is a basis $a_{1} e_{1}, \dots, a_{r} e_{r}$ of the submodule with $r \leq n$ .

Facts & Assumptions

Given: Induction on natural-number rank (The principle of mathematical induction) and the rank convention of Invariant basis number and the rank of a free module.

[L1]

If $0 \neq N \leq M$ with $M$ finite free over a PID, there are $ψ \in M^{*}$ , $e_{1} \in M$ , and $0 \neq a \in R$ such that $ψ (e_{1}) = 1$ , $M = R e_{1} \oplus \ker ψ$ , $N = R a e_{1} \oplus (N \cap \ker ψ)$ , and $ψ (N) = (a)$ is maximal among the functional value ideals containing a fixed nonzero value ideal (A nonzero PID submodule has a maximal coordinate ideal and a primitive pivot).

Proof

technique · induction

1.1base

If $n = 0$ , then $M = N = 0$ and both bases are empty, giving $r = 0$ . If $N = 0$ for any $n$ , choose any basis of $M$ and the empty basis of $N$ .

1.2ih

Assume the theorem for free ambient modules of rank less than a fixed $n \geq 1$ .

1.3L1

For nonzero $N \leq M$ of rank $n$ , apply [L1] to obtain $M = R e_{1} \oplus M_{1}$ and $N = R a_{1} e_{1} \oplus N_{1}$ , where $M_{1} = \ker ψ$ is free of rank $n - 1$ and $N_{1} = N \cap M_{1}$ .

2.1step 1.3step 1.2L1discharge-induction∎

Apply the induction hypothesis of step 1.2 to $N_{1} \leq M_{1}$ , obtaining basis vectors $e_{2}, \dots, e_{n}$ and, when $N_{1} \neq 0$ , factors $a_{2} ∣ \dots ∣ a_{r}$ . If $N_{1} = 0$ , then $r = 1$ and the required chain consists only of $a_{1}$ . Otherwise let $e_{1}^{*}, e_{2}^{*}$ be the coordinate functionals of the combined ambient basis and put $φ = e_{1}^{*} + e_{2}^{*}$ . Since $φ (a_{1} e_{1}) = a_{1}$ , one has $(a_{1}) \subseteq φ (N)$ ; maximality of the pivot value ideal in [L1] forces equality, and $a_{2} = φ (a_{2} e_{2}) \in (a_{1})$ , so $a_{1} ∣ a_{2}$ . Concatenating the bases gives the required aligned bases and chain, with $r \leq n$ , and completes the induction.

Depends on

Used by

Dependency tree · two levels

10 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

K. Conrad, Modules over a PID, Theorem 2.14 (standard reference, not scraped)