Smith normal form over ℤ with special linear transformations

Every square integer matrix with positive determinant can be brought to diagonal form with positive diagonal entries in which each entry divides the next, using row and column operations of determinant one:

• Matrix.exists_smith_normal_form_of_det_pos: for A : Matrix (Fin n) (Fin n) ℤ with 0 < A.det there are L R : SpecialLinearGroup (Fin n) ℤ and a positive d : Fin n → ℤ, monotone under divisibility, with L * A * R = diagonal d.
• Matrix.exists_smith_normal_form_of_det_ne_zero: without a sign assumption, the same positive diagonal is obtained using general-linear transformations.
• Matrix.smith_normal_form_unique: two nonnegative chained diagonals in the same GL_n(ℤ)-equivalence class are equal, so the invariant factors of A are well defined.
• Matrix.invariant_factor_zero_dvd_entries: the first entry of a chained diagonal form divides every entry of A. The converse direction, and the general fact both rest on, are Matrix.dvd_diag_of_dvd_entries and Matrix.dvd_mul_mul_apply in TauCeti/LinearAlgebra/Matrix/Divisibility.lean — neither carries a Smith-normal-form hypothesis, so neither lives here.
• Matrix.associated_invariant_factor_zero_gcd and Matrix.invariant_factor_zero_eq_gcd: hence the first entry is an associate of the gcd of the entries of A, and equals it once its sign is known — so it is readable off the matrix without choosing a factorisation.
• Matrix.exists_SL_mul_mul_eq_of_det_eq_of_dvd_iff: consequently a nonsingular 2 × 2 integer matrix is determined up to SL₂(ℤ)-equivalence by its determinant and the common divisors of its entries.

Mathlib's Submodule.smithNormalForm provides basis-level diagonalization over a PID; this file supplies the matrix-level statement over ℤ, refined in three ways that the basis-level result does not give: the transforming matrices have determinant 1 (not merely unit determinant), the diagonal entries are positive, and successive entries divide each other (the invariant-factor chain). The proof first diagonalises using the basis-level theorem, corrects signs, and then establishes the divisibility chain by repeated Bézout pivot steps on 2 × 2 blocks.

This is the elementary divisor theorem in the form needed for the theory of Hecke rings of GL_n: it produces the diagonal double coset representatives of Shimura, chapter 3.

Ported from the AINTLIB LeanModularForms project (Chris Birkbeck), Apache-2.0, at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08: the diagonalisation and uniqueness half from LeanModularForms/HeckeRIngs/GLn/DiagonalCosets.lean — the pure-matrix part of that file, its Hecke-theoretic part being ported separately on top of the arithmetic Hecke triple — and the content characterisation from HeckeRIngs/GLn/CongruenceHecke/AtkinLehner.lean.

References

• Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, §3.2

Diagonalisation with special linear transformations

The divisibility chain

Bézout pivot steps on 2 × 2 blocks replace a pair of diagonal entries a, b by gcd a b and (a / g) * (b / g) * g, strictly decreasing the head entry unless it already divides b. Iterating produces a diagonal in which each entry divides the next.

