Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation
2import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.Coeff
4/-!
5# Fox differential: prime-power completed group algebra — in class — system — basic
7The principal declarations in this module are:
9- `PrimePowerCompletedGroupAlgebraStageInClass`
10 The class-restricted prime-power stage at index \((a,U)\), namely
11 \((\mathrm{ZMod}\,\ell^a)[G/U]\).
12- `primePowerCompletedGroupAlgebraTransitionInClass`
13 The combined transition map for class-restricted prime-power stage calculus.
14- `finite_primePowerCompletedGroupAlgebraStageInClass`
15 Each class-indexed prime-power finite stage is finite.
16- `primePowerCompletedGroupAlgebraTransitionInClass_of`
17 The transition map sends a group-like basis element to the basis element supported at its image in
18 the coarser quotient in the Fox differential construction.
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.InverseSystems
26open ProCGroups.ProC
28universe u
30variable (ℓ : ℕ) [Fact (0 < ℓ)]
31variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33omit [Fact (0 < ℓ)] in
34/--
35The class-restricted prime-power stage at index \((a,U)\), namely
36\((\mathrm{ZMod}\,\ell^a)[G/U]\).
37-/
38abbrev PrimePowerCompletedGroupAlgebraStageInClass
39 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
40 Type _ :=
41 ModNCompletedGroupAlgebraStageInClass (ℓ ^ i.1) G C i.2
43/-- Each class-indexed prime-power finite stage is finite. -/
44theorem finite_primePowerCompletedGroupAlgebraStageInClass
45 (C : ProCGroups.FiniteGroupClass.{u})
46 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
47 Finite (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := by
48 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
49 exact finite_modNCompletedGroupAlgebraStageInClass
50 (n := ℓ ^ i.1) (G := G) C i.2
52omit [Fact (0 < ℓ)] in
53/-- The combined transition map for class-restricted prime-power stage calculus. -/
54def primePowerCompletedGroupAlgebraTransitionInClass
55 (C : ProCGroups.FiniteGroupClass.{u})
56 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
57 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j →+*
58 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i := by
59 exact
60 (modNCompletedGroupAlgebraStageCoeffMapInClass
61 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
62 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
63 (modNCompletedGroupAlgebraTransitionInClass (n := ℓ ^ j.1) (G := G) C hij.2)
65omit [Fact (0 < ℓ)] in
66/--
67The transition map sends a group-like basis element to the basis element supported at its image
68in the coarser quotient in the Fox differential construction.
69-/
70@[simp]
71theorem primePowerCompletedGroupAlgebraTransitionInClass_of
72 (C : ProCGroups.FiniteGroupClass.{u})
73 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j)
74 (q : CompletedGroupAlgebraQuotientInClass G C j.2) :
75 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
76 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _ q) =
77 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
78 ((OpenNormalSubgroupInClass.map
79 (C := C) (G := G)
80 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) := by
81 rw [primePowerCompletedGroupAlgebraTransitionInClass, RingHom.comp_apply,
82 modNCompletedGroupAlgebraTransitionInClass_of]
83 change
84 (modNCompletedGroupAlgebraStageCoeffMapInClass
85 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
86 (primePow_dvd_primePow (ℓ := ℓ) hij.1))
87 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1)) _
88 ((OpenNormalSubgroupInClass.map
89 (C := C) (G := G)
90 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)) =
91 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
92 ((OpenNormalSubgroupInClass.map
93 (C := C) (G := G)
94 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
95 exact modNCompletedGroupAlgebraStageCoeffMapInClass_of
96 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
97 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
98 ((OpenNormalSubgroupInClass.map
99 (C := C) (G := G)
100 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
102omit [Fact (0 < ℓ)] in
103/--
104The \(C\)-indexed transition map between finite stages sends a singleton supported at a class of
105the finer quotient to the singleton supported at its image in the coarser quotient, preserving
106the coefficient.
107-/
108@[simp]
109theorem primePowerCompletedGroupAlgebraTransitionInClass_single
110 (C : ProCGroups.FiniteGroupClass.{u})
111 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j)
112 (q : CompletedGroupAlgebraQuotientInClass G C j.2)
113 (a : ModNCompletedCoeff (ℓ ^ j.1)) :
114 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
115 (MonoidAlgebra.single q a) =
116 MonoidAlgebra.single
117 ((OpenNormalSubgroupInClass.map
118 (C := C) (G := G)
119 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
120 (modNCompletedCoeffMap
121 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
122 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) := by
123 change
124 (modNCompletedGroupAlgebraStageCoeffMapInClass
125 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
126 (primePow_dvd_primePow (ℓ := ℓ) hij.1))
127 (modNCompletedGroupAlgebraTransitionInClass
128 (n := ℓ ^ j.1) (G := G) C hij.2 (MonoidAlgebra.single q a)) =
129 MonoidAlgebra.single
130 ((OpenNormalSubgroupInClass.map
131 (C := C) (G := G)
132 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
133 (modNCompletedCoeffMap
134 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
135 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a)
136 rw [modNCompletedGroupAlgebraTransitionInClass_single]
137 exact modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply
138 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
139 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
140 ((OpenNormalSubgroupInClass.map
141 (C := C) (G := G)
142 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) a
144omit [Fact (0 < ℓ)] in
145/--
146The transition map for the prime-power completed group algebra commutes with the finite-stage
147coordinate maps.
148-/
149@[simp]
150theorem primePowerCompletedGroupAlgebraTransitionInClass_eq
151 (C : ProCGroups.FiniteGroupClass.{u})
152 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
153 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij =
154 (modNCompletedGroupAlgebraStageCoeffMapInClass
155 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
156 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
157 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hij.2) := by
158 rfl
160omit [Fact (0 < ℓ)] in
161/--
162The class-indexed prime-power transition agrees with the explicit coefficient-and-quotient
163transition formula.
164-/
165theorem primePowerCompletedGroupAlgebraTransitionInClass_eq'
166 (C : ProCGroups.FiniteGroupClass.{u})
167 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
168 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij =
169 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C hij.2).comp
170 (modNCompletedGroupAlgebraStageCoeffMapInClass
171 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C j.2
172 (primePow_dvd_primePow (ℓ := ℓ) hij.1)) := by
173 rw [primePowerCompletedGroupAlgebraTransitionInClass_eq]
174 exact modNCompletedGroupAlgebraStageCoeffMapInClass_compatible
175 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C
176 (U := i.2) (V := j.2) hij.2
177 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
179omit [Fact (0 < ℓ)] in
180/--
181The transition map attached to the identity refinement is the identity homomorphism in the Fox
182differential construction.
183-/
184@[simp]
185theorem primePowerCompletedGroupAlgebraTransitionInClass_id
186 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
187 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
188 (le_rfl : i ≤ i) =
189 RingHom.id _ := by
190 rw [primePowerCompletedGroupAlgebraTransitionInClass_eq]
191 rw [modNCompletedGroupAlgebraTransitionInClass_id,
192 modNCompletedGroupAlgebraStageCoeffMapInClass_rfl]
193 simp only [RingHomCompTriple.comp_eq]
195omit [Fact (0 < ℓ)] in
196/--
197Class-indexed prime-power completed group-algebra transitions compose along quotient refinements.
198-/
199@[simp 900]
200theorem primePowerCompletedGroupAlgebraTransitionInClass_comp
201 (C : ProCGroups.FiniteGroupClass.{u})
202 {i j k : PrimePowerCompletedGroupAlgebraIndexInClass G C}
203 (hij : i ≤ j) (hjk : j ≤ k) :
204 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij).comp
205 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hjk) =
206 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
207 (hij.trans hjk) := by
208 calc
209 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij).comp
210 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hjk)
211 =
212 ((modNCompletedGroupAlgebraStageCoeffMapInClass
213 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
214 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
215 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hij.2)).comp
216 ((modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hjk.2).comp
217 (modNCompletedGroupAlgebraStageCoeffMapInClass
218 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
219 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
220 rw [primePowerCompletedGroupAlgebraTransitionInClass_eq,
221 primePowerCompletedGroupAlgebraTransitionInClass_eq']
222 _ =
223 (modNCompletedGroupAlgebraStageCoeffMapInClass
224 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
225 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
226 (((modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hij.2).comp
227 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C hjk.2)).comp
228 (modNCompletedGroupAlgebraStageCoeffMapInClass
229 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
230 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
231 apply RingHom.ext
232 intro x
233 rfl
234 _ =
235 (modNCompletedGroupAlgebraStageCoeffMapInClass
236 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
237 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
238 ((modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C
239 (hij.2.trans hjk.2)).comp
240 (modNCompletedGroupAlgebraStageCoeffMapInClass
241 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
242 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
243 rw [modNCompletedGroupAlgebraTransitionInClass_comp]
244 _ =
245 ((modNCompletedGroupAlgebraStageCoeffMapInClass
246 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
247 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
248 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ j.1) G C
249 (hij.2.trans hjk.2))).comp
250 (modNCompletedGroupAlgebraStageCoeffMapInClass
251 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
252 (primePow_dvd_primePow (ℓ := ℓ) hjk.1)) := by
253 rw [← RingHom.comp_assoc]
254 _ =
255 ((modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C
256 (hij.2.trans hjk.2)).comp
257 (modNCompletedGroupAlgebraStageCoeffMapInClass
258 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C k.2
259 (primePow_dvd_primePow (ℓ := ℓ) hij.1))).comp
260 (modNCompletedGroupAlgebraStageCoeffMapInClass
261 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
262 (primePow_dvd_primePow (ℓ := ℓ) hjk.1)) := by
263 rw [modNCompletedGroupAlgebraStageCoeffMapInClass_compatible
264 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C
265 (U := i.2) (V := k.2) (hUV := hij.2.trans hjk.2)
266 (hnm := primePow_dvd_primePow (ℓ := ℓ) hij.1)]
267 _ =
268 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C
269 (hij.2.trans hjk.2)).comp
270 ((modNCompletedGroupAlgebraStageCoeffMapInClass
271 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C k.2
272 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
273 (modNCompletedGroupAlgebraStageCoeffMapInClass
274 (n := ℓ ^ j.1) (m := ℓ ^ k.1) (G := G) C k.2
275 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) := by
276 rw [RingHom.comp_assoc]
277 _ =
278 (modNCompletedGroupAlgebraTransitionInClass (ℓ ^ i.1) G C
279 (hij.2.trans hjk.2)).comp
280 (modNCompletedGroupAlgebraStageCoeffMapInClass
281 (n := ℓ ^ i.1) (m := ℓ ^ k.1) (G := G) C k.2
282 (primePow_dvd_primePow (ℓ := ℓ) (hij.trans hjk).1)) := by
283 rw [modNCompletedGroupAlgebraStageCoeffMapInClass_comp
284 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1) (G := G) C
285 (U := k.2)
286 (hnm := primePow_dvd_primePow (ℓ := ℓ) hij.1)
287 (hmk := primePow_dvd_primePow (ℓ := ℓ) hjk.1)]
288 _ =
289 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C
290 (hij.trans hjk) := by
291 rw [← primePowerCompletedGroupAlgebraTransitionInClass_eq'
292 (ℓ := ℓ) (G := G) C (hij := hij.trans hjk)]
294omit [Fact (0 < ℓ)] in
295/--
296Class-indexed finite-stage prime-power augmentation is compatible with transition maps and
297coefficient reduction.
298-/
299@[simp]
300theorem primePowerCompletedGroupAlgebraStageAugmentationInClass_comp_transition
301 (C : ProCGroups.FiniteGroupClass.{u})
302 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
303 (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2).comp
304 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij) =
305 (modNCompletedCoeffMap
306 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
307 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
308 (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ j.1) G C j.2) := by
309 rw [primePowerCompletedGroupAlgebraTransitionInClass]
310 rw [← RingHom.comp_assoc]
311 rw [modNCompletedGroupAlgebraStageAugmentationInClass_comp_coeffMap]
312 rw [RingHom.comp_assoc]
313 rw [modNCompletedGroupAlgebraStageAugmentationInClass_compatible]
315omit [Fact (0 < ℓ)] in
316/-- The class-restricted inverse system indexed by prime powers and \(C\)-quotients. -/
317def primePowerCompletedGroupAlgebraSystemInClass
318 (C : ProCGroups.FiniteGroupClass.{u}) :
319 InverseSystem (I := PrimePowerCompletedGroupAlgebraIndexInClass G C) where
320 X := PrimePowerCompletedGroupAlgebraStageInClass ℓ G C
321 topologicalSpace := fun _ => ⊥
322 map := fun {i j} hij =>
323 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
324 continuous_map := by
325 intro i j hij
326 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) := ⊥
327 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) := ⊥
328 letI : DiscreteTopology (PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) := ⟨rfl⟩
329 exact continuous_of_discreteTopology
330 map_id := by
331 intro i
332 funext x
333 exact congrFun
334 (congrArg DFunLike.coe
335 (primePowerCompletedGroupAlgebraTransitionInClass_id
336 (ℓ := ℓ) (G := G) C i)) x
337 map_comp := by
338 intro i j k hij hjk
339 funext x
340 exact congrFun
341 (congrArg DFunLike.coe
342 (primePowerCompletedGroupAlgebraTransitionInClass_comp
343 (ℓ := ℓ) (G := G) C hij hjk)) x
345omit [IsTopologicalGroup G] in
346/--
347The class-restricted prime-power group-algebra index family is directed under componentwise
348order when \(C\) is a formation.
349-/
350theorem directed_primePowerCompletedGroupAlgebraIndexInClass
351 (C : ProCGroups.FiniteGroupClass.{u}) (hForm : ProCGroups.FiniteGroupClass.Formation C) :
352 Directed (· ≤ ·) (id : PrimePowerCompletedGroupAlgebraIndexInClass G C →
353 PrimePowerCompletedGroupAlgebraIndexInClass G C) := by
354 intro i j
355 rcases directed_openNormalSubgroupInClass
356 (C := C) (G := G) hForm i.2 j.2 with
357 ⟨U, hiU, hjU⟩
358 refine ⟨(max i.1 j.1, U), ?_, ?_⟩
359 · exact ⟨le_max_left _ _, hiU⟩
360 · exact ⟨le_max_right _ _, hjU⟩
362omit [Fact (0 < ℓ)] in
363/--
364Every transition in the class-restricted prime-power completed group-algebra system is
365surjective.
366-/
367theorem primePowerCompletedGroupAlgebraTransitionInClass_surjective
368 (C : ProCGroups.FiniteGroupClass.{u})
369 {i j : PrimePowerCompletedGroupAlgebraIndexInClass G C} (hij : i ≤ j) :
370 Function.Surjective
371 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij) := by
372 intro x
373 rcases modNCompletedGroupAlgebraStageCoeffMapInClass_surjective
374 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (G := G) C i.2
375 (primePow_dvd_primePow (ℓ := ℓ) hij.1) x with
376 ⟨y, hy⟩
377 rcases modNCompletedGroupAlgebraTransitionInClass_surjective
378 (n := ℓ ^ j.1) (G := G) C hij.2 y with
379 ⟨z, hz⟩
380 refine ⟨z, ?_⟩
381 rw [primePowerCompletedGroupAlgebraTransitionInClass_eq, RingHom.comp_apply, hz, hy]
383omit [Fact (0 < ℓ)] in
384/-- Compatibility for a class-restricted prime-power completed group algebra family. -/
385def PrimePowerCompletedGroupAlgebraCompatibleInClass
386 (C : ProCGroups.FiniteGroupClass.{u})
387 (x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
388 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) : Prop :=
389 (primePowerCompletedGroupAlgebraSystemInClass ℓ G C).Compatible x
391omit [Fact (0 < ℓ)] in
392/--
393The class-restricted prime-power completed group algebra as an inverse-limit subtype. The
394all-finite PrimePowerCompletedGroupAlgebra below remains the ringed concrete formulation; this
395type is the class-indexed completed object that later Fox layers should target.
396-/
397abbrev PrimePowerCompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
398 {x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
399 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i //
400 PrimePowerCompletedGroupAlgebraCompatibleInClass (ℓ := ℓ) (G := G) C x}
402omit [Fact (0 < ℓ)] in
403/-- The projection from the class-restricted completed group algebra to a prime-power stage. -/
404def primePowerCompletedGroupAlgebraProjectionInClass
405 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
406 PrimePowerCompletedGroupAlgebraInClass ℓ G C →
407 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i :=
408 (primePowerCompletedGroupAlgebraSystemInClass ℓ G C).projection i
410/--
411Every finite-stage projection from the class-restricted prime-power completed group algebra is
412surjective when \(C\) is a formation of finite quotient groups.
413-/
414theorem primePowerCompletedGroupAlgebraProjectionInClass_surjective
415 (C : ProCGroups.FiniteGroupClass.{u})
416 (hForm : ProCGroups.FiniteGroupClass.Formation C)
417 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
418 Function.Surjective
419 (primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i) := by
420 let S := primePowerCompletedGroupAlgebraSystemInClass ℓ G C
421 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C, TopologicalSpace (S.X i) :=
422 fun i => S.topologicalSpace i
423 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C, DiscreteTopology (S.X i) :=
424 fun _ => ⟨rfl⟩
425 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C, CompactSpace (S.X i) :=
426 fun i => by
427 letI : Finite (S.X i) := by
428 dsimp [S, primePowerCompletedGroupAlgebraSystemInClass]
429 exact finite_primePowerCompletedGroupAlgebraStageInClass
430 (ℓ := ℓ) (G := G) C i
431 letI : Fintype (S.X i) := Fintype.ofFinite _
432 infer_instance
433 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C, T2Space (S.X i) :=
434 fun _ => inferInstance
435 change Function.Surjective (S.projection i)
436 exact
437 S.surjective_π
438 (directed_primePowerCompletedGroupAlgebraIndexInClass (G := G) C hForm)
439 (fun {i j} hij =>
440 primePowerCompletedGroupAlgebraTransitionInClass_surjective (ℓ := ℓ) (G := G) C hij)
441 i
443end
445end FoxDifferential