ActualGroupIndex111.lean

1 import PaperXI.ActualCoordinateDeepIdeal111
2 import PaperXI.ActualOnePlusTopology111
3 import PaperXI.MoritaEndomorphismCoordinates111
4 import PaperXI.MoritaPairIndex110
5 import PaperXI.MoritaRadicalDictionary110
6 import PaperXI.DegreeIndex110
7 
8 /-! The exact ambient group index from two supplied open coordinate lattices
9 and two finite full Morita lattices. Canonical H1/J1 identifications remain
10 source matches; no index identity or common ideal is assumed. -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.ActualGroupIndex111
14 open Matrix Module ValuativeRel Topology
15 open PaperXI.OnePlusIntersection110 PaperXI.ActualCoordinateDeepIdeal111
16 open PaperXI.MoritaLattice110 PaperXI.MoritaCornerRank110
17 open PaperXI.MoritaActualCartan110 PaperXI.MoritaRadicalDictionary110
18 open PaperXI.MoritaEndomorphismCoordinates111
19 
20 section GroupOrientation
21 variable {S : Type*} [Ring S]
22 
23 /-- Ring conjugation by g inverse is the inverse group conjugation map. -/
24 theorem units_innerRing_inv (g : Sˣ) :
25     Units.map (innerRing g⁻¹).toMonoidHom = (MulAut.conj g).symm.toMonoidHom := by
26   ext u
27   change (g⁻¹ : Sˣ) * (u : S) * ((g⁻¹)⁻¹ : Sˣ) =
28     ((MulAut.conj g).symm u : S)
29   rw [MulAut.conj_symm_apply]
30   simp only [Units.val_mul, inv_inv]
31 
32 /-- The literal g-inverse image is the g-conjugation pullback. -/
33 theorem map_inner_inv_eq_comap (K : Subgroup Sˣ) (g : Sˣ) :
34     K.map (Units.map (innerRing g⁻¹).toMonoidHom) =
35       K.comap (MulAut.conj g).toMonoidHom := by
36   rw [units_innerRing_inv]
37   exact Subgroup.map_equiv_eq_comap_symm' (MulAut.conj g).symm K
38 
39 end GroupOrientation
40 
41 variable (F : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
42   [IsNonarchimedeanLocalField F]
43 variable (n : Type*) [Fintype n] [DecidableEq n]
44 
45 omit [TopologicalSpace F] [IsNonarchimedeanLocalField F] in
46 /-- This is the actual existing entrywise integral general-linear embedding. -/
47 theorem integralUnitMap_eq_actualEmbedding :
48     Units.map (integralEmbedding F n).toMonoidHom =
49       ActualIntegralGeneralLinear.embedding F n := rfl
50 
51 /-- At the literal first-coordinate orientation, the common deep ideal is
52 constructed from openness rather than supplied as an arithmetic hypothesis. -/
53 theorem onePlus_backward_relIndex
54     (L : AddSubgroup (Matrix n n 𝒪[F])) (hopen : IsOpen (L : Set (Matrix n n 𝒪[F])))
55     (K : Subgroup (Matrix n n 𝒪[F])ˣ)
56     (hK : ∀ u : K, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) - 1 ∈ L)
57     (hL : ∀ x : L, ∃ u : K, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) = 1 + (x : _))
58     (g : GL n F) :
59     ((K.map (ActualIntegralGeneralLinear.embedding F n)) ⊓
60       (K.map (ActualIntegralGeneralLinear.embedding F n)).comap
61         (MulAut.conj g).toMonoidHom).relIndex
62           (K.map (ActualIntegralGeneralLinear.embedding F n)) =
63     ((L.map (integralEmbedding F n).toAddMonoidHom) ⊓
64       (L.map (integralEmbedding F n).toAddMonoidHom).map
65         (innerRing g⁻¹).toAddMonoidHom).relIndex
66           (L.map (integralEmbedding F n).toAddMonoidHom) := by
67   have h := onePlus_conjugate_relIndex F n L hopen K hK hL g⁻¹
68   have hm : Units.map
69       ((innerRing g⁻¹).toRingHom.comp (integralEmbedding F n)).toMonoidHom =
70       (Units.map (innerRing g⁻¹).toMonoidHom).comp
71         (Units.map (integralEmbedding F n).toMonoidHom) := rfl
72   rw [hm, ← Subgroup.map_map, map_inner_inv_eq_comap,
73     integralUnitMap_eq_actualEmbedding] at h
74   have ha : L.map
75       ((innerRing g⁻¹).toRingHom.comp (integralEmbedding F n)).toAddMonoidHom =
76       (L.map (integralEmbedding F n).toAddMonoidHom).map
77         (innerRing g⁻¹).toAddMonoidHom := by
78     change L.map ((innerRing g⁻¹).toAddMonoidHom.comp
79       (integralEmbedding F n).toAddMonoidHom) = _
80     exact (AddSubgroup.map_map L (innerRing g⁻¹).toAddMonoidHom
81       (integralEmbedding F n).toAddMonoidHom).symm
82   rw [ha] at h
83   simpa only [Subgroup.inf_relIndex_left, AddSubgroup.inf_relIndex_left] using h
84 
85 
86 variable (E : Type*) [Field E] [Algebra F E] [Module.Finite F E]
87   [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E]
88 variable (m : Type*) [Fintype m] [DecidableEq m] [Nonempty m]
89 
90 omit [Module.Finite F E] [ValuativeRel E] [IsNonarchimedeanLocalField E] [Nonempty m] in
91 /-- Explicit lattice image matching transports the one-plus group index to the
92 original Morita carrier, with the required inverse centralizer orientation. -/
93 theorem onePlus_index_of_Morita_image
94     (e : (m → E) ≃L[F] (n → F))
95     (L : AddSubgroup (Matrix n n 𝒪[F])) (hopen : IsOpen (L : Set (Matrix n n 𝒪[F])))
96     (K : Subgroup (Matrix n n 𝒪[F])ˣ)
97     (hK : ∀ u : K, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) - 1 ∈ L)
98     (hL : ∀ x : L, ∃ u : K, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) = 1 + (x : _))
99     (M : AddSubgroup (Matrix m m (Module.End F E)))
100     (himage : L.map (integralEmbedding F n).toAddMonoidHom =
101       M.map (coordinateRingEquiv F E m n e).toAddMonoidHom)
102     (y : GL m E) :
103     ((K.map (ActualIntegralGeneralLinear.embedding F n)) ⊓
104       (K.map (ActualIntegralGeneralLinear.embedding F n)).comap
105         (MulAut.conj (ActualCuspidalCandidate105.centralizerMap F E m n e y)).toMonoidHom).relIndex
106           (K.map (ActualIntegralGeneralLinear.embedding F n)) =
107     (M ⊓ M.map (unitConjugation (centralizerEmbedding F E m y⁻¹)).toAddMonoidHom).relIndex M := by
108   have h := onePlus_backward_relIndex F n L hopen K hK hL
109     (ActualCuspidalCandidate105.centralizerMap F E m n e y)
110   rw [himage] at h
111   have hy : coordinateUnitMap F E m n e (centralizerEmbedding F E m y⁻¹) =
112       (ActualCuspidalCandidate105.centralizerMap F E m n e y)⁻¹ := by
113     rw [coordinateUnitMap_centralizer, map_inv]
114   have ha : (innerRing (ActualCuspidalCandidate105.centralizerMap F E m n e y)⁻¹).toAddMonoidHom =
115       (unitConjugation (coordinateUnitMap F E m n e
116         (centralizerEmbedding F E m y⁻¹))).toAddMonoidHom := by
117     rw [hy]
118     rfl
119   rw [ha] at h
120   exact h.trans (coordinate_intersection_relIndex F E m n e M
121     (centralizerEmbedding F E m y⁻¹))
122 
123 /-- Two actual numerical Cartan formulas at the same inverse y prove the
124 ambient H/J index equality. All one-plus and lattice image matches are literal. -/
125 theorem ambient_pair_index
126     (e : (m → E) ≃L[F] (n → F))
127     (L₁ L₂ : AddSubgroup (Matrix n n 𝒪[F]))
128     (hopen₁ : IsOpen (L₁ : Set (Matrix n n 𝒪[F])))
129     (hopen₂ : IsOpen (L₂ : Set (Matrix n n 𝒪[F])))
130     (K₁ K₂ : Subgroup (Matrix n n 𝒪[F])ˣ)
131     (hK₁ : ∀ u : K₁, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) - 1 ∈ L₁)
132     (hL₁ : ∀ x : L₁, ∃ u : K₁, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) = 1 + (x : _))
133     (hK₂ : ∀ u : K₂, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) - 1 ∈ L₂)
134     (hL₂ : ∀ x : L₂, ∃ u : K₂, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) = 1 + (x : _))
135     (M₁ M₂ : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
136     (himage₁ : L₁.map (integralEmbedding F n).toAddMonoidHom =
137       M₁.toAddSubgroup.map (coordinateRingEquiv F E m n e).toAddMonoidHom)
138     (himage₂ : L₂.map (integralEmbedding F n).toAddMonoidHom =
139       M₂.toAddSubgroup.map (coordinateRingEquiv F E m n e).toAddMonoidHom)
140     (hM₁ : IsMatrixBimodule (coefficientMap F E) M₁.toAddSubgroup)
141     (hM₂ : IsMatrixBimodule (coefficientMap F E) M₂.toAddSubgroup)
142     (hfg₁ : M₁.FG) (hfg₂ : M₂.FG)
143     (hfull₁ : Submodule.span F (M₁ : Set (Matrix m m (Module.End F E))) = ⊤)
144     (hfull₂ : Submodule.span F (M₂ : Set (Matrix m m (Module.End F E))) = ⊤)
145     (hcomm₁ : RadicalCommutes F E m M₁.toAddSubgroup)
146     (hcomm₂ : RadicalCommutes F E m M₂.toAddSubgroup) (y : GL m E) :
147     ((K₁.map (ActualIntegralGeneralLinear.embedding F n)) ⊓
148       (K₁.map (ActualIntegralGeneralLinear.embedding F n)).comap
149         (MulAut.conj (ActualCuspidalCandidate105.centralizerMap F E m n e y)).toMonoidHom).relIndex
150           (K₁.map (ActualIntegralGeneralLinear.embedding F n)) =
151     ((K₂.map (ActualIntegralGeneralLinear.embedding F n)) ⊓
152       (K₂.map (ActualIntegralGeneralLinear.embedding F n)).comap
153         (MulAut.conj (ActualCuspidalCandidate105.centralizerMap F E m n e y)).toMonoidHom).relIndex
154           (K₂.map (ActualIntegralGeneralLinear.embedding F n)) := by
155   rw [onePlus_index_of_Morita_image F n E m e L₁ hopen₁ K₁ hK₁ hL₁
156       M₁.toAddSubgroup himage₁ y,
157     onePlus_index_of_Morita_image F n E m e L₂ hopen₂ K₂ hK₂ hL₂
158       M₂.toAddSubgroup himage₂ y]
159   exact MoritaPairIndex110.actual_pair_index F E m M₁ M₂ hM₁ hM₂
160     hfg₁ hfg₂ hfull₁ hfull₂ hcomm₁ hcomm₂ y⁻¹
161 
162 /-- Source-style radical-product equalities supply both scalar-radical premises. -/
163 theorem ambient_pair_index_of_radical_products
164     (e : (m → E) ≃L[F] (n → F))
165     (L₁ L₂ : AddSubgroup (Matrix n n 𝒪[F]))
166     (hopen₁ : IsOpen (L₁ : Set (Matrix n n 𝒪[F])))
167     (hopen₂ : IsOpen (L₂ : Set (Matrix n n 𝒪[F])))
168     (K₁ K₂ : Subgroup (Matrix n n 𝒪[F])ˣ)
169     (hK₁ : ∀ u : K₁, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) - 1 ∈ L₁)
170     (hL₁ : ∀ x : L₁, ∃ u : K₁, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) = 1 + (x : _))
171     (hK₂ : ∀ u : K₂, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) - 1 ∈ L₂)
172     (hL₂ : ∀ x : L₂, ∃ u : K₂, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) = 1 + (x : _))
173     (M₁ M₂ : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
174     (himage₁ : L₁.map (integralEmbedding F n).toAddMonoidHom =
175       M₁.toAddSubgroup.map (coordinateRingEquiv F E m n e).toAddMonoidHom)
176     (himage₂ : L₂.map (integralEmbedding F n).toAddMonoidHom =
177       M₂.toAddSubgroup.map (coordinateRingEquiv F E m n e).toAddMonoidHom)
178     (hM₁ : IsMatrixBimodule (coefficientMap F E) M₁.toAddSubgroup)
179     (hM₂ : IsMatrixBimodule (coefficientMap F E) M₂.toAddSubgroup)
180     (hfg₁ : M₁.FG) (hfg₂ : M₂.FG)
181     (hfull₁ : Submodule.span F (M₁ : Set (Matrix m m (Module.End F E))) = ⊤)
182     (hfull₂ : Submodule.span F (M₂ : Set (Matrix m m (Module.End F E))) = ⊤)
183     (hrad₁ : additiveProduct (actualRadical F E m) M₁.toAddSubgroup =
184       additiveProduct M₁.toAddSubgroup (actualRadical F E m))
185     (hrad₂ : additiveProduct (actualRadical F E m) M₂.toAddSubgroup =
186       additiveProduct M₂.toAddSubgroup (actualRadical F E m)) (y : GL m E) :
187     ((K₁.map (ActualIntegralGeneralLinear.embedding F n)) ⊓
188       (K₁.map (ActualIntegralGeneralLinear.embedding F n)).comap
189         (MulAut.conj (ActualCuspidalCandidate105.centralizerMap F E m n e y)).toMonoidHom).relIndex
190           (K₁.map (ActualIntegralGeneralLinear.embedding F n)) =
191     ((K₂.map (ActualIntegralGeneralLinear.embedding F n)) ⊓
192       (K₂.map (ActualIntegralGeneralLinear.embedding F n)).comap
193         (MulAut.conj (ActualCuspidalCandidate105.centralizerMap F E m n e y)).toMonoidHom).relIndex
194           (K₂.map (ActualIntegralGeneralLinear.embedding F n)) :=
195   ambient_pair_index F n E m e L₁ L₂ hopen₁ hopen₂ K₁ K₂ hK₁ hL₁ hK₂ hL₂
196     M₁ M₂ himage₁ himage₂ hM₁ hM₂ hfg₁ hfg₂ hfull₁ hfull₂
197     (RadicalCommutes_of_actual_radical_products F E m M₁.toAddSubgroup hM₁ hrad₁)
198     (RadicalCommutes_of_actual_radical_products F E m M₂.toAddSubgroup hM₂ hrad₂) y
199 
200 /-- Exact source matches only. Openness, common deep ideals, finite congruence
201 quotients and the final relative-index identity are not fields of this data. -/
202 structure ActualLatticeData
203     (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
204     [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
205     [IsNonarchimedeanLocalField E] [Algebra F E]
206     (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
207     [Nonempty n] (e : (m → E) ≃L[F] (n → F))
208     (D : Subgroup (GL n F)) (θ : D →* ℂˣ) where
209   L1 : AddSubgroup (Matrix n n 𝒪[F])
210   L2 : AddSubgroup (Matrix n n 𝒪[F])
211   K1 : Subgroup (Matrix n n 𝒪[F])ˣ
212   K2 : Subgroup (Matrix n n 𝒪[F])ˣ
213   offsets1 : ∀ u : K1, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) - 1 ∈ L1
214   onePlus1 : ∀ x : L1, ∃ u : K1,
215     ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) = 1 + (x : _)
216   offsets2 : ∀ u : K2, ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) - 1 ∈ L2
217   onePlus2 : ∀ x : L2, ∃ u : K2,
218     ((u : (Matrix n n 𝒪[F])ˣ) : Matrix n n 𝒪[F]) = 1 + (x : _)
219   M1 : Submodule 𝒪[E] (Matrix m m (Module.End F E))
220   M2 : Submodule 𝒪[E] (Matrix m m (Module.End F E))
221   image1 : L1.map (integralEmbedding F n).toAddMonoidHom =
222     M1.toAddSubgroup.map (coordinateRingEquiv F E m n e).toAddMonoidHom
223   image2 : L2.map (integralEmbedding F n).toAddMonoidHom =
224     M2.toAddSubgroup.map (coordinateRingEquiv F E m n e).toAddMonoidHom
225   bimodule1 : IsMatrixBimodule (coefficientMap F E) M1.toAddSubgroup
226   bimodule2 : IsMatrixBimodule (coefficientMap F E) M2.toAddSubgroup
227   finite1 : M1.FG
228   finite2 : M2.FG
229   full1 : Submodule.span F (M1 : Set (Matrix m m (Module.End F E))) = ⊤
230   full2 : Submodule.span F (M2 : Set (Matrix m m (Module.End F E))) = ⊤
231   radical1 : additiveProduct (actualRadical F E m) M1.toAddSubgroup =
232     additiveProduct M1.toAddSubgroup (actualRadical F E m)
233   radical2 : additiveProduct (actualRadical F E m) M2.toAddSubgroup =
234     additiveProduct M2.toAddSubgroup (actualRadical F E m)
235   groupImage1 : K1.map (ActualIntegralGeneralLinear.embedding F n) =
236     (ActualIntersection108.embedding F E m n e D θ).range
237   groupImage2 : K2.map (ActualIntegralGeneralLinear.embedding F n) = D
238 
239 variable [Nonempty n]
240 
241 /-- The exact H/J index hypothesis consumed by the original-character
242 candidate. Existing open-group hypotheses derive lattice openness; the actual
243 Cartan formulas then supply the index at the required inverse orientation. -/
244 theorem ActualLatticeData.actual_index
245     (e : (m → E) ≃L[F] (n → F)) (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
246     (data : ActualLatticeData F E m n e D θ)
247     (hF : Continuous (algebraMap F E)) (hDo : IsOpen (D : Set (GL n F)))
248     (y : GL m E) :
249     ((ActualIntersection108.embedding F E m n e D θ).range ⊓
250       (ActualIntersection108.embedding F E m n e D θ).range.comap
251         (MulAut.conj (ActualCuspidalCandidate105.centralizerMap F E m n e y)).toMonoidHom).relIndex
252           (ActualIntersection108.embedding F E m n e D θ).range =
253     (D ⊓ D.comap
254       (MulAut.conj (ActualCuspidalCandidate105.centralizerMap F E m n e y)).toMonoidHom).relIndex D := by
255   have ho1 : IsOpen
256       (data.K1.map (Units.map (integralEmbedding F n).toMonoidHom) : Set (GL n F)) := by
257     rw [integralUnitMap_eq_actualEmbedding, data.groupImage1]
258     exact DegreeIndex110.actual_embedding_range_open F E m n e D θ hF hDo
259   have ho2 : IsOpen
260       (data.K2.map (Units.map (integralEmbedding F n).toMonoidHom) : Set (GL n F)) := by
261     rw [integralUnitMap_eq_actualEmbedding, data.groupImage2]
262     exact hDo
263   have hL1 := ActualOnePlusTopology111.additive_open_of_image_group_open
264     F n data.L1 data.K1 data.offsets1 data.onePlus1 ho1
265   have hL2 := ActualOnePlusTopology111.additive_open_of_image_group_open
266     F n data.L2 data.K2 data.offsets2 data.onePlus2 ho2
267   have h := ambient_pair_index_of_radical_products F n E m e data.L1 data.L2
268     hL1 hL2 data.K1 data.K2 data.offsets1 data.onePlus1 data.offsets2 data.onePlus2
269     data.M1 data.M2 data.image1 data.image2 data.bimodule1 data.bimodule2
270     data.finite1 data.finite2 data.full1 data.full2 data.radical1 data.radical2 y
271   simpa only [data.groupImage1, data.groupImage2] using h
272 
273 end PaperXI.ActualGroupIndex111

Back to source controls