FoxDifferential/Completed/FreeProC/StageProjection.lean

1import FoxDifferential.Completed.FreeProC.RelationSubmoduleApproximation

2import FoxDifferential.Completed.FreeProC.QuotientKernelBasis

4/-

5PUBLIC_PAGE_SNAPSHOT

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

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

8translation_root: data/translation

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

10placement: after imports, never before imports

11-/

12/-!

13# Completed-to-finite semidirect stage projections

15This file builds the reusable projection layer needed by the completed Crowell density argument.

16A finite semidirect projection is constructed from its mathematical coordinates:

18* a coordinate projection on completed Fox vectors;

19* a quotient map on the target group;

20* compatibility of the coordinate projection with the semidirect scalar action.

22The resulting API expresses finite-stage comparison by the actual boundary and derivative

23coordinate formulas.

24-/

26namespace FoxDifferential

28noncomputable section

30open scoped Topology

31open ProCGroups.ProC

33universe u v

35section CompletedFiniteStageMap

37variable {ProC : ProCGroups.ProC.ProCGroupPredicate}

38variable {X H : Type u}

39variable [DecidableEq X]

40variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

41variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

43/-- A semidirect projection from the completed Fox semidirect product to a finite Fox stage,

44constructed from a left coordinate map and a right target quotient map.

46The only compatibility required is that the left coordinate map respects the scalar action used in

47semidirect multiplication. This is the abstract form of the finite quotient map

48`Z_C[[H]]^X ⋊ H -> (Z/n)[F/N]^X ⋊ F/N`. -/

49def freeProCZCCompletedFoxSemidirectStageMap

50 (stageLeft :

51 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

52 finiteFoxStageCoordinateVector (X := X) N n)

53 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)

54 (hscalar :

55 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

56 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =

57 (MonoidAlgebra.of (ModNCompletedCoeff n)

58 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •

59 stageLeft v) :

60 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

61 FiniteFoxStageSemidirect (X := X) N n where

62 toFun y :=

63 { left := stageLeft y.left

64 right := stageRight y.right }

65 map_one' := by

66 apply FiniteFoxStageSemidirect.ext

67 · change stageLeft 0 = 0

68 exact map_zero stageLeft

69 · exact map_one stageRight

70 map_mul' a b := by

71 apply FiniteFoxStageSemidirect.ext

72 · change

73 stageLeft (a.left + zcGroupLike ProC.finiteQuotientClass H a.right • b.left) =

74 stageLeft a.left +

75 (MonoidAlgebra.of (ModNCompletedCoeff n)

76 (finiteFoxStageTargetQuotient (X := X) N) (stageRight a.right)) •

77 stageLeft b.left

78 rw [map_add, hscalar]

79 · change stageRight (a.right * b.right) = stageRight a.right * stageRight b.right

80 exact map_mul stageRight a.right b.right

82omit [DecidableEq X] in

83@[simp]

84theorem freeProCZCCompletedFoxSemidirectStageMap_left

85 (stageLeft :

86 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

87 finiteFoxStageCoordinateVector (X := X) N n)

88 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)

