PrimitiveMatrix.lean

1 import Mathlib.RingTheory.DiscreteValuationRing.Basic
2 import Mathlib.RingTheory.Localization.Integer
3 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
4 import Mathlib.Data.Fintype.Lattice
5 
6 /-! Primitive normalization over a discrete valuation ring.  A nonzero finite
7 family over the fraction field can be rescaled so that all entries are integral
8 and one entry is exactly one.  Neither a lattice normalization nor an integral
9 comparison is supplied as a premise. -/
10 set_option autoImplicit false
11 
12 namespace PaperX.PrimitiveMatrix
13 
14 variable {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
15 variable {K : Type*} [Field K] [Algebra R K] [IsFractionRing R K]
16 
17 /-- Divide a nonzero integral finite family by an entry of least valuation. -/
18 theorem integral_family_normalization {ι : Type*} [Finite ι]
19     (a : ι → R) (ha : ∃ i, a i ≠ 0) :
20     ∃ (b : R) (p : ι → R), b ≠ 0 ∧ (∀ i, a i = b * p i) ∧ ∃ i, p i = 1 := by
21   classical
22   obtain ⟨j, hj⟩ := ha
23   let : Nonempty ι := ⟨j⟩
24   obtain ⟨i, hi⟩ := Finite.exists_min (fun i => IsDiscreteValuationRing.addVal R (a i))
25   have hd : ∀ k, a i ∣ a k := fun k =>
26     IsDiscreteValuationRing.addVal_le_iff_dvd.mp (hi k)
27   have hn : a i ≠ 0 := by
28     intro h
29     have := hd j
30     rw [h, zero_dvd_iff] at this
31     exact hj this
32   choose p hp using hd
33   refine ⟨a i, p, hn, hp, i, ?_⟩
34   apply mul_left_cancel₀ hn
35   simpa using (hp i).symm
36 
37 /-- Actual fraction-field normalization, with an entry equal to one. -/
38 theorem fraction_family_normalization {ι : Type*} [Finite ι]
39     (q : ι → K) (hq : ∃ i, q i ≠ 0) :
40     ∃ (s : K) (p : ι → R), s ≠ 0 ∧
41       (∀ i, algebraMap R K (p i) = s * q i) ∧ ∃ i, p i = 1 := by
42   classical
43   obtain ⟨b, hb⟩ := IsLocalization.exist_integer_multiples_of_finite
44     (nonZeroDivisors R) q
45   choose a ha using hb
46   have hb0 : (b : R) ≠ 0 := nonZeroDivisors.ne_zero b.property
47   have hbK : algebraMap R K (b : R) ≠ 0 := by
48     exact fun h => hb0 ((IsFractionRing.injective R K) (h.trans (map_zero _).symm))
49   have han : ∃ i, a i ≠ 0 := by
50     obtain ⟨i, hi⟩ := hq
51     refine ⟨i, ?_⟩
52     intro h
53     have he := ha i
54     rw [h, map_zero, Algebra.smul_def] at he
55     exact (mul_ne_zero hbK hi) he.symm
56   obtain ⟨d, p, hd, hp, hpi⟩ := integral_family_normalization a han
57   have hdK : algebraMap R K d ≠ 0 :=
58     fun h => hd ((IsFractionRing.injective R K) (h.trans (map_zero _).symm))
59   refine ⟨algebraMap R K (b : R) / algebraMap R K d, p,
60     div_ne_zero hbK hdK, ?_, hpi⟩
61   intro i
62   apply (mul_left_cancel₀ hdK)
63   have he := ha i
64   rw [hp i, map_mul, Algebra.smul_def] at he
65   rw [he]
66   field_simp
67 
68 variable {n : Type*} [Fintype n]
69 
70 /-- A nonzero matrix is a scalar multiple of a primitive integral matrix. -/
71 theorem matrix_normalization (Q : Matrix n n K) (hQ : Q ≠ 0) :
72     ∃ (s : K) (P : Matrix n n R), s ≠ 0 ∧
73       P.map (algebraMap R K) = s • Q ∧ ∃ i j, P i j = 1 := by
74   classical
75   have hn : ∃ ij : n × n, Q ij.1 ij.2 ≠ 0 := by
76     by_contra h
77     push Not at h
78     apply hQ
79     ext i j
80     exact h (i, j)
81   obtain ⟨s, p, hs, hp, ij, hij⟩ := fraction_family_normalization (R := R)
82     (fun ij : n × n => Q ij.1 ij.2) hn
83   refine ⟨s, fun i j => p (i, j), hs, ?_, ij.1, ij.2, hij⟩
84   ext i j
85   exact hp (i, j)
86 
87 /-- Primitive normalization preserves every integral intertwining equation.
88 The indexing type may be an arbitrary group; the proof uses only its supplied
89 matrices and hence also applies to several actions at once. -/
90 theorem intertwiner_normalization {G : Type*}
91     (ρ τ : G → Matrix n n R) (Q : Matrix n n K) (hQ : Q ≠ 0)
92     (hinter : ∀ g, (ρ g).map (algebraMap R K) * Q =
93       Q * (τ g).map (algebraMap R K)) :
94     ∃ (s : K) (P : Matrix n n R), s ≠ 0 ∧
95       P.map (algebraMap R K) = s • Q ∧
96       (∃ i j, P i j = 1) ∧ ∀ g, ρ g * P = P * τ g := by
97   obtain ⟨s, P, hs, hP, hprim⟩ := matrix_normalization (R := R) Q hQ
98   refine ⟨s, P, hs, hP, hprim, ?_⟩
99   intro g
100   have hm : (ρ g * P).map (algebraMap R K) =
101       (P * τ g).map (algebraMap R K) := by
102     simp only [Matrix.map_mul, hP, Matrix.mul_smul, Matrix.smul_mul, hinter g]
103   ext i j
104   exact IsFractionRing.injective R K (congrFun (congrFun hm i) j)
105 
106 /-- A nonsingular comparison in positive rank admits a nonsingular primitive
107 integral comparison, preserving the actual actions. -/
108 theorem nonsingular_intertwiner_normalization [Nonempty n] [DecidableEq n]
109     {G : Type*} (ρ τ : G → Matrix n n R) (Q : Matrix n n K)
110     (hQ : Q.det ≠ 0)
111     (hinter : ∀ g, (ρ g).map (algebraMap R K) * Q =
112       Q * (τ g).map (algebraMap R K)) :
113     ∃ P : Matrix n n R, P.det ≠ 0 ∧ (∃ i j, P i j = 1) ∧
114       ∀ g, ρ g * P = P * τ g := by
115   have hn : Q ≠ 0 := by
116     intro h
117     apply hQ
118     simp [h]
119   obtain ⟨s, P, hs, hP, hprim, hcomm⟩ := intertwiner_normalization ρ τ Q hn hinter
120   refine ⟨P, ?_, hprim, hcomm⟩
121   have hdet : (P.map (algebraMap R K)).det ≠ 0 := by
122     rw [hP, Matrix.det_smul]
123     exact mul_ne_zero (pow_ne_zero _ hs) hQ
124   intro h
125   apply hdet
126   change ((algebraMap R K).mapMatrix P).det = 0
127   rw [← RingHom.map_det, h, map_zero]
128 
129 end PaperX.PrimitiveMatrix

Back to source controls