Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteQuotients
ProCGroups/CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteQuotients/Source

Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteQuotients

1import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients
3/-!
4# The open-finite quotient system
6Open coefficient ideals and open normal group subgroups index a cofiltered system of finite group
7algebras. This file defines its stages, transitions, projections, and the kernel-neighborhood
8topology they induce on the algebraic group algebra.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
20open ProCGroups.Completion
22universe u v
24variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
25variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
26variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
28/--
29The open coefficient ideals used in the kernel-neighborhood topology of Ribes--Zalesskii Section
30\(5.3\).
31-/
32abbrev CompletedGroupAlgebraOpenIdeal
33 (R : Type u) [CommRing R] [TopologicalSpace R] : Type u :=
34 {I : Ideal R // IsOpen (I : Set R)}
36omit G [Group G] [TopologicalSpace G] [IsTopologicalGroup G] in
37/--
38In a profinite coefficient ring, the open-ideal quotients separate points. This is the
39coefficient part of the kernel-intersection statement in Lemma 5.3.5(a).
40-/
41theorem profiniteRing_eq_zero_of_forall_openIdeal_quotient_eq_zero
42 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] {r : R}
43 (hr : ∀ I : CompletedGroupAlgebraOpenIdeal R, Ideal.Quotient.mk I.1 r = 0) :
44 r = 0 := by
45 by_contra hne
46 letI : T1Space R := inferInstance
47 have h0 : (0 : R) ∈ ({r}ᶜ : Set R) := by
48 exact fun h0r => hne h0r.symm
49 have hU : ({r}ᶜ : Set R) ∈ 𝓝 (0 : R) :=
50 isOpen_compl_singleton.mem_nhds h0
51 rcases profiniteRing_hasOpenIdealBasisAtZero R ({r}ᶜ) hU with
52 ⟨I, hIopen, hIU⟩
53 have hrI : r ∈ I := by
54 exact Ideal.Quotient.eq_zero_iff_mem.1 (hr ⟨I, hIopen⟩)
55 exact (hIU hrI) rfl
57/--
58The two-parameter index set for the kernel-neighborhood quotients \((R/I)[G/U]\), with open
59ideals in the coefficient direction and finite group quotients in the group direction.
60-/
61abbrev CompletedGroupAlgebraOpenQuotientIndex
62 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
63 [TopologicalSpace G] : Type (max u v) :=
64 OrderDual (CompletedGroupAlgebraOpenIdeal R) × CompletedGroupAlgebraIndex G
66/--
67The finite quotient index type is nonempty, witnessed by the terminal quotient or canonical base
68object.
69-/
70instance instNonemptyCompletedGroupAlgebraOpenIdeal
71 (R : Type u) [CommRing R] [TopologicalSpace R] :
72 Nonempty (CompletedGroupAlgebraOpenIdeal R) :=
73 ⟨⟨⊤, isOpen_univ⟩⟩
75/-- The family of completed-group-algebra open quotient indices is directed under refinement. -/
76theorem directed_completedGroupAlgebraOpenQuotientIndex
77 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
78 [TopologicalSpace G] :
79 Directed (α := CompletedGroupAlgebraOpenQuotientIndex R G) (· ≤ ·) fun K => K := by
80 intro K L
81 rcases directed_openNormalSubgroupInClass
84 K.2 L.2 with
85 ⟨W, hKW, hLW⟩
86 let I : CompletedGroupAlgebraOpenIdeal R :=
87 ⟨(OrderDual.ofDual K.1).1 ⊓ (OrderDual.ofDual L.1).1, by
88 simpa using (OrderDual.ofDual K.1).2.inter (OrderDual.ofDual L.1).2⟩
89 refine ⟨(OrderDual.toDual I, W), ?_, ?_⟩
90 · constructor
91 · change (I.1 : Ideal R) ≤ (OrderDual.ofDual K.1).1
92 exact inf_le_left
93 · exact hKW
94 · constructor
95 · change (I.1 : Ideal R) ≤ (OrderDual.ofDual L.1).1
96 exact inf_le_right
97 · exact hLW
99/-- The stage \((R/I)[G/U]\) attached to an open-ideal/finite-group quotient index. -/
100abbrev CompletedGroupAlgebraOpenQuotientStage
101 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
102 [TopologicalSpace G] [IsTopologicalGroup G]
103 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
104 Type (max u v) :=
105 CompletedGroupAlgebraCoeffQuotientStage R G ((OrderDual.ofDual K.1).1 : Ideal R) K.2
107/-- The quotient map \(R[G] \to (R/I)[G/U]\) for an open-ideal/finite-group quotient index. -/
108def groupAlgebraOpenFiniteQuotientMap
109 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
110 [TopologicalSpace G] [IsTopologicalGroup G]
111 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
112 MonoidAlgebra R G →+* CompletedGroupAlgebraOpenQuotientStage R G K :=
113 groupAlgebraFiniteQuotientMap R G ((OrderDual.ofDual K.1).1 : Ideal R) K.2
115/-- The kernel neighborhood attached to an open-ideal/finite-group quotient index. -/
116def groupAlgebraOpenFiniteQuotientKernel
117 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
118 [TopologicalSpace G] [IsTopologicalGroup G]
119 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
120 Ideal (MonoidAlgebra R G) :=
121 groupAlgebraFiniteQuotientKernel R G ((OrderDual.ofDual K.1).1 : Ideal R) K.2
123/--
124An element of \(R[G]\) lies in the kernel attached to the open quotient index \(K\) exactly when
125`groupAlgebraOpenFiniteQuotientMap` sends it to zero.
126-/
127@[simp]
128theorem mem_groupAlgebraOpenFiniteQuotientKernel_iff
129 {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R] [Group G]
130 [TopologicalSpace G] [IsTopologicalGroup G]
131 {K : CompletedGroupAlgebraOpenQuotientIndex R G} {x : MonoidAlgebra R G} :
132 x ∈ groupAlgebraOpenFiniteQuotientKernel R G K ↔
133 groupAlgebraOpenFiniteQuotientMap R G K x = 0 :=
134 Iff.rfl
136/-- The transition \((R/I_L)[G/U]_L \to (R/I_K)[G/U]_K\) for \(K \leq L\). -/
137def completedGroupAlgebraOpenFiniteQuotientTransition
138 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
139 [TopologicalSpace G] [IsTopologicalGroup G]
140 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
141 CompletedGroupAlgebraOpenQuotientStage R G L →+*
142 CompletedGroupAlgebraOpenQuotientStage R G K :=
143 completedGroupAlgebraFiniteQuotientTransition R G
144 (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
145 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1)
146 hKL.2
148/--
149The open finite-quotient transition from \(L\) to \(K\), composed with the abstract quotient map
150at \(L\), is the abstract quotient map at \(K\).
151-/
152@[simp]
153theorem completedGroupAlgebraOpenFiniteQuotientTransition_comp_map
154 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
155 [TopologicalSpace G] [IsTopologicalGroup G]
156 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
157 (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
158 (groupAlgebraOpenFiniteQuotientMap R G L) =
159 groupAlgebraOpenFiniteQuotientMap R G K := by
160 exact completedGroupAlgebraFiniteQuotientTransition_comp_finiteQuotientMap
161 (R := R) (G := G)
162 (hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
163 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
164 (hUV := hKL.2)
166/--
167The projection \(\widehat{R[G]} \to (R/I)[G/U]\) for an open-ideal/finite-group quotient index.
168-/
169def completedGroupAlgebraOpenFiniteQuotientProjection
170 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
171 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
172 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
173 CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraOpenQuotientStage R G K :=
174 completedGroupAlgebraFiniteQuotientProjection R G
175 ((OrderDual.ofDual K.1).1 : Ideal R) K.2
177/--
178Composing the completed-group-algebra projection at the open quotient index \(K\) with the
179canonical dense ring homomorphism gives the corresponding open finite-quotient map.
180-/
181@[simp]
182theorem completedGroupAlgebraOpenFiniteQuotientProjection_toCompletedGroupAlgebra
183 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
184 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
185 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
186 (completedGroupAlgebraOpenFiniteQuotientProjection R G K).comp
187 (toCompletedGroupAlgebraRingHom R G) =
188 groupAlgebraOpenFiniteQuotientMap R G K := by
189 rfl
191/--
192The transition from \(L\) to \(K\), composed with the completed projection at \(L\), is the
193completed projection at \(K\).
194-/
195@[simp]
196theorem completedGroupAlgebraOpenFiniteQuotientTransition_comp_projection
197 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
198 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
199 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
200 (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
201 (completedGroupAlgebraOpenFiniteQuotientProjection R G L) =
202 completedGroupAlgebraOpenFiniteQuotientProjection R G K := by
203 exact completedGroupAlgebraFiniteQuotientTransition_comp_projection
204 (R := R) (G := G)
205 (hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
206 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
207 (hUV := hKL.2)
209/-- The open-finite quotient kernel is antitone with respect to quotient refinement. -/
210theorem groupAlgebraOpenFiniteQuotientKernel_antitone
211 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
212 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
213 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
214 groupAlgebraOpenFiniteQuotientKernel R G L ≤
215 groupAlgebraOpenFiniteQuotientKernel R G K := by
216 intro x hx
217 rw [mem_groupAlgebraOpenFiniteQuotientKernel_iff] at hx ⊢
218 have hcomp := congrFun
219 (congrArg DFunLike.coe
220 (completedGroupAlgebraOpenFiniteQuotientTransition_comp_map (R := R) (G := G) hKL))
221 x
222 rw [RingHom.comp_apply, hx, map_zero] at hcomp
223 exact hcomp.symm
225/--
226The discrete topology on each kernel-neighborhood quotient \((R/I)[G/U]\). This is the topology
227used in the construction of the abstract group-algebra topology.
228-/
229@[reducible]
230def completedGroupAlgebraOpenFiniteQuotientStageTopology
231 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
232 [TopologicalSpace G] [IsTopologicalGroup G]
233 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
234 TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
235 ⊥
237/--
238The finite stage completed group algebra open-finite quotient stage is discrete for its finite
239quotient topology.
240-/
241theorem completedGroupAlgebraOpenFiniteQuotientStage_discrete
242 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
243 [TopologicalSpace G] [IsTopologicalGroup G]
244 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
245 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
246 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
247 DiscreteTopology (CompletedGroupAlgebraOpenQuotientStage R G K) := by
248 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
249 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
250 exact ⟨rfl⟩
252/--
253The coefficient quotient from the finite stage \(R[G/U]\) to the kernel-neighborhood quotient
254\((R/I)[G/U]\) is continuous when the target carries the discrete quotient topology.
255-/
256theorem continuous_completedGroupAlgebraStageCoeffQuotientMap_openIdeal
257 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
258 letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
259 (completedGroupAlgebraSystem R G).topologicalSpace K.2
260 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
261 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
262 Continuous (completedGroupAlgebraStageCoeffQuotientMap R G
263 ((OrderDual.ofDual K.1).1 : Ideal R) K.2) := by
264 let Iopen : CompletedGroupAlgebraOpenIdeal R := OrderDual.ofDual K.1
265 let Q := CompletedGroupAlgebraQuotient G K.2
266 letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
267 (completedGroupAlgebraSystem R G).topologicalSpace K.2
268 letI : TopologicalSpace (R ⧸ (Iopen.1 : Ideal R)) := ⊥
269 haveI : DiscreteTopology (R ⧸ (Iopen.1 : Ideal R)) := ⟨rfl⟩
270 have hmk : Continuous (Ideal.Quotient.mk (Iopen.1 : Ideal R)) :=
271 continuous_idealQuotient_mk_openIdeal_discrete
272 (R := R) (I := Iopen.1) Iopen.2
273 have hcont :
274 letI : TopologicalSpace (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) :=
275 finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
276 Continuous (completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 K.2) := by
277 dsimp [CompletedGroupAlgebraStage, CompletedGroupAlgebraCoeffQuotientStage, Q]
278 exact finiteGroupAlgebra_mapRangeRingHom_continuous
279 (R := R) (S := R ⧸ (Iopen.1 : Ideal R)) Q
280 (Ideal.Quotient.mk (Iopen.1 : Ideal R)) hmk
281 have hdisc :
282 letI : TopologicalSpace (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) :=
283 finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
284 DiscreteTopology (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) := by
285 dsimp [CompletedGroupAlgebraCoeffQuotientStage, Q]
286 exact finiteGroupAlgebraTopology_discrete_of_discrete_coeff
287 (S := R ⧸ (Iopen.1 : Ideal R)) Q
288 let tfin : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
289 finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
290 let tdisc : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
291 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
292 have ht : tfin = tdisc := by
293 dsimp [tfin, tdisc, completedGroupAlgebraOpenFiniteQuotientStageTopology]
294 exact hdisc.eq_bot
295 change @Continuous (CompletedGroupAlgebraStage R G K.2)
296 (CompletedGroupAlgebraOpenQuotientStage R G K)
297 ((completedGroupAlgebraSystem R G).topologicalSpace K.2) tdisc
298 (completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 K.2)
299 rw [← ht]
300 exact hcont
302/--
303The projection \(\widehat{R[G]} \to (R/I)[G/U]\) to any two-parameter finite quotient is
304continuous.
305-/
306theorem continuous_completedGroupAlgebraOpenFiniteQuotientProjection
307 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
308 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
309 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
310 Continuous (completedGroupAlgebraOpenFiniteQuotientProjection R G K) := by
311 letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
312 (completedGroupAlgebraSystem R G).topologicalSpace K.2
313 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
314 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
315 exact (continuous_completedGroupAlgebraStageCoeffQuotientMap_openIdeal
316 (R := R) (G := G) K).comp ((completedGroupAlgebraSystem R G).continuous_projection K.2)
318/-- The product of all open-finite quotient maps \(R[G] \to (R/I)[G/U]\). -/
319def groupAlgebraOpenFiniteQuotientProductMap
320 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
321 [TopologicalSpace G] [IsTopologicalGroup G] :
322 MonoidAlgebra R G →
323 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
324 CompletedGroupAlgebraOpenQuotientStage R G K :=
325 fun x K => groupAlgebraOpenFiniteQuotientMap R G K x
327/--
328The kernel-neighborhood topology on \(R[G]\), induced by all maps \(R[G] \to (R/I)[G/U]\) with
329\(I\) open and \(U\) open normal with finite quotient.
330-/
331@[reducible]
332def groupAlgebraOpenFiniteQuotientKernelTopology
333 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
334 [TopologicalSpace G] [IsTopologicalGroup G] :
335 TopologicalSpace (MonoidAlgebra R G) :=
336 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
337 TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
338 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
339 TopologicalSpace.induced (groupAlgebraOpenFiniteQuotientProductMap R G) inferInstance
341/-- The product of the finite quotient maps is continuous for the kernel-neighborhood topology. -/
342theorem continuous_groupAlgebraOpenFiniteQuotientProductMap_kernelTopology
343 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
344 [TopologicalSpace G] [IsTopologicalGroup G] :
345 letI : TopologicalSpace (MonoidAlgebra R G) :=
346 groupAlgebraOpenFiniteQuotientKernelTopology R G
347 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
348 TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
349 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
350 Continuous (groupAlgebraOpenFiniteQuotientProductMap R G) := by
351 letI : TopologicalSpace (MonoidAlgebra R G) :=
352 groupAlgebraOpenFiniteQuotientKernelTopology R G
353 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
354 TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
355 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
356 exact continuous_induced_dom
358/--
359The finite quotient map \(R[G]\to (R/I)[G/U]\) is continuous for the kernel-neighborhood
360topology.
361-/
362theorem continuous_groupAlgebraOpenFiniteQuotientMap_kernelTopology
363 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
364 [TopologicalSpace G] [IsTopologicalGroup G]
365 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
366 letI : TopologicalSpace (MonoidAlgebra R G) :=
367 groupAlgebraOpenFiniteQuotientKernelTopology R G
368 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
369 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
370 Continuous (groupAlgebraOpenFiniteQuotientMap R G K) := by
371 letI : TopologicalSpace (MonoidAlgebra R G) :=
372 groupAlgebraOpenFiniteQuotientKernelTopology R G
373 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
374 TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
375 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
376 change Continuous fun x : MonoidAlgebra R G =>
377 groupAlgebraOpenFiniteQuotientProductMap R G x K
378 exact (continuous_apply K).comp
379 (continuous_groupAlgebraOpenFiniteQuotientProductMap_kernelTopology R G)
381/-- Each open-finite quotient kernel is open in the kernel topology. -/
382theorem groupAlgebraOpenFiniteQuotientKernel_isOpen_kernelTopology
383 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
384 [TopologicalSpace G] [IsTopologicalGroup G]
385 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
386 letI : TopologicalSpace (MonoidAlgebra R G) :=
387 groupAlgebraOpenFiniteQuotientKernelTopology R G
388 IsOpen (groupAlgebraOpenFiniteQuotientKernel R G K : Set (MonoidAlgebra R G)) := by
389 letI : TopologicalSpace (MonoidAlgebra R G) :=
390 groupAlgebraOpenFiniteQuotientKernelTopology R G
391 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
392 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
393 haveI : DiscreteTopology (CompletedGroupAlgebraOpenQuotientStage R G K) :=
394 completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
395 change IsOpen ((groupAlgebraOpenFiniteQuotientMap R G K) ⁻¹'
396 ({0} : Set (CompletedGroupAlgebraOpenQuotientStage R G K)))
397 exact (isOpen_discrete ({0} : Set (CompletedGroupAlgebraOpenQuotientStage R G K))).preimage
398 (continuous_groupAlgebraOpenFiniteQuotientMap_kernelTopology R G K)
400/-- Every open-finite quotient kernel is a neighborhood of zero for the kernel topology. -/
401theorem groupAlgebraOpenFiniteQuotientKernel_mem_nhds_zero_kernelTopology
402 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
403 [TopologicalSpace G] [IsTopologicalGroup G]
404 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
405 letI : TopologicalSpace (MonoidAlgebra R G) :=
406 groupAlgebraOpenFiniteQuotientKernelTopology R G
407 (groupAlgebraOpenFiniteQuotientKernel R G K : Set (MonoidAlgebra R G)) ∈
408 𝓝 (0 : MonoidAlgebra R G) := by
409 letI : TopologicalSpace (MonoidAlgebra R G) :=
410 groupAlgebraOpenFiniteQuotientKernelTopology R G
411 apply IsOpen.mem_nhds
412 (groupAlgebraOpenFiniteQuotientKernel_isOpen_kernelTopology R G K)
413 change (0 : MonoidAlgebra R G) ∈ groupAlgebraOpenFiniteQuotientKernel R G K
414 rw [mem_groupAlgebraOpenFiniteQuotientKernel_iff]
415 exact map_zero (groupAlgebraOpenFiniteQuotientMap R G K)
417/--
418An open finite-quotient transition sends a singleton by applying the induced group-quotient map
419to its support and the induced ideal-quotient factor to its coefficient.
420-/
421@[simp]
422theorem completedGroupAlgebraOpenFiniteQuotientTransition_single
423 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
424 [TopologicalSpace G] [IsTopologicalGroup G]
425 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L)
426 (q : CompletedGroupAlgebraQuotient G L.2)
427 (r : R ⧸ ((OrderDual.ofDual L.1).1 : Ideal R)) :
428 completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
429 (MonoidAlgebra.single q r) =
430 MonoidAlgebra.single
431 ((OpenNormalSubgroupInClass.map
433 (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual L.2) hKL.2) q)
434 (Ideal.Quotient.factor
435 (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
436 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1) r) := by
437 exact completedGroupAlgebraFiniteQuotientTransition_single (R := R) (G := G)
438 (hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
439 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
440 (hUV := hKL.2) q r
442/-- The open finite-quotient transition associated to \(K\leq K\) is the identity ring map. -/
443@[simp]
444theorem completedGroupAlgebraOpenFiniteQuotientTransition_id
445 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
446 [TopologicalSpace G] [IsTopologicalGroup G]
447 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
448 completedGroupAlgebraOpenFiniteQuotientTransition R G (le_rfl : K ≤ K) =
449 RingHom.id (CompletedGroupAlgebraOpenQuotientStage R G K) := by
450 apply MonoidAlgebra.ringHom_ext
451 · intro r
452 rw [completedGroupAlgebraOpenFiniteQuotientTransition_single,
453 Ideal.Quotient.factor_eq]
454 change MonoidAlgebra.single
455 ((OpenNormalSubgroupInClass.map
457 (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual K.2)
458 (le_rfl : K.2 ≤ K.2)) 1) r =
459 MonoidAlgebra.single 1 r
460 rw [OpenNormalSubgroupInClass.map_id]
461 rfl
462 · intro q
463 rw [completedGroupAlgebraOpenFiniteQuotientTransition_single]
464 change MonoidAlgebra.single
465 ((OpenNormalSubgroupInClass.map
467 (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual K.2)
468 (le_rfl : K.2 ≤ K.2)) q) 1 =
469 MonoidAlgebra.single q 1
470 rw [OpenNormalSubgroupInClass.map_id]
471 rfl
473/--
474Successive open finite-quotient transitions from \(M\) through \(L\) to \(K\) equal the transition
475attached to the composite refinement \(K\leq M\).
476-/
477@[simp 900]
478theorem completedGroupAlgebraOpenFiniteQuotientTransition_comp
479 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
480 [TopologicalSpace G] [IsTopologicalGroup G]
481 {K L M : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) (hLM : L ≤ M) :
482 (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
483 (completedGroupAlgebraOpenFiniteQuotientTransition R G hLM) =
484 completedGroupAlgebraOpenFiniteQuotientTransition R G (hKL.trans hLM) := by
485 change
486 (completedGroupAlgebraFiniteQuotientTransition R G
487 (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
488 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1) hKL.2).comp
489 (completedGroupAlgebraFiniteQuotientTransition R G
490 (show ((OrderDual.ofDual M.1).1 : Ideal R) ≤
491 ((OrderDual.ofDual L.1).1 : Ideal R) from hLM.1) hLM.2) =
492 completedGroupAlgebraFiniteQuotientTransition R G
493 (show ((OrderDual.ofDual M.1).1 : Ideal R) ≤
494 ((OrderDual.ofDual K.1).1 : Ideal R) from (hKL.trans hLM).1)
495 (hKL.trans hLM).2
496 simp only [completedGroupAlgebraFiniteQuotientTransition,
497 completedGroupAlgebraCoeffQuotientTransition,
498 completedGroupAlgebraCoeffQuotientGroupTransition]
499 let fKL := Ideal.Quotient.factor
500 (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
501 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1)
502 let fLM := Ideal.Quotient.factor
503 (show ((OrderDual.ofDual M.1).1 : Ideal R) ≤
504 ((OrderDual.ofDual L.1).1 : Ideal R) from hLM.1)
505 let fKM := Ideal.Quotient.factor
506 (show ((OrderDual.ofDual M.1).1 : Ideal R) ≤
507 ((OrderDual.ofDual K.1).1 : Ideal R) from (hKL.trans hLM).1)
508 let gKL :=
509 OpenNormalSubgroupInClass.map
511 (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual L.2) hKL.2
512 let gLM :=
513 OpenNormalSubgroupInClass.map
515 (U := OrderDual.ofDual L.2) (V := OrderDual.ofDual M.2) hLM.2
516 let gKM :=
517 OpenNormalSubgroupInClass.map
519 (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual M.2)
520 (hKL.trans hLM).2
521 let cKL := MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G K.2) fKL
522 let cLM := MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G L.2) fLM
523 let cKM := MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G K.2) fKM
524 let dKL := MonoidAlgebra.mapDomainRingHom
525 (R ⧸ ((OrderDual.ofDual L.1).1 : Ideal R)) gKL
526 let dLM := MonoidAlgebra.mapDomainRingHom
527 (R ⧸ ((OrderDual.ofDual M.1).1 : Ideal R)) gLM
528 let dKM := MonoidAlgebra.mapDomainRingHom
529 (R ⧸ ((OrderDual.ofDual M.1).1 : Ideal R)) gKM
530 let cLMK := MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G K.2) fLM
531 let dKLM := MonoidAlgebra.mapDomainRingHom
532 (R ⧸ ((OrderDual.ofDual M.1).1 : Ideal R)) gKL
533 change (cKL.comp dKL).comp (cLM.comp dLM) = cKM.comp dKM
534 have hswap : dKL.comp cLM = cLMK.comp dKLM := by
535 exact (MonoidAlgebra.mapRingHom_comp_mapDomainRingHom fLM gKL).symm
536 have hcoeff : fKL.comp fLM = fKM := by
537 dsimp [fKL, fLM, fKM]
538 exact Ideal.Quotient.factor_comp _ _
539 have hgroup : gKL.comp gLM = gKM := by
540 dsimp [gKL, gLM, gKM]
541 exact OpenNormalSubgroupInClass.map_comp
543 (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual L.2)
544 (W := OrderDual.ofDual M.2) hKL.2 hLM.2
545 calc
546 (cKL.comp dKL).comp (cLM.comp dLM) =
547 cKL.comp ((dKL.comp cLM).comp dLM) := by
548 rfl
549 _ = cKL.comp ((cLMK.comp dKLM).comp dLM) := by
550 rw [hswap]
551 rfl
552 _ = (cKL.comp cLMK).comp (dKLM.comp dLM) := by
553 rfl
554 _ = (MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G K.2)
555 (fKL.comp fLM)).comp
556 (MonoidAlgebra.mapDomainRingHom
557 (R ⧸ ((OrderDual.ofDual M.1).1 : Ideal R)) (gKL.comp gLM)) := by
558 rw [← MonoidAlgebra.mapRingHom_comp,
559 ← MonoidAlgebra.mapDomainRingHom_comp]
560 rfl
561 _ = cKM.comp dKM := by
562 rw [hcoeff, hgroup]
563 rfl
565/-- Every open finite-quotient transition associated to \(K\leq L\) is surjective. -/
566theorem completedGroupAlgebraOpenFiniteQuotientTransition_surjective
567 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
568 [TopologicalSpace G] [IsTopologicalGroup G]
569 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
570 Function.Surjective (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) :=
571 completedGroupAlgebraFiniteQuotientTransition_surjective
572 (R := R) (G := G)
573 (hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
574 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
575 (hUV := hKL.2)
576end
578end CompletedGroupAlgebra