Alphabeta Math
LemmaStatement: 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.

A nonzero PID submodule has a maximal coordinate ideal and a primitive pivot

Statement

Let R be a PID, let M be a nonzero finite free R-module, and let 0NM. A nonzero submodule of a finite free PID module admits a primitive pivot splitting both the ambient module and submodule. More precisely, there are ψM, e1M, a nonzero aR, and v=ae1N such that ψ(e1)=1, the ideal ψ(N)=(a) is maximal among value ideals φ(N) containing a fixed nonzero value ideal, and

M=Re1kerψ,N=Rae1(Nkerψ).

Moreover e1 belongs to a basis of M, and kerψ is free of rank one less than the rank of M.

The maximality is taken among all functional value ideals, so it remains available after the pivot is split off.

Facts & Assumptions

Given: The dual module M=HomR(M,R) of The R-module HomR(M,N) over a commutative ring and coordinate functionals from a finite free basis (The free module on a set and its standard basis).

[L1]

Every principal ideal domain is a unique factorisation domain (Every principal ideal domain is a unique factorisation domain).

Proof

technique · direct
1.1

Some coordinate functional has a nonzero value on N. Fix one such nonzero value ideal I0. By [L1], a nonzero generator of I0 has only finitely many divisor classes, so only finitely many principal ideals can contain I0. Choose a maximal value ideal among them, write it as ψ(N)=(a) with a0, and choose vN with ψ(v)=a.

L1choose
2.1

For any coordinate functional φ, let d generate (a,φ(v)) and choose r,s with d=ra+sφ(v). The functional rψ+sφ takes v to d, so its value ideal contains (d)(a); maximality in step 1.1 forces (d)=(a), hence aφ(v).

step 1.1algebra
3.1

Divisibility of every coordinate of v gives v=ae1 for some e1M. Since a=ψ(v)=aψ(e1) and a0, cancellation gives ψ(e1)=1, so e1 is primitive.

step 2.1algebra
4.1

The ideal generated by the coordinates of e1 in a basis of M is {φ(e1):φM}, so it does not depend on the basis, and ψ(e1)=1 makes it all of R. Fix a basis f1,,fn of M and let b1,,bn be the coordinates of e1 in it. For j2 let d generate (b1,bj). If d=0 then b1=bj=0 and nothing is done; otherwise write d=rb1+sbj and put A=(rsbj/db1/d), whose entries lie in R and whose determinant is (rb1+sbj)/d=1, so A1 has entries in R as well. Replacing the basis pair (f1,fj) by the pair whose coordinates are the columns of A1 again gives a basis of M, in which the coordinates of e1 at 1 and j are the entries of A(b1,bj)T=(d,0)T and the other coordinates are unchanged. Doing this for j=2,,n in turn clears the coordinates 2,,n, so the resulting basis g1,,gn has e1=cg1 with (c) the coordinate ideal, which is R. Hence c is a unit and e1,g2,,gn is a basis of M.

step 3.1algebra
5.1

Put uj=gjψ(gj)e1 for 2jn. The passage from e1,g2,,gn to e1,u2,,un is triangular with 1 on the diagonal, so the latter is again a basis of M, and each uj lies in kerψ. If m=λ1e1+j2λjuj lies in kerψ, applying ψ gives λ1=0; hence u2,,un is a basis of kerψ, which is therefore free of rank n1, and zero when n=1. Every mM is ψ(m)e1+(mψ(m)e1) with the second summand in kerψ, and Re1kerψ=0 because ψ(re1)=r, so M=Re1kerψ. For wN one has ψ(w)ψ(N)=(a), say ψ(w)=ra, and then w=rv+(wrv) with wrvNkerψ; also Rvkerψ=0, since ψ(rv)=ra and a0 in the domain R. Hence N=Rae1(Nkerψ). When a is a unit, v and e1 generate the same submodule and the second decomposition reads N=Re1(Nkerψ).

step 4.1step 3.1step 1.1algebra

Depends on

Used by

Dependency tree · two levels

11 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