FoxDifferential/Completed/FreeProC/FiniteQuotientStages.lean

1import FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageRightProjection

2import ProCGroups.FiniteGeneration.Basic

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/FoxDifferential/Completed/FreeProC/FiniteQuotientStages.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

11-/

12/-!

13# Finite quotient stages for the completed Crowell approximation route

15This file packages the honest finite quotient stages used by the graph-word density route. Given

16a finite quotient `H/U` and a family `X -> H`, the corresponding finite Fox relation subgroup is

17the kernel of the free-group map `F_X -> H/U`. When the family topologically generates `H`, this

18map is surjective on every discrete quotient, so `H/U` is canonically identified with `F_X / ker`.

19-/

21namespace FoxDifferential

23noncomputable section

25open scoped Topology

26open ProCGroups.ProC

27open ProCGroups.Completion

29universe u v

31section OneStage

33variable {C : ProCGroups.FiniteGroupClass.{u}}

34variable {X H : Type u}

35variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

37/-- The free-group map to a finite quotient of `H` induced by a family `X -> H`. -/

38def freeProCFiniteQuotientStageHom

39 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :

40 FreeGroup X →* CompletedGroupAlgebraQuotientInClass H C U :=

41 FreeGroup.lift fun x : X =>

42 openNormalSubgroupInClassProj (C := C) (G := H) U (φ x)

44@[simp]

45theorem freeProCFiniteQuotientStageHom_of

46 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) (x : X) :

47 freeProCFiniteQuotientStageHom (C := C) φ U (FreeGroup.of x) =

48 (QuotientGroup.mk (φ x) :

49 CompletedGroupAlgebraQuotientInClass H C U) := by

50 simp only [freeProCFiniteQuotientStageHom, openNormalSubgroupInClassProj, QuotientGroup.mk'_apply,

51 FreeGroup.lift_apply_of]

53/-- The free quotient-stage map is the quotient projection after the original free-group map. -/

54theorem freeProCFiniteQuotientStageHom_eq_comp

55 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :

56 freeProCFiniteQuotientStageHom (C := C) φ U =

57 (openNormalSubgroupInClassProj (C := C) (G := H) U).comp (FreeGroup.lift φ) := by

58 ext x

59 unfold freeProCFiniteQuotientStageHom

60 rw [FreeGroup.lift_apply_of]

61 change

62 openNormalSubgroupInClassProj (C := C) (G := H) U (φ x) =

63 openNormalSubgroupInClassProj (C := C) (G := H) U

64 (FreeGroup.lift φ (FreeGroup.of x))

65 rw [FreeGroup.lift_apply_of]

67/-- Compatibility of finite quotient-stage maps under quotient refinement. -/

68theorem freeProCFiniteQuotientStageHom_transition

69 (φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V)

70 (w : FreeGroup X) :