89 (hscalar :

90 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

91 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =

92 (MonoidAlgebra.of (ModNCompletedCoeff n)

93 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •

94 stageLeft v)

95 (y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :

96 (freeProCZCCompletedFoxSemidirectStageMap

97 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y).left =

98 stageLeft y.left :=

99 rfl

100

101omit [DecidableEq X] in

102@[simp]

103theorem freeProCZCCompletedFoxSemidirectStageMap_right

104 (stageLeft :

105 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

106 finiteFoxStageCoordinateVector (X := X) N n)

107 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)

108 (hscalar :

109 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

110 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =

111 (MonoidAlgebra.of (ModNCompletedCoeff n)

112 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •

113 stageLeft v)

114 (y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :

115 (freeProCZCCompletedFoxSemidirectStageMap

116 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y).right =

117 stageRight y.right :=

118 rfl

119

120omit [DecidableEq X] in

121/-- Membership in the kernel of a completed-to-finite semidirect stage map, read in the two

122coordinates. -/

123theorem freeProCZCCompletedFoxSemidirectStageMap_mem_ker_iff

124 (stageLeft :

125 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

126 finiteFoxStageCoordinateVector (X := X) N n)

127 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)

128 (hscalar :

129 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

130 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =

131 (MonoidAlgebra.of (ModNCompletedCoeff n)

132 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •

133 stageLeft v)

134 {y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H} :

135 y ∈ (freeProCZCCompletedFoxSemidirectStageMap

136 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar).ker ↔

137 stageLeft y.left = 0 ∧ stageRight y.right = 1 := by

138 constructor

139 · intro hy

140 change

141 freeProCZCCompletedFoxSemidirectStageMap

142 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y = 1 at hy

143 have hleft := congrArg (fun z : FiniteFoxStageSemidirect (X := X) N n => z.left) hy

144 have hright := congrArg (fun z : FiniteFoxStageSemidirect (X := X) N n => z.right) hy

145 exact ⟨by simpa using hleft, by simpa using hright⟩

146 · rintro ⟨hleft, hright⟩

147 change

148 freeProCZCCompletedFoxSemidirectStageMap

149 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y = 1

150 apply FiniteFoxStageSemidirect.ext

151 · simpa using hleft

152 · simpa using hright

153

154omit [DecidableEq X] in

155/-- A completed boundary-cycle point projects to a finite boundary-cycle point once the left

156coordinate projection commutes with the source-shaped Fox boundary. -/

157theorem freeProCZCCompletedFoxSemidirectStageMap_mem_finiteBoundaryCycleSet

158 [Fintype X]

159 (φ : X → H)

160 (stageLeft :

161 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

162 finiteFoxStageCoordinateVector (X := X) N n)

163 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)

164 (hscalar :

165 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

166 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =

167 (MonoidAlgebra.of (ModNCompletedCoeff n)

168 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •

169 stageLeft v)

170 (stageBoundary :

171 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+

172 finiteFoxStageTargetGroupAlgebra (X := X) N n)

173 (hboundary :

174 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),

175 finiteFoxStageFoxBoundary (X := X) N n (stageLeft v) =

176 stageBoundary

177 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))

178 {y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}

179 (hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ) :

180 freeProCZCCompletedFoxSemidirectStageMap

181 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y ∈

182 finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n := by

183 rcases hy with ⟨hyright, hyboundary⟩

184 constructor

185 · change stageRight y.right = 1

186 rw [hyright]

187 exact map_one stageRight

188 · rw [mem_finiteFoxStageBoundaryCycleSubmodule]

189 calc

190 finiteFoxStageFoxBoundary (X := X) N n

191 ((freeProCZCCompletedFoxSemidirectStageMap

192 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar y).left)

193 = finiteFoxStageFoxBoundary (X := X) N n (stageLeft y.left) := rfl

194 _ = stageBoundary

195 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) y.left) :=

196 hboundary y.left

197 _ = 0 := by

198 rw [hyboundary]

199 exact map_zero stageBoundary

200

201/-- The stage map sends the completed kernel-word point `(D w, 1)` to the corresponding finite

202kernel-word point, provided the left coordinate projection commutes with Fox derivatives. -/

203theorem freeProCZCCompletedFoxSemidirectStageMap_kernelWordPoint

204 (φ : X → H)

205 (stageLeft :

206 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

207 finiteFoxStageCoordinateVector (X := X) N n)

208 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)

209 (hscalar :

210 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

211 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =

212 (MonoidAlgebra.of (ModNCompletedCoeff n)

213 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •

214 stageLeft v)

215 (hderivative :

216 ∀ w : FreeGroup X,

217 stageLeft

218 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

219 (FreeGroup.lift φ) w) =

220 finiteFoxStageDerivativeVector (X := X) N n w)

221 (w : FreeGroup X) :

222 freeProCZCCompletedFoxSemidirectStageMap

223 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar

224 (freeProCZCCompletedFoxSemidirectKernelWordPoint (ProC := ProC) φ w) =

225 finiteFoxStageSemidirectKernelWordPoint (X := X) N n w := by

226 apply FiniteFoxStageSemidirect.ext

227 · change

228 stageLeft

229 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

230 (FreeGroup.lift φ) w) =

231 finiteFoxStageDerivativeVector (X := X) N n w

232 exact hderivative w

233 · simp only [freeProCZCCompletedFoxSemidirectKernelWordPoint, freeProCZCCompletedFoxSemidirectStageMap_right,

234 map_one, finiteFoxStageSemidirectKernelWordPoint]

235

236/-- The stage map sends a completed graph-word point `(D w, φ(w))` to the corresponding finite

237stage graph point. -/

238theorem freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint

239 (φ : X → H)

240 (stageLeft :

241 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

242 finiteFoxStageCoordinateVector (X := X) N n)

243 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)

244 (hscalar :

245 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

246 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =

247 (MonoidAlgebra.of (ModNCompletedCoeff n)

248 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •

249 stageLeft v)

250 (hderivative :

251 ∀ w : FreeGroup X,

252 stageLeft

253 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

254 (FreeGroup.lift φ) w) =

255 finiteFoxStageDerivativeVector (X := X) N n w)

256 (w : FreeGroup X) :

257 freeProCZCCompletedFoxSemidirectStageMap

258 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar

259 (freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w) =

260 ({ left := finiteFoxStageDerivativeVector (X := X) N n w,

261 right := stageRight (FreeGroup.lift φ w) } :

262 FiniteFoxStageSemidirect (X := X) N n) := by

263 apply FiniteFoxStageSemidirect.ext

264 · exact hderivative w

265 · rfl

266

267/-- If a word is in the finite-stage relation subgroup, the stage image of its completed graph

268point is the finite kernel-word point. -/

269theorem freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint_of_stage_kernel

270 (φ : X → H)

271 (stageLeft :

272 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

273 finiteFoxStageCoordinateVector (X := X) N n)

274 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)

275 (hscalar :

276 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

277 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =

278 (MonoidAlgebra.of (ModNCompletedCoeff n)

279 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •

280 stageLeft v)

281 (hderivative :

282 ∀ w : FreeGroup X,

283 stageLeft

284 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

285 (FreeGroup.lift φ) w) =

286 finiteFoxStageDerivativeVector (X := X) N n w)

287 (hright_word :

288 ∀ w : FreeGroup X, stageRight (FreeGroup.lift φ w) = QuotientGroup.mk' N w)

289 (w : FreeGroup X) (hw : w ∈ N) :

290 freeProCZCCompletedFoxSemidirectStageMap

291 (ProC := ProC) (X := X) (H := H) N n stageLeft stageRight hscalar

292 (freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w) =

293 finiteFoxStageSemidirectKernelWordPoint (X := X) N n w := by

294 rw [freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint

295 (ProC := ProC) (X := X) (H := H) N n φ stageLeft stageRight hscalar hderivative w]

296 apply FiniteFoxStageSemidirect.ext

297 · rfl

298 · change stageRight (FreeGroup.lift φ w) = 1

299 rw [hright_word w]

300 exact (QuotientGroup.eq_one_iff (N := N) w).2 hw

301

302end CompletedFiniteStageMap

303

304section StageMapDensityRoute

305

306variable {ProC : ProCGroups.ProC.ProCGroupPredicate}

307variable {X H : Type u}

308variable [DecidableEq X]

309variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

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

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

312

313omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in

314/-- Completed Fox density from a family of concrete completed-to-finite semidirect stage maps.

315

316The finite exactness input is the relation-ideal derivative theorem already proved at every

317finite stage. The remaining data are now exactly the two projection formulas expected from the

318completed Fox construction: boundary compatibility and derivative compatibility. -/

319theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stageMaps_relDeriv

320 [Fintype X] (φ : X → H)

321 {J : Type v}

322 (Nstage : J → Subgroup (FreeGroup X))

323 [∀ j, (Nstage j).Normal]

324 (nstage : J → ℕ)

325 (stageLeft : ∀ j : J,

326 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

327 finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))

