Diagonalization of possibly singular matrices over a PID

Every square matrix over a principal ideal domain admits unimodular row and column transformations to a diagonal matrix, including matrices with nontrivial kernel. No divisibility ordering or normalization of the diagonal entries is asserted.

The construction uses Mathlib's Submodule.smithNormalForm on the image. Since the image is free, its basis lifts along the matrix map; adjoining a basis of the kernel gives a basis of the source. A finite permutation aligns the lifted basis with the image's diagonal positions. Thus zero diagonal positions are retained, as required when computing fixed modules of integral automorphisms after scalar extension.

The basis-level Smith form is due to Mathlib's finite-free PID development. The kernel/image basis assembly uses Module.Basis.ofExactLift. The matrix conversion uses Module.Basis.toMatrix_eq_diagonal_iff, change-of-basis identities and Equiv.Perm.exists_extending_pair to align the nonzero diagonal positions.

theorem Matrix.exists_mul_mul_eq_diagonal {R : Type u_1} {ι : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [Fintype ι] [DecidableEq ι] (A : Matrix ι ι R) : ∃ (L : Matrix ι ι R) (Q : Matrix ι ι R) (d : ι → R), IsUnit L.det ∧ IsUnit Q.det ∧ L * A * Q = diagonal d

Every square matrix over a principal ideal domain is equivalent to a diagonal matrix by transformations of unit determinant. The matrix may be singular, and zero diagonal entries are allowed; no divisibility chain is asserted.