71 (OpenNormalSubgroupInClass.map

72 (C := C) (G := H)

73 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

74 (freeProCFiniteQuotientStageHom (C := C) φ V w) =

75 freeProCFiniteQuotientStageHom (C := C) φ U w := by

76 rw [freeProCFiniteQuotientStageHom_eq_comp,

77 freeProCFiniteQuotientStageHom_eq_comp]

78 exact congrFun

79 (openNormalSubgroupInClassProj_compatible (C := C) (G := H) U V hUV)

80 (FreeGroup.lift φ w)

82/-- The finite-stage relation subgroup `ker(F_X -> H/U)`. -/

83def freeProCFiniteQuotientStageKernel

84 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :

85 Subgroup (FreeGroup X) :=

86 (freeProCFiniteQuotientStageHom (C := C) φ U).ker

88instance freeProCFiniteQuotientStageKernel_normal

89 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :

90 (freeProCFiniteQuotientStageKernel (C := C) φ U).Normal := by

91 dsimp [freeProCFiniteQuotientStageKernel]

92 infer_instance

94/-- The finite-stage relation kernels are antitone with respect to quotient refinement. -/

95theorem freeProCFiniteQuotientStageKernel_antitone

96 (φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V) :

97 freeProCFiniteQuotientStageKernel (C := C) φ V ≤

98 freeProCFiniteQuotientStageKernel (C := C) φ U := by

99 intro w hw

100 change freeProCFiniteQuotientStageHom (C := C) φ U w = 1

101 calc

102 freeProCFiniteQuotientStageHom (C := C) φ U w

103 =

104 (OpenNormalSubgroupInClass.map

105 (C := C) (G := H)

106 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

107 (freeProCFiniteQuotientStageHom (C := C) φ V w) :=

108 (freeProCFiniteQuotientStageHom_transition (C := C) φ hUV w).symm

109 _ = 1 := by

110 rw [show freeProCFiniteQuotientStageHom (C := C) φ V w = 1 from hw]

111 exact map_one _

112

113/-- If the original family topologically generates `H`, then its image generates every discrete

114finite quotient `H/U`, so the corresponding free-group map is surjective. -/

115theorem freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates

116 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)

117 [DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C U)]

118 (hφgen :

119 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :

120 Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U) := by

121 let π : H →ₜ* CompletedGroupAlgebraQuotientInClass H C U :=

122 { toMonoidHom := openNormalSubgroupInClassProj (C := C) (G := H) U

123 continuous_toFun := by

124 change Continuous

125 (QuotientGroup.mk'

126 (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H))

127 exact continuous_quotient_mk' }

128 have hπsurj : Function.Surjective π :=

129 openNormalSubgroupInClassProj_surjective (C := C) (G := H) U

130 have hgen :

131 ProCGroups.Generation.TopologicallyGenerates

132 (G := CompletedGroupAlgebraQuotientInClass H C U)

133 (Set.range (π ∘ φ)) :=

134 ProCGroups.FiniteGeneration.topologicallyGenerates_range_comp_of_surjective

135 (G := H) (H := CompletedGroupAlgebraQuotientInClass H C U)

136 π hπsurj φ hφgen

137 simpa [π, freeProCFiniteQuotientStageHom, Function.comp] using

138 ProCGroups.FiniteGeneration.freeGroup_lift_surjective_of_topologicallyGenerates_discrete

139 (G := CompletedGroupAlgebraQuotientInClass H C U)

140 (g := fun x : X => π (φ x)) hgen

141

142/-- The canonical identification `F_X / ker(F_X -> H/U) ≃ H/U`. -/

143def freeProCFiniteQuotientStageTargetEquiv

144 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)

145 (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)) :

146 finiteFoxStageTargetQuotient

147 (X := X) (freeProCFiniteQuotientStageKernel (C := C) φ U) ≃*

148 CompletedGroupAlgebraQuotientInClass H C U :=

149 QuotientGroup.quotientKerEquivOfSurjective

150 (freeProCFiniteQuotientStageHom (C := C) φ U) hsurj

151

152@[simp]

153theorem freeProCFiniteQuotientStageTargetEquiv_mk

154 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)

155 (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))

156 (w : FreeGroup X) :

157 freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj

158 (QuotientGroup.mk'

159 (freeProCFiniteQuotientStageKernel (C := C) φ U) w) =

160 freeProCFiniteQuotientStageHom (C := C) φ U w := by

161 rfl

162

163/-- The map `H/U -> F_X / ker(F_X -> H/U)` used as `qmap` in the bifiltered stage API. -/

164def freeProCFiniteQuotientStageQMap

165 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)

166 (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)) :

167 CompletedGroupAlgebraQuotientInClass H C U →*

168 finiteFoxStageTargetQuotient

169 (X := X) (freeProCFiniteQuotientStageKernel (C := C) φ U) :=

170 (freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj).symm.toMonoidHom

171

172theorem freeProCFiniteQuotientStageQMap_injective

173 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)

