MoritaLattice110.lean

1 import Mathlib.Data.Matrix.Basis
2 import Mathlib.Algebra.Ring.AddAut
3 import Mathlib.GroupTheory.QuotientGroup.Basic
4 
5 /-! The common-corner and diagonal-transport part of the maximal-order
6 Morita calculation. The coefficient ring acts through an arbitrary ring
7 homomorphism into a possibly noncommutative endomorphism ring. In particular,
8 no false centrality assumption on O_E inside End_F(E) is imposed. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.MoritaLattice110
12 
13 open Matrix
14 
15 variable {R D m : Type*} [Ring R] [Ring D] [Fintype m] [DecidableEq m]
16 
17 /-- Stability under the actual mapped coefficient matrices on both sides. -/
18 def IsMatrixBimodule (φ : R →+* D) (L : AddSubgroup (Matrix m m D)) : Prop :=
19   (∀ b : Matrix m m R, ∀ x ∈ L, b.map φ * x ∈ L) ∧
20   (∀ b : Matrix m m R, ∀ x ∈ L, x * b.map φ ∈ L)
21 
22 /-- The literal insertion into a chosen diagonal corner. -/
23 def cornerEmbedding (p : m) : D →+ Matrix m m D where
24   toFun x := single p p x
25   map_zero' := single_zero p p
26   map_add' := single_add p p
27 
28 /-- The actual corner subgroup, not an independently supplied module. -/
29 def corner (L : AddSubgroup (Matrix m m D)) (p : m) : AddSubgroup D :=
30   L.comap (cornerEmbedding p)
31 
32 omit [Fintype m] in
33 @[simp] theorem mem_corner (L : AddSubgroup (Matrix m m D)) (p : m) (x : D) :
34     x ∈ corner L p ↔ single p p x ∈ L := Iff.rfl
35 
36 /-- Multiplying by matrix units extracts an entry into the chosen corner. -/
37 theorem entry_mem_corner (φ : R →+* D) (L : AddSubgroup (Matrix m m D))
38     (hL : IsMatrixBimodule φ L) (p : m) {x : Matrix m m D} (hx : x ∈ L)
39     (i j : m) : x i j ∈ corner L p := by
40   have hleft := hL.1 (single p i 1) x hx
41   have hright := hL.2 (single j p 1) _ hleft
42   simpa [mem_corner, single_mul_mul_single] using hright
43 
44 /-- An allowed corner entry can be inserted at every matrix position. -/
45 theorem single_mem_of_corner (φ : R →+* D) (L : AddSubgroup (Matrix m m D))
46     (hL : IsMatrixBimodule φ L) (p i j : m) {x : D}
47     (hx : x ∈ corner L p) : single i j x ∈ L := by
48   have hleft := hL.1 (single i p 1) (single p p x) hx
49   have hright := hL.2 (single p j 1) _ hleft
50   simpa [single_mul_mul_single] using hright
51 
52 /-- Matrix-unit Morita reduction, as equality of the actual additive subgroups. -/
53 theorem eq_matrix_corner (φ : R →+* D) (L : AddSubgroup (Matrix m m D))
54     (hL : IsMatrixBimodule φ L) (p : m) : L = (corner L p).matrix := by
55   ext x
56   constructor
57   · intro hx i j
58     exact entry_mem_corner φ L hL p hx i j
59   · intro hx
60     rw [matrix_eq_sum_single x]
61     apply L.sum_mem
62     intro i _
63     apply L.sum_mem
64     intro j _
65     exact single_mem_of_corner φ L hL p i j (hx i j)
66 
67 /-- The corner inherits genuine left and right coefficient-ring stability. -/
68 theorem corner_bimodule (φ : R →+* D) (L : AddSubgroup (Matrix m m D))
69     (hL : IsMatrixBimodule φ L) (p : m) (a : R) {x : D}
70     (hx : x ∈ corner L p) :
71     φ a * x ∈ corner L p ∧ x * φ a ∈ corner L p := by
72   constructor
73   · have h := hL.1 (single p p a) (single p p x) hx
74     simpa [mem_corner] using h
75   · have h := hL.2 (single p p a) (single p p x) hx
76     simpa [mem_corner] using h
77 
78 section ScalarTransport
79 variable {D : Type*} [Ring D]
80 
81 /-- Conjugation by a genuine unit of the noncommutative coefficient ring. -/
82 def unitConjugation (u : Dˣ) : D ≃+ D where
83   toFun x := (u : D) * x * ((u⁻¹ : Dˣ) : D)
84   invFun x := ((u⁻¹ : Dˣ) : D) * x * (u : D)
85   left_inv x := by simp [mul_assoc]
86   right_inv x := by simp [mul_assoc]
87   map_add' x y := by simp [mul_add, add_mul]
88 
89 @[simp] theorem unitConjugation_apply (u : Dˣ) (x : D) :
90     unitConjugation u x = (u : D) * x * ((u⁻¹ : Dˣ) : D) := rfl
91 
92 /-- The units that normalize the literal additive subgroup. -/
93 def normalizingUnits (Λ : AddSubgroup D) : Subgroup Dˣ where
94   carrier := {u | ∀ x : D, unitConjugation u x ∈ Λ ↔ x ∈ Λ}
95   one_mem' := by intro x; simp [unitConjugation]
96   mul_mem' {u v} hu hv := by
97     intro x
98     have he : unitConjugation u (unitConjugation v x) =
99         unitConjugation (u * v) x := by simp [unitConjugation, mul_assoc]
100     rw [← he, hu, hv]
101   inv_mem' {u} hu := by
102     intro x
103     have h := hu (unitConjugation u⁻¹ x)
104     simpa [unitConjugation, mul_assoc] using h.symm
105 
106 @[simp] theorem mem_normalizingUnits (Λ : AddSubgroup D) (u : Dˣ) :
107     u ∈ normalizingUnits Λ ↔ ∀ x, unitConjugation u x ∈ Λ ↔ x ∈ Λ := Iff.rfl
108 
109 /-- Radical commutation implies normalization; no centrality is assumed. -/
110 theorem normalizes_of_left_right_map_eq (Λ : AddSubgroup D) (u : Dˣ)
111     (hcomm : Λ.map (AddMonoidHom.mulLeft (u : D)) =
112       Λ.map (AddMonoidHom.mulRight (u : D))) :
113     u ∈ normalizingUnits Λ := by
114   intro x
115   constructor
116   · intro hx
117     have hmem : (u : D) * x ∈ Λ.map (AddMonoidHom.mulRight (u : D)) := by
118       refine ⟨unitConjugation u x, hx, ?_⟩
119       simp [unitConjugation, mul_assoc]
120     rw [← hcomm] at hmem
121     obtain ⟨z, hz, he⟩ := hmem
122     have hzx : z = x := by
123       have h := congrArg (fun t : D => ((u⁻¹ : Dˣ) : D) * t) he
124       simpa [mul_assoc] using h
125     exact hzx ▸ hz
126   · intro hx
127     have hmem : (u : D) * x ∈ Λ.map (AddMonoidHom.mulLeft (u : D)) :=
128       ⟨x, hx, rfl⟩
129     rw [hcomm] at hmem
130     obtain ⟨z, hz, he⟩ := hmem
131     have hzx : z = unitConjugation u x := by
132       have h := congrArg (fun t : D => t * ((u⁻¹ : Dˣ) : D)) he
133       simpa [unitConjugation, mul_assoc] using h
134     exact hzx ▸ hz
135 
136 /-- All positive and negative powers normalize, derived from one commutation. -/
137 theorem zpow_normalizes (Λ : AddSubgroup D) (u : Dˣ)
138     (hu : u ∈ normalizingUnits Λ) (a : ℤ) :
139     u ^ a ∈ normalizingUnits Λ := (normalizingUnits Λ).zpow_mem hu a
140 
141 /-- The right scalar can be transferred to the left in a membership test. -/
142 theorem two_sided_mem_iff_left (Λ : AddSubgroup D) (u : Dˣ)
143     (hu : u ∈ normalizingUnits Λ) (a b : ℤ) (x : D) :
144     ((u ^ a : Dˣ) : D) * x * ((u ^ b : Dˣ) : D) ∈ Λ ↔
145       ((u ^ (a + b) : Dˣ) : D) * x ∈ Λ := by
146   have h := zpow_normalizes Λ u hu b
147   have he : unitConjugation (u ^ b)
148       (((u ^ a : Dˣ) : D) * x * ((u ^ b : Dˣ) : D)) =
149       ((u ^ (a + b) : Dˣ) : D) * x := by
150     simp only [unitConjugation_apply]
151     calc
152       _ = (((u ^ b : Dˣ) : D) * ((u ^ a : Dˣ) : D)) * x *
153           (((u ^ b : Dˣ) : D) * (((u ^ b)⁻¹ : Dˣ) : D)) := by simp [mul_assoc]
154       _ = ((u ^ (a + b) : Dˣ) : D) * x := by
155         rw [Units.mul_inv, mul_one, ← Units.val_mul, ← zpow_add, add_comm b a]
156   exact (h _).symm.trans (by rw [he])
157 
158 /-- The actual left power translate of the corner subgroup. -/
159 def leftPower (Λ : AddSubgroup D) (u : Dˣ) (a : ℤ) : AddSubgroup D :=
160   Λ.map (AddMonoidHom.mulLeft ((u ^ a : Dˣ) : D))
161 
162 theorem mem_leftPower (Λ : AddSubgroup D) (u : Dˣ) (a : ℤ) (x : D) :
163     x ∈ leftPower Λ u a ↔ ((u ^ (-a) : Dˣ) : D) * x ∈ Λ := by
164   constructor
165   · rintro ⟨z, hz, rfl⟩
166     simpa [leftPower, ← mul_assoc, ← Units.val_mul, ← zpow_add] using hz
167   · intro hx
168     refine ⟨((u ^ (-a) : Dˣ) : D) * x, hx, ?_⟩
169     simp [← mul_assoc, ← Units.val_mul]
170 
171 end ScalarTransport
172 
173 section DiagonalTransport
174 variable {D m : Type*} [Ring D] [Fintype m] [DecidableEq m]
175 
176 /-- A diagonal matrix unit, including its explicit inverse. -/
177 def diagonalUnit (d : m → Dˣ) : (Matrix m m D)ˣ where
178   val := diagonal (fun i => (d i : D))
179   inv := diagonal (fun i => (((d i)⁻¹ : Dˣ) : D))
180   val_inv := by
181     rw [diagonal_mul_diagonal]
182     ext i j
183     by_cases h : i = j
184     · subst j; simp [diagonal]
185     · simp [diagonal, h]
186   inv_val := by
187     rw [diagonal_mul_diagonal]
188     ext i j
189     by_cases h : i = j
190     · subst j; simp [diagonal]
191     · simp [diagonal, h]
192 
193 /-- Conjugation really acts separately on the actual matrix entries. -/
194 theorem diagonal_conjugation_apply (d : m → Dˣ) (x : Matrix m m D) (i j : m) :
195     unitConjugation (diagonalUnit d) x i j =
196       (d i : D) * x i j * (((d j)⁻¹ : Dˣ) : D) := by
197   simp [unitConjugation, diagonalUnit, diagonal_mul, mul_diagonal]
198 
199 /-- A scalar diagonal preserves the chosen corner insertion. -/
200 theorem scalar_conjugation_single (u : Dˣ) (p : m) (x : D) :
201     unitConjugation (diagonalUnit (fun _ : m => u)) (single p p x) =
202       single p p (unitConjugation u x) := by
203   ext i j
204   rw [diagonal_conjugation_apply]
205   by_cases h : p = i ∧ p = j <;> simp [single, h, unitConjugation]
206 
207 /-- Radical commutation on the actual matrix subgroup descends to its corner. -/
208 theorem corner_normalizes_of_scalar_commutation
209     (L : AddSubgroup (Matrix m m D)) (u : Dˣ) (p : m)
210     (hcomm : L.map (AddMonoidHom.mulLeft
211         (diagonalUnit (fun _ : m => u) : Matrix m m D)) =
212       L.map (AddMonoidHom.mulRight
213         (diagonalUnit (fun _ : m => u) : Matrix m m D))) :
214     u ∈ normalizingUnits (corner L p) := by
215   have hnorm := normalizes_of_left_right_map_eq L
216     (diagonalUnit (fun _ : m => u)) hcomm
217   intro x
218   simpa only [mem_corner, scalar_conjugation_single] using hnorm (single p p x)
219 
220 /-- Membership in the actual conjugate image is tested by inverse conjugation. -/
221 theorem mem_conjugate (L : AddSubgroup D) (u : Dˣ) (x : D) :
222     x ∈ L.map (unitConjugation u).toAddMonoidHom ↔
223       unitConjugation u⁻¹ x ∈ L := by
224   constructor
225   · rintro ⟨z, hz, rfl⟩
226     simpa [unitConjugation, mul_assoc] using hz
227   · intro hx
228     refine ⟨unitConjugation u⁻¹ x, hx, ?_⟩
229     simp [unitConjugation, mul_assoc]
230 
231 /-- A family of actual allowed-entry additive subgroups. -/
232 def entrywise (S : m → m → AddSubgroup D) : AddSubgroup (Matrix m m D) where
233   carrier := {x | ∀ i j, x i j ∈ S i j}
234   zero_mem' i j := (S i j).zero_mem
235   add_mem' hx hy i j := (S i j).add_mem (hx i j) (hy i j)
236   neg_mem' hx i j := (S i j).neg_mem (hx i j)
237 
238 omit [Fintype m] [DecidableEq m] in
239 @[simp] theorem mem_entrywise (S : m → m → AddSubgroup D) (x : Matrix m m D) :
240     x ∈ entrywise S ↔ ∀ i j, x i j ∈ S i j := Iff.rfl
241 
242 /-- Diagonal conjugation of the genuine Morita lattice is the family of left
243 power translates, with the correct signed Cartan differences. -/
244 theorem conjugate_eq_entrywise_leftPower
245     (φ : R →+* D) (L : AddSubgroup (Matrix m m D))
246     (hL : IsMatrixBimodule φ L) (p : m) (u : Dˣ)
247     (hu : u ∈ normalizingUnits (corner L p)) (a : m → ℤ) :
248     L.map (unitConjugation (diagonalUnit (fun i => u ^ a i))).toAddMonoidHom =
249       entrywise (fun i j => leftPower (corner L p) u (a i - a j)) := by
250   ext x
251   rw [mem_conjugate]
252   conv_lhs => rw [eq_matrix_corner φ L hL p]
253   change (∀ i j, unitConjugation (diagonalUnit (fun i => u ^ a i))⁻¹ x i j ∈
254       corner L p) ↔ ∀ i j, x i j ∈ leftPower (corner L p) u (a i - a j)
255   have hdiag : (diagonalUnit (fun i => u ^ a i))⁻¹ =
256       diagonalUnit (fun i => (u ^ a i)⁻¹) := by
257     apply Units.ext
258     rfl
259   simp only [hdiag, diagonal_conjugation_apply, inv_inv]
260   constructor <;> intro hx i j
261   · rw [mem_leftPower]
262     have h := (two_sided_mem_iff_left (corner L p) u hu (-a i) (a j) (x i j)).mp
263       (by simpa only [zpow_neg] using hx i j)
264     have he : -(a i - a j) = -a i + a j := by omega
265     rw [he]
266     exact h
267   · have h := (mem_leftPower (corner L p) u (a i - a j) (x i j)).mp (hx i j)
268     have h' : ((u ^ (-a i + a j) : Dˣ) : D) * x i j ∈ corner L p := by
269       have he : -(a i - a j) = -a i + a j := by omega
270       rw [he] at h
271       exact h
272     simpa only [zpow_neg] using
273       (two_sided_mem_iff_left (corner L p) u hu (-a i) (a j) (x i j)).mpr h'
274 
275 /-- The actual conjugate intersection is the entrywise corner intersection. -/
276 theorem intersection_eq_entrywise
277     (φ : R →+* D) (L : AddSubgroup (Matrix m m D))
278     (hL : IsMatrixBimodule φ L) (p : m) (u : Dˣ)
279     (hu : u ∈ normalizingUnits (corner L p)) (a : m → ℤ) :
280     L ⊓ L.map (unitConjugation (diagonalUnit (fun i => u ^ a i))).toAddMonoidHom =
281       entrywise (fun i j => corner L p ⊓ leftPower (corner L p) u (a i - a j)) := by
282   rw [conjugate_eq_entrywise_leftPower φ L hL p u hu a]
283   nth_rw 1 [eq_matrix_corner φ L hL p]
284   ext x
285   change ((∀ i j, x i j ∈ corner L p) ∧
286     (∀ i j, x i j ∈ leftPower (corner L p) u (a i - a j))) ↔
287       ∀ i j, x i j ∈ corner L p ∧ x i j ∈ leftPower (corner L p) u (a i - a j)
288   exact ⟨fun h i j => ⟨h.1 i j, h.2 i j⟩,
289     fun h => ⟨fun i j => (h i j).1, fun i j => (h i j).2⟩⟩
290 
291 end DiagonalTransport
292 
293 section PowerIntersection
294 variable {D : Type*} [Ring D]
295 
296 /-- Integral scalar stability is iterated, rather than supplied for each power. -/
297 theorem pow_mul_mem (Λ : AddSubgroup D) (u : Dˣ)
298     (hstable : ∀ x ∈ Λ, (u : D) * x ∈ Λ) (n : ℕ) {x : D} (hx : x ∈ Λ) :
299     ((u ^ n : Dˣ) : D) * x ∈ Λ := by
300   induction n with
301   | zero => simpa using hx
302   | succ n ih => simpa [pow_succ', mul_assoc] using hstable _ ih
303 
304 theorem leftPower_zero (Λ : AddSubgroup D) (u : Dˣ) : leftPower Λ u 0 = Λ := by
305   ext x
306   rw [mem_leftPower]
307   simp
308 
309 /-- The actual nested intersection is the nonnegative scalar-power translate. -/
310 theorem inf_leftPower_eq_toNat (Λ : AddSubgroup D) (u : Dˣ)
311     (hstable : ∀ x ∈ Λ, (u : D) * x ∈ Λ) (a : ℤ) :
312     Λ ⊓ leftPower Λ u a = leftPower Λ u (a.toNat : ℤ) := by
313   cases a with
314   | ofNat n =>
315     have hle : leftPower Λ u (n : ℤ) ≤ Λ := by
316       rintro x ⟨z, hz, rfl⟩
317       change ((u ^ (n : ℤ) : Dˣ) : D) * z ∈ Λ
318       simpa only [zpow_natCast] using pow_mul_mem Λ u hstable n hz
319     simpa using inf_eq_right.mpr hle
320   | negSucc n =>
321     have hle : Λ ≤ leftPower Λ u (Int.negSucc n) := by
322       intro x hx
323       rw [mem_leftPower]
324       simpa only [Int.neg_negSucc, zpow_natCast] using pow_mul_mem Λ u hstable (n + 1) hx
325     simpa only [Int.toNat_negSucc, Nat.cast_zero, leftPower_zero] using inf_eq_left.mpr hle
326 
327 end PowerIntersection
328 
329 /-- Left integral scalar stability for the actual corner follows from the
330 coefficient bimodule; the uniformizer unit is tied to its coefficient value. -/
331 theorem corner_scalar_stable (φ : R →+* D) (L : AddSubgroup (Matrix m m D))
332     (hL : IsMatrixBimodule φ L) (p : m) (π : R) (u : Dˣ)
333     (hπ : (u : D) = φ π) : ∀ x ∈ corner L p, (u : D) * x ∈ corner L p := by
334   intro x hx
335   rw [hπ]
336   exact (corner_bimodule φ L hL p π hx).1
337 
338 /-- The final entrywise intersection reduction, with each negative Cartan
339 difference contributing zero. Its remaining numerical leaf is a genuine DVR
340 quotient of the actual corner module. -/
341 theorem intersection_eq_nonnegative_entrywise
342     (φ : R →+* D) (L : AddSubgroup (Matrix m m D))
343     (hL : IsMatrixBimodule φ L) (p : m) (π : R) (u : Dˣ)
344     (hπ : (u : D) = φ π)
345     (hu : u ∈ normalizingUnits (corner L p)) (a : m → ℤ) :
346     L ⊓ L.map (unitConjugation (diagonalUnit (fun i => u ^ a i))).toAddMonoidHom =
347       entrywise (fun i j => leftPower (corner L p) u ((a i - a j).toNat : ℤ)) := by
348   rw [intersection_eq_entrywise φ L hL p u hu a]
349   congr 1
350   funext i j
351   exact inf_leftPower_eq_toNat (corner L p) u
352     (corner_scalar_stable φ L hL p π u hπ) (a i - a j)
353 
354 end PaperXI.MoritaLattice110

Back to source controls