328 (stageRight : ∀ j : J,

329 H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))

330 (hscalar :

331 ∀ j : J, ∀ (h : H)

332 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

333 stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =

334 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))

335 (finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •

336 stageLeft j v)

337 (hquotient_basis :

338 HasLeftQuotientKernelNeighbourhoodBasis

339 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

340 (fun j : J =>

341 freeProCZCCompletedFoxSemidirectStageMap

342 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

343 (stageLeft j) (stageRight j) (hscalar j)))

344 (stageBoundary : ∀ j : J,

345 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+

346 finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))

347 (hboundary :

348 ∀ j : J,

349 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),

350 finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =

351 stageBoundary j

352 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))

353 (hNstage_kernel :

354 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)

355 (hderivative :

356 ∀ j : J, ∀ w : FreeGroup X,

357 stageLeft j

358 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

359 (FreeGroup.lift φ) w) =

360 finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :

361 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

362 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by

363 let π : ∀ j : J,

364 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

365 FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j) :=

366 fun j =>

367 freeProCZCCompletedFoxSemidirectStageMap

368 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

369 (stageLeft j) (stageRight j) (hscalar j)

370 refine

371 freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv

372 (ProC := ProC) φ Nstage nstage π ?_ ?_ hNstage_kernel ?_

373 · exact hquotient_basis

374 · intro y hy j

375 exact

376 freeProCZCCompletedFoxSemidirectStageMap_mem_finiteBoundaryCycleSet

377 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

378 φ (stageLeft j) (stageRight j) (hscalar j) (stageBoundary j)

379 (hboundary j) hy

380 · intro j w hw

381 exact

382 freeProCZCCompletedFoxSemidirectStageMap_kernelWordPoint

383 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

384 φ (stageLeft j) (stageRight j) (hscalar j) (hderivative j) w

385

386omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in

387/-- Completed graph-word density from concrete completed-to-finite semidirect stage maps.

388

389Unlike the kernel-word route, this theorem does not ask for

390`w ∈ Nstage j -> FreeGroup.lift φ w = 1`. Finite-stage exactness supplies `w ∈ Nstage j`, and

391the completed approximating point is the graph point `(D w, φ(w))`. -/

392theorem freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_stageMaps_relDeriv

393 [Fintype X] (φ : X → H)

394 {J : Type v}

395 (Nstage : J → Subgroup (FreeGroup X))

396 [∀ j, (Nstage j).Normal]

397 (nstage : J → ℕ)

398 (stageLeft : ∀ j : J,

399 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

400 finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))

401 (stageRight : ∀ j : J,

402 H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))

403 (hscalar :

404 ∀ j : J, ∀ (h : H)

405 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

406 stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =

407 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))

408 (finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •

409 stageLeft j v)

410 (hquotient_basis :

411 HasLeftQuotientKernelNeighbourhoodBasis

412 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

413 (fun j : J =>

414 freeProCZCCompletedFoxSemidirectStageMap

415 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

416 (stageLeft j) (stageRight j) (hscalar j)))

417 (stageBoundary : ∀ j : J,

418 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+

419 finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))

420 (hboundary :

421 ∀ j : J,

422 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),

423 finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =

424 stageBoundary j

425 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))

426 (hright_word :

427 ∀ j : J, ∀ w : FreeGroup X,

428 stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)

429 (hderivative :

430 ∀ j : J, ∀ w : FreeGroup X,

431 stageLeft j

432 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

433 (FreeGroup.lift φ) w) =

434 finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :

435 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

436 closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ) := by

437 let π : ∀ j : J,

438 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*

439 FiniteFoxStageSemidirect (X := X) (Nstage j) (nstage j) :=

440 fun j =>

441 freeProCZCCompletedFoxSemidirectStageMap

442 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

443 (stageLeft j) (stageRight j) (hscalar j)

