Two-sided unimodular equivalence of matrices

Matrices related by L * A * R with L and R in SL. Nothing here assumes a Smith normal form or a divisibility chain along a diagonal, so these facts sit below that theory rather than inside it, and hold over an arbitrary finite index type. The corresponding statement for merely invertible factors is Matrix.GeneralLinearGroup.inv_mul_mul_inv_of_mul_mul_eq, in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Equivalence.

Main results

• Matrix.prod_eq_det_of_mul_mul_eq_diagonal: the product of a diagonalisation's diagonal entries is the determinant.
• Matrix.exists_SL_mul_mul_eq_of_mul_mul_eq: two matrices carried to a common value by SL-transformations are themselves SL-equivalent.
• Matrix.exists_eq_diagonal_mul_iff: a matrix A with det A = ∏ i, d i a non-zero-divisor lies in diagonal d * SL exactly when d i divides every entry of the i-th row of A.

theorem Matrix.prod_eq_det_of_mul_mul_eq_diagonal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Type u_3} [CommRing S] {A : Matrix ι ι S} {L R : SpecialLinearGroup ι S} {d : ι → S} (h : ↑L * A * ↑R = diagonal d) : ∏ i : ι, d i = A.det

The product of a diagonalisation's diagonal entries is the determinant. Both SL factors have determinant 1, so taking determinants through L * A * R = diagonal d leaves the product of the diagonal.

No divisibility chain is assumed, so d need not be the invariant factors.

theorem Matrix.exists_SL_mul_mul_eq_of_mul_mul_eq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {S : Type u_3} [CommRing S] {A B : Matrix ι κ S} {LA LB : SpecialLinearGroup ι S} {RA RB : SpecialLinearGroup κ S} (h : ↑LA * A * ↑RA = ↑LB * B * ↑RB) : ∃ (P : SpecialLinearGroup ι S) (Q : SpecialLinearGroup κ S), ↑P * A * ↑Q = B

Matrices sharing an SL-transform are SL-equivalent. If L_A A R_A = L_B B R_B then L_B⁻¹ L_A and R_A R_B⁻¹ carry A to B.

Pure group algebra: nothing is assumed about the common value, which need not be diagonal. Callers holding two diagonalisations with equal diagonals compose them into this single hypothesis.

theorem Matrix.exists_eq_diagonal_mul_iff {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Type u_3} [CommRing S] {d : ι → S} {A : Matrix ι ι S} (hA : A.det = ∏ i : ι, d i) (hA₀ : IsLeftRegular A.det) : (∃ (g : SpecialLinearGroup ι S), A = diagonal d * ↑g) ↔ ∀ (i j : ι), d i ∣ A i j

Right SL-cosets of a diagonal matrix. If det A = ∏ i, d i is a left non-zero-divisor, then A = diagonal d * g for some g ∈ SL exactly when d i divides every entry of the i-th row of A.