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

The index of a full-rank subgroup of Zn is the absolute determinant of a generating matrix

Statement

Let n≥1.

  1. Let A∈Mn(Z) and let L=AZn⊆Zn be the subgroup generated by the columns of A. If det⁡A≠0, then the quotient group Zn/L is finite of order ∣det⁡A∣; if det⁡A=0, then Zn/L is infinite.
  2. Every subgroup L⊆Zn is AZn for some A∈Mn(Z).

So a subgroup of Zn has finite index exactly when it is generated by the columns of a square integer matrix of nonzero determinant, and its index is then the absolute determinant of every such matrix.

Facts & Assumptions

Given: A natural number n≥1, and for clause 1 a matrix A∈Mn(Z) with L=AZn.

[F1]

Abelian groups and Z-modules have the same objects and morphisms, so a subgroup of Zn is a Z-submodule and the quotient group is the quotient module (Abelian groups and Z-modules have the same objects and morphisms). The ring Z is a commutative ring with identity in which a product of nonzero elements is nonzero, so it is an integral domain, and every subgroup of (Z,+) is cyclic, so every ideal of Z is principal: Z is a principal ideal domain (The integers form a commutative ring, The integers have no zero divisors; multiplicative cancellation, Every subgroup of (Z,+) is ⟨n⟩=nZ for exactly one natural number n, Principal ideal domain).

[F2]

For every A∈Mm×n(R) over a PID there are invertible P,Q with PAQ=diag⁡(d1,…,dr,0,…,0) and d1∣⋯∣dr, every di≠0; equivalence means B=PAQ with P∈GL⁡m(R) and Q∈GL⁡n(R) (Every matrix over a PID has a Smith normal form, Matrix equivalence and Smith normal form over a PID).

[F4]

For every module homomorphism f:M→N there is an isomorphism M/ker⁡f≅im⁡f (First isomorphism theorem for modules: M/ker⁡f≅im⁡f).

[F5]

For a submodule of a free module of finite rank n over a PID there is a basis e1,…,en of the ambient module and nonzero elements a1∣⋯∣ar with r≤n such that a1e1,…,arer is a basis of the submodule (Simultaneous bases for a submodule of a finite free module over a PID).

Proof

technique · direct
1.1givenF1F2

By [F1] the quotient Zn/L is a quotient of Z-modules, and by [F2] applied over the PID Z there are P,Q∈GL⁡n(Z) with PAQ=D=diag⁡(d1,…,dr,0,…,0), every di≠0.

1.2givenF3algebra

By [F3], det⁡P and det⁡Q are units of Z, hence ±1, so ∣det⁡D∣=∣det⁡P∣∣det⁡A∣∣det⁡Q∣=∣det⁡A∣; and D is diagonal, so det⁡D=d1⋯dr⋅0 n−r, which is d1⋯dn when r=n and 0 when r<n.

2.1step 1.1algebra

Since Q is invertible over Z, QZn=Zn, so AZn=AQZn=P−1DZn. The map x↦Px is an automorphism of Zn carrying L=P−1DZn onto DZn, so it induces an isomorphism Zn/L≅Zn/DZn.

3.1step 2.1F4algebra

Write di=0 for r<i≤n, and let π:Zn→⨁i=1nZ/diZ send x to the tuple of residues xi+diZ, a surjective homomorphism whose kernel is DZn. By [F4], Zn/DZn≅⨁i=1nZ/diZ, and with step 2.1 this group is isomorphic to Zn/L.

4.1step 1.2step 3.1algebra

If det⁡A≠0 then det⁡D≠0 by step 1.2, so r=n and every di is nonzero; each Z/diZ is then finite of order ∣di∣, so by step 3.1 the quotient Zn/L is finite of order ∣d1⋯dn∣=∣det⁡D∣=∣det⁡A∣.

4.2step 1.2step 3.1algebra

If det⁡A=0 then det⁡D=0 by step 1.2, so r<n and dn=0; the summand Z/dnZ=Z is infinite, so by step 3.1 the quotient Zn/L is infinite. This proves clause 1.

5.1givenF1F5step 4.1step 4.2construct∎

For clause 2, let L be any subgroup of Zn. By [F1] it is a Z-submodule of the free module Zn of rank n over the PID Z, so [F5] gives a basis e1,…,en of Zn and nonzero a1∣⋯∣ar, r≤n, with a1e1,…,arer a basis of L. Let A be the matrix whose first r columns are a1e1,…,arer and whose remaining n−r columns are zero; its entries are integers because the ei and the ai are. Then AZn is the set of integer combinations of those columns, which is exactly L, so clause 2 holds; combining it with clause 1 gives the final sentence of the Statement.

Remark

The corollary is what makes the determinant a counting invariant: clause 2 says every subgroup of Zn is a column lattice, and for A with nonzero determinant the columns of A generate a subgroup of Zn of index exactly ∣det⁡A∣, and the Smith invariant factors d1∣⋯∣dn refine that single number into the isomorphism type ⨁iZ/diZ of the quotient. Nothing here needs a Euclidean volume: the count comes from the invariant factors, and the determinant enters only because it is unchanged up to sign by multiplication with matrices invertible over Z.

Depends on

Used by

Dependency tree · two levels

77 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