174 (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)) :

175 Function.Injective (freeProCFiniteQuotientStageQMap (C := C) φ U hsurj) :=

176 (freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj).symm.injective

177

178@[simp]

179theorem freeProCFiniteQuotientStageQMap_generator

180 (φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)

181 (hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))

182 (x : X) :

183 freeProCFiniteQuotientStageQMap (C := C) φ U hsurj

184 (QuotientGroup.mk (φ x)) =

185 QuotientGroup.mk'

186 (freeProCFiniteQuotientStageKernel (C := C) φ U) (FreeGroup.of x) := by

187 apply (freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj).injective

188 rw [freeProCFiniteQuotientStageTargetEquiv_mk]

189 simp only [freeProCFiniteQuotientStageQMap, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe,

190 MulEquiv.apply_symm_apply, freeProCFiniteQuotientStageHom_of]

191

192/-- Compatibility between the canonical `F_X/ker -> H/U` equivalences and quotient refinement. -/

193theorem freeProCFiniteQuotientStageTargetEquiv_transition

194 (φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V)

195 (hsurjU : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))

196 (hsurjV : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ V))

197 (y : finiteFoxStageTargetQuotient

198 (X := X) (freeProCFiniteQuotientStageKernel (C := C) φ V)) :

199 freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurjU

200 (finiteFoxStageTargetQuotientMap

201 (X := X) (freeProCFiniteQuotientStageKernel_antitone (C := C) φ hUV) y) =

202 (OpenNormalSubgroupInClass.map

203 (C := C) (G := H)

204 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

205 (freeProCFiniteQuotientStageTargetEquiv (C := C) φ V hsurjV y) := by

206 rcases QuotientGroup.mk'_surjective

207 (freeProCFiniteQuotientStageKernel (C := C) φ V) y with ⟨w, rfl⟩

208 rw [finiteFoxStageTargetQuotientMap_mk,

209 freeProCFiniteQuotientStageTargetEquiv_mk,

210 freeProCFiniteQuotientStageTargetEquiv_mk,

211 freeProCFiniteQuotientStageHom_transition]

212

213/-- The canonical `qmap`s commute with quotient refinement. -/

214theorem freeProCFiniteQuotientStageQMap_transition

215 (φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V)

216 (hsurjU : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))

217 (hsurjV : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ V))

218 (q : CompletedGroupAlgebraQuotientInClass H C V) :

219 freeProCFiniteQuotientStageQMap (C := C) φ U hsurjU

