MoritaActualCartan110.lean

1 import PaperXI.MoritaIndex110
2 import PaperXI.ActualLocalCartan106
3 import PaperXI.MoritaCartanTransport110
4 import PaperXI.MoritaScalarUpgrade110
5 
6 /-! Actual centralizer matrices act in the noncommutative endomorphism ring
7 through explicit ring homomorphisms. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.MoritaActualCartan110
11 open Matrix Module ValuativeRel
12 open PaperXI.MoritaLattice110 PaperXI.MoritaCornerRank110 PaperXI.MoritaIndex110
13 open PaperXI.MoritaCartanTransport110
14 variable (F E : Type*) [Field F] [Field E] [Algebra F E]
15   [Module.Finite F E] [ValuativeRel E] [TopologicalSpace E]
16   [IsNonarchimedeanLocalField E]
17 variable (m : Type*) [Fintype m] [DecidableEq m]
18 
19 /-- The actual E-linear centralizer embedded in F-linear matrix endomorphisms.
20 Units.map is used because the target coefficient ring need not be commutative. -/
21 def centralizerEmbedding : GL m E →* (Matrix m m (Module.End F E))ˣ :=
22   Units.map (RingHom.mapMatrix (Algebra.lmul F E).toRingHom).toMonoidHom
23 
24 def scalarEmbedding : Eˣ →* (Matrix m m (Module.End F E))ˣ :=
25   (centralizerEmbedding F E m).comp (GeneralLinearGroup.scalar m)
26 
27 def uniformizerEndUnit : (Module.End F E)ˣ := coefficientUnit F E
28   (ActualLocalUnitDecomposition.uniformizer E)
29   (ActualLocalUnitDecomposition.uniformizer_ne_zero E)
30 
31 omit [Module.Finite F E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
32 theorem centralizerEmbedding_integral (k : GL m 𝒪[E]) :
33     centralizerEmbedding F E m (ActualIntegralGeneralLinear.embedding E m k) =
34       mappedMatrixUnit (coefficientMap F E) k := by
35   apply Units.ext
36   rfl
37 
38 omit [Module.Finite F E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
39 theorem scalarEmbedding_integralUnit (v : 𝒪[E]ˣ) :
40     scalarEmbedding F E m (ActualLocalUnitTopology.unitEmbedding E v) =
41       mappedMatrixUnit (coefficientMap F E) (GeneralLinearGroup.scalar m v) := by
42   apply Units.ext
43   ext i j
44   have hmap (x : 𝒪[E]) : algebraMap 𝒪[E] E x = (x : E) := rfl
45   by_cases hij : i = j
46   · subst j
47     simp [scalarEmbedding, centralizerEmbedding, GeneralLinearGroup.scalar,
48       Matrix.scalar_apply, Matrix.diagonal, mappedMatrixUnit, coefficientMap,
49       ActualLocalUnitTopology.unitEmbedding, hmap]
50   · simp [scalarEmbedding, centralizerEmbedding, GeneralLinearGroup.scalar,
51       Matrix.scalar_apply, Matrix.diagonal, mappedMatrixUnit, hij]
52 
53 omit [Module.Finite F E] in
54 theorem scalarEmbedding_uniformizer :
55     scalarEmbedding F E m (ActualLocalUnitDecomposition.uniformizerUnit E) =
56       diagonalUnit (fun _ : m => coefficientUnit F E
57         (ActualLocalUnitDecomposition.uniformizer E)
58         (ActualLocalUnitDecomposition.uniformizer_ne_zero E)) := by
59   apply Units.ext
60   ext i j
61   by_cases hij : i = j
62   · subst j
63     simp [scalarEmbedding, centralizerEmbedding, GeneralLinearGroup.scalar,
64       Matrix.scalar_apply, diagonalUnit, Matrix.diagonal,
65       coefficientUnit, ActualLocalUnitDecomposition.uniformizerUnit]
66   · simp [scalarEmbedding, centralizerEmbedding, GeneralLinearGroup.scalar,
67       Matrix.scalar_apply, diagonalUnit, Matrix.diagonal, hij]
68 
69 omit [Module.Finite F E] in
70 /-- Radical commutation and integral-unit stability imply that every actual
71 extension-field scalar normalizes the endomorphism lattice. -/
72 theorem scalarEmbedding_normalizes
73     (L : AddSubgroup (Matrix m m (Module.End F E)))
74     (hL : IsMatrixBimodule (coefficientMap F E) L)
75     (hcomm : L.map (AddMonoidHom.mulLeft
76         ((diagonalUnit (fun _ : m => uniformizerEndUnit F E) :
77           (Matrix m m (Module.End F E))ˣ) : Matrix m m (Module.End F E))) =
78       L.map (AddMonoidHom.mulRight
79         ((diagonalUnit (fun _ : m => uniformizerEndUnit F E) :
80           (Matrix m m (Module.End F E))ˣ) : Matrix m m (Module.End F E))))
81     (c : Eˣ) : scalarEmbedding F E m c ∈ normalizingUnits L := by
82   obtain ⟨⟨v, n⟩, rfl⟩ := ActualLocalUnitDecomposition.normalForm_surjective E c
83   rw [ActualLocalUnitDecomposition.normalFormHom_apply, map_mul, map_zpow,
84     scalarEmbedding_integralUnit F E m, scalarEmbedding_uniformizer F E m]
85   exact (normalizingUnits L).mul_mem
86     (mappedMatrixUnit_mem_normalizingUnits (coefficientMap F E) L hL
87       (GeneralLinearGroup.scalar m v))
88     ((normalizingUnits L).zpow_mem
89       (normalizes_of_left_right_map_eq L (diagonalUnit (fun _ : m => uniformizerEndUnit F E))
90         hcomm) n.toAdd)
91 
92 omit [Module.Finite F E] in
93 theorem centralizerEmbedding_cartan (a : m → ℕ) :
94     centralizerEmbedding F E m
95       (PaperXI.SplitRadical105.cartan
96         (ActualLocalUnitDecomposition.uniformizer E : E)
97         (ActualLocalUnitDecomposition.uniformizer_ne_zero E) a) =
98       diagonalUnit (fun i => uniformizerEndUnit F E ^ (-(a i : ℤ))) := by
99   apply Units.ext
100   apply Matrix.ext
101   intro i j
102   have hp (n : ℕ) :
103       ((uniformizerEndUnit F E ^ (-(n : ℤ)) : (Module.End F E)ˣ) : Module.End F E) =
104         (Algebra.lmul F E).toRingHom (((ActualLocalUnitDecomposition.uniformizer E : E) ^ n)⁻¹) := by
105     change (((Units.map (Algebra.lmul F E).toRingHom)
106       (ActualLocalUnitDecomposition.uniformizerUnit E) ^ (-(n : ℤ)) :
107         (Module.End F E)ˣ) : Module.End F E) = _
108     rw [← map_zpow]
109     change (Algebra.lmul F E).toRingHom
110       (((ActualLocalUnitDecomposition.uniformizerUnit E ^ (-(n : ℤ)) : Eˣ) : E)) = _
111     congr 1
112     simp [ActualLocalUnitDecomposition.uniformizerUnit]
113   by_cases hij : i = j
114   · subst j
115     change (Algebra.lmul F E).toRingHom
116       ((Matrix.diagonal (fun k =>
117         ((ActualLocalUnitDecomposition.uniformizer E : E) ^ a k)⁻¹)) i i) =
118       (Matrix.diagonal (fun k =>
119         ((uniformizerEndUnit F E ^ (-(a k : ℤ)) : (Module.End F E)ˣ) : Module.End F E))) i i
120     simp only [Matrix.diagonal_apply_eq]
121     exact (hp (a i)).symm
122   · simp [centralizerEmbedding, PaperXI.SplitRadical105.cartan,
123       PaperXI.SplitRadical105.diagonalGL, diagonalUnit, Matrix.diagonal, hij]
124 
125 /-- Literal equality of scalar-uniformizer images, the matrix form of radical
126 commutation used by this arithmetic calculation. -/
127 def RadicalCommutes (L : AddSubgroup (Matrix m m (Module.End F E))) : Prop :=
128   L.map (AddMonoidHom.mulLeft
129       ((diagonalUnit (fun _ : m => uniformizerEndUnit F E) :
130         (Matrix m m (Module.End F E))ˣ) : Matrix m m (Module.End F E))) =
131     L.map (AddMonoidHom.mulRight
132       ((diagonalUnit (fun _ : m => uniformizerEndUnit F E) :
133         (Matrix m m (Module.End F E))ˣ) : Matrix m m (Module.End F E)))
134 
135 /-- Every actual Cartan factorization gives the same index for every finite full
136 integer-ring bimodule commuting with the scalar radical. -/
137 theorem relIndex_of_actual_cartan [Nonempty m]
138     (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
139     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup)
140     (hfg : L.FG)
141     (hfull : Submodule.span F (L : Set (Matrix m m (Module.End F E))) = ⊤)
142     (hcomm : RadicalCommutes F E m L.toAddSubgroup)
143     (y : GL m E) (c : Eˣ) (l r : GL m 𝒪[E]) (a : m → ℕ)
144     (hy : y = GeneralLinearGroup.scalar m c *
145       (ActualIntegralGeneralLinear.embedding E m l *
146         PaperXI.SplitRadical105.cartan (ActualLocalUnitDecomposition.uniformizer E : E)
147           (ActualLocalUnitDecomposition.uniformizer_ne_zero E) a *
148             ActualIntegralGeneralLinear.embedding E m r)) :
149     (L.toAddSubgroup ⊓ L.toAddSubgroup.map
150       (unitConjugation (centralizerEmbedding F E m y)).toAddMonoidHom).relIndex
151         L.toAddSubgroup =
152       Nat.card 𝓀[E] ^ (Module.finrank F E * ∑ i, ∑ j, ((a i : ℤ) - (a j : ℤ)).toNat) := by
153   let k₁ := scalarEmbedding F E m c * mappedMatrixUnit (coefficientMap F E) l
154   let d := diagonalUnit (fun i => uniformizerEndUnit F E ^ (-(a i : ℤ)))
155   let k₂ := mappedMatrixUnit (coefficientMap F E) r
156   have he : centralizerEmbedding F E m y = k₁ * d * k₂ := by
157     rw [hy]
158     simp only [map_mul, centralizerEmbedding_integral, centralizerEmbedding_cartan]
159     change scalarEmbedding F E m c * (_ * _ * _) = _
160     simp only [k₁, d, k₂, mul_assoc]
161   have hk₁ : k₁ ∈ normalizingUnits L.toAddSubgroup :=
162     (normalizingUnits L.toAddSubgroup).mul_mem
163       (scalarEmbedding_normalizes F E m L.toAddSubgroup hL hcomm c)
164       (mappedMatrixUnit_mem_normalizingUnits (coefficientMap F E) L.toAddSubgroup hL l)
165   have hk₂ : k₂ ∈ normalizingUnits L.toAddSubgroup :=
166     mappedMatrixUnit_mem_normalizingUnits (coefficientMap F E) L.toAddSubgroup hL r
167   rw [he, intersection_relIndex_outer_factors L.toAddSubgroup k₁ d k₂ hk₁ hk₂]
168   have hd := diagonal_relIndex_of_radical_commutation F E L hL
169     (Classical.choice (inferInstance : Nonempty m)) hfg hfull
170     (ActualLocalUnitDecomposition.uniformizer E)
171     (ActualLocalUnitDecomposition.uniformizer_irreducible E)
172     (uniformizerEndUnit F E) (coefficientUnit_coe F E _ _) hcomm
173     (fun i => -(a i : ℤ))
174   have hs : (∑ i, ∑ j, (-(a i : ℤ) - -(a j : ℤ)).toNat) =
175       ∑ i, ∑ j, ((a i : ℤ) - (a j : ℤ)).toNat := by
176     simp only [neg_sub_neg]
177     exact Finset.sum_comm
178   simpa only [hs] using hd
179 
180 /-- The Cartan factorization is obtained from the authenticated actual local
181 field theorem, rather than supplied as an arithmetic-index hypothesis. -/
182 theorem exists_actual_cartan_index [Nonempty m]
183     (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
184     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup)
185     (hfg : L.FG)
186     (hfull : Submodule.span F (L : Set (Matrix m m (Module.End F E))) = ⊤)
187     (hcomm : RadicalCommutes F E m L.toAddSubgroup) (y : GL m E) :
188     ∃ c : Eˣ, ∃ l r : GL m 𝒪[E], ∃ a : m → ℕ,
189       (∃ i, a i = 0) ∧
190       y = GeneralLinearGroup.scalar m c *
191         (ActualIntegralGeneralLinear.embedding E m l *
192           PaperXI.SplitRadical105.cartan (ActualLocalUnitDecomposition.uniformizer E : E)
193             (ActualLocalUnitDecomposition.uniformizer_ne_zero E) a *
194               ActualIntegralGeneralLinear.embedding E m r) ∧
195       (L.toAddSubgroup ⊓ L.toAddSubgroup.map
196         (unitConjugation (centralizerEmbedding F E m y)).toAddMonoidHom).relIndex
197           L.toAddSubgroup =
198         Nat.card 𝓀[E] ^ (Module.finrank F E * ∑ i, ∑ j, ((a i : ℤ) - (a j : ℤ)).toNat) := by
199   obtain ⟨c, l, r, a, ha, hy⟩ := PaperXI.ActualLocalCartan106.hasCartan E m y
200   exact ⟨c, l, r, a, ha, hy,
201     relIndex_of_actual_cartan F E m L hL hfg hfull hcomm y c l r a hy⟩
202 
203 /-- The finite-generation hypothesis may start with the genuine base-ring
204 lattice. Scalar stability is derived from its matrix bimodule, and the larger
205 scalar module keeps exactly the same additive carrier and full span. -/
206 theorem exists_actual_cartan_index_of_base_lattice [Nonempty m]
207     {R : Type*} [Ring R]
208     [Module R (Matrix m m (Module.End F E))] [SMul R 𝒪[E]]
209     [IsScalarTower R 𝒪[E] (Matrix m m (Module.End F E))]
210     (L : Submodule R (Matrix m m (Module.End F E)))
211     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup)
212     (hfg : L.FG)
213     (hfull : Submodule.span F (L : Set (Matrix m m (Module.End F E))) = ⊤)
214     (hcomm : RadicalCommutes F E m L.toAddSubgroup) (y : GL m E) :
215     ∃ a : m → ℕ,
216       (L.toAddSubgroup ⊓ L.toAddSubgroup.map
217         (unitConjugation (centralizerEmbedding F E m y)).toAddMonoidHom).relIndex
218           L.toAddSubgroup =
219         Nat.card 𝓀[E] ^ (Module.finrank F E * ∑ i, ∑ j, ((a i : ℤ) - (a j : ℤ)).toNat) := by
220   have hsmul : ∀ (s : 𝒪[E]) (x : Module.End F E),
221       s • x = coefficientMap F E s * x := by intro s x; ext v; rfl
222   let hstable := PaperXI.MoritaScalarUpgrade110.scalar_stable_of_matrix_bimodule
223     (coefficientMap F E) hsmul L.toAddSubgroup hL
224   let L' := PaperXI.MoritaScalarUpgrade110.upgrade L hstable
225   have hfg' : L'.FG := PaperXI.MoritaScalarUpgrade110.upgrade_fg L hstable hfg
226   obtain ⟨c, l, r, a, _, _, hindex⟩ :=
227     exists_actual_cartan_index F E m L' hL hfg' hfull hcomm y
228   exact ⟨a, hindex⟩
229 
230 omit [Module.Finite F E] [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
231 /-- Matrix rank zero has trivial lattice index. -/
232 theorem relIndex_isEmpty [IsEmpty m]
233     (L : AddSubgroup (Matrix m m (Module.End F E))) (y : GL m E) :
234     (L ⊓ L.map (unitConjugation (centralizerEmbedding F E m y)).toAddMonoidHom).relIndex L = 1 := by
235   let K := (L ⊓ L.map (unitConjugation (centralizerEmbedding F E m y)).toAddMonoidHom).addSubgroupOf L
236   have hz (z : L) : z = 0 := Subsingleton.elim _ _
237   have hx (x : L ⧸ K) : x = 0 := by
238     refine Quotient.inductionOn x ?_
239     intro z
240     rw [hz z]
241     rfl
242   let : Subsingleton (L ⧸ K) := ⟨fun x z => (hx x).trans (hx z).symm⟩
243   exact Nat.card_unique
244 
245 /-- Matrix rank one has no nonzero Cartan difference. -/
246 theorem relIndex_subsingleton [Nonempty m] [Subsingleton m]
247     (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
248     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup)
249     (hfg : L.FG)
250     (hfull : Submodule.span F (L : Set (Matrix m m (Module.End F E))) = ⊤)
251     (hcomm : RadicalCommutes F E m L.toAddSubgroup) (y : GL m E) :
252     (L.toAddSubgroup ⊓ L.toAddSubgroup.map
253       (unitConjugation (centralizerEmbedding F E m y)).toAddMonoidHom).relIndex
254         L.toAddSubgroup = 1 := by
255   obtain ⟨c, l, r, a, _, _, hindex⟩ :=
256     exists_actual_cartan_index F E m L hL hfg hfull hcomm y
257   have hs : (∑ i, ∑ j, ((a i : ℤ) - (a j : ℤ)).toNat) = 0 := by
258     apply Finset.sum_eq_zero
259     intro i _
260     apply Finset.sum_eq_zero
261     intro j _
262     rw [Subsingleton.elim i j]
263     simp
264   simpa only [hs, Nat.mul_zero, pow_zero] using hindex
265 
266 end PaperXI.MoritaActualCartan110

Back to source controls