Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09
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.

Integer abelian structure and rank by finite reduction

Statement

Every subgroup of Zn is free of rank at most n. Every subgroup of a finitely generated abelian group is finitely generated. Every finitely generated abelian group M has a decomposition M≅Zr⊕⨁j=1tZ/djZ, where dj>1. Its torsion subgroup is precisely the finite summand, and r is intrinsic. A surjection between finitely generated abelian groups with finite kernel preserves r. Empty sums and n=0 are allowed.

Facts & Assumptions

Given: n is a nonnegative integer; all groups in the decomposition and rank assertions are abelian.

[F3]

A nonempty set of natural numbers has a least member (The well-ordering principle).

[F4]

The quotient by a homomorphism kernel is its image (First isomorphism theorem for groups: G/ker⁡f≅im⁡f).

[F5]
[F7]

Integer multiplication identifies abelian groups with Z-modules (Abelian groups and Z-modules have the same objects and morphisms).

Proof

1.1F1F7given

For K≤Zn, induct on n. When n=0, K=0 has the empty basis. For n>0, project to the last coordinate: its image is dZ. If d=0, apply the induction hypothesis in Zn−1. If d>0, take v∈K projecting to d. For each x∈K, write its last coordinate uniquely as ad; then x−av lies in the projection kernel K0. Thus K=Zv⊕K0: the intersection is zero because ad=0 implies a=0. A basis of K0 together with v spans and is independent, so has at most n members. Only one lift at each of at most n stages is selected.

2.1F7step 1.1

Choose a finite ordered generating list of M, giving π:Zn↠M. For any subgroup L≤M, its inverse image under π is free with a finite basis by step 1.1. Images of that basis generate L, since every l∈L has a preimage. In particular K=ker⁡π has a finite basis, whose columns form an integer matrix A.

3.1step 2.1algebra

Row swaps, column swaps, sign changes, and adding an integer multiple of another row or column are invertible: undo the swap or sign, or subtract the same multiple. Column operations preserve the image subgroup, while a row operation carries it by an automorphism of Zn and therefore induces an isomorphism of quotients. If the current rectangle is zero, stop. Otherwise move a nonzero entry to its top left and change its sign to obtain a positive pivot d.

4.1F2F3step 3.1

If an entry in the pivot row is a=qd+r with 0<r<d, subtract q times the pivot column and swap that column into the pivot position. The new positive pivot is r<d. The same procedure with rows treats the pivot column. If all row and column entries are divisible by d, clear them. If the remaining rectangle has an entry b not divisible by d, add its row to the pivot row. The first pivot stays d, while the pivot row now contains b; column division again decreases the pivot. Each failed divisibility therefore strictly decreases a positive integer. Such descents terminate, since the attained pivots have a least member.

5.1F4step 3.1step 4.1

The terminal pivot divides the entire rectangle. Clear its row and column and repeat on the smaller rectangle. There are at most min⁡(n,columns⁡(A)) pivots. The resulting diagonal d1,…,dk>0 presents the quotient as ⨁j=1kZ/djZ⊕Zn−k: the coordinate quotient map is onto and its kernel is exactly the diagonal image. Delete unit summands, which are zero. A zero matrix has k=0; an empty matrix gives the same rule.

6.1F2step 5.1

Each finite cyclic summand has exactly the dj residues 0,…,dj−1. Their finite product is finite and torsion. A nonzero integer vector has infinite order, since a nonzero coordinate cannot be annihilated by a nonzero integer. Hence the displayed finite summand is exactly the torsion subgroup. In particular a finitely generated torsion group is finite, and a finitely generated torsion-free abelian group is free.

7.1F5F6step 5.1step 6.1

Let V(M)=Hom⁡(M,(Q,+)) with pointwise rational addition and scalar multiplication. The vector space laws follow pointwise from the field laws. A map to Q kills every finite-order element: da=0 implies a=0. Evaluation on the r free generators identifies V(M) with Qr: any assigned rational values extend by ∑njej+t↦∑njaj, and this is the only extension. If a second decomposition has r′ free generators, the resulting two bases of V(M) give r≤r′ and r′≤r. Thus r=r′, including r=0.

8.1F6step 7.1∎

If f:M↠N has finite kernel, every u:M→Q kills that kernel by step 7.1. Define uˉ(f(x))=u(x); different lifts differ by the kernel, so this is well-defined, additive and unique. Thus precomposition by f is a rational-linear bijection V(N)→V(M). Transporting bases and applying the independence bound twice proves equal ranks.

Source notes

Keith Conrad, Modules over a PID, Theorem 2.2, pp.2–3; finite coordinate induction specialized to Z; Michael Brussel, Finitely Generated Modules over a PID, Theorem 1.0.1, p.3; Theorem 2.1.2, pp.4–5, Euclidean branch; section 3.2, p.8. Rank invariance via Hom(-,Q) is proved locally. Conrad Theorem 2.2 supports the finite projection splitting; Brussel Theorem 2.1.2 supports integer pivot descent. Both passages were read in full. Rank invariance is derived here using Hom(-,Q); no general PID factorization, maximal ideal, or choice axiom is used.

Depends on

Used by

Dependency tree · two levels

56 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