Yamaguchi Lean 4 Library
FoxDifferential/Completed/FreeProC/Density.lean
FoxDifferential/Completed/FreeProC/Density/Source

FoxDifferential/Completed/FreeProC/Density.lean

1import FoxDifferential.Completed.FreeProC.SemidirectLift
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FreeProC/Density.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Density criteria for the free pro-C completed Fox graph
14This file turns the remaining completion step into reusable topology and finite-stage APIs.
15The main target is the statement that every completed Fox boundary cycle `(v, 1)` is a limit of
16algebraic kernel-word cycles `(D w, 1)`.
18The declarations below do not assert that density is automatic. They reduce it to concrete
19neighbourhood or open-subgroup approximation statements, which are the forms produced by finite
20quotient arguments.
21-/
23namespace FoxDifferential
25noncomputable section
27universe u v
29section GenericClosureAPI
31variable {Y : Type u} [TopologicalSpace Y]
32variable {S T : Set Y}
34/-- A direct neighbourhood approximation criterion for set-theoretic closure.
36This is the form used when a finite-stage argument has already produced an algebraic point of
37`S` inside every open neighbourhood of a boundary point. -/
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/-- Left open subgroup neighbourhood basis, stated as a proposition rather than a structure.
58For every neighbourhood `U` of `y`, one can find an open subgroup `V` such that the left coset
59`y V` is contained in `U`. This is the exact topological input needed to pass from finite/open
60subgroup approximations to ordinary closure. -/
61def HasLeftOpenSubgroupNeighbourhoodBasis (Y : Type u) [Group Y] [TopologicalSpace Y] : Prop :=
62 ∀ (y : Y) (U : Set Y), IsOpen U → y ∈ U →
63 ∃ V : Subgroup Y, IsOpen ((V : Subgroup Y) : Set Y) ∧
64 ∀ z : Y, z ∈ V → y * z ∈ U
66/-- A normal-subgroup version of the left open subgroup neighbourhood basis.
68This is the form naturally supplied by profinite finite-quotient separation, where neighbourhoods
69of the identity are refined by open normal subgroups. -/
71 (Y : Type u) [Group Y] [TopologicalSpace Y] : Prop :=
72 ∀ (y : Y) (U : Set Y), IsOpen U → y ∈ U →
73 ∃ V : Subgroup Y, V.Normal ∧ IsOpen ((V : Subgroup Y) : Set Y) ∧
74 ∀ z : Y, z ∈ V → y * z ∈ U
76/-- The normal-subgroup basis implies the subgroup basis. -/
80 intro y U hU hyU
81 rcases hbasis y U hU hyU with ⟨V, _hVnormal, hVopen, hVcoset⟩
82 exact ⟨V, hVopen, hVcoset⟩
84/-- Closure criterion using open-subgroup approximations.
86It is enough to approximate each `y ∈ T` modulo every open subgroup `V`, in the sense that for
87some `s ∈ S` the correction `y⁻¹ * s` lies in `V`. -/
90 (happrox :
91 ∀ y : Y, y ∈ T → ∀ V : Subgroup Y,
92 IsOpen ((V : Subgroup Y) : Set Y) →
93 ∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
94 T ⊆ closure S := by
96 intro y hy U hU hyU
97 rcases hbasis y U hU hyU with ⟨V, hVopen, hVcoset⟩
98 rcases happrox y hy V hVopen with ⟨s, hsS, hsV⟩
99 refine ⟨s, hsS, ?_⟩
100 have hcoset : y * (y⁻¹ * s) ∈ U := hVcoset (y⁻¹ * s) hsV
101 simpa [mul_assoc] using hcoset
103/-- Closure criterion using open-normal-subgroup approximations. -/
106 (happrox :
107 ∀ y : Y, y ∈ T → ∀ V : Subgroup Y,
108 V.Normal → IsOpen ((V : Subgroup Y) : Set Y) →
109 ∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
110 T ⊆ closure S := by
112 intro y hy U hU hyU
113 rcases hbasis y U hU hyU with ⟨V, hVnormal, hVopen, hVcoset⟩
114 rcases happrox y hy V hVnormal hVopen with ⟨s, hsS, hsV⟩
115 refine ⟨s, hsS, ?_⟩
116 have hcoset : y * (y⁻¹ * s) ∈ U := hVcoset (y⁻¹ * s) hsV
117 simpa [mul_assoc] using hcoset
119/-- Coset approximation gives a pointwise closure statement. -/
122 {y : Y} (_hy : y ∈ T)
123 (happrox :
124 ∀ V : Subgroup Y, IsOpen ((V : Subgroup Y) : Set Y) →
125 ∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
126 y ∈ closure S := by
127 rw [mem_closure_iff]
128 intro U hU hyU
129 rcases hbasis y U hU hyU with ⟨V, hVopen, hVcoset⟩
130 rcases happrox V hVopen with ⟨s, hsS, hsV⟩
131 refine ⟨s, ?_, hsS⟩
132 have hcoset : y * (y⁻¹ * s) ∈ U := hVcoset (y⁻¹ * s) hsV
133 simpa [mul_assoc] using hcoset
135end OpenSubgroupClosureAPI
137section QuotientKernelClosureAPI
139variable {Y : Type u} [Group Y] [TopologicalSpace Y]
140variable {S T : Set Y}
142/-- A left neighbourhood basis expressed directly by kernels of quotient maps.
144This is the form produced by finite-stage maps: every open neighbourhood of `y` contains a
145left coset `y * ker π_j`. -/
147 {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
148 (π : ∀ j : J, Y →* Q j) : Prop :=
149 ∀ (y : Y) (U : Set Y), IsOpen U → y ∈ U →
150 ∃ j : J, ∀ z : Y, z ∈ (π j).ker → y * z ∈ U
152/-- If quotient kernels form a left neighbourhood basis, then equality at every quotient stage
153gives closure.
155This is the abstract topology step for the remaining Crowell density theorem: finite quotient
156exactness supplies `s ∈ S` with `π_j s = π_j y`; the quotient-kernel basis turns this into
157ordinary topological approximation. -/
159 {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
160 (π : ∀ j : J, Y →* Q j)
162 (happrox :
163 ∀ y : Y, y ∈ T → ∀ j : J,
164 ∃ s : Y, s ∈ S ∧ π j s = π j y) :
165 T ⊆ closure S := by
167 intro y hy U hU hyU
168 rcases hbasis y U hU hyU with ⟨j, hj⟩
169 rcases happrox y hy j with ⟨s, hsS, hπ⟩
170 have hker : y⁻¹ * s ∈ (π j).ker := by
171 change π j (y⁻¹ * s) = 1
172 rw [map_mul, map_inv, hπ]
173 simp only [inv_mul_cancel]
174 refine ⟨s, hsS, ?_⟩
175 have hsU : y * (y⁻¹ * s) ∈ U := hj (y⁻¹ * s) hker
176 simpa [mul_assoc] using hsU
178end QuotientKernelClosureAPI
180section CompletedFoxDensity
182open scoped Topology
185variable {X H : Type u}
186variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
187variable [DecidableEq X]
188variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
189variable [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
191/-- The semidirect point `(D w, 1)` attached to an abstract free-group kernel word candidate.
193The word may or may not actually lie in the kernel. Kernel membership is recorded separately in
195def freeProCZCCompletedFoxSemidirectKernelWordPoint (φ : X → H) (w : FreeGroup X) :
196 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
197 { left :=
198 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w,
199 right := (1 : H) }
201omit [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
202@[simp]
204 (φ : X → H) (w : FreeGroup X) :
206 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w :=
207 rfl
209omit [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
210@[simp]
212 (φ : X → H) (w : FreeGroup X) :
213 (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w).right = 1 :=
214 rfl
216omit [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
217 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
218/-- A genuine kernel word gives an element of the algebraic kernel-word cycle set. -/
220 (φ : X → H) {w : FreeGroup X} (hw : FreeGroup.lift φ w = 1) :
223 exact ⟨w, hw, rfl⟩
225omit [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
226 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
227/-- Expanded membership form for the algebraic kernel-word cycle set. -/
229 (φ : X → H)
230 (y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
232 ∃ w : FreeGroup X, FreeGroup.lift φ w = 1 ∧
234 constructor
235 · intro hy
236 rcases hy with ⟨w, hw, hy⟩
237 exact ⟨w, hw, hy⟩
238 · rintro ⟨w, hw, hy⟩
239 rw [hy]
241 (ProC := ProC) φ hw
243omit [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
244 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
245omit [DecidableEq X] in
246/-- Boundary-cycle membership for a displayed point `(v, 1)`. -/
248 [Fintype X] (φ : X → H)
249 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)) :
250 ({ left := v, right := (1 : H) } :
251 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) ∈
253 zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v = 0 := by
254 constructor
255 · intro h
256 exact h.2
257 · intro h
258 exact ⟨rfl, h⟩
260omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
261/-- Quotient-kernel approximation form of the completed Fox density statement.
263This is the finite-stage attack surface for the remaining density theorem: once finite quotient
264exactness produces, for every finite quotient stage `j`, a kernel word whose semidirect point has
265the same `j`-th quotient image as the boundary cycle, the completed density statement follows. -/
267 [Fintype X] (φ : X → H)
268 {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
269 (π : ∀ j : J,
270 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →* Q j)
271 (hbasis :
273 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) π)
274 (happrox :
275 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
277 ∀ j : J,
278 ∃ w : FreeGroup X,
279 FreeGroup.lift φ w = 1 ∧
281 (ProC := ProC) φ w) = π j y) :
283 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by
285 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
288 π hbasis ?_
289 intro y hy j
290 rcases happrox y hy j with ⟨w, hw, hπ⟩
291 exact
294 (ProC := ProC) φ hw,
295 hπ⟩
297omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
298/-- Neighbourhood approximation form of the completed Fox density statement.
300For every boundary cycle and every open neighbourhood of it in the completed semidirect product,
301there is a genuine kernel word whose point `(D w, 1)` lies in that neighbourhood. This proves the
302set-level density statement used by the Crowell middle exactness theorem. -/
304 [Fintype X] (φ : X → H)
305 (happrox :
306 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
308 ∀ U : Set (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
309 IsOpen U → y ∈ U →
310 ∃ w : FreeGroup X,
311 FreeGroup.lift φ w = 1 ∧
314 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by
316 intro y hy U hU hyU
317 rcases happrox y hy U hU hyU with ⟨w, hw, hUmem⟩
318 refine ⟨freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w, ?_, hUmem⟩
320 (ProC := ProC) φ hw
322omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
323/-- Open-subgroup approximation form of the completed Fox density statement.
325This is the intended entry point for finite quotient arguments: for every open subgroup `V` of
326the completed Fox semidirect group, approximate a boundary cycle `y` by a kernel-word cycle point
327modulo the left coset `y V`. -/
329 [Fintype X] (φ : X → H)
330 (hbasis :
332 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
333 (happrox :
334 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
336 ∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
337 IsOpen ((V : Subgroup
338 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
339 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
340 ∃ w : FreeGroup X,
341 FreeGroup.lift φ w = 1 ∧
343 (ProC := ProC) φ w ∈ V) :
345 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by
347 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
350 hbasis ?_
351 intro y hy V hVopen
352 rcases happrox y hy V hVopen with ⟨w, hw, hVmem⟩
353 exact
356 (ProC := ProC) φ hw,
357 hVmem⟩
359omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
360/-- Open-normal-subgroup approximation form of the completed Fox density statement. -/
362 [Fintype X] (φ : X → H)
363 (hbasis :
365 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
366 (happrox :
367 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
369 ∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
370 V.Normal →
371 IsOpen ((V : Subgroup
372 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
373 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
374 ∃ w : FreeGroup X,
375 FreeGroup.lift φ w = 1 ∧
377 (ProC := ProC) φ w ∈ V) :
379 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by
381 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
384 hbasis ?_
385 intro y hy V hVnormal hVopen
386 rcases happrox y hy V hVnormal hVopen with ⟨w, hw, hVmem⟩
387 exact
390 (ProC := ProC) φ hw,
391 hVmem⟩
393/-- Open-subgroup approximation places every completed boundary cycle inside the closed
394generated Fox graph target. -/
396 [Fintype X] (φ : X → H)
397 (hbasis :
399 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
400 (happrox :
401 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
403 ∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
404 IsOpen ((V : Subgroup
405 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
406 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
407 ∃ w : FreeGroup X,
408 FreeGroup.lift φ w = 1 ∧
410 (ProC := ProC) φ w ∈ V) :
413 (ProC := ProC) φ : Subgroup
414 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
415 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
416 exact
418 (ProC := ProC) φ
420 (ProC := ProC) φ hbasis happrox)
422/-- Open-normal-subgroup approximation places every completed boundary cycle inside the closed
423generated Fox graph target. -/
425 [Fintype X] (φ : X → H)
426 (hbasis :
428 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
429 (happrox :
430 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
432 ∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
433 V.Normal →
434 IsOpen ((V : Subgroup
435 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
436 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
437 ∃ w : FreeGroup X,
438 FreeGroup.lift φ w = 1 ∧
440 (ProC := ProC) φ w ∈ V) :
443 (ProC := ProC) φ : Subgroup
444 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
445 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
446 exact
448 (ProC := ProC) φ
450 (ProC := ProC) φ hbasis happrox)
452omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
453/-- Under the standard continuity inputs, open-subgroup approximation upgrades the one-sided
454closure statement to the equality between boundary cycles and the closure of kernel-word cycles. -/
456 [Fintype X] [T1Space H]
457 [TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
458 [T1Space (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
459 (φ : X → H)
460 (hleft :
461 Continuous
462 (fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.left))
463 (hright :
464 Continuous
465 (fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.right))
466 (hboundary :
467 Continuous
468 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ)))
469 (hbasis :
471 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
472 (happrox :
473 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
475 ∀ V : Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
476 IsOpen ((V : Subgroup
477 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
478 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) →
479 ∃ w : FreeGroup X,
480 FreeGroup.lift φ w = 1 ∧
482 (ProC := ProC) φ w ∈ V) :
485 exact
487 (ProC := ProC) φ hleft hright hboundary).2
489 (ProC := ProC) φ hbasis happrox)
491end CompletedFoxDensity
493end
495end FoxDifferential