SmithMatrix106.lean

1 import Mathlib.LinearAlgebra.FreeModule.PID
2 import Mathlib.LinearAlgebra.Matrix.Basis
3 import Mathlib.LinearAlgebra.Matrix.Nondegenerate
4 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
5 import Mathlib.LinearAlgebra.Dimension.Finrank
6 
7 /-! Integral left and right basis changes for an injective square matrix over
8 a PID. The changes of basis are retained as actual general linear matrices. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.SmithMatrix106
12 open Matrix Module
13 variable {ι R : Type*} [Fintype ι] [DecidableEq ι]
14   [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
15 
16 def basisGL (b : Basis ι R (ι → R)) : GL ι R where
17   val := (Pi.basisFun R ι).toMatrix b
18   inv := b.toMatrix (Pi.basisFun R ι)
19   val_inv := by rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]
20   inv_val := by rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]
21 
22 omit [IsDomain R] [IsPrincipalIdealRing R] in
23 @[simp] theorem basisGL_apply (b : Basis ι R (ι → R)) (i j : ι) :
24     basisGL b i j = b j i := by
25   simp [basisGL, Basis.toMatrix_apply]
26 
27 theorem exists_diagonal (A : Matrix ι ι R) (hA : A.det ≠ 0) :
28     ∃ P Q : GL ι R, ∃ d : ι → R,
29       (∀ i, d i ≠ 0) ∧ A = P.val * diagonal d * Q.val := by
30   let f := A.mulVecLin
31   have hf : Function.Injective f := Matrix.mulVec_injective_of_det_ne_zero hA
32   let e := LinearEquiv.ofInjective f hf
33   have hr : Module.finrank R (LinearMap.range f) = Module.finrank R (ι → R) :=
34     e.finrank_eq.symm
35   let b := (LinearMap.range f).smithNormalFormTopBasis (Pi.basisFun R ι) hr
36   let c := (LinearMap.range f).smithNormalFormBotBasis (Pi.basisFun R ι) hr
37   let d := (LinearMap.range f).smithNormalFormCoeffs (Pi.basisFun R ι) hr
38   let q := c.map e.symm
39   have hd : ∀ i, d i ≠ 0 :=
40     (LinearMap.range f).smithNormalFormCoeffs_ne_zero (Pi.basisFun R ι) hr
41   have hcol : ∀ j, A *ᵥ q j = d j • b j := by
42     intro j
43     have h := (LinearMap.range f).smithNormalFormBotBasis_def (Pi.basisFun R ι) hr j
44     change (c j : ι → R) = d j • b j at h
45     change f (e.symm (c j)) = d j • b j
46     rw [LinearEquiv.ofInjective_symm_apply]
47     exact h
48   have heq : A * (basisGL q).val = (basisGL b).val * diagonal d := by
49     ext i j
50     rw [Matrix.mul_diagonal]
51     have h := congrFun (hcol j) i
52     simpa [Matrix.mul_apply, Matrix.mulVec, dotProduct, mul_comm] using h
53   refine ⟨basisGL b, (basisGL q)⁻¹, d, hd, ?_⟩
54   have h := congrArg (fun X : Matrix ι ι R => X * ((basisGL q)⁻¹).val) heq
55   simpa only [Matrix.mul_assoc, Units.mul_inv, Matrix.mul_one] using h
56 
57 end PaperXI.SmithMatrix106

Back to source controls