CompletedGroupAlgebra/OpenFiniteQuotientTopology/FiniteQuotients.lean
1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/OpenFiniteQuotientTopology/FiniteQuotients.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed group algebras
14The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.
15-/
16open scoped Topology
18namespace CompletedGroupAlgebra
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
24open ProCGroups.InverseSystems
25open ProCGroups.Completion
27universe u v w
29variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/-- An open coefficient ideal gives a continuous quotient map when the quotient is equipped
34with the discrete topology. This is the coefficient-side continuity used in RZ §5.3. -/
36 (I : Ideal R) (hI : IsOpen (I : Set R)) :
37 letI : TopologicalSpace (R ⧸ I) := ⊥
38 Continuous (Ideal.Quotient.mk I) := by
39 letI : TopologicalSpace (R ⧸ I) := ⊥
40 haveI : DiscreteTopology (R ⧸ I) := ⟨rfl⟩
41 rw [continuous_discrete_rng]
42 intro b
43 rcases Ideal.Quotient.mk_surjective (I := I) b with ⟨a, rfl⟩
44 have hpre :
45 (Ideal.Quotient.mk I) ⁻¹' ({Ideal.Quotient.mk I a} : Set (R ⧸ I)) =
46 (fun x : R => x - a) ⁻¹' (I : Set R) := by
47 ext x
48 simp only [Set.mem_preimage, Set.mem_singleton_iff, Ideal.Quotient.eq, SetLike.mem_coe]
49 rw [hpre]
50 exact hI.preimage (continuous_id.sub continuous_const)
52omit G [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [IsTopologicalRing R] in
53/-- Finite-stage group algebras are functorial in the coefficient ring by continuous maps. -/
55 (S : Type u) [CommRing S] [TopologicalSpace S]
56 (Q : Type v) [Group Q] [Finite Q]
57 (f : R →+* S) (hf : Continuous f) :
58 letI : TopologicalSpace (MonoidAlgebra R Q) := finiteGroupAlgebraTopology R Q
59 letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
60 Continuous (MonoidAlgebra.mapRangeRingHom Q f :
61 MonoidAlgebra R Q → MonoidAlgebra S Q) := by
62 classical
63 letI : Fintype Q := Fintype.ofFinite Q
64 letI : TopologicalSpace (MonoidAlgebra R Q) := finiteGroupAlgebraTopology R Q
65 letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
66 let eR : MonoidAlgebra R Q ≃ (Q → R) := Finsupp.equivFunOnFinite
67 let eS : MonoidAlgebra S Q ≃ (Q → S) := Finsupp.equivFunOnFinite
68 have heS : Topology.IsInducing (eS : MonoidAlgebra S Q → Q → S) :=
69 Topology.IsInducing.induced eS
70 have hcoordR : ∀ q : Q, Continuous fun x : MonoidAlgebra R Q => x q := by
71 intro q
72 simpa [eR] using
73 (continuous_apply q).comp
74 (continuous_induced_dom : Continuous (eR : MonoidAlgebra R Q → Q → R))
75 rw [heS.continuous_iff]
76 apply continuous_pi
77 intro q
78 change Continuous fun x : MonoidAlgebra R Q =>
79 (MonoidAlgebra.mapRangeRingHom Q f x : MonoidAlgebra S Q) q
80 simpa [MonoidAlgebra.mapRangeRingHom_apply] using hf.comp (hcoordR q)
82omit R G [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G]
83 [TopologicalSpace G] [IsTopologicalGroup G] in
84/-- If the coefficient ring is discrete, then the finite-stage group algebra has the discrete
87 (S : Type u) [CommRing S] [TopologicalSpace S] [DiscreteTopology S]
88 (Q : Type v) [Group Q] [Finite Q] :
89 letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
90 DiscreteTopology (MonoidAlgebra S Q) := by
91 classical
92 letI : Fintype Q := Fintype.ofFinite Q
93 letI : TopologicalSpace (MonoidAlgebra S Q) := finiteGroupAlgebraTopology S Q
94 let e : MonoidAlgebra S Q ≃ (Q → S) := 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/-- The RZ §5.3 finite quotient `[(R/I)(G/U)]`, with both coefficient and group quotient
101applied, used in the kernel-neighborhood topology. -/
103 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
104 [IsTopologicalGroup G] (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
105 Type (max u v) :=
106 MonoidAlgebra (R ⧸ I) (CompletedGroupAlgebraQuotient G U)
108omit [TopologicalSpace R] [IsTopologicalRing R] in
109/-- The coefficient quotient map `R[G/U] -> (R/I)[G/U]`. -/
111 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
112 [IsTopologicalGroup G]
113 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
114 CompletedGroupAlgebraStage R G U →+*
115 CompletedGroupAlgebraCoeffQuotientStage R G I U :=
116 MonoidAlgebra.mapRangeRingHom (CompletedGroupAlgebraQuotient G U)
117 (Ideal.Quotient.mk I)
119omit [TopologicalSpace R] [IsTopologicalRing R] in
120@[simp]
122 (I : Ideal R) (U : CompletedGroupAlgebraIndex G)
123 (q : CompletedGroupAlgebraQuotient G U) (r : R) :
124 completedGroupAlgebraStageCoeffQuotientMap R G I U (MonoidAlgebra.single q r) =
125 MonoidAlgebra.single q (Ideal.Quotient.mk I r) := by
126 exact MonoidAlgebra.mapRangeRingHom_single (Ideal.Quotient.mk I) q r
128omit [TopologicalSpace R] [IsTopologicalRing R] in
130 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
131 Function.Surjective (completedGroupAlgebraStageCoeffQuotientMap R G I U) := by
132 classical
133 intro x
134 induction x using Finsupp.induction with
136 exact ⟨0, map_zero (completedGroupAlgebraStageCoeffQuotientMap R G I U)⟩
137 | single_add q r x _ _ ih =>
138 rcases Ideal.Quotient.mk_surjective (I := I) r with ⟨a, ha⟩
139 rcases ih with ⟨y, hy⟩
140 refine ⟨(MonoidAlgebra.single q a : CompletedGroupAlgebraStage R G U) + y, ?_⟩
141 rw [map_add, completedGroupAlgebraStageCoeffQuotientMap_single, hy, ha]
143omit [TopologicalSpace R] [IsTopologicalRing R] in
144/-- The RZ §5.3 quotient map `[R G] -> [(R/I)(G/U)]`. -/
146 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
147 [IsTopologicalGroup G]
148 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
149 MonoidAlgebra R G →+* CompletedGroupAlgebraCoeffQuotientStage R G I U :=
150 (completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
151 (completedGroupAlgebraStageMap R G U)
153omit [TopologicalSpace R] [IsTopologicalRing R] in
154@[simp]
156 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (g : G) (r : R) :
157 groupAlgebraFiniteQuotientMap R G I U (MonoidAlgebra.single g r) =
158 MonoidAlgebra.single
160 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)
161 (Ideal.Quotient.mk I r) := by
162 rw [groupAlgebraFiniteQuotientMap, RingHom.comp_apply,
165omit [TopologicalSpace R] [IsTopologicalRing R] in
166@[simp]
168 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (g : G) :
169 groupAlgebraFiniteQuotientMap R G I U (MonoidAlgebra.of R G g) =
170 MonoidAlgebra.of (R ⧸ I) (CompletedGroupAlgebraQuotient G U)
172 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) := by
173 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk,
174 groupAlgebraFiniteQuotientMap_single (R := R) (G := G) I U g (1 : R), map_one]
176omit [TopologicalSpace R] [IsTopologicalRing R] in
177/-- The quotient map `[R G] -> [(R/I)(G/U)]` factors equally as coefficient quotient followed
178by group quotient, or group quotient followed by coefficient quotient. -/
180 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
181 groupAlgebraFiniteQuotientMap R G I U =
182 (MonoidAlgebra.mapDomainRingHom (R ⧸ I)
184 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U)).comp
185 (MonoidAlgebra.mapRangeRingHom G (Ideal.Quotient.mk I)) := by
187 completedGroupAlgebraStageMap] using
188 (MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom
189 (f := Ideal.Quotient.mk I)
191 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U))
193omit [TopologicalSpace R] [IsTopologicalRing R] in
195 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
196 Function.Surjective (groupAlgebraFiniteQuotientMap R G I U) := by
197 classical
198 intro x
199 induction x using Finsupp.induction with
201 exact ⟨0, map_zero (groupAlgebraFiniteQuotientMap R G I U)⟩
202 | single_add q r x _ _ ih =>
204 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U q with
205 ⟨g, hg⟩
206 rcases Ideal.Quotient.mk_surjective (I := I) r with ⟨a, ha⟩
207 rcases ih with ⟨y, hy⟩
208 refine ⟨(MonoidAlgebra.single g a : MonoidAlgebra R G) + y, ?_⟩
209 rw [map_add, groupAlgebraFiniteQuotientMap_single, hy, hg, ha]
211omit [TopologicalSpace R] [IsTopologicalRing R] in
212/-- The kernels used in Ribes--Zalesskii's natural topology on `[R G]`; for the
213kernel-neighborhood topology this family is restricted to open ideals `I` and open normal
214subgroups `U`. -/
216 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
217 [IsTopologicalGroup G]
218 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
219 Ideal (MonoidAlgebra R G) :=
220 RingHom.ker (groupAlgebraFiniteQuotientMap R G I U)
222omit [TopologicalSpace R] [IsTopologicalRing R] in
223@[simp]
225 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
226 x ∈ groupAlgebraFiniteQuotientKernel R G I U ↔
227 groupAlgebraFiniteQuotientMap R G I U x = 0 :=
228 Iff.rfl
230omit [TopologicalSpace R] [IsTopologicalRing R] in
232 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
233 groupAlgebraFiniteQuotientKernel R G I U =
234 Ideal.comap (completedGroupAlgebraStageMap R G U)
235 (RingHom.ker (completedGroupAlgebraStageCoeffQuotientMap R G I U)) :=
236 rfl
238omit [TopologicalSpace R] [IsTopologicalRing R] in
239/-- Coefficient transition `(R/I)[G/U] -> (R/J)[G/U]` induced by an inclusion `I ≤ J`. -/
241 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
242 [IsTopologicalGroup G] {I J : Ideal R} (hIJ : I ≤ J)
243 (U : CompletedGroupAlgebraIndex G) :
244 CompletedGroupAlgebraCoeffQuotientStage R G I U →+*
245 CompletedGroupAlgebraCoeffQuotientStage R G J U :=
246 MonoidAlgebra.mapRangeRingHom (CompletedGroupAlgebraQuotient G U)
247 (Ideal.Quotient.factor hIJ)
249omit [TopologicalSpace R] [IsTopologicalRing R] in
250@[simp]
252 {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G)
253 (q : CompletedGroupAlgebraQuotient G U) (r : R ⧸ I) :
254 completedGroupAlgebraCoeffQuotientTransition R G hIJ U (MonoidAlgebra.single q r) =
255 MonoidAlgebra.single q (Ideal.Quotient.factor hIJ r) := by
256 exact MonoidAlgebra.mapRangeRingHom_single (Ideal.Quotient.factor hIJ) q r
258omit [TopologicalSpace R] [IsTopologicalRing R] in
259@[simp]
261 {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G) :
262 (completedGroupAlgebraCoeffQuotientTransition R G hIJ U).comp
263 (completedGroupAlgebraStageCoeffQuotientMap R G I U) =
264 completedGroupAlgebraStageCoeffQuotientMap R G J U := by
267 ← MonoidAlgebra.mapRangeRingHom_comp]
268 simp only [Ideal.Quotient.factor_comp_mk]
270omit [TopologicalSpace R] [IsTopologicalRing R] in
272 {I J : Ideal R} (hIJ : I ≤ J) (U : CompletedGroupAlgebraIndex G) :
273 Function.Surjective (completedGroupAlgebraCoeffQuotientTransition R G hIJ U) := by
274 classical
275 intro x
276 induction x using Finsupp.induction with
278 exact ⟨0, map_zero (completedGroupAlgebraCoeffQuotientTransition R G hIJ U)⟩
279 | single_add q r x _ _ ih =>
280 rcases Ideal.Quotient.factor_surjective hIJ r with ⟨a, ha⟩
281 rcases ih with ⟨y, hy⟩
282 refine ⟨(MonoidAlgebra.single q a :
283 CompletedGroupAlgebraCoeffQuotientStage R G I U) + y, ?_⟩
284 rw [map_add, completedGroupAlgebraCoeffQuotientTransition_single, hy, ha]
286omit [TopologicalSpace R] [IsTopologicalRing R] in
287/-- Group-quotient transition `(R/I)[G/V] -> (R/I)[G/U]` induced by `U ≤ V`. -/
289 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
290 [IsTopologicalGroup G] (I : Ideal R) {U V : CompletedGroupAlgebraIndex G}
291 (hUV : U ≤ V) :
292 CompletedGroupAlgebraCoeffQuotientStage R G I V →+*
293 CompletedGroupAlgebraCoeffQuotientStage R G I U :=
294 MonoidAlgebra.mapDomainRingHom (R ⧸ I)
295 (OpenNormalSubgroupInClass.map
296 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
297 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
299omit [TopologicalSpace R] [IsTopologicalRing R] in
300@[simp]
302 (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
303 (q : CompletedGroupAlgebraQuotient G V) (r : R ⧸ I) :
305 (MonoidAlgebra.single q r) =
306 MonoidAlgebra.single
307 ((OpenNormalSubgroupInClass.map
308 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
309 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) r := by
310 classical
311 simp only [completedGroupAlgebraCoeffQuotientGroupTransition, MonoidAlgebra.single,
312 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
313 rfl
315omit [TopologicalSpace R] [IsTopologicalRing R] in
316@[simp]
318 (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
319 (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV).comp
320 (completedGroupAlgebraStageCoeffQuotientMap R G I V) =
321 (completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
322 (completedGroupAlgebraTransition R G hUV) := by
326 exact (MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom
327 (f := Ideal.Quotient.mk I)
328 (g := OpenNormalSubgroupInClass.map
329 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
330 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)).symm
332omit [TopologicalSpace R] [IsTopologicalRing R] [IsTopologicalGroup G] in
334 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
335 Function.Surjective
336 (OpenNormalSubgroupInClass.map
337 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
338 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) := by
339 intro q
340 rcases QuotientGroup.mk'_surjective
341 ((((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)) q with
342 ⟨g, rfl⟩
343 refine ⟨QuotientGroup.mk'
344 ((((OrderDual.ofDual V).1 : OpenNormalSubgroup G) : Subgroup G)) g, rfl⟩
346omit [TopologicalSpace R] [IsTopologicalRing R] in
348 (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
349 Function.Surjective (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV) := by
350 classical
351 intro x
352 induction x using Finsupp.induction with
354 exact ⟨0, map_zero (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV)⟩
355 | single_add q r x _ _ ih =>
357 (G := G) hUV q with
358 ⟨p, hp⟩
359 rcases ih with ⟨y, hy⟩
360 refine ⟨(MonoidAlgebra.single p r :
361 CompletedGroupAlgebraCoeffQuotientStage R G I V) + y, ?_⟩
364omit [TopologicalSpace R] [IsTopologicalRing R] in
365/-- The combined transition `(R/I)[G/V] -> (R/J)[G/U]`. -/
367 (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
368 [IsTopologicalGroup G] {I J : Ideal R} (hIJ : I ≤ J)
369 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
370 CompletedGroupAlgebraCoeffQuotientStage R G I V →+*
371 CompletedGroupAlgebraCoeffQuotientStage R G J U :=
372 (completedGroupAlgebraCoeffQuotientTransition R G hIJ U).comp
373 (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV)
375omit [TopologicalSpace R] [IsTopologicalRing R] in
376@[simp]
378 {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
379 (hUV : U ≤ V) (q : CompletedGroupAlgebraQuotient G V) (r : R ⧸ I) :
380 completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV
381 (MonoidAlgebra.single q r) =
382 MonoidAlgebra.single
383 ((OpenNormalSubgroupInClass.map
384 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
385 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q)
386 (Ideal.Quotient.factor hIJ r) := by
387 rw [completedGroupAlgebraFiniteQuotientTransition, RingHom.comp_apply,
391omit [TopologicalSpace R] [IsTopologicalRing R] in
392@[simp]
394 (I : Ideal R) {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
395 (completedGroupAlgebraCoeffQuotientGroupTransition R G I hUV).comp
396 (groupAlgebraFiniteQuotientMap R G I V) =
397 groupAlgebraFiniteQuotientMap R G I U := by
400 rw [completedGroupAlgebraCoeffQuotientGroupTransition, ← RingHom.comp_assoc,
401 ← MonoidAlgebra.mapDomainRingHom_comp]
402 congr 1
404omit [TopologicalSpace R] [IsTopologicalRing R] in
405@[simp]
407 {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
408 (hUV : U ≤ V) :
409 (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV).comp
410 (groupAlgebraFiniteQuotientMap R G I V) =
411 groupAlgebraFiniteQuotientMap R G J U := by
412 rw [completedGroupAlgebraFiniteQuotientTransition, RingHom.comp_assoc,
415 rw [← RingHom.comp_assoc,
418omit [TopologicalSpace R] [IsTopologicalRing R] in
420 {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
421 (hUV : U ≤ V) :
422 Function.Surjective (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV) := by
423 intro x
425 (R := R) (G := G) hIJ U x with
426 ⟨y, hy⟩
428 (R := R) (G := G) I hUV y with
429 ⟨z, hz⟩
430 exact ⟨z, by rw [completedGroupAlgebraFiniteQuotientTransition, RingHom.comp_apply, hz, hy]⟩
432/-- The corresponding projection from the completed group algebra to `[(R/I)(G/U)]`. -/
434 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
435 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
436 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
437 Carrier R G →+*
438 CompletedGroupAlgebraCoeffQuotientStage R G I U :=
439 (completedGroupAlgebraStageCoeffQuotientMap R G I U).comp
442@[simp]
444 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) :
445 (completedGroupAlgebraFiniteQuotientProjection R G I U).comp
446 (toCompletedGroupAlgebraRingHom R G) =
447 groupAlgebraFiniteQuotientMap R G I U := by
448 apply RingHom.ext
449 intro x
450 rfl
452@[simp]
454 (I : Ideal R) (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
456 (toCompletedGroupAlgebra R G x) =
457 groupAlgebraFiniteQuotientMap R G I U x :=
458 rfl
460@[simp 900]
462 {I J : Ideal R} (hIJ : I ≤ J) {U V : CompletedGroupAlgebraIndex G}
463 (hUV : U ≤ V) :
464 (completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV).comp
465 (completedGroupAlgebraFiniteQuotientProjection R G I V) =
466 completedGroupAlgebraFiniteQuotientProjection R G J U := by
467 apply RingHom.ext
468 intro x
469 calc
470 completedGroupAlgebraFiniteQuotientTransition R G hIJ hUV
471 (completedGroupAlgebraFiniteQuotientProjection R G I V x)
472 =
476 (completedGroupAlgebraProjection R G V x))) := rfl
477 _ =
480 (completedGroupAlgebraTransition R G hUV
481 (completedGroupAlgebraProjection R G V x))) := by
482 have hstage := congrFun
483 (congrArg DFunLike.coe
485 (R := R) (G := G) I (U := U) (V := V) hUV))
486 (completedGroupAlgebraProjection R G V x)
487 exact congrArg (completedGroupAlgebraCoeffQuotientTransition R G hIJ U) hstage
488 _ =
491 (completedGroupAlgebraProjection R G U x)) := by
492 rw [completedGroupAlgebraProjection_compatible (R := R) (G := G) x hUV]
493 _ =
495 (completedGroupAlgebraProjection R G U x) := by
496 exact congrFun
497 (congrArg DFunLike.coe
499 (R := R) (G := G) (I := I) (J := J) hIJ U))
500 (completedGroupAlgebraProjection R G U x)
501 _ = completedGroupAlgebraFiniteQuotientProjection R G J U x := rfl
502end