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

Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients

1import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps
3/-!
4# Finite coefficient-and-group quotients
6This file constructs the finite group-algebra stages obtained by quotienting both coefficients
7and the group. It develops their quotient maps, kernels, transition maps, basis formulas,
8continuity, and surjectivity.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
20open ProCGroups.Completion
22universe u v w
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/--
29An open coefficient ideal gives a continuous quotient map when the quotient is equipped with the
30discrete topology. This is the coefficient-side continuity used in Ribes--Zalesskii Section
31\(5.3\).
32-/
33theorem continuous_idealQuotient_mk_openIdeal_discrete
34 (I : Ideal R) (hI : IsOpen (I : Set R)) :
35 letI : TopologicalSpace (R ⧸ I) := ⊥
36 Continuous (Ideal.Quotient.mk I) := by
37 letI : TopologicalSpace (R ⧸ I) := ⊥
38 haveI : DiscreteTopology (R ⧸ I) := ⟨rfl⟩
39 rw [continuous_discrete_rng]
40 intro b
41 rcases Ideal.Quotient.mk_surjective (I := I) b with ⟨a, rfl⟩
42 have hpre :
43 (Ideal.Quotient.mk I) ⁻¹' ({Ideal.Quotient.mk I a} : Set (R ⧸ I)) =
44 (fun x : R => x - a) ⁻¹' (I : Set R) := by
45 ext x
46 simp only [Set.mem_preimage, Set.mem_singleton_iff, Ideal.Quotient.eq, SetLike.mem_coe]
47 rw [hpre]
48 exact hI.preimage (continuous_id.sub continuous_const)
50omit G [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [IsTopologicalRing R] in
51/-- Finite-stage group algebras are functorial in the coefficient ring by continuous maps. -/
52theorem finiteGroupAlgebra_mapRangeRingHom_continuous
53 (S : Type u) [CommRing S] [TopologicalSpace S]
54 (Q : Type v) [Group Q] [Finite Q]
55 (f : R →+* S) (hf : Continuous f) :
56 letI : TopologicalSpace (MonoidAlgebra R Q) := finiteGroupAlgebraTopology R Q
57 letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
58 Continuous (MonoidAlgebra.mapRingHom Q f :
59 MonoidAlgebra R Q → MonoidAlgebra S Q) := by
60 classical
61 letI : Fintype Q := Fintype.ofFinite Q
62 letI : TopologicalSpace (MonoidAlgebra R Q) := finiteGroupAlgebraTopology R Q
63 letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
64 let eS : MonoidAlgebra S Q ≃ (Q → S) :=
65 MonoidAlgebra.coeffEquiv.trans Finsupp.equivFunOnFinite
66 have heS : Topology.IsInducing (eS : MonoidAlgebra S Q → Q → S) :=
67 Topology.IsInducing.induced eS
68 have hcoordR : ∀ q : Q, Continuous fun x : MonoidAlgebra R Q => x.coeff q := by
69 intro q
70 exact finiteGroupAlgebra_coordinate_continuous R Q q
71 rw [heS.continuous_iff]
72 apply continuous_pi
73 intro q
74 change Continuous fun x : MonoidAlgebra R Q =>
75 (MonoidAlgebra.mapRingHom Q f x : MonoidAlgebra S Q).coeff q
76 change Continuous (f ∘ fun x : MonoidAlgebra R Q => x.coeff q)
77 exact hf.comp (hcoordR q)
79omit R G [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G]
80 [TopologicalSpace G] [IsTopologicalGroup G] in
81/--
82If the coefficient ring is discrete, then the finite-stage group algebra has the discrete
83finite-product topology.
84-/
85theorem finiteGroupAlgebraTopology_discrete_of_discrete_coeff
86 (S : Type u) [CommRing S] [TopologicalSpace S] [DiscreteTopology S]
87 (Q : Type v) [Finite Q] :
88 letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
89 DiscreteTopology (MonoidAlgebra S Q) := by
90 classical
91 letI : Fintype Q := Fintype.ofFinite Q
92 letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
93 let e : MonoidAlgebra S Q ≃ (Q → S) :=
94 MonoidAlgebra.coeffEquiv.trans Finsupp.equivFunOnFinite
95 haveI : DiscreteTopology (Q → S) := inferInstance
96 exact DiscreteTopology.of_continuous_injective
97 (continuous_induced_dom : Continuous (e : MonoidAlgebra S Q → Q → S)) e.injective
99omit [TopologicalSpace R] [IsTopologicalRing R] in
100/--
101The Ribes--Zalesskii Section \(5.3\) finite quotient \((R/I)[G/U]\) applies both the coefficient
102quotient and the group quotient and is used in the kernel-neighborhood topology.
103-/
104abbrev CompletedGroupAlgebraCoeffQuotientStage
105 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
106 [IsTopologicalGroup G] (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
107 Type (max u v) :=
108 MonoidAlgebra (R ⧸ I) (CompletedGroupAlgebraQuotient G U)
110omit [TopologicalSpace R] [IsTopologicalRing R] in
111/-- The coefficient quotient map \(R[G/U]\) \(\to\) \((R/I)[G/U]\). -/
112def completedGroupAlgebraStageCoeffQuotientMap
113 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
114 [IsTopologicalGroup G]
115 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
116 CompletedGroupAlgebraStage R G U →+*
117 CompletedGroupAlgebraCoeffQuotientStage R G I U :=
118 MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G U)
119 (Ideal.Quotient.mk I)
121omit [TopologicalSpace R] [IsTopologicalRing R] in
122/--
123The coefficient-quotient map sends a singleton supported at a finite quotient class to the
124corresponding singleton with transformed coefficient and unchanged quotient support.
125-/
126@[simp]
127theorem completedGroupAlgebraStageCoeffQuotientMap_single
128 (I : Ideal R) (U : CompletedGroupAlgebraIndex G)
129 (q : CompletedGroupAlgebraQuotient G U) (r : R) :
130 completedGroupAlgebraStageCoeffQuotientMap R G I U (MonoidAlgebra.single q r) =
131 MonoidAlgebra.single q (Ideal.Quotient.mk I r) := by
132 exact MonoidAlgebra.mapRingHom_single (Ideal.Quotient.mk I) q r
134omit [TopologicalSpace R] [IsTopologicalRing R] in
135/--
136The finite-stage coefficient-quotient map is surjective; every target singleton is lifted by
137keeping the quotient support and lifting the coefficient.
138-/
139theorem completedGroupAlgebraStageCoeffQuotientMap_surjective
140 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
141 Function.Surjective (completedGroupAlgebraStageCoeffQuotientMap R G I U) := by
142 classical
143 intro x
144 obtain ⟨y, hy⟩ :=
145 MonoidAlgebra.map_surjective (M := CompletedGroupAlgebraQuotient G U)
146 (Ideal.Quotient.mk I).toAddMonoidHom Ideal.Quotient.mk_surjective x
147 exact ⟨y, hy⟩
149omit [TopologicalSpace R] [IsTopologicalRing R] in
150/-- The finite-quotient map \(R[G]\to (R/I)[G/U]\) used in Ribes--Zalesskii Section \(5.3\). -/
151def groupAlgebraFiniteQuotientMap
152 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
153 [IsTopologicalGroup G]
154 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
155 MonoidAlgebra R G →+* CompletedGroupAlgebraCoeffQuotientStage R G I U :=
156 (completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
157 (completedGroupAlgebraStageMap R G U)
159omit [TopologicalSpace R] [IsTopologicalRing R] in
160/--
161The finite quotient map on a group algebra sends a singleton \(r[g]\) to the singleton \(\bar
162r[\bar g]\) in \((R/I)[G/U]\).
163-/
164@[simp]
165theorem groupAlgebraFiniteQuotientMap_single
166 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (g : G) (r : R) :
167 groupAlgebraFiniteQuotientMap R G I U (MonoidAlgebra.single g r) =
168 MonoidAlgebra.single
169 (openNormalSubgroupInClassProj
171 (Ideal.Quotient.mk I r) := by
172 change
173 MonoidAlgebra.map (Ideal.Quotient.mk I)
174 (MonoidAlgebra.mapDomain
175 (openNormalSubgroupInClassProj
177 (MonoidAlgebra.single g r)) =
178 MonoidAlgebra.single
179 (openNormalSubgroupInClassProj
181 (Ideal.Quotient.mk I r)
182 rw [MonoidAlgebra.mapDomain_single, MonoidAlgebra.map_single]
183 rfl
185omit [TopologicalSpace R] [IsTopologicalRing R] in
186/--
187The finite quotient group-algebra map is computed by choosing representatives and applying the
188quotient map to supports.
189-/
190@[simp]
191theorem groupAlgebraFiniteQuotientMap_of
192 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (g : G) :
193 groupAlgebraFiniteQuotientMap R G I U (MonoidAlgebra.of R G g) =
194 MonoidAlgebra.of (R ⧸ I) (CompletedGroupAlgebraQuotient G U)
195 (openNormalSubgroupInClassProj
196 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) := by
197 change
198 groupAlgebraFiniteQuotientMap R G I U (MonoidAlgebra.single g 1) =
199 MonoidAlgebra.single
200 (openNormalSubgroupInClassProj
202 rw [groupAlgebraFiniteQuotientMap_single]
203 exact congrArg
204 (MonoidAlgebra.single
205 (openNormalSubgroupInClassProj
207 (Ideal.Quotient.mk I).map_one
209omit [TopologicalSpace R] [IsTopologicalRing R] in
210/--
211The quotient map \(R[G] \to (R/I)[G/U]\) factors equally as coefficient quotient followed by
212group quotient, or group quotient followed by coefficient quotient.
213-/
214theorem groupAlgebraFiniteQuotientMap_eq_mapDomain_comp_mapRange
215 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
216 groupAlgebraFiniteQuotientMap R G I U =
217 (MonoidAlgebra.mapDomainRingHom (R ⧸ I)
218 (openNormalSubgroupInClassProj
220 (MonoidAlgebra.mapRingHom G (Ideal.Quotient.mk I)) := by
221 change
222 (MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G U)
223 (Ideal.Quotient.mk I)).comp
224 (MonoidAlgebra.mapDomainRingHom R
225 (openNormalSubgroupInClassProj
227 (MonoidAlgebra.mapDomainRingHom (R ⧸ I)
228 (openNormalSubgroupInClassProj
230 (MonoidAlgebra.mapRingHom G (Ideal.Quotient.mk I))
231 exact MonoidAlgebra.mapRingHom_comp_mapDomainRingHom
232 (f := Ideal.Quotient.mk I)
233 (g := openNormalSubgroupInClassProj
236omit [TopologicalSpace R] [IsTopologicalRing R] in
237/--
238The finite quotient map on group algebras is surjective, expressing functoriality after passage
239to finite quotient stages.
240-/
241theorem groupAlgebraFiniteQuotientMap_surjective
242 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
243 Function.Surjective (groupAlgebraFiniteQuotientMap R G I U) := by
244 classical
245 exact
246 (completedGroupAlgebraStageCoeffQuotientMap_surjective
247 (R := R) (G := G) I U).comp
248 (completedGroupAlgebraStageMap_surjective (R := R) (G := G) U)
250omit [TopologicalSpace R] [IsTopologicalRing R] in
251/--
252The kernels used in Ribes--Zalesskii's natural topology on \(R[G]\); for the kernel-neighborhood
253topology this family is restricted to open ideals \(I\) and open normal subgroups \(U\).
254-/
255def groupAlgebraFiniteQuotientKernel
256 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
257 [IsTopologicalGroup G]
258 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
259 Ideal (MonoidAlgebra R G) :=
260 RingHom.ker (groupAlgebraFiniteQuotientMap R G I U)
262omit [TopologicalSpace R] [IsTopologicalRing R] in
263/--
264An element of \(R[G]\) lies in `groupAlgebraFiniteQuotientKernel` exactly when its image in
265\((R/I)[G/U]\) is zero.
266-/
267@[simp]
268theorem mem_groupAlgebraFiniteQuotientKernel_iff
269 {R : Type u} {G : Type v} [CommRing R] [Group G] [TopologicalSpace G]
270 [IsTopologicalGroup G]
271 {I : Ideal R} {U : CompletedGroupAlgebraIndex G} {x : MonoidAlgebra R G} :
272 x ∈ groupAlgebraFiniteQuotientKernel R G I U ↔
273 groupAlgebraFiniteQuotientMap R G I U x = 0 :=
274 Iff.rfl
276omit [TopologicalSpace R] [IsTopologicalRing R] in
277/--
278The kernel of the finite quotient group-algebra map is the comap of the corresponding
279quotient-kernel data.
280-/
281theorem groupAlgebraFiniteQuotientKernel_eq_comap
282 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
283 groupAlgebraFiniteQuotientKernel R G I U =
284 Ideal.comap (completedGroupAlgebraStageMap R G U)
285 (RingHom.ker (completedGroupAlgebraStageCoeffQuotientMap R G I U)) :=
286 rfl
288omit [TopologicalSpace R] [IsTopologicalRing R] in
289/--
290Coefficient transition \((R/I)[G/U]\) \(\to\) \((R/J)[G/U]\) induced by an inclusion \(I\le J\).
291-/
292def completedGroupAlgebraCoeffQuotientTransition
293 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
294 [IsTopologicalGroup G] {I J : Ideal R} (hIJ : I ≤ J)
295 (U : CompletedGroupAlgebraIndex G) :
296 CompletedGroupAlgebraCoeffQuotientStage R G I U →+*
297 CompletedGroupAlgebraCoeffQuotientStage R G J U :=
298 MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotient G U)
299 (Ideal.Quotient.factor hIJ)
301omit [TopologicalSpace R] [IsTopologicalRing R] in
302/--
303The coefficient transition from \(R/I\) to \(R/J\) fixes the support \(q\) and applies
304`Ideal.Quotient.factor` to the singleton coefficient.
305-/
306@[simp]
307theorem completedGroupAlgebraCoeffQuotientTransition_single
308 {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G)
309 (q : CompletedGroupAlgebraQuotient G U) (r : R ⧸ I) :
310 completedGroupAlgebraCoeffQuotientTransition R G hIJ U (MonoidAlgebra.single q r) =
311 MonoidAlgebra.single q (Ideal.Quotient.factor hIJ r) := by
312 exact MonoidAlgebra.mapRingHom_single (Ideal.Quotient.factor hIJ) q r
314omit [TopologicalSpace R] [IsTopologicalRing R] in
315/--
316Applying the coefficient transition after reduction modulo \(I\) agrees with reducing the stage
317coefficients directly modulo \(J\).
318-/
319@[simp]
320theorem completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap
321 {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G) :
322 (completedGroupAlgebraCoeffQuotientTransition R G hIJ U).comp
323 (completedGroupAlgebraStageCoeffQuotientMap R G I U) =
324 completedGroupAlgebraStageCoeffQuotientMap R G J U := by
325 rw [completedGroupAlgebraCoeffQuotientTransition,
326 completedGroupAlgebraStageCoeffQuotientMap, completedGroupAlgebraStageCoeffQuotientMap,
327 ← MonoidAlgebra.mapRingHom_comp]
328 simp only [Ideal.Quotient.factor_comp_mk]
330omit [TopologicalSpace R] [IsTopologicalRing R] in
331/--
332At a fixed quotient stage \(U\), the coefficient transition induced by \(I\leq J\) is
333surjective.
334-/
335theorem completedGroupAlgebraCoeffQuotientTransition_surjective
336 {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G) :
337 Function.Surjective (completedGroupAlgebraCoeffQuotientTransition R G hIJ U) := by
338 classical
339 intro x
340 obtain ⟨y, hy⟩ :=
341 MonoidAlgebra.map_surjective (M := CompletedGroupAlgebraQuotient G U)
342 (Ideal.Quotient.factor hIJ).toAddMonoidHom
343 (Ideal.Quotient.factor_surjective hIJ) x
344 exact ⟨y, hy⟩
346omit [TopologicalSpace R] [IsTopologicalRing R] in
347/-- Group-quotient transition \((R/I)[G/V]\) \(\to\) \((R/I)[G/U]\) induced by \(U\le V\). -/
348def completedGroupAlgebraCoeffQuotientGroupTransition
349 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
350 [IsTopologicalGroup G] (I : Ideal R) {U V : CompletedGroupAlgebraIndex G}
351 (hUV : U ≤ V) :
352 CompletedGroupAlgebraCoeffQuotientStage R G I V →+*
353 CompletedGroupAlgebraCoeffQuotientStage R G I U :=
354 MonoidAlgebra.mapDomainRingHom (R ⧸ I)
355 (OpenNormalSubgroupInClass.map
357 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
359omit [TopologicalSpace R] [IsTopologicalRing R] in
360/--
361The group-quotient transition from \(G/V\) to \(G/U\) sends a singleton to the singleton at the
362induced quotient image and leaves its \(R/I\)-coefficient unchanged.
363-/
364@[simp]
365theorem completedGroupAlgebraCoeffQuotientGroupTransition_single
366 (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
367 (q : CompletedGroupAlgebraQuotient G V) (r : R ⧸ I) :
368 completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV
369 (MonoidAlgebra.single q r) =
370 MonoidAlgebra.single
371 ((OpenNormalSubgroupInClass.map
373 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) r := by
374 change
375 MonoidAlgebra.mapDomain
376 (OpenNormalSubgroupInClass.map
378 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
379 (MonoidAlgebra.single q r) =
380 MonoidAlgebra.single
381 ((OpenNormalSubgroupInClass.map
383 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) r
384 exact MonoidAlgebra.mapDomain_single
386omit [TopologicalSpace R] [IsTopologicalRing R] in
387/--
388Changing the group quotient after reducing coefficients modulo \(I\) agrees with first applying
389the group-stage transition and then reducing coefficients.
390-/
391@[simp]
392theorem completedGroupAlgebraCoeffQuotientGroupTransition_comp_stageCoeffQuotientMap
393 (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
394 (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV).comp
395 (completedGroupAlgebraStageCoeffQuotientMap R G I V) =
396 (completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
397 (completedGroupAlgebraTransition R G hUV) := by
398 rw [completedGroupAlgebraCoeffQuotientGroupTransition,
399 completedGroupAlgebraStageCoeffQuotientMap, completedGroupAlgebraStageCoeffQuotientMap,
400 completedGroupAlgebraTransition]
401 exact (MonoidAlgebra.mapRingHom_comp_mapDomainRingHom
402 (f := Ideal.Quotient.mk I)
403 (g := OpenNormalSubgroupInClass.map
405 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)).symm
407omit [TopologicalSpace R] [IsTopologicalRing R] [IsTopologicalGroup G] in
408/-- The canonical quotient homomorphism \(G/V\to G/U\) induced by \(U\leq V\) is surjective. -/
409theorem completedGroupAlgebraQuotientTransition_surjective
410 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
411 Function.Surjective
412 (OpenNormalSubgroupInClass.map
414 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) := by
415 intro q
416 rcases QuotientGroup.mk'_surjective
417 ((((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)) q with
418 ⟨g, rfl⟩
419 refine ⟨QuotientGroup.mk'
420 ((((OrderDual.ofDual V).1 : OpenNormalSubgroup G) : Subgroup G)) g, rfl⟩
422omit [TopologicalSpace R] [IsTopologicalRing R] in
423/--
424The group-quotient transition \((R/I)[G/V]\to(R/I)[G/U]\) is surjective.
425-/
426theorem completedGroupAlgebraCoeffQuotientGroupTransition_surjective
427 (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
428 Function.Surjective (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV) := by
429 classical
430 intro x
431 obtain ⟨y, hy⟩ :=
432 Finsupp.mapDomain_surjective (M := R ⧸ I)
433 (completedGroupAlgebraQuotientTransition_surjective
434 (G := G) hUV) x.coeff
435 refine ⟨MonoidAlgebra.ofCoeff y, ?_⟩
436 apply MonoidAlgebra.coeff_injective
437 exact hy
439omit [TopologicalSpace R] [IsTopologicalRing R] in
440/-- The combined transition (R/I)[G/V] -> (R/J)[G/U]. -/
441def completedGroupAlgebraFiniteQuotientTransition
442 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
443 [IsTopologicalGroup G] {I J : Ideal R} (hIJ : I ≤ J)
444 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
445 CompletedGroupAlgebraCoeffQuotientStage R G I V →+*
446 CompletedGroupAlgebraCoeffQuotientStage R G J U :=
447 (completedGroupAlgebraCoeffQuotientTransition R G hIJ U).comp
448 (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV)
450omit [TopologicalSpace R] [IsTopologicalRing R] in
451/--
452The combined finite-quotient transition sends a singleton by transporting its support from
453\(G/V\) to \(G/U\) and its coefficient from \(R/I\) to \(R/J\).
454-/
455@[simp]
456theorem completedGroupAlgebraFiniteQuotientTransition_single
457 {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
458 (hUV : U ≤ V) (q : CompletedGroupAlgebraQuotient G V) (r : R ⧸ I) :
459 completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV
460 (MonoidAlgebra.single q r) =
461 MonoidAlgebra.single
462 ((OpenNormalSubgroupInClass.map
464 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q)
465 (Ideal.Quotient.factor hIJ r) := by
466 change
467 MonoidAlgebra.map (Ideal.Quotient.factor hIJ)
468 (MonoidAlgebra.mapDomain
469 (OpenNormalSubgroupInClass.map
471 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
472 (MonoidAlgebra.single q r)) =
473 MonoidAlgebra.single
474 ((OpenNormalSubgroupInClass.map
476 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q)
477 (Ideal.Quotient.factor hIJ r)
478 rw [MonoidAlgebra.mapDomain_single, MonoidAlgebra.map_single]
479 rfl
481omit [TopologicalSpace R] [IsTopologicalRing R] in
482/--
483At fixed coefficient quotient \(R/I\), applying the group-quotient transition after the abstract
484finite-quotient map at \(V\) gives the finite-quotient map at \(U\).
485-/
486@[simp]
487theorem completedGroupAlgebraCoeffQuotientGroupTransition_comp_finiteQuotientMap
488 (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
489 (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV).comp
490 (groupAlgebraFiniteQuotientMap R G I V) =
491 groupAlgebraFiniteQuotientMap R G I U := by
492 apply RingHom.ext
493 intro x
494 calc
495 completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV
496 (groupAlgebraFiniteQuotientMap R G I V x) =
497 completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV
498 (completedGroupAlgebraStageCoeffQuotientMap R G I V
499 (completedGroupAlgebraStageMap R G V x)) := rfl
500 _ =
501 completedGroupAlgebraStageCoeffQuotientMap R G I U
502 (completedGroupAlgebraTransition R G hUV
503 (completedGroupAlgebraStageMap R G V x)) := by
504 exact congrFun
505 (congrArg DFunLike.coe
506 (completedGroupAlgebraCoeffQuotientGroupTransition_comp_stageCoeffQuotientMap
507 (R := R) (G := G) I (U := U) (V := V) hUV))
508 (completedGroupAlgebraStageMap R G V x)
509 _ =
510 completedGroupAlgebraStageCoeffQuotientMap R G I U
511 (completedGroupAlgebraStageMap R G U x) := by
512 congr 1
513 exact congrFun
514 (congrArg DFunLike.coe
515 (completedGroupAlgebraStageMap_compatible
516 (R := R) (G := G) (U := U) (V := V) hUV))
517 x
518 _ = groupAlgebraFiniteQuotientMap R G I U x := rfl
520omit [TopologicalSpace R] [IsTopologicalRing R] in
521/--
522The combined transition from \((R/I)[G/V]\) to \((R/J)[G/U]\), composed with the source
523finite-quotient map, is the target finite-quotient map.
524-/
525@[simp]
526theorem completedGroupAlgebraFiniteQuotientTransition_comp_finiteQuotientMap
527 {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
528 (hUV : U ≤ V) :
529 (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV).comp
530 (groupAlgebraFiniteQuotientMap R G I V) =
531 groupAlgebraFiniteQuotientMap R G J U := by
532 rw [completedGroupAlgebraFiniteQuotientTransition, RingHom.comp_assoc,
533 completedGroupAlgebraCoeffQuotientGroupTransition_comp_finiteQuotientMap]
534 rw [groupAlgebraFiniteQuotientMap, groupAlgebraFiniteQuotientMap]
535 rw [← RingHom.comp_assoc,
536 completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap]
538omit [TopologicalSpace R] [IsTopologicalRing R] in
539/--
540The combined coefficient-and-group transition
541\((R/I)[G/V]\to(R/J)[G/U]\) is surjective.
542-/
543theorem completedGroupAlgebraFiniteQuotientTransition_surjective
544 {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
545 (hUV : U ≤ V) :
546 Function.Surjective (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV) := by
547 intro x
548 rcases completedGroupAlgebraCoeffQuotientTransition_surjective
549 (R := R) (G := G) hIJ U x with
550 ⟨y, hy⟩
551 rcases completedGroupAlgebraCoeffQuotientGroupTransition_surjective
552 (R := R) (G := G) I hUV y with
553 ⟨z, hz⟩
554 exact ⟨z, by rw [completedGroupAlgebraFiniteQuotientTransition, RingHom.comp_apply, hz, hy]⟩
556/-- The corresponding projection from the completed group algebra to \((R/I)[G/U]\). -/
557def completedGroupAlgebraFiniteQuotientProjection
558 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
559 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
560 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
561 CompletedGroupAlgebraCarrier R G →+*
562 CompletedGroupAlgebraCoeffQuotientStage R G I U :=
563 (completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
564 (completedGroupAlgebraProjection R G U)
566/--
567Composing the finite-quotient projection from the completed group algebra with its canonical dense
568ring homomorphism gives `groupAlgebraFiniteQuotientMap`.
569-/
570@[simp]
571theorem completedGroupAlgebraFiniteQuotientProjection_toCompletedGroupAlgebra
572 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
573 (completedGroupAlgebraFiniteQuotientProjection R G I U).comp
574 (toCompletedGroupAlgebraRingHom R G) =
575 groupAlgebraFiniteQuotientMap R G I U := by
576 apply RingHom.ext
577 intro x
578 rfl
580/--
581The finite-quotient projection of the canonical dense element is computed by the associated
582quotient-stage map.
583-/
584@[simp]
585theorem completedGroupAlgebraFiniteQuotientProjection_apply_toCompletedGroupAlgebra
586 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
587 completedGroupAlgebraFiniteQuotientProjection R G I U
588 (toCompletedGroupAlgebra R G x) =
589 groupAlgebraFiniteQuotientMap R G I U x :=
590 rfl
592/--
593Projecting to \((R/I)[G/V]\) and then applying the combined transition agrees with projecting
594directly to \((R/J)[G/U]\).
595-/
596@[simp 900]
597theorem completedGroupAlgebraFiniteQuotientTransition_comp_projection
598 {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
599 (hUV : U ≤ V) :
600 (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV).comp
601 (completedGroupAlgebraFiniteQuotientProjection R G I V) =
602 completedGroupAlgebraFiniteQuotientProjection R G J U := by
603 apply RingHom.ext
604 intro x
605 calc
606 completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV
607 (completedGroupAlgebraFiniteQuotientProjection R G I V x)
608 =
609 completedGroupAlgebraCoeffQuotientTransition R G hIJ U
610 (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV
611 (completedGroupAlgebraStageCoeffQuotientMap R G I V
612 (completedGroupAlgebraProjection R G V x))) := rfl
613 _ =
614 completedGroupAlgebraCoeffQuotientTransition R G hIJ U
615 (completedGroupAlgebraStageCoeffQuotientMap R G I U
616 (completedGroupAlgebraTransition R G hUV
617 (completedGroupAlgebraProjection R G V x))) := by
618 have hstage := congrFun
619 (congrArg DFunLike.coe
620 (completedGroupAlgebraCoeffQuotientGroupTransition_comp_stageCoeffQuotientMap
621 (R := R) (G := G) I (U := U) (V := V) hUV))
622 (completedGroupAlgebraProjection R G V x)
623 exact congrArg (completedGroupAlgebraCoeffQuotientTransition R G hIJ U) hstage
624 _ =
625 completedGroupAlgebraCoeffQuotientTransition R G hIJ U
626 (completedGroupAlgebraStageCoeffQuotientMap R G I U
627 (completedGroupAlgebraProjection R G U x)) := by
628 rw [completedGroupAlgebraProjection_compatible (R := R) (G := G) x hUV]
629 _ =
630 completedGroupAlgebraStageCoeffQuotientMap R G J U
631 (completedGroupAlgebraProjection R G U x) := by
632 exact congrFun
633 (congrArg DFunLike.coe
634 (completedGroupAlgebraCoeffQuotientTransition_comp_stageCoeffQuotientMap
635 (R := R) (G := G) (I := I) (J := J) hIJ U))
636 (completedGroupAlgebraProjection R G U x)
637 _ = completedGroupAlgebraFiniteQuotientProjection R G J U x := rfl
638end
640end CompletedGroupAlgebra