220 ((OpenNormalSubgroupInClass.map

221 (C := C) (G := H)

222 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) =

223 finiteFoxStageTargetQuotientMap

224 (X := X) (freeProCFiniteQuotientStageKernel_antitone (C := C) φ hUV)

225 (freeProCFiniteQuotientStageQMap (C := C) φ V hsurjV q) := by

226 apply (freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurjU).injective

227 rw [freeProCFiniteQuotientStageTargetEquiv_transition

228 (C := C) φ hUV hsurjU hsurjV]

229 simp only [freeProCFiniteQuotientStageQMap, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe,

230 MulEquiv.apply_symm_apply]

231

232end OneStage

233

234section StageFamily

235

236variable {C : ProCGroups.FiniteGroupClass.{u}}

237variable {X H : Type u}

238variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

239variable {J : Type v}

240

241/-- The finite relation subgroup family attached to a family of `Z_C[[H]]` stage indices. -/

242def freeProCFiniteQuotientStageKernelFamily

243 (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H) :

244 J → Subgroup (FreeGroup X) :=

245 fun j => freeProCFiniteQuotientStageKernel (C := C) φ (zcIndex j).2

246

247instance freeProCFiniteQuotientStageKernelFamily_normal

248 (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H) (j : J) :

249 (freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j).Normal := by

250 dsimp [freeProCFiniteQuotientStageKernelFamily]

251 infer_instance

252

253/-- The finite relation subgroup family is antitone under refinement of the `Z_C[[H]]` stages. -/

254theorem freeProCFiniteQuotientStageKernelFamily_antitone

255 (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)

256 [Preorder J]

257 (hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j) :

258 ∀ {i j : J}, i ≤ j →

259 freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j ≤

260 freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex i := by

261 intro i j hij

262 exact freeProCFiniteQuotientStageKernel_antitone (C := C) φ (hzcIndex hij).2

263

264/-- The canonical `H/U_j -> F/N_j` comparison maps for a finite quotient stage family. -/

265def freeProCFiniteQuotientStageQMapFamily

266 (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)

267 [∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]

268 (hφgen :

269 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :

270 ∀ j : J,

271 CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2 →*

272 finiteFoxStageTargetQuotient

273 (X := X) (freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j) :=

274 fun j =>

275 freeProCFiniteQuotientStageQMap (C := C) φ (zcIndex j).2

276 (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates

277 (C := C) φ (zcIndex j).2 hφgen)

278

279theorem freeProCFiniteQuotientStageQMapFamily_injective

280 (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)

281 [∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]

282 (hφgen :

283 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :

284 ∀ j : J,

285 Function.Injective

286 (freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen j) := by

287 intro j

288 exact freeProCFiniteQuotientStageQMap_injective (C := C) φ (zcIndex j).2

289 (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates

290 (C := C) φ (zcIndex j).2 hφgen)

291

292@[simp]

293theorem freeProCFiniteQuotientStageQMapFamily_generator

294 (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)

295 [∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]

296 (hφgen :

297 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))

298 (j : J) (x : X) :

299 freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen j

300 (QuotientGroup.mk (φ x)) =

301 QuotientGroup.mk'

302 (freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j)

303 (FreeGroup.of x) := by

304 exact freeProCFiniteQuotientStageQMap_generator (C := C) φ (zcIndex j).2

305 (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates

306 (C := C) φ (zcIndex j).2 hφgen) x

307

308/-- The canonical comparison maps commute with refinement of the `Z_C[[H]]` stage family. -/

309theorem freeProCFiniteQuotientStageQMapFamily_transition

310 (φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)

311 [Preorder J]

312 (hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j)

313 [∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]

314 (hφgen :

315 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :

316 ∀ {i j : J} (hij : i ≤ j),

317 ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,

318 freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen i

319 ((OpenNormalSubgroupInClass.map

320 (C := C) (G := H)

321 (U := OrderDual.ofDual (zcIndex i).2)

322 (V := OrderDual.ofDual (zcIndex j).2)

323 (hzcIndex hij).2) q) =

324 finiteFoxStageTargetQuotientMap

325 (X := X)

326 (freeProCFiniteQuotientStageKernelFamily_antitone

327 (C := C) φ zcIndex hzcIndex hij)

328 (freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen j q) := by

329 intro i j hij q

330 exact freeProCFiniteQuotientStageQMap_transition (C := C) φ (hzcIndex hij).2

331 (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates

332 (C := C) φ (zcIndex i).2 hφgen)

333 (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates

334 (C := C) φ (zcIndex j).2 hφgen)

335 q

336

337end StageFamily

338

339section BifilteredFiniteQuotientStages

340

341variable {ProC : ProCGroups.ProC.ProCGroupPredicate}

342variable {X H : Type u}

343variable [DecidableEq X]

344variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

345variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]

346variable [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]

347variable {J : Type v} [Preorder J]

348

349/-- The completed-to-finite coefficient map for the actual finite quotient stages

350`F_X -> H/U_j`. -/

351def freeProCZCBifilteredFiniteQuotientStageCoeffMap

352 (φ : X → H) (nstage : J → ℕ) [∀ j, Fact (0 < nstage j)]

353 (zcIndex : J → ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H)

354 (hmod : ∀ j : J, nstage j ∣ (zcIndex j).1.modulus)

355 [∀ j, DiscreteTopology

356 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2)]

357 (hφgen :

358 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))

359 (j : J) :

360 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+*

361 finiteFoxStageTargetGroupAlgebra

362 (X := X)

363 (freeProCFiniteQuotientStageKernelFamily

364 (C := ProC.finiteQuotientClass) φ zcIndex j)

365 (nstage j) :=

366 zcCompletedGroupAlgebraBifilteredStageCoeffMap

367 (ProC := ProC) (X := X) (H := H)

368 (freeProCFiniteQuotientStageKernelFamily

369 (C := ProC.finiteQuotientClass) φ zcIndex)

370 nstage zcIndex hmod

371 (freeProCFiniteQuotientStageQMapFamily

372 (C := ProC.finiteQuotientClass) φ zcIndex hφgen) j

373

374/-- The completed-to-finite coefficient map for the standard all-stage family

375`j : ZCCompletedGroupAlgebraIndex C H`, with finite relation subgroup

376`ker(F_X -> H/U_j)` and coefficient modulus `j.1.modulus`. -/

377def freeProCZCBifilteredAllFiniteQuotientStageCoeffMap

378 (φ : X → H)

379 (hφgen :

380 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))

381 (j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) :

382 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+*

383 finiteFoxStageTargetGroupAlgebra

384 (X := X)

385 (freeProCFiniteQuotientStageKernelFamily

386 (C := ProC.finiteQuotientClass) φ

387 (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →

388 ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) j)

389 j.1.modulus := by

390 letI :

391 ∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,

392 Fact (0 < j.1.modulus) :=

393 fun j => ProCIntegerIndex.positiveFact j.1

394 letI :

395 ∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,

396 DiscreteTopology

397 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2) :=

398 fun j =>

399 QuotientGroup.discreteTopology

400 (ProCGroups.openNormalSubgroup_isOpen (G := H)

401 ((OrderDual.ofDual j.2).1 : OpenNormalSubgroup H))

402 exact

403 freeProCZCBifilteredFiniteQuotientStageCoeffMap

404 (ProC := ProC) (X := X) (H := H) φ (fun j => j.1.modulus)

405 (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →

406 ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H)

407 (fun _ => dvd_rfl) hφgen j

408

409end BifilteredFiniteQuotientStages

410

411section FullStageQuotientBasis

412

413variable {C : ProCGroups.FiniteGroupClass.{u}}

414variable {H : Type u}

415variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

416

417omit [IsTopologicalGroup H] in

418/-- The full family of quotient maps `H -> H/U` indexed by

419`ZCCompletedGroupAlgebraIndex C H` has identity-neighbourhood kernels for any pro-`C` group `H`.

420

421The coefficient coordinate of the index is irrelevant here; it is filled with the terminal

422coefficient quotient. -/

423theorem zcCompletedGroupAlgebraAllStageQuotientMap_identity_basis_of_isProCGroup

424 [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]

425 (hH : IsProCGroup C H) :

426 HasIdentityQuotientKernelNeighbourhoodBasis

427 (Y := H)

428 (fun j : ZCCompletedGroupAlgebraIndex C H =>

429 openNormalSubgroupInClassProj (C := C) (G := H) j.2) := by

430 intro U hU hUone

431 rcases hH.hasOpenNormalBasisInClass U hU hUone with ⟨V, hVU, hCV⟩

432 let Vc : OpenNormalSubgroupInClass C H := ⟨V, hCV⟩

433 refine ⟨(ProCIntegerIndex.terminal (C := C) inferInstance, OrderDual.toDual Vc), ?_⟩

434 intro z hz

435 apply hVU

436 exact

437 (QuotientGroup.eq_one_iff

438 (N := ((V : OpenNormalSubgroup H) : Subgroup H)) z).1 hz

439

440end FullStageQuotientBasis

441

442end

443

444end FoxDifferential