MoritaRadicalDictionary110.lean

1 import PaperXI.MoritaActualCartan110
2 import Mathlib.Data.Matrix.Basic
3 
4 /-! The literal additive product with the actual mapped maximal-order radical.
5 Only mapped coefficient matrices commute with its scalar; no centrality in the
6 whole endomorphism ring is asserted. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.MoritaRadicalDictionary110
10 open Matrix PaperXI.MoritaLattice110 PaperXI.MoritaCornerRank110
11 open PaperXI.MoritaActualCartan110
12 
13 section Product
14 variable {A : Type*} [Ring A]
15 
16 /-- The additive subgroup generated by literal products of its two factors. -/
17 def additiveProduct (P L : AddSubgroup A) : AddSubgroup A :=
18   AddSubgroup.closure {z | ∃ q ∈ P, ∃ x ∈ L, q * x = z}
19 
20 theorem mul_mem_additiveProduct (P L : AddSubgroup A) {q x : A}
21     (hq : q ∈ P) (hx : x ∈ L) : q * x ∈ additiveProduct P L :=
22   AddSubgroup.subset_closure ⟨q, hq, x, hx, rfl⟩
23 
24 end Product
25 
26 section MappedMaximalOrder
27 variable {R D m : Type*} [CommRing R] [Ring D] [Fintype m] [DecidableEq m]
28 
29 /-- The literal image of `π M_m(R)` in the ambient coefficient matrix ring. -/
30 def maximalOrderRadical (φ : R →+* D) (π : R) : AddSubgroup (Matrix m m D) :=
31   (⊤ : AddSubgroup (Matrix m m R)).map
32     ((AddMonoidHom.mulLeft (Matrix.scalar m (φ π))).comp φ.mapMatrix.toAddMonoidHom)
33 
34 theorem scalar_mem_maximalOrderRadical (φ : R →+* D) (π : R) :
35     Matrix.scalar m (φ π) ∈ maximalOrderRadical φ π := by
36   refine ⟨1, AddSubgroup.mem_top _, ?_⟩
37   change Matrix.scalar m (φ π) * (1 : Matrix m m R).map φ = _
38   simp
39 
40 /-- The radical scalar commutes with actual mapped integral matrices, even
41 though it need not commute with arbitrary ambient coefficient matrices. -/
42 theorem scalar_commutes_mapped (φ : R →+* D) (π : R) (b : Matrix m m R) :
43     Matrix.scalar m (φ π) * b.map φ = b.map φ * Matrix.scalar m (φ π) := by
44   apply Matrix.scalar_comm_iff.mpr
45   ext i j
46   exact (Commute.all π (b i j)).map φ
47 
48 /-- The actual left radical product is the scalar-uniformizer image. -/
49 theorem radical_product_eq_left_image (φ : R →+* D) (π : R)
50     (L : AddSubgroup (Matrix m m D)) (hL : IsMatrixBimodule φ L) :
51     additiveProduct (maximalOrderRadical φ π) L =
52       L.map (AddMonoidHom.mulLeft (Matrix.scalar m (φ π))) := by
53   apply le_antisymm
54   · apply (AddSubgroup.closure_le _).mpr
55     rintro z ⟨q, hq, x, hx, rfl⟩
56     obtain ⟨b, _, hb⟩ := hq
57     change Matrix.scalar m (φ π) * b.map φ = q at hb
58     subst q
59     refine ⟨b.map φ * x, hL.1 b x hx, ?_⟩
60     change Matrix.scalar m (φ π) * (b.map φ * x) = _
61     exact (mul_assoc _ _ _).symm
62   · rintro z ⟨x, hx, rfl⟩
63     change Matrix.scalar m (φ π) * x ∈ additiveProduct (maximalOrderRadical φ π) L
64     exact mul_mem_additiveProduct (q := Matrix.scalar m (φ π)) (x := x)
65       (maximalOrderRadical φ π) L
66       (scalar_mem_maximalOrderRadical (m := m) φ π) hx
67 
68 /-- The actual right radical product is the right scalar-uniformizer image. -/
69 theorem product_radical_eq_right_image (φ : R →+* D) (π : R)
70     (L : AddSubgroup (Matrix m m D)) (hL : IsMatrixBimodule φ L) :
71     additiveProduct L (maximalOrderRadical φ π) =
72       L.map (AddMonoidHom.mulRight (Matrix.scalar m (φ π))) := by
73   apply le_antisymm
74   · apply (AddSubgroup.closure_le _).mpr
75     rintro z ⟨x, hx, q, hq, rfl⟩
76     obtain ⟨b, _, hb⟩ := hq
77     change Matrix.scalar m (φ π) * b.map φ = q at hb
78     subst q
79     refine ⟨x * b.map φ, hL.2 b x hx, ?_⟩
80     change (x * b.map φ) * Matrix.scalar m (φ π) = _
81     rw [mul_assoc, ← scalar_commutes_mapped φ π b]
82   · rintro z ⟨x, hx, rfl⟩
83     change x * Matrix.scalar m (φ π) ∈ additiveProduct L (maximalOrderRadical φ π)
84     exact mul_mem_additiveProduct (q := x) (x := Matrix.scalar m (φ π))
85       L (maximalOrderRadical φ π) hx
86       (scalar_mem_maximalOrderRadical (m := m) φ π)
87 
88 /-- Literal source-style radical-product commutation implies scalar-image
89 commutation; the desired scalar equality is a conclusion, not a premise. -/
90 theorem scalar_images_eq_of_radical_products_eq (φ : R →+* D) (π : R)
91     (L : AddSubgroup (Matrix m m D)) (hL : IsMatrixBimodule φ L)
92     (hcomm : additiveProduct (maximalOrderRadical φ π) L =
93       additiveProduct L (maximalOrderRadical φ π)) :
94     L.map (AddMonoidHom.mulLeft (Matrix.scalar m (φ π))) =
95       L.map (AddMonoidHom.mulRight (Matrix.scalar m (φ π))) := by
96   rw [← radical_product_eq_left_image φ π L hL,
97     ← product_radical_eq_right_image φ π L hL]
98   exact hcomm
99 
100 end MappedMaximalOrder
101 
102 section ActualEndomorphismRing
103 open Module ValuativeRel
104 variable (F E : Type*) [Field F] [Field E] [Algebra F E]
105   [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E]
106 variable (m : Type*) [Fintype m] [DecidableEq m]
107 
108 /-- The actual maximal centralizer-order radical in `M_m(End_F(E))`. -/
109 def actualRadical : AddSubgroup (Matrix m m (Module.End F E)) :=
110   maximalOrderRadical (coefficientMap F E) (PaperXI.ActualLocalUnitDecomposition.uniformizer E)
111 
112 /-- The literal actual-radical product equality supplies the named input of the
113 checked Cartan arithmetic theorem. Canonical order/basis identification remains
114 a separate source attachment. -/
115 theorem RadicalCommutes_of_actual_radical_products
116     (L : AddSubgroup (Matrix m m (Module.End F E)))
117     (hL : IsMatrixBimodule (coefficientMap F E) L)
118     (hcomm : additiveProduct (actualRadical F E m) L =
119       additiveProduct L (actualRadical F E m)) : RadicalCommutes F E m L := by
120   have h := scalar_images_eq_of_radical_products_eq (coefficientMap F E)
121     (PaperXI.ActualLocalUnitDecomposition.uniformizer E) L hL hcomm
122   have he : Matrix.scalar m ((coefficientMap F E)
123       (PaperXI.ActualLocalUnitDecomposition.uniformizer E)) =
124       ((diagonalUnit (fun _ : m => uniformizerEndUnit F E) :
125         (Matrix m m (Module.End F E))ˣ) : Matrix m m (Module.End F E)) := by
126     rfl
127   unfold RadicalCommutes
128   rw [← he]
129   exact h
130 
131 end ActualEndomorphismRing
132 end PaperXI.MoritaRadicalDictionary110

Back to source controls