444 refine

445 freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_finiteStage_semi_exact

446 (ProC := ProC) φ Nstage nstage π ?_ ?_ ?_ ?_

447 · exact hquotient_basis

448 · intro y hy j

449 exact

450 freeProCZCCompletedFoxSemidirectStageMap_mem_finiteBoundaryCycleSet

451 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

452 φ (stageLeft j) (stageRight j) (hscalar j) (stageBoundary j)

453 (hboundary j) hy

454 · intro j

455 exact finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationIdeal_derivatives

456 (X := X) (Nstage j) (nstage j)

457 · intro j w hw

458 exact

459 freeProCZCCompletedFoxSemidirectStageMap_graphWordPoint_of_stage_kernel

460 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

461 φ (stageLeft j) (stageRight j) (hscalar j) (hderivative j)

462 (hright_word j) w hw

463

464/-- Concrete stage-map graph-word density, phrased as closed-generated-target membership. -/

465theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_graphRelDeriv

466 [Fintype X] (φ : X → H)

467 {J : Type v}

468 (Nstage : J → Subgroup (FreeGroup X))

469 [∀ j, (Nstage j).Normal]

470 (nstage : J → ℕ)

471 (stageLeft : ∀ j : J,

472 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

473 finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))

474 (stageRight : ∀ j : J,

475 H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))

476 (hscalar :

477 ∀ j : J, ∀ (h : H)

478 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

479 stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =

480 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))

481 (finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •

482 stageLeft j v)

483 (hquotient_basis :

484 HasLeftQuotientKernelNeighbourhoodBasis

485 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

486 (fun j : J =>

487 freeProCZCCompletedFoxSemidirectStageMap

488 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

489 (stageLeft j) (stageRight j) (hscalar j)))

490 (stageBoundary : ∀ j : J,

491 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+

492 finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))

493 (hboundary :

494 ∀ j : J,

495 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),

496 finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =

497 stageBoundary j

498 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))

499 (hright_word :

500 ∀ j : J, ∀ w : FreeGroup X,

501 stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)

502 (hderivative :

503 ∀ j : J, ∀ w : FreeGroup X,

504 stageLeft j

505 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

506 (FreeGroup.lift φ) w) =

507 finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :

508 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

509 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

510 (ProC := ProC) φ : Subgroup

511 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set

512 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by

513 exact

514 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density

515 (ProC := ProC) φ

516 (freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_stageMaps_relDeriv

517 (ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar hquotient_basis

518 stageBoundary hboundary hright_word hderivative)

519

520/-- The same concrete stage-map route, with the conclusion phrased as membership in the

521closed-generated Fox graph target. -/

522theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_relDeriv

523 [Fintype X] (φ : X → H)

524 {J : Type v}

525 (Nstage : J → Subgroup (FreeGroup X))

526 [∀ j, (Nstage j).Normal]

527 (nstage : J → ℕ)

528 (stageLeft : ∀ j : J,

529 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

530 finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))

531 (stageRight : ∀ j : J,

532 H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))

533 (hscalar :

534 ∀ j : J, ∀ (h : H)

535 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

536 stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =

537 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))

538 (finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •

539 stageLeft j v)

540 (hquotient_basis :

541 HasLeftQuotientKernelNeighbourhoodBasis

542 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

543 (fun j : J =>

544 freeProCZCCompletedFoxSemidirectStageMap

545 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

546 (stageLeft j) (stageRight j) (hscalar j)))

547 (stageBoundary : ∀ j : J,

548 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+

549 finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))

550 (hboundary :

551 ∀ j : J,

552 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),

553 finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =

554 stageBoundary j

555 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))

556 (hNstage_kernel :

557 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)

558 (hderivative :

559 ∀ j : J, ∀ w : FreeGroup X,

560 stageLeft j

561 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

562 (FreeGroup.lift φ) w) =

563 finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :

564 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

565 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

566 (ProC := ProC) φ : Subgroup

567 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set

568 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by

569 exact