theorem Matrix.exists_smith_normal_form_of_det_pos {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (hA : 0 < A.det) : ∃ (L : SpecialLinearGroup (Fin n) ℤ) (R : SpecialLinearGroup (Fin n) ℤ) (d : Fin n → ℤ), (∀ (i : Fin n), 0 < d i) ∧ (∀ ⦃i j : Fin n⦄, i ≤ j → d i ∣ d j) ∧ ↑L * A * ↑R = diagonal d

Smith normal form over ℤ with special linear transformations. Every square integer matrix A with positive determinant can be brought to diagonal form by determinant-one row and column operations, with positive diagonal entries each dividing the next (the invariant factors of A).

theorem Matrix.exists_smith_normal_form_of_det_ne_zero {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (hA : A.det ≠ 0) : ∃ (L : GL (Fin n) ℤ) (R : GL (Fin n) ℤ) (d : Fin n → ℤ), (∀ (i : Fin n), 0 < d i) ∧ (∀ ⦃i j : Fin n⦄, i ≤ j → d i ∣ d j) ∧ ↑L * A * ↑R = diagonal d

Smith normal form for every nonsingular integer matrix. Every square integer matrix with nonzero determinant is equivalent under general-linear row and column operations to a positive diagonal whose entries form a divisibility chain.

When the determinant is positive, the transformations can be chosen special linear by exists_smith_normal_form_of_det_pos. For a negative determinant, changing the sign of one row makes it positive; the resulting single-coordinate sign matrix is absorbed into the left general-linear factor.

Uniqueness of the invariant factors

The partial products d 0 * ⋯ * d (k-1) of a chained diagonal are determined by the GL_n(ℤ)-equivalence class, by a Cauchy–Binet expansion of the leading k × k minor.

theorem Matrix.smith_normal_form_unique {n : ℕ} {c d : Fin n → ℤ} (hc_pos : ∀ (i : Fin n), 0 ≤ c i) (hd_pos : ∀ (i : Fin n), 0 ≤ d i) (hc : ∀ ⦃i j : Fin n⦄, i ≤ j → c i ∣ c j) (hd : ∀ ⦃i j : Fin n⦄, i ≤ j → d i ∣ d j) (L R : GL (Fin n) ℤ) (h : ↑L * diagonal c * ↑R = diagonal d) : c = d

Uniqueness of the Smith normal form: two nonnegative diagonals with divisibility chains in the same GL_n(ℤ)-equivalence class are equal — including singular forms, whose chains vanish from the first zero on. Together with Matrix.exists_smith_normal_form_of_det_pos this makes the invariant factors of a positive-determinant integer matrix well defined.

The first entry of a chained diagonal form is the content

The first entry of a chained diagonal form is a common divisor of the entries of the original matrix, and every common divisor divides it — so it is an associate of the gcd of the entries (equal to it up to a unit), and in particular depends only on the matrix and not on the chosen factorisation. Over ℤ, where the units are ±1, the nonnegativity that Matrix.exists_smith_normal_form_of_det_pos supplies pins the sign and the equality is exact.

Adapted from AINTLIB (Chris Birkbeck), Apache-2.0, at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/AtkinLehner.lean. The source states the two divisibility directions privately at Fin 2 as snf_first_dvd_entry₂ and dvd_snf_first_of_dvd_entries, proved by entrywise cofactor algebra; the proofs here are a re-derivation at general n, where inverting the unimodular factors removes the need for that algebra.

theorem Matrix.invariant_factor_zero_dvd_entries {n : ℕ} {S : Type u_1} [CommSemiring S] [NeZero n] (A : Matrix (Fin n) (Fin n) S) (d : Fin n → S) (hd0 : ∀ (k : Fin n), d 0 ∣ d k) (L R : GL (Fin n) S) (h : ↑L * A * ↑R = diagonal d) (i j : Fin n) : d 0 ∣ A i j

The first entry of a chained diagonal form divides every entry. If L * A * R = diagonal d with L, R unimodular and d 0 dividing every d k, then d 0 divides every entry of A.

Inverting the unimodular factors writes A = L⁻¹ * diagonal d * R⁻¹, and d 0 divides every entry of diagonal d, so dvd_mul_mul_apply carries it to every entry of A. No step is integer-specific, so this holds over any commutative semiring.

theorem Matrix.associated_invariant_factor_zero_gcd {n : ℕ} {S : Type u_1} [CommSemiring S] [NormalizedGCDMonoid S] [NeZero n] (A : Matrix (Fin n) (Fin n) S) (d : Fin n → S) (hd0 : ∀ (k : Fin n), d 0 ∣ d k) (L R : GL (Fin n) S) (h : ↑L * A * ↑R = diagonal d) : Associated (d 0) (Finset.univ.gcd fun (p : Fin n × Fin n) => A p.1 p.2)

The first entry is an associate of the content. It equals the gcd of the entries up to a unit, so up to that unit it is determined by the matrix alone — the factorisation may be chosen freely.

Matrix.smith_normal_form_unique says the whole chained diagonal is determined; this says the first entry is determined, up to a unit, by something directly readable off the matrix. The hypotheses are exactly what Finset.gcd needs; over ℤ they hold by instance, and Matrix.invariant_factor_zero_eq_gcd then pins the sign when d 0 is known nonnegative.

theorem Matrix.invariant_factor_zero_eq_gcd {n : ℕ} [NeZero n] (A : Matrix (Fin n) (Fin n) ℤ) (d : Fin n → ℤ) (hd0 : ∀ (k : Fin n), d 0 ∣ d k) (hnonneg : 0 ≤ d 0) (L R : GL (Fin n) ℤ) (h : ↑L * A * ↑R = diagonal d) : d 0 = Finset.univ.gcd fun (p : Fin n × Fin n) => A p.1 p.2

The first entry is the content, once its sign is known. This is the integer specialization of Matrix.associated_invariant_factor_zero_gcd: Finset.gcd over ℤ is normalized, so nonnegativity of d 0 — which Matrix.exists_smith_normal_form_of_det_pos supplies — upgrades the associate relation to an equality, and consumers need not redo the sign argument. The sign is the only integer-specific part; the two results above hold over a commutative semiring and a normalized GCD monoid respectively.

theorem Matrix.exists_SL_mul_mul_eq_of_det_eq_of_dvd_iff {A B : Matrix (Fin 2) (Fin 2) ℤ} (hA : A.det ≠ 0) (hdet : B.det = A.det) (hdvd : ∀ (e : ℤ), (∀ (i j : Fin 2), e ∣ A i j) ↔ ∀ (i j : Fin 2), e ∣ B i j) : ∃ (P : SpecialLinearGroup (Fin 2) ℤ) (Q : SpecialLinearGroup (Fin 2) ℤ), ↑P * A * ↑Q = B

The 2 × 2 elementary divisor classification. Two nonsingular integer matrices with the same determinant, whose entries have the same common divisors, are equivalent under SL₂(ℤ) on both sides: P * A * Q = B.

At size two the invariant factors are the content d₀ and det / d₀, and the hypothesis says exactly that the contents agree. For negative determinant, multiplying both matrices on the left by diag(-1, 1) reduces to the positive case.