Source: ProCGroups.FoxDifferential.Completed.FreeProC.Density
1import ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift
3/-!
4# Fox differential: completed — free pro-\(C\) — density
6The principal declarations in this module are:
8- `HasLeftOpenSubgroupNeighbourhoodBasis`
9 Left open subgroup neighborhood basis, expressed as a proposition rather than a structure. For
10 every neighborhood \(U\) of \(y\), one can find an open subgroup \(V\) such that the left coset
11 \(yV\) is contained in \(U\). This is the topological input used to pass from finite or
12 open-subgroup approximations to ordinary closure.
13- `HasLeftOpenNormalSubgroupNeighbourhoodBasis`
14 This is the normal-subgroup version of the left open-subgroup neighborhood basis: in a profinite
15 group, every identity neighborhood can be refined by an open normal subgroup.
16- `subset_closure_of_open_neighbourhood_approximation`
17 A point belongs to the set-theoretic closure of \(S\) when every open neighborhood of it contains
18 an algebraic point of \(S\).
19- `HasLeftOpenNormalSubgroupNeighbourhoodBasis.to_subgroup_basis`
20 The normal-subgroup basis implies the subgroup basis.
21-/
23namespace FoxDifferential
25noncomputable section
27universe u v
29section GenericClosureAPI
31variable {Y : Type u} [TopologicalSpace Y]
32variable {S T : Set Y}
34/--
35A point belongs to the set-theoretic closure of \(S\) when every open neighborhood of it
36contains an algebraic point of \(S\).
37-/
38theorem subset_closure_of_open_neighbourhood_approximation
39 (happrox :
40 ∀ y : Y, y ∈ T → ∀ U : Set Y, IsOpen U → y ∈ U →
41 ∃ s : Y, s ∈ S ∧ s ∈ U) :
42 T ⊆ closure S := by
43 intro y hy
44 rw [mem_closure_iff]
45 intro U hU hyU
46 rcases happrox y hy U hU hyU with ⟨s, hsS, hsU⟩
47 exact ⟨s, hsU, hsS⟩
49end GenericClosureAPI
51section OpenSubgroupClosureAPI
53variable {Y : Type u} [Group Y] [TopologicalSpace Y]
54variable {S T : Set Y}
56/--
57Left open subgroup neighborhood basis, expressed as a proposition rather than a structure. For
58every neighborhood \(U\) of \(y\), one can find an open subgroup \(V\) such that the left coset
59\(yV\) is contained in \(U\). This is the topological input used to pass from finite or
60open-subgroup approximations to ordinary closure.
61-/
62def HasLeftOpenSubgroupNeighbourhoodBasis (Y : Type u) [Group Y] [TopologicalSpace Y] : Prop :=
63 ∀ (y : Y) (U : Set Y), IsOpen U → y ∈ U →
64 ∃ V : Subgroup Y, IsOpen ((V : Subgroup Y) : Set Y) ∧
65 ∀ z : Y, z ∈ V → y * z ∈ U
67/--
68This is the normal-subgroup version of the left open-subgroup neighborhood basis: in a profinite
69group, every identity neighborhood can be refined by an open normal subgroup.
70-/
71def HasLeftOpenNormalSubgroupNeighbourhoodBasis
72 (Y : Type u) [Group Y] [TopologicalSpace Y] : Prop :=
73 ∀ (y : Y) (U : Set Y), IsOpen U → y ∈ U →
74 ∃ V : Subgroup Y, V.Normal ∧ IsOpen ((V : Subgroup Y) : Set Y) ∧
75 ∀ z : Y, z ∈ V → y * z ∈ U
77/-- The normal-subgroup basis implies the subgroup basis. -/
78theorem HasLeftOpenNormalSubgroupNeighbourhoodBasis.to_subgroup_basis
79 (hbasis : HasLeftOpenNormalSubgroupNeighbourhoodBasis Y) :
80 HasLeftOpenSubgroupNeighbourhoodBasis Y := by
81 intro y U hU hyU
82 rcases hbasis y U hU hyU with ⟨V, _hVnormal, hVopen, hVcoset⟩
83 exact ⟨V, hVopen, hVcoset⟩
85/--
86If for every \(y \in T\) and every open subgroup \(V\) there is \(s \in S\) with \(y^{-1}s \in
87V\), then \(T\) is contained in the closure of \(S\).
88-/
89theorem subset_closure_of_openSubgroup_approximation
90 (hbasis : HasLeftOpenSubgroupNeighbourhoodBasis Y)
91 (happrox :
92 ∀ y : Y, y ∈ T → ∀ V : Subgroup Y,
93 IsOpen ((V : Subgroup Y) : Set Y) →
94 ∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
95 T ⊆ closure S := by
96 refine subset_closure_of_open_neighbourhood_approximation ?_
97 intro y hy U hU hyU
98 rcases hbasis y U hU hyU with ⟨V, hVopen, hVcoset⟩
99 rcases happrox y hy V hVopen with ⟨s, hsS, hsV⟩
100 refine ⟨s, hsS, ?_⟩
101 have hcoset : y * (y⁻¹ * s) ∈ U := hVcoset (y⁻¹ * s) hsV
102 simpa [mul_assoc] using hcoset
104/--
105The completed Fox graph or boundary-cycle set lies in the required closed generated submodule by
106finite-stage separation.
107-/
108theorem subset_closure_of_openNormalSubgroup_approximation
109 (hbasis : HasLeftOpenNormalSubgroupNeighbourhoodBasis Y)
110 (happrox :
111 ∀ y : Y, y ∈ T → ∀ V : Subgroup Y,
112 V.Normal → IsOpen ((V : Subgroup Y) : Set Y) →
113 ∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
114 T ⊆ closure S := by
115 refine subset_closure_of_open_neighbourhood_approximation ?_
116 intro y hy U hU hyU
117 rcases hbasis y U hU hyU with ⟨V, hVnormal, hVopen, hVcoset⟩
118 rcases happrox y hy V hVnormal hVopen with ⟨s, hsS, hsV⟩
119 refine ⟨s, hsS, ?_⟩
120 have hcoset : y * (y⁻¹ * s) ∈ U := hVcoset (y⁻¹ * s) hsV
121 simpa [mul_assoc] using hcoset
123/-- Coset approximation gives a pointwise closure statement. -/
124theorem mem_closure_of_openSubgroup_approximation
125 (hbasis : HasLeftOpenSubgroupNeighbourhoodBasis Y)
126 {y : Y}
127 (happrox :
128 ∀ V : Subgroup Y, IsOpen ((V : Subgroup Y) : Set Y) →
129 ∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
130 y ∈ closure S := by
131 rw [mem_closure_iff]
132 intro U hU hyU
133 rcases hbasis y U hU hyU with ⟨V, hVopen, hVcoset⟩
134 rcases happrox V hVopen with ⟨s, hsS, hsV⟩
135 refine ⟨s, ?_, hsS⟩
136 have hcoset : y * (y⁻¹ * s) ∈ U := hVcoset (y⁻¹ * s) hsV
137 simpa [mul_assoc] using hcoset
139end OpenSubgroupClosureAPI
141section QuotientKernelClosureAPI
143variable {Y : Type u} [Group Y] [TopologicalSpace Y]
144variable {S T : Set Y}
146/--
147A left neighborhood basis expressed directly by kernels of quotient maps. This is the form
148produced by finite-stage maps: every open neighborhood of \(y\) contains a left coset
149\(y\ker(\pi_j)\).
150-/
151def HasLeftQuotientKernelNeighbourhoodBasis
152 {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
153 (π : ∀ j : J, Y →* Q j) : Prop :=
154 ∀ (y : Y) (U : Set Y), IsOpen U → y ∈ U →
155 ∃ j : J, ∀ z : Y, z ∈ (π j).ker → y * z ∈ U
157/--
158If quotient kernels form a left neighborhood basis, then equality at every quotient stage gives
159closure. This is the abstract topology step for the remaining Crowell density theorem: finite
160quotient exactness supplies \(s\in S\) with \(\pi_j s = \pi_j y\); the quotient-kernel basis
161turns this into ordinary topological approximation.
162-/
163theorem subset_closure_of_quotientKernel_approximation
164 {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
165 (π : ∀ j : J, Y →* Q j)
166 (hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
167 (happrox :
168 ∀ y : Y, y ∈ T → ∀ j : J,
169 ∃ s : Y, s ∈ S ∧ π j s = π j y) :
170 T ⊆ closure S := by
171 refine subset_closure_of_open_neighbourhood_approximation ?_
172 intro y hy U hU hyU
173 rcases hbasis y U hU hyU with ⟨j, hj⟩
174 rcases happrox y hy j with ⟨s, hsS, hπ⟩
175 have hker : y⁻¹ * s ∈ (π j).ker := by
176 change π j (y⁻¹ * s) = 1
177 rw [map_mul, map_inv, hπ]
178 simp only [inv_mul_cancel]
179 refine ⟨s, hsS, ?_⟩
180 have hsU : y * (y⁻¹ * s) ∈ U := hj (y⁻¹ * s) hker
181 simpa [mul_assoc] using hsU
183end QuotientKernelClosureAPI
185section CompletedFoxDensity
187open scoped Topology
189variable {C : ProCGroups.FiniteGroupClass}
190variable {X H : Type u}
191variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
192variable [DecidableEq X]
193variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
194variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
196/--
197The semidirect point \((D w, 1)\) attached to an abstract free-group kernel-word candidate. The
198word may or may not actually lie in the kernel; kernel membership is recorded separately by the
199corresponding kernel-cycle-set lemma.
200-/
201def freeProCZCCompletedFoxSemidirectKernelWordPoint (φ : X → H) (w : FreeGroup X) :
202 ZCCompletedFoxSemidirect C X H :=
203 { left :=
204 zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w,
205 right := (1 : H) }
207omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
208 (ZCCompletedFoxSemidirect C X H)] in
209/--
210The left coordinate of a completed Fox semidirect kernel-word point is its completed Fox
211derivative vector.
212-/
213@[simp]
214theorem freeProCZCCompletedFoxSemidirectKernelWordPoint_left
215 (φ : X → H) (w : FreeGroup X) :
216 (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w).left =
217 zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w :=
218 rfl
220omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
221 (ZCCompletedFoxSemidirect C X H)] in
222/-- The right coordinate of a completed Fox semidirect kernel-word point is the identity element. -/
223@[simp]
224theorem freeProCZCCompletedFoxSemidirectKernelWordPoint_right
225 (φ : X → H) (w : FreeGroup X) :
226 (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w).right = 1 :=
227 rfl
229omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
230 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
231/-- A genuine kernel word gives an element of the algebraic kernel-word cycle set. -/
232theorem freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
233 (φ : X → H) {w : FreeGroup X} (hw : FreeGroup.lift φ w = 1) :
234 freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w ∈
235 freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ := by
236 exact ⟨w, hw, rfl⟩
238omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
239 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
240/--
241Membership in the completed Fox semidirect kernel-cycle set is equivalent to vanishing of the
242corresponding finite-stage coordinate.
243-/
244theorem mem_freeProCZCCompletedFoxSemidirectKernelCycleSet_iff
245 {φ : X → H}
246 {y : ZCCompletedFoxSemidirect C X H} :
247 y ∈ freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ ↔
248 ∃ w : FreeGroup X, FreeGroup.lift φ w = 1 ∧
249 y = freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w := by
250 constructor
251 · intro hy
252 rcases hy with ⟨w, hw, hy⟩
253 exact ⟨w, hw, hy⟩
254 · rintro ⟨w, hw, hy⟩
255 rw [hy]
256 exact freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
257 (C := C) φ hw
259omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
260 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
261omit [DecidableEq X] in
262/-- Boundary-cycle membership for a point of the form \((v,1)\). -/
263theorem freeProCZCCompletedFoxSemidirectBoundaryCycleSet_mk_iff
264 [Fintype X] {φ : X → H}
265 {v : ZCFreeFoxCoordinates C (X := X) (H := H)} :
266 ({ left := v, right := (1 : H) } :
267 ZCCompletedFoxSemidirect C X H) ∈
268 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ↔
269 zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v = 0 := by
270 constructor
271 · intro h
272 exact h.2
273 · intro h
274 exact ⟨rfl, h⟩
276omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
277/--
278Quotient-kernel approximation form of the completed Fox density statement. This is the
279finite-stage attack surface for the remaining density theorem: once finite quotient exactness
280produces, for every finite quotient stage j, a kernel word whose semidirect point has the same
281j-th quotient image as the boundary cycle, the completed density statement follows.
282-/
283theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_quotKernel_approx
284 [Fintype X] (φ : X → H)
285 {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
286 (π : ∀ j : J,
287 ZCCompletedFoxSemidirect C X H →* Q j)
288 (hbasis :
289 HasLeftQuotientKernelNeighbourhoodBasis
290 (Y := ZCCompletedFoxSemidirect C X H) π)
291 (happrox :
292 ∀ y : ZCCompletedFoxSemidirect C X H,
293 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
294 ∀ j : J,
295 ∃ w : FreeGroup X,
296 FreeGroup.lift φ w = 1 ∧
297 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint
298 (C := C) φ w) = π j y) :
299 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
300 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) := by
301 refine subset_closure_of_quotientKernel_approximation
302 (Y := ZCCompletedFoxSemidirect C X H)
303 (S := freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)
304 (T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ)
305 π hbasis ?_
306 intro y hy j
307 rcases happrox y hy j with ⟨w, hw, hπ⟩
308 exact
309 ⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w,
310 freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
311 (C := C) φ hw,
312 hπ⟩
314omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
315/--
316For every boundary cycle and every open neighborhood in the completed semidirect product, there
317is a genuine kernel word whose point \((D w, 1)\) lies in that neighborhood; this is the density
318statement used by Crowell middle exactness.
319-/
320theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_open_neighbourhood_approx
321 [Fintype X] (φ : X → H)
322 (happrox :
323 ∀ y : ZCCompletedFoxSemidirect C X H,
324 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
325 ∀ U : Set (ZCCompletedFoxSemidirect C X H),
326 IsOpen U → y ∈ U →
327 ∃ w : FreeGroup X,
328 FreeGroup.lift φ w = 1 ∧
329 freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w ∈ U) :
330 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
331 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) := by
332 refine subset_closure_of_open_neighbourhood_approximation ?_
333 intro y hy U hU hyU
334 rcases happrox y hy U hU hyU with ⟨w, hw, hUmem⟩
335 refine ⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w, ?_, hUmem⟩
336 exact freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
337 (C := C) φ hw
339omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
340/--
341For every open subgroup \(V\) of the completed Fox semidirect group, a boundary cycle \(y\) is
342approximated by a kernel-word cycle point modulo the left coset \(yV\).
343-/
344theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openSubgroup_approx
345 [Fintype X] (φ : X → H)
346 (hbasis :
347 HasLeftOpenSubgroupNeighbourhoodBasis
348 (ZCCompletedFoxSemidirect C X H))
349 (happrox :
350 ∀ y : ZCCompletedFoxSemidirect C X H,
351 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
352 ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
353 IsOpen ((V : Subgroup
354 (ZCCompletedFoxSemidirect C X H)) : Set
355 (ZCCompletedFoxSemidirect C X H)) →
356 ∃ w : FreeGroup X,
357 FreeGroup.lift φ w = 1 ∧
358 y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
359 (C := C) φ w ∈ V) :
360 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
361 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) := by
362 refine subset_closure_of_openSubgroup_approximation
363 (Y := ZCCompletedFoxSemidirect C X H)
364 (S := freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)
365 (T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ)
366 hbasis ?_
367 intro y hy V hVopen
368 rcases happrox y hy V hVopen with ⟨w, hw, hVmem⟩
369 exact
370 ⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w,
371 freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
372 (C := C) φ hw,
373 hVmem⟩
375omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
376/-- Open-normal-subgroup approximation form of the completed Fox density statement. -/
377theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openNormalSubgroup_approx
378 [Fintype X] (φ : X → H)
379 (hbasis :
380 HasLeftOpenNormalSubgroupNeighbourhoodBasis
381 (ZCCompletedFoxSemidirect C X H))
382 (happrox :
383 ∀ y : ZCCompletedFoxSemidirect C X H,
384 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
385 ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
386 V.Normal →
387 IsOpen ((V : Subgroup
388 (ZCCompletedFoxSemidirect C X H)) : Set
389 (ZCCompletedFoxSemidirect C X H)) →
390 ∃ w : FreeGroup X,
391 FreeGroup.lift φ w = 1 ∧
392 y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
393 (C := C) φ w ∈ V) :
394 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
395 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) := by
396 refine subset_closure_of_openNormalSubgroup_approximation
397 (Y := ZCCompletedFoxSemidirect C X H)
398 (S := freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)
399 (T := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ)
400 hbasis ?_
401 intro y hy V hVnormal hVopen
402 rcases happrox y hy V hVnormal hVopen with ⟨w, hw, hVmem⟩
403 exact
404 ⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w,
405 freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
406 (C := C) φ hw,
407 hVmem⟩
409/--
410Open-subgroup approximation places every completed boundary cycle inside the closed generated
411Fox graph target.
412-/
413theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_openSubgroup_approx
414 [Fintype X] (φ : X → H)
415 (hbasis :
416 HasLeftOpenSubgroupNeighbourhoodBasis
417 (ZCCompletedFoxSemidirect C X H))
418 (happrox :
419 ∀ y : ZCCompletedFoxSemidirect C X H,
420 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
421 ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
422 IsOpen ((V : Subgroup
423 (ZCCompletedFoxSemidirect C X H)) : Set
424 (ZCCompletedFoxSemidirect C X H)) →
425 ∃ w : FreeGroup X,
426 FreeGroup.lift φ w = 1 ∧
427 y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
428 (C := C) φ w ∈ V) :
429 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
430 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
431 (ZCCompletedFoxSemidirect C X H)) : Set
432 (ZCCompletedFoxSemidirect C X H)) := by
433 exact
434 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density (C := C) φ
435 (freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openSubgroup_approx
436 (C := C) φ hbasis happrox)
438/--
439Open-normal-subgroup approximation places every completed boundary cycle inside the closed
440generated Fox graph target.
441-/
442theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_openNormalSubgroup_approx
443 [Fintype X] (φ : X → H)
444 (hbasis :
445 HasLeftOpenNormalSubgroupNeighbourhoodBasis
446 (ZCCompletedFoxSemidirect C X H))
447 (happrox :
448 ∀ y : ZCCompletedFoxSemidirect C X H,
449 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
450 ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
451 V.Normal →
452 IsOpen ((V : Subgroup
453 (ZCCompletedFoxSemidirect C X H)) : Set
454 (ZCCompletedFoxSemidirect C X H)) →
455 ∃ w : FreeGroup X,
456 FreeGroup.lift φ w = 1 ∧
457 y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
458 (C := C) φ w ∈ V) :
459 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
460 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
461 (ZCCompletedFoxSemidirect C X H)) : Set
462 (ZCCompletedFoxSemidirect C X H)) := by
463 exact
464 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density (C := C) φ
465 (freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openNormalSubgroup_approx
466 (C := C) φ hbasis happrox)
468omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
469/--
470Under the standard continuity inputs, open-subgroup approximation upgrades the one-sided closure
471statement to the equality between boundary cycles and the closure of kernel-word cycles.
472-/
473theorem closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_of_openSubgroup_approx
474 [Fintype X] [T1Space H]
475 [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
476 [T1Space (ZCCompletedGroupAlgebra C H)]
477 (φ : X → H)
478 (hleft :
479 Continuous
480 (fun y : ZCCompletedFoxSemidirect C X H => y.left))
481 (hright :
482 Continuous
483 (fun y : ZCCompletedFoxSemidirect C X H => y.right))
484 (hboundary :
485 Continuous
486 (zcFreeGroupFoxBoundary C (FreeGroup.lift φ)))
487 (hbasis :
488 HasLeftOpenSubgroupNeighbourhoodBasis
489 (ZCCompletedFoxSemidirect C X H))
490 (happrox :
491 ∀ y : ZCCompletedFoxSemidirect C X H,
492 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
493 ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
494 IsOpen ((V : Subgroup
495 (ZCCompletedFoxSemidirect C X H)) : Set
496 (ZCCompletedFoxSemidirect C X H)) →
497 ∃ w : FreeGroup X,
498 FreeGroup.lift φ w = 1 ∧
499 y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
500 (C := C) φ w ∈ V) :
501 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) =
502 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ := by
503 exact
504 (closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_iff_density (C := C) (φ := φ)
505 hleft hright hboundary).2
506 (freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openSubgroup_approx
507 (C := C) φ hbasis happrox)
509end CompletedFoxDensity
511end
513end FoxDifferential