570 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density

571 (ProC := ProC) φ

572 (freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stageMaps_relDeriv

573 (ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar hquotient_basis

574 stageBoundary hboundary hNstage_kernel hderivative)

575

576

577/-- Stage-map density using identity-neighbourhood kernels rather than left-coset kernels.

578

579This is the topological form naturally produced by profinite finite quotient separation. The

580conversion to the left-coset closure basis is performed internally. -/

581theorem boundaryCycles_subset_kernelClosure_of_stageMaps

582 [Fintype X] (φ : X → H)

583 {J : Type v}

584 (Nstage : J → Subgroup (FreeGroup X))

585 [∀ j, (Nstage j).Normal]

586 (nstage : J → ℕ)

587 (stageLeft : ∀ j : J,

588 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

589 finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))

590 (stageRight : ∀ j : J,

591 H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))

592 (hscalar :

593 ∀ j : J, ∀ (h : H)

594 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

595 stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =

596 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))

597 (finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •

598 stageLeft j v)

599 (hidentity_basis :

600 HasIdentityQuotientKernelNeighbourhoodBasis

601 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

602 (fun j : J =>

603 freeProCZCCompletedFoxSemidirectStageMap

604 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

605 (stageLeft j) (stageRight j) (hscalar j)))

606 (stageBoundary : ∀ j : J,

607 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+

608 finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))

609 (hboundary :

610 ∀ j : J,

611 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),

612 finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =

613 stageBoundary j

614 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))

615 (hNstage_kernel :

616 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)

617 (hderivative :

618 ∀ j : J, ∀ w : FreeGroup X,

619 stageLeft j

620 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

621 (FreeGroup.lift φ) w) =

622 finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :

623 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

624 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by

625 refine

626 freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stageMaps_relDeriv

627 (ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar ?_

628 stageBoundary hboundary hNstage_kernel hderivative

629 exact HasIdentityQuotientKernelNeighbourhoodBasis.to_left

630 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

631 (π := fun j : J =>

632 freeProCZCCompletedFoxSemidirectStageMap

633 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

634 (stageLeft j) (stageRight j) (hscalar j))

635 hidentity_basis

636

637/-- Graph-word density using identity-neighbourhood kernels rather than left-coset kernels. -/

638theorem boundaryCycles_subset_graphWordClosure_of_stageMaps

639 [Fintype X] (φ : X → H)

640 {J : Type v}

641 (Nstage : J → Subgroup (FreeGroup X))

642 [∀ j, (Nstage j).Normal]

643 (nstage : J → ℕ)

644 (stageLeft : ∀ j : J,

645 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

646 finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))

647 (stageRight : ∀ j : J,

648 H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))

649 (hscalar :

650 ∀ j : J, ∀ (h : H)

651 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

652 stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =

653 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))

654 (finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •

655 stageLeft j v)

656 (hidentity_basis :

657 HasIdentityQuotientKernelNeighbourhoodBasis

658 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

659 (fun j : J =>

660 freeProCZCCompletedFoxSemidirectStageMap

661 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

662 (stageLeft j) (stageRight j) (hscalar j)))

663 (stageBoundary : ∀ j : J,

664 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+

665 finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))

666 (hboundary :

667 ∀ j : J,

668 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),

669 finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =

670 stageBoundary j

671 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))

672 (hright_word :

673 ∀ j : J, ∀ w : FreeGroup X,

674 stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)

675 (hderivative :

676 ∀ j : J, ∀ w : FreeGroup X,

677 stageLeft j

678 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

679 (FreeGroup.lift φ) w) =

680 finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :

681 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

682 closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ) := by

683 refine

684 freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_stageMaps_relDeriv

