FractionMatrix106.lean

1 import PaperXI.SmithMatrix106
2 import PaperXI.SplitRadical105
3 import Mathlib.RingTheory.Localization.FractionRing
4 import Mathlib.RingTheory.Localization.Integer
5 
6 /-! Clear denominators and retain both integral basis changes. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.FractionMatrix106
10 open Matrix
11 open scoped nonZeroDivisors
12 variable {ι R F : Type*} [Fintype ι] [DecidableEq ι]
13   [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
14   [Field F] [Algebra R F] [IsFractionRing R F]
15 
16 omit [IsPrincipalIdealRing R] in
17 theorem exists_integral_multiple (g : GL ι F) :
18     ∃ b : R, ∃ A : Matrix ι ι R,
19       b ≠ 0 ∧ A.det ≠ 0 ∧ A.map (algebraMap R F) = (algebraMap R F b) • g.val := by
20   obtain ⟨b, hb⟩ := IsLocalization.exist_integer_multiples_of_finite
21     (R⁰) (fun ij : ι × ι => g ij.1 ij.2)
22   choose A hA using hb
23   have hb0 : (b : R) ≠ 0 := nonZeroDivisors.ne_zero b.property
24   have hbF : algebraMap R F (b : R) ≠ 0 := fun h => hb0 ((IsFractionRing.injective R F) (h.trans (map_zero _).symm))
25   let M : Matrix ι ι R := fun i j => A (i, j)
26   have hm : M.map (algebraMap R F) = (algebraMap R F (b : R)) • g.val := by
27     ext i j
28     change algebraMap R F (A (i, j)) = algebraMap R F (b : R) * g i j
29     simpa only [Algebra.smul_def] using hA (i, j)
30   have hdet : M.det ≠ 0 := by
31     intro h
32     have he := congrArg Matrix.det hm
33     change (RingHom.mapMatrix (algebraMap R F) M).det = _ at he
34     rw [← RingHom.map_det, h, map_zero, Matrix.det_smul] at he
35     exact (mul_ne_zero (pow_ne_zero _ hbF) g.det_ne_zero) he.symm
36   exact ⟨b, M, hb0, hdet, hm⟩
37 
38 theorem exists_integral_diagonal (g : GL ι F) :
39     ∃ c : Fˣ, ∃ P Q : GL ι R, ∃ d : ι → R, ∃ hd : ∀ i, algebraMap R F (d i) ≠ 0,
40       g = GeneralLinearGroup.scalar ι c *
41         (GeneralLinearGroup.map (algebraMap R F) P *
42           SplitRadical105.diagonalGL (fun i => algebraMap R F (d i)) hd *
43           GeneralLinearGroup.map (algebraMap R F) Q) := by
44   obtain ⟨b, A, hb, hA, he⟩ := exists_integral_multiple (R := R) g
45   obtain ⟨P, Q, d, hd, hdiag⟩ := SmithMatrix106.exists_diagonal A hA
46   have hbF : algebraMap R F b ≠ 0 := fun h => hb ((IsFractionRing.injective R F) (h.trans (map_zero _).symm))
47   let c : Fˣ := (Units.mk0 (algebraMap R F b) hbF)⁻¹
48   refine ⟨c, P, Q, d, fun i h => hd i ((IsFractionRing.injective R F) (h.trans (map_zero _).symm)), ?_⟩
49   apply Units.ext
50   change g.val = Matrix.scalar ι (algebraMap R F b)⁻¹ *
51     (P.val.map (algebraMap R F) * diagonal (fun i => algebraMap R F (d i)) *
52       Q.val.map (algebraMap R F))
53   have hdmap := congrArg (fun M : Matrix ι ι R => M.map (algebraMap R F)) hdiag
54   rw [Matrix.map_mul, Matrix.map_mul, Matrix.diagonal_map (map_zero _)] at hdmap
55   rw [← hdmap, he, Matrix.scalar_apply, ← Matrix.smul_eq_diagonal_mul, smul_smul, inv_mul_cancel₀ hbF, one_smul]
56 
57 end PaperXI.FractionMatrix106

Back to source controls