685 (ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar ?_

686 stageBoundary hboundary hright_word hderivative

687 exact HasIdentityQuotientKernelNeighbourhoodBasis.to_left

688 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

689 (π := fun j : J =>

690 freeProCZCCompletedFoxSemidirectStageMap

691 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

692 (stageLeft j) (stageRight j) (hscalar j))

693 hidentity_basis

694

695/-- Closed-generated-target version of the identity-kernel graph-word stage-map theorem. -/

696theorem boundaryCycles_subset_closedGenTarget_of_stageGraph

697 [Fintype X] (φ : X → H)

698 {J : Type v}

699 (Nstage : J → Subgroup (FreeGroup X))

700 [∀ j, (Nstage j).Normal]

701 (nstage : J → ℕ)

702 (stageLeft : ∀ j : J,

703 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

704 finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))

705 (stageRight : ∀ j : J,

706 H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))

707 (hscalar :

708 ∀ j : J, ∀ (h : H)

709 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

710 stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =

711 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))

712 (finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •

713 stageLeft j v)

714 (hidentity_basis :

715 HasIdentityQuotientKernelNeighbourhoodBasis

716 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

717 (fun j : J =>

718 freeProCZCCompletedFoxSemidirectStageMap

719 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

720 (stageLeft j) (stageRight j) (hscalar j)))

721 (stageBoundary : ∀ j : J,

722 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+

723 finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))

724 (hboundary :

725 ∀ j : J,

726 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),

727 finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =

728 stageBoundary j

729 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))

730 (hright_word :

731 ∀ j : J, ∀ w : FreeGroup X,

732 stageRight j (FreeGroup.lift φ w) = QuotientGroup.mk' (Nstage j) w)

733 (hderivative :

734 ∀ j : J, ∀ w : FreeGroup X,

735 stageLeft j

736 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

737 (FreeGroup.lift φ) w) =

738 finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :

739 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

740 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

741 (ProC := ProC) φ : Subgroup

742 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set

743 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by

744 exact

745 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density

746 (ProC := ProC) φ

747 (boundaryCycles_subset_graphWordClosure_of_stageMaps

748 (ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar hidentity_basis

749 stageBoundary hboundary hright_word hderivative)

750

751/-- Closed-generated-target version of the identity-kernel stage-map density theorem. -/

752theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_stageMaps_identityKernel_relDeriv

753 [Fintype X] (φ : X → H)

754 {J : Type v}

755 (Nstage : J → Subgroup (FreeGroup X))

756 [∀ j, (Nstage j).Normal]

757 (nstage : J → ℕ)

758 (stageLeft : ∀ j : J,

759 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+

760 finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))

761 (stageRight : ∀ j : J,

762 H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))

763 (hscalar :

764 ∀ j : J, ∀ (h : H)

765 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),

766 stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =

767 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))

768 (finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •

769 stageLeft j v)

770 (hidentity_basis :

771 HasIdentityQuotientKernelNeighbourhoodBasis

772 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)

773 (fun j : J =>

774 freeProCZCCompletedFoxSemidirectStageMap

775 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)

776 (stageLeft j) (stageRight j) (hscalar j)))

777 (stageBoundary : ∀ j : J,

778 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+

779 finiteFoxStageTargetGroupAlgebra (X := X) (Nstage j) (nstage j))

780 (hboundary :

781 ∀ j : J,

782 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),

783 finiteFoxStageFoxBoundary (X := X) (Nstage j) (nstage j) (stageLeft j v) =

784 stageBoundary j

785 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))

786 (hNstage_kernel :

787 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)

788 (hderivative :

789 ∀ j : J, ∀ w : FreeGroup X,

790 stageLeft j

791 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

792 (FreeGroup.lift φ) w) =

793 finiteFoxStageDerivativeVector (X := X) (Nstage j) (nstage j) w) :

794 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆

795 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

796 (ProC := ProC) φ : Subgroup

797 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set

798 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by

799 exact

800 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density

801 (ProC := ProC) φ

802 (boundaryCycles_subset_kernelClosure_of_stageMaps

803 (ProC := ProC) φ Nstage nstage stageLeft stageRight hscalar hidentity_basis

804 stageBoundary hboundary hNstage_kernel hderivative)

805

806end StageMapDensityRoute

807

808end

809

810end FoxDifferential