Source: ProCGroups.FoxDifferential.Completed.Continuous.Universal.NaturalTopology

1import ProCGroups.FoxDifferential.Completed.Continuous.Universal.System

3/-!

4# Fox differential: completed — continuous — universal — natural topology

6The principal declarations in this module are:

8- `zcCompletedDifferentialModuleStageProjectionAdd`

9 The additive finite-stage projection from the algebraic completed differential module.

10- `zcCompletedDifferentialModuleStageProjectionProduct`

11 The product of all finite source/target/coefficient projections of the algebraic quotient.

12- `zcCompletedDifferentialModuleStageProjectionAdd_apply`

13 The additive stage projection has the same underlying function as the unbundled completed

14 differential-module stage projection.

15- `zcCompletedDifferentialModuleStageProjectionAdd_universal`

16 The additive finite-stage projection sends the universal differential to the corresponding

17 finite-stage differential.

18-/

20namespace FoxDifferential

22noncomputable section

24open ProCGroups.Completion

25open ProCGroups.ProC

26open scoped commutatorElement

28universe u

30variable (C : ProCGroups.FiniteGroupClass.{u})

31variable {G H : Type u}

32variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

33variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

34variable (ψ : G →* H)

36/-- The additive finite-stage projection from the algebraic completed differential module. -/

37def zcCompletedDifferentialModuleStageProjectionAdd

38 (i : ZCCompletedDifferentialModuleIndex C ψ) :

39 ZCCompletedDifferentialModule C ψ →+

40 ZCCompletedDifferentialModuleStage C ψ i :=

41 (zcCompletedDifferentialModuleStageProjection C ψ i).toAddMonoidHom

43omit [IsTopologicalGroup G] in

44/--

45The additive stage projection has the same underlying function as the unbundled completed

46differential-module stage projection.

47-/

48@[simp]

49theorem zcCompletedDifferentialModuleStageProjectionAdd_apply

50 (i : ZCCompletedDifferentialModuleIndex C ψ)

51 (a : ZCCompletedDifferentialModule C ψ) :

52 zcCompletedDifferentialModuleStageProjectionAdd C ψ i a =

53 zcCompletedDifferentialModuleStageProjection C ψ i a :=

54 rfl

56omit [IsTopologicalGroup G] in

57/--

58The additive finite-stage projection sends the universal differential to the corresponding

59finite-stage differential.

60-/

61@[simp]

62theorem zcCompletedDifferentialModuleStageProjectionAdd_universal

63 (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :

64 zcCompletedDifferentialModuleStageProjectionAdd C ψ i

65 (zcUniversalDifferential C ψ g) =

66 zcCompletedDifferentialModuleStageDifferential C ψ i g :=

67 zcCompletedDifferentialModuleStageProjection_universal C ψ i g

69/-- The product of all finite source/target/coefficient projections of the algebraic quotient. -/

70def zcCompletedDifferentialModuleStageProjectionProduct :

71 ZCCompletedDifferentialModule C ψ →

72 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

73 ZCCompletedDifferentialModuleStage C ψ i :=

74 fun a i => zcCompletedDifferentialModuleStageProjectionAdd C ψ i a

76omit [IsTopologicalGroup G] in

77/-- The product of additive stage projections evaluates at `i` as the additive projection at `i`. -/

78@[simp]

79theorem zcCompletedDifferentialModuleStageProjectionProduct_apply

80 (a : ZCCompletedDifferentialModule C ψ)

81 (i : ZCCompletedDifferentialModuleIndex C ψ) :

82 zcCompletedDifferentialModuleStageProjectionProduct C ψ a i =

83 zcCompletedDifferentialModuleStageProjectionAdd C ψ i a :=

84 rfl

86/--

87The finite-stage completed topology on the algebraic completed differential module. This

88topology is named deliberately: it is not installed as a global instance.

89-/

90@[implicit_reducible]

91def zcCompletedDifferentialModuleNaturalTopology :

92 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

93 TopologicalSpace.induced

94 (zcCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstance

96omit [IsTopologicalGroup G] in

97/-- The product map defining the finite-stage completed topology is continuous. -/

98theorem continuous_zcCompletedDifferentialModuleStageProjectionProduct_naturalTopology :

99 @Continuous (ZCCompletedDifferentialModule C ψ)

100 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,

101 ZCCompletedDifferentialModuleStage C ψ i)

102 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance

103 (zcCompletedDifferentialModuleStageProjectionProduct C ψ) :=

104 continuous_induced_dom

105

106omit [IsTopologicalGroup G] in

107/-- Each finite-stage projection is continuous for the finite-stage completed topology. -/

108theorem continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology

109 (i : ZCCompletedDifferentialModuleIndex C ψ) :

110 @Continuous (ZCCompletedDifferentialModule C ψ)

111 (ZCCompletedDifferentialModuleStage C ψ i)

112 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance

113 (zcCompletedDifferentialModuleStageProjectionAdd C ψ i) := by

114 change @Continuous (ZCCompletedDifferentialModule C ψ)

115 (ZCCompletedDifferentialModuleStage C ψ i)

116 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance

117 (zcCompletedDifferentialModuleStageProjection C ψ i)

118 have hprod :=

119 continuous_zcCompletedDifferentialModuleStageProjectionProduct_naturalTopology C ψ

120 simpa [zcCompletedDifferentialModuleStageProjectionProduct, Function.comp_def] using

121 (@Continuous.comp

122 (ZCCompletedDifferentialModule C ψ)

123 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,

124 ZCCompletedDifferentialModuleStage C ψ i)

125 (ZCCompletedDifferentialModuleStage C ψ i)

126 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance inferInstance

127 (f := zcCompletedDifferentialModuleStageProjectionProduct C ψ)

128 (g := fun x => x i)

129 (continuous_apply i) hprod)

130

131omit [IsTopologicalGroup G] in

132/--

133Continuity of the completed differential-module stage projection is characterized by the natural

134topology.

135-/

136theorem continuous_zcCompletedDifferentialModuleStageProjection_naturalTopology

137 (i : ZCCompletedDifferentialModuleIndex C ψ) :

138 @Continuous (ZCCompletedDifferentialModule C ψ)

139 (ZCCompletedDifferentialModuleStage C ψ i)

140 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance

141 (zcCompletedDifferentialModuleStageProjection C ψ i) := by

142 change @Continuous (ZCCompletedDifferentialModule C ψ)

143 (ZCCompletedDifferentialModuleStage C ψ i)

144 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance

145 (zcCompletedDifferentialModuleStageProjectionAdd C ψ i)

146 exact continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ i

147

148/--

149A named predicate for the algebraic separation still needed to make the natural topology

150Hausdorff. It is false for arbitrary sources without a residual finite-stage hypothesis.

151-/

152def zcCompletedDifferentialModuleStageProjectionsSeparate : Prop :=

153 Function.Injective (zcCompletedDifferentialModuleStageProjectionProduct C ψ)

154

155/--

156Pre-quotient finite-stage separation says that elements killed by every finite-stage

157crossed-differential projection are exactly the defining crossed-differential relations.

158-/

159def zcCompletedDifferentialModulePreStageProjectionsSeparate : Prop :=

160 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,

161 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,

162 crossedDifferentialModuleLiftLinear

163 (R := ZCCompletedGroupAlgebra C H)

164 (zcCompletedDifferentialModuleStageDifferential C ψ i) x = 0) →

165 x ∈ crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)

166

167/-- The kernel on the pre-module cut out by one finite source/target/coefficient stage. -/

168def zcCompletedDifferentialModulePreStageKernel

169 (i : ZCCompletedDifferentialModuleIndex C ψ) :

170 Submodule (ZCCompletedGroupAlgebra C H)

171 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

172 LinearMap.ker

173 (crossedDifferentialModuleLiftLinear

174 (R := ZCCompletedGroupAlgebra C H)

175 (zcCompletedDifferentialModuleStageDifferential C ψ i))

176

177omit [IsTopologicalGroup G] in

178/--

179Membership in a completed differential-module pre-stage kernel is equivalent to vanishing of the

180corresponding finite-stage coordinate.

181-/

182@[simp]

183theorem mem_zcCompletedDifferentialModulePreStageKernel_iff

184 {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}

185 {i : ZCCompletedDifferentialModuleIndex C ψ}

186 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G} :

187 x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i ↔

188 crossedDifferentialModuleLiftLinear

189 (R := ZCCompletedGroupAlgebra C H)

190 (zcCompletedDifferentialModuleStageDifferential C ψ i) x = 0 :=

191 Iff.rfl

192

193omit [IsTopologicalGroup G] in

194/--

195Membership in a finite pre-stage kernel is equivalently membership of the explicit

196source-and-coefficient reduction in the finite crossed-differential relation submodule.

197-/

198theorem mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule

199 {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}

200 {i : ZCCompletedDifferentialModuleIndex C ψ}

201 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G} :

202 x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i ↔

203 zcCompletedDifferentialModulePreStageMap C ψ i x ∈

204 crossedDifferentialRelationSubmodule

205 (zcCompletedDifferentialModuleStageScalar C ψ i) := by

206 constructor

207 · intro hx

208 have hq :

209 (crossedDifferentialRelationSubmodule

210 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

211 (zcCompletedDifferentialModulePreStageMap C ψ i x) = 0 := by

212 rw [zcCompletedDifferentialModulePreStageMap_mkQ]

213 exact hx

214 exact

215 (Submodule.Quotient.mk_eq_zero

216 (p := crossedDifferentialRelationSubmodule

217 (zcCompletedDifferentialModuleStageScalar C ψ i))

218 (x := zcCompletedDifferentialModulePreStageMap C ψ i x)).1 hq

219 · intro hx

220 have hq :

221 (crossedDifferentialRelationSubmodule

222 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

223 (zcCompletedDifferentialModulePreStageMap C ψ i x) = 0 :=

224 (Submodule.Quotient.mk_eq_zero

225 (p := crossedDifferentialRelationSubmodule

226 (zcCompletedDifferentialModuleStageScalar C ψ i))

227 (x := zcCompletedDifferentialModulePreStageMap C ψ i x)).2 hx

228 rw [mem_zcCompletedDifferentialModulePreStageKernel_iff]

229 rw [← zcCompletedDifferentialModulePreStageMap_mkQ]

230 exact hq

231

232omit [IsTopologicalGroup G] in

233/-- Every defining crossed-differential relation is killed by every finite stage. -/

234theorem crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel

235 (i : ZCCompletedDifferentialModuleIndex C ψ) :

236 crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) ≤

237 zcCompletedDifferentialModulePreStageKernel C ψ i := by

238 simpa [zcCompletedDifferentialModulePreStageKernel] using

239 crossedHomRelationSubmodule_le_ker

240 (A := ZCCompletedDifferentialModuleStage C ψ i)

241 (zcCompletedGroupAlgebraScalar C ψ)

242 (zcCompletedDifferentialModuleStageDifferential C ψ i)

243

244omit [IsTopologicalGroup G] in

245/--

246The explicit finite pre-stage map sends completed crossed-differential relations to finite

247crossed-differential relations.

248-/

249theorem zcCompletedDifferentialModulePreStageMap_mem_relationSubmodule_of_mem

250 (i : ZCCompletedDifferentialModuleIndex C ψ)

251 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}

252 (hx : x ∈ crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)) :

253 zcCompletedDifferentialModulePreStageMap C ψ i x ∈

254 crossedDifferentialRelationSubmodule

255 (zcCompletedDifferentialModuleStageScalar C ψ i) :=

256 (mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule (C := C) (ψ := ψ) (i := i) (x

257 := x)).1

258 (crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel

259 (C := C) (ψ := ψ) i hx)

260

261/-- The common finite-stage kernel on the pre-module. -/

262def zcCompletedDifferentialModulePreStageKernelIntersection :

263 Submodule (ZCCompletedGroupAlgebra C H)

264 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

265 ⨅ i : ZCCompletedDifferentialModuleIndex C ψ,

266 zcCompletedDifferentialModulePreStageKernel C ψ i

267

268omit [IsTopologicalGroup G] in

269/--

270Membership in the intersection of completed differential-module pre-stage kernels is equivalent

271to vanishing of the corresponding finite-stage coordinate.

272-/

273theorem mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff

274 {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}

275 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G} :

276 x ∈ zcCompletedDifferentialModulePreStageKernelIntersection C ψ ↔

277 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

278 zcCompletedDifferentialModulePreStageMap C ψ i x ∈

279 crossedDifferentialRelationSubmodule

280 (zcCompletedDifferentialModuleStageScalar C ψ i) := by

281 rw [zcCompletedDifferentialModulePreStageKernelIntersection, Submodule.mem_iInf]

282 constructor

283 · intro hx i

284 exact

285 (mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule (C := C) (ψ := ψ) (i :=

286 i) (x := x)).1 (hx i)

287 · intro hx i

288 exact

289 (mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule (C := C) (ψ := ψ) (i :=

290 i) (x := x)).2 (hx i)

291

292/--

293The finite-stage closed relation submodule defining the separated completed

294\(\psi\)-differential module.

295-/

296abbrev zcCompletedDifferentialRelationFiniteClosedSubmodule :

297 Submodule (ZCCompletedGroupAlgebra C H)

298 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

299 zcCompletedDifferentialModulePreStageKernelIntersection C ψ

300

301/--

302The separated completed \(\psi\)-differential module. This is the finite-stage separated

303quotient used for the profinite Crowell middle term.

304-/

305abbrev ZCSeparatedCompletedDifferentialModule : Type u :=

306 CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G ⧸

307 zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ

308

309/--

310Mathematical Crowell module \(A_{\psi}(C)\). By convention in this development, \(A_{\psi}(C)\)

311is the closed/separated finite-stage quotient, not the algebraic quotient of the

312\(\mathbb{Z}_C\)-completed differential module.

313-/

314abbrev ZCApsi : Type u :=

315 ZCSeparatedCompletedDifferentialModule C ψ

316

317omit [IsTopologicalGroup G] in

318/-- Algebraic crossed-differential relations vanish in the finite-stage separated quotient. -/

319theorem crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule :

320 crossedDifferentialRelationSubmodule

321 (zcCompletedGroupAlgebraScalar C ψ) ≤

322 zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ := by

323 intro x hx

324 rw [zcCompletedDifferentialRelationFiniteClosedSubmodule,

325 mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff]

326 intro i

327 exact zcCompletedDifferentialModulePreStageMap_mem_relationSubmodule_of_mem C ψ i hx

328

329/-- The universal crossed differential into the separated completed quotient. -/

330def zcSeparatedUniversalDifferential :

331 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)

332 (ZCSeparatedCompletedDifferentialModule C ψ) where

333 toFun g :=

334 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

335 (Finsupp.single g 1)

336 map_mul' := by

337 intro g h

338 let δ : G → ZCSeparatedCompletedDifferentialModule C ψ := fun x =>

339 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

340 (Finsupp.single x 1)

341 change δ (g * h) = δ g + zcCompletedGroupAlgebraScalar C ψ g • δ h

342 have hzero :

343 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

344 (crossedDifferentialRelationElement

345 (zcCompletedGroupAlgebraScalar C ψ) g h) = 0 := by

346 exact

347 (Submodule.Quotient.mk_eq_zero

348 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

349 (x := crossedDifferentialRelationElement

350 (zcCompletedGroupAlgebraScalar C ψ) g h)).2

351 (crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule C ψ

352 (crossedDifferentialRelationElement_mem

353 (zcCompletedGroupAlgebraScalar C ψ) g h))

354 have hzero' :

355 δ (g * h) -

356 (δ g +

357 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

358 (zcCompletedGroupAlgebraScalar C ψ g • Finsupp.single h 1)) = 0 := by

359 simpa [δ, crossedDifferentialRelationElement] using hzero

360 have hsmul :

361 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

362 (zcCompletedGroupAlgebraScalar C ψ g • Finsupp.single h 1) =

363 zcCompletedGroupAlgebraScalar C ψ g • δ h := by

364 simpa [δ, Submodule.mkQ_apply] using

365 (Submodule.Quotient.mk_smul

366 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

367 (r := zcCompletedGroupAlgebraScalar C ψ g)

368 (x := Finsupp.single h 1))

369 rw [hsmul] at hzero'

370 exact sub_eq_zero.mp hzero'

371

372omit [IsTopologicalGroup G] in

373/--

374Commutator formula for the separated universal differential when the right factor lies in the

375kernel of the target homomorphism.

376-/

377theorem zcSeparatedUniversalDifferential_commutator_right_kernel

378 (g h : G) (hh : ψ h = 1) :

379 zcSeparatedUniversalDifferential C ψ ⁅g, h⁆ =

380 (zcGroupLike C H (ψ g) - 1) •

381 zcSeparatedUniversalDifferential C ψ h := by

382 let δ := zcSeparatedUniversalDifferential C ψ

383 let coeff := zcCompletedGroupAlgebraScalar C ψ

384 have hcomm := (zcSeparatedUniversalDifferential C ψ).map_commutator g h

385 have hconj : ψ (g * h * g⁻¹) = 1 := by

386 simp only [map_mul, hh, mul_one, map_inv, mul_inv_cancel]

387 have hcommKer : ψ ⁅g, h⁆ = 1 := by

388 simp only [commutatorElement_def, map_mul, hh, mul_one, map_inv, mul_inv_cancel, inv_one]

389 calc

390 δ ⁅g, h⁆ =

391 δ g + zcGroupLike C H (ψ g) • δ h - δ g - δ h := by

392 simpa only [δ, coeff, zcCompletedGroupAlgebraScalar_apply, hconj,

393 hcommKer, map_one, one_smul] using hcomm

394 _ = zcGroupLike C H (ψ g) • δ h - δ h := by

395 abel

396 _ = (zcGroupLike C H (ψ g) - 1) • δ h := by

397 rw [sub_smul, one_smul]

398

399omit [IsTopologicalGroup G] in

400/--

401A representative is zero in the separated quotient exactly when all finite reductions are finite

402crossed-differential relations.

403-/

404theorem zcSeparatedCompletedDifferentialModule_mk_eq_zero_iff

405 {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}

406 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G} :

407 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x =

408 (0 : ZCSeparatedCompletedDifferentialModule C ψ) ↔

409 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

410 zcCompletedDifferentialModulePreStageMap C ψ i x ∈

411 crossedDifferentialRelationSubmodule

412 (zcCompletedDifferentialModuleStageScalar C ψ i) := by

413 constructor

414 · intro hx

415 exact

416 (mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff (C := C) (ψ := ψ) (x := x)).1

417 ((Submodule.Quotient.mk_eq_zero

418 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

419 (x := x)).1 hx)

420 · intro hx

421 exact

422 (Submodule.Quotient.mk_eq_zero

423 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

424 (x := x)).2

425 ((mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff (C := C) (ψ := ψ) (x

426 := x)).2 hx)

427

428/-- Finite-stage projection from the separated completed quotient. -/

429def zcSeparatedCompletedDifferentialModuleStageProjectionAdd

430 (i : ZCCompletedDifferentialModuleIndex C ψ) :

431 ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]

432 ZCCompletedDifferentialModuleStage C ψ i :=

433 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).liftQ

434 (crossedDifferentialModuleLiftLinear

435 (R := ZCCompletedGroupAlgebra C H)

436 (zcCompletedDifferentialModuleStageDifferential C ψ i))

437 (by

438 intro x hx

439 rw [LinearMap.mem_ker]

440 have hxstage :

441 zcCompletedDifferentialModulePreStageMap C ψ i x ∈

442 crossedDifferentialRelationSubmodule

443 (zcCompletedDifferentialModuleStageScalar C ψ i) :=

444 (mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff (C := C) (ψ := ψ) (x :=

445 x)).1

446 (by

447 simpa [zcCompletedDifferentialRelationFiniteClosedSubmodule] using hx) i

448 have hq :

449 (crossedDifferentialRelationSubmodule

450 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

451 (zcCompletedDifferentialModulePreStageMap C ψ i x) = 0 :=

452 (Submodule.Quotient.mk_eq_zero

453 (p := crossedDifferentialRelationSubmodule

454 (zcCompletedDifferentialModuleStageScalar C ψ i))

455 (x := zcCompletedDifferentialModulePreStageMap C ψ i x)).2 hxstage

456 rw [zcCompletedDifferentialModulePreStageMap_mkQ] at hq

457 exact hq)

458

459omit [IsTopologicalGroup G] in

460/--

461The separated finite-stage projection of a quotient representative is the finite-stage

462crossed-differential lift of that representative.

463-/

464@[simp]

465theorem zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ

466 (i : ZCCompletedDifferentialModuleIndex C ψ)

467 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :

468 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i

469 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x) =

470 crossedDifferentialModuleLiftLinear

471 (R := ZCCompletedGroupAlgebra C H)

472 (zcCompletedDifferentialModuleStageDifferential C ψ i) x := by

473 rw [zcSeparatedCompletedDifferentialModuleStageProjectionAdd, Submodule.mkQ_apply,

474 Submodule.liftQ_apply]

475

476omit [IsTopologicalGroup G] in

477/--

478The separated finite-stage projection sends the separated universal differential to the

479corresponding finite-stage differential.

480-/

481@[simp]

482theorem zcSeparatedCompletedDifferentialModuleStageProjectionAdd_universal

483 (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :

484 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i

485 (zcSeparatedUniversalDifferential C ψ g) =

486 zcCompletedDifferentialModuleStageDifferential C ψ i g := by

487 change

488 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i

489 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

490 (Finsupp.single g 1)) =

491 zcCompletedDifferentialModuleStageDifferential C ψ i g

492 rw [zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ]

493 simp only [crossedDifferentialModuleLiftLinear_single, one_smul]

494

495/-- The product of all finite-stage projections from the separated completed quotient. -/

496def zcSeparatedCompletedDifferentialModuleStageProjectionProduct :

497 ZCSeparatedCompletedDifferentialModule C ψ →

498 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

499 ZCCompletedDifferentialModuleStage C ψ i :=

500 fun a i => zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a

501

502omit [IsTopologicalGroup G] in

503/--

504The product projection from the separated completed differential module evaluates at `i` as its

505additive stage projection.

506-/

507@[simp]

508theorem zcSeparatedCompletedDifferentialModuleStageProjectionProduct_apply

509 (a : ZCSeparatedCompletedDifferentialModule C ψ)

510 (i : ZCCompletedDifferentialModuleIndex C ψ) :

511 zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ a i =

512 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a :=

513 rfl

514

515omit [IsTopologicalGroup G] in

516/-- The finite-stage projections separate points of the separated completed quotient. -/

517theorem zcSeparatedCompletedDifferentialModuleStageProjectionsSeparate :

518 ∀ x : ZCSeparatedCompletedDifferentialModule C ψ,

519 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,

520 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x = 0) →

521 x = 0 := by

522 intro x

523 refine Submodule.Quotient.induction_on

524 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

525 (C := fun x =>

526 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,

527 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x = 0) →

528 x = 0)

529 x ?_

530 intro y hy

531 apply

532 (Submodule.Quotient.mk_eq_zero

533 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

534 (x := y)).2

535 exact

536 (mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff (C := C) (ψ := ψ) (x := y)).2

537 (by

538 intro i

539 have hlin :

540 crossedDifferentialModuleLiftLinear

541 (R := ZCCompletedGroupAlgebra C H)

542 (zcCompletedDifferentialModuleStageDifferential C ψ i) y = 0 := by

543 have hyi := hy i

544 change zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i

545 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ y) = 0 at hyi

546 rw [zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ] at hyi

547 exact hyi

548 have hq :

549 (crossedDifferentialRelationSubmodule

550 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

551 (zcCompletedDifferentialModulePreStageMap C ψ i y) = 0 := by

552 rw [zcCompletedDifferentialModulePreStageMap_mkQ]

553 exact hlin

554 exact

555 (Submodule.Quotient.mk_eq_zero

556 (p := crossedDifferentialRelationSubmodule

557 (zcCompletedDifferentialModuleStageScalar C ψ i))

558 (x := zcCompletedDifferentialModulePreStageMap C ψ i y)).1 hq)

559

560omit [IsTopologicalGroup G] in

561/-- The finite-stage projection product is injective on the separated completed quotient. -/

562theorem zcSeparatedCompletedDifferentialModuleStageProjectionProduct_injective :

563 Function.Injective

564 (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) := by

565 intro x y hxy

566 apply sub_eq_zero.mp

567 apply zcSeparatedCompletedDifferentialModuleStageProjectionsSeparate C ψ

568 intro i

569 have hi :

570 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x =

571 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i y := by

572 simpa [zcSeparatedCompletedDifferentialModuleStageProjectionProduct] using congrFun hxy i

573 rw [map_sub, hi, sub_self]

574

575omit [IsTopologicalGroup G] in

576/-- Extensionality for the separated completed quotient by finite-stage projections. -/

577theorem zcSeparatedCompletedDifferentialModuleStageProjection_ext

578 {a b : ZCSeparatedCompletedDifferentialModule C ψ}

579 (h : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

580 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a =

581 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i b) :

582 a = b :=

583 zcSeparatedCompletedDifferentialModuleStageProjectionProduct_injective C ψ

584 (funext h)

585

586/-- The natural map from the algebraic quotient to the finite-stage separated quotient. -/

587def zcCompletedDifferentialModuleToSeparated :

588 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]

589 ZCSeparatedCompletedDifferentialModule C ψ :=

590 (crossedDifferentialRelationSubmodule

591 (zcCompletedGroupAlgebraScalar C ψ)).liftQ

592 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

593 (by

594 intro x hx

595 rw [LinearMap.mem_ker]

596 exact

597 (Submodule.Quotient.mk_eq_zero

598 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

599 (x := x)).2

600 (crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule C ψ hx))

601

602omit [IsTopologicalGroup G] in

603/--

604The quotient map to the separated completed module sends the universal differential to the

605separated universal differential.

606-/

607@[simp]

608theorem zcCompletedDifferentialModuleToSeparated_universal (g : G) :

609 zcCompletedDifferentialModuleToSeparated C ψ

610 (zcUniversalDifferential C ψ g) =

611 zcSeparatedUniversalDifferential C ψ g := by

612 change

613 zcCompletedDifferentialModuleToSeparated C ψ

614 ((crossedDifferentialRelationSubmodule

615 (zcCompletedGroupAlgebraScalar C ψ)).mkQ (Finsupp.single g 1)) =

616 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

617 (Finsupp.single g 1)

618 rw [zcCompletedDifferentialModuleToSeparated, Submodule.mkQ_apply,

619 Submodule.liftQ_apply]

620

621omit [IsTopologicalGroup G] in

622/--

623The pre-quotient completed boundary kills the finite-stage closed relation submodule. This is

624the descent input for the separated boundary \(A_{\psi}(C)_{\mathrm{sep}} \to

625\mathbb{Z}_C\llbracket H\rrbracket\).

626-/

627theorem crossedDifferentialBoundaryLiftLinear_kills_finiteClosedSubmodule

628 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

629 (ψc : ContinuousMonoidHom G H)

630 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}

631 (hx : x ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψc.toMonoidHom) :

632 crossedDifferentialModuleLiftLinear

633 (R := ZCCompletedGroupAlgebra C H)

634 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x = 0 := by

635 apply zcCompletedGroupAlgebraProjection_ext

636 intro j

637 let i := zcCompletedDifferentialModuleComapIndex C hC ψc j

638 have hxall :

639 ∀ i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom,

640 zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x ∈

641 crossedDifferentialRelationSubmodule

642 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i) := by

643 rw [zcCompletedDifferentialRelationFiniteClosedSubmodule] at hx

644 exact

645 (mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff (C := C) (ψ :=

646 ψc.toMonoidHom) (x := x)).1 hx

647 have hxstage :

648 zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x ∈

649 crossedDifferentialRelationSubmodule

650 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i) :=

651 hxall i

652 have hstage_zero :

653 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i

654 ((crossedDifferentialRelationSubmodule

655 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ

656 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) = 0 := by

657 have hq :

658 (crossedDifferentialRelationSubmodule

659 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ

660 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x) = 0 :=

661 (Submodule.Quotient.mk_eq_zero

662 (p := crossedDifferentialRelationSubmodule

663 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i))

664 (x := zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)).2 hxstage

665 rw [hq, map_zero]

666 have hcompat :=

667 congrArg

668 (fun f =>

669 f

670 ((crossedDifferentialRelationSubmodule

671 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x))

672 (zcDiffModuleStageBoundaryCompletedLinearMap_comp_stageProj

673 C ψc.toMonoidHom i)

674 have hstage_proj :

675 zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i

676 ((crossedDifferentialRelationSubmodule

677 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x) =

678 (crossedDifferentialRelationSubmodule

679 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ

680 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x) := by

681 rw [zcCompletedDifferentialModuleStageProjection_mkQ]

682 exact

683 (zcCompletedDifferentialModulePreStageMap_mkQ

684 C ψc.toMonoidHom i x).symm

685 have hboundary_quot :

686 zcToCompletedGroupAlgebra C ψc.toMonoidHom

687 ((crossedDifferentialRelationSubmodule

688 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x) =

689 crossedDifferentialModuleLiftLinear

690 (R := ZCCompletedGroupAlgebra C H)

691 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x := by

692 rfl

693 have hproj_eq :

694 zcCompletedGroupAlgebraProjection C H j

695 (crossedDifferentialModuleLiftLinear

696 (R := ZCCompletedGroupAlgebra C H)

697 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x) =

698 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i

699 ((crossedDifferentialRelationSubmodule

700 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ

701 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) := by

702 calc

703 zcCompletedGroupAlgebraProjection C H j

704 (crossedDifferentialModuleLiftLinear

705 (R := ZCCompletedGroupAlgebra C H)

706 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x) =

707 zcCompletedGroupAlgebraProjection C H i.target

708 (zcToCompletedGroupAlgebra C ψc.toMonoidHom

709 ((crossedDifferentialRelationSubmodule

710 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x)) := by

711 rw [hboundary_quot]

712 simp only [ContinuousMonoidHom.coe_toMonoidHom,

713 zcCompletedDifferentialModuleComapIndex, i]

714 _ =

715 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i

716 (zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i

717 ((crossedDifferentialRelationSubmodule

718 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x)) := by

719 change

720 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i

721 (zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i

722 ((crossedDifferentialRelationSubmodule

723 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x)) =

724 zcCompletedGroupAlgebraProjectionLinearMap C H i.target

725 (zcToCompletedGroupAlgebra C ψc.toMonoidHom

726 ((crossedDifferentialRelationSubmodule

727 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x))

728 at hcompat

729 exact hcompat.symm

730 _ =

731 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i

732 ((crossedDifferentialRelationSubmodule

733 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ

734 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) := by

735 rw [hstage_proj]

736 rw [hproj_eq, hstage_zero]

737 simp only [zcCompletedGroupAlgebraProjection_zero]

738 rfl

739

740/-- The completed boundary descends to the separated completed differential module. -/

741def zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra

742 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

743 (ψc : ContinuousMonoidHom G H) :

744 ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]

745 ZCCompletedGroupAlgebra C H :=

746 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψc.toMonoidHom).liftQ

747 (crossedDifferentialModuleLiftLinear

748 (R := ZCCompletedGroupAlgebra C H)

749 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom))

750 (by

751 intro x hx

752 rw [LinearMap.mem_ker]

753 exact crossedDifferentialBoundaryLiftLinear_kills_finiteClosedSubmodule

754 C hC ψc hx)

755

756omit [IsTopologicalGroup G] in

757/--

758The universal completed Fox map from the separated completed differential module to the

759completed group algebra is characterized by finite-stage Fox coordinate formulas.

760-/

761@[simp]

762theorem zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_universal

763 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

764 (ψc : ContinuousMonoidHom G H)

765 (g : G) :

766 zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC ψc

767 (zcSeparatedUniversalDifferential C ψc.toMonoidHom g) =

768 zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom g := by

769 change

770 zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC ψc

771 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψc.toMonoidHom).mkQ

772 (Finsupp.single g 1)) =

773 zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom g

774 rw [zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra,

775 Submodule.mkQ_apply, Submodule.liftQ_apply]

776 simp only [ContinuousMonoidHom.coe_toMonoidHom,

777 crossedDifferentialModuleLiftLinear_single, one_smul]

778

779omit [IsTopologicalGroup G] in

780/--

781The completed Fox map to the completed group algebra agrees with the separated quotient map on

782finite-stage coordinates.

783-/

784theorem zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_comp_toSeparated

785 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

786 (ψc : ContinuousMonoidHom G H) :

787 (zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC ψc).comp

788 (zcCompletedDifferentialModuleToSeparated C ψc.toMonoidHom) =

789 zcToCompletedGroupAlgebra C ψc.toMonoidHom := by

790 apply crossedDifferentialModuleHom_ext

791 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)

792 intro g

793 change

794 zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC ψc

795 (zcCompletedDifferentialModuleToSeparated C ψc.toMonoidHom

796 (zcUniversalDifferential C ψc.toMonoidHom g)) =

797 zcToCompletedGroupAlgebra C ψc.toMonoidHom

798 (zcUniversalDifferential C ψc.toMonoidHom g)

799 rw [zcCompletedDifferentialModuleToSeparated_universal,

800 zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_universal,

801 zcToCompletedGroupAlgebra_universal]

802

803/--

804Algebraic relation-reflection form of finite-stage separation: if every finite source, target,

805and coefficient reduction of a completed pre-module element is a finite crossed-differential

806relation, then the original element is already in the raw completed crossed-differential

807relation submodule. This is an algebraic compatibility predicate for the

808\(\mathbb{Z}_C\)-completed differential module, not an input for the final separated profinite

809Crowell middle term.

810-/

811def zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations : Prop :=

812 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,

813 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,

814 zcCompletedDifferentialModulePreStageMap C ψ i x ∈

815 crossedDifferentialRelationSubmodule

816 (zcCompletedDifferentialModuleStageScalar C ψ i)) →

817 x ∈ crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)

818

819/--

820The finite-stage topology on the completed pre-module, before quotienting by the

821crossed-differential relations.

822-/

823@[implicit_reducible]

824def zcCompletedDifferentialPreModuleNaturalTopology :

825 TopologicalSpace (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

826 TopologicalSpace.induced

827 (zcCompletedDifferentialPreModuleStageFamilyMap C ψ) inferInstance

828

829omit [IsTopologicalGroup G] in

830/--

831Each finite pre-stage reduction is continuous for the finite-stage topology on the completed

832pre-module.

833-/

834theorem continuous_zcCompletedDifferentialModulePreStageMap_naturalTopology

835 (i : ZCCompletedDifferentialModuleIndex C ψ) :

836 @Continuous

837 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

838 (CrossedDifferentialPreModule

839 (zcCompletedDifferentialModuleStageRing C ψ i)

840 (zcCompletedDifferentialModuleStageSource C ψ i))

841 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

842 (⊥ : TopologicalSpace

843 (CrossedDifferentialPreModule

844 (zcCompletedDifferentialModuleStageRing C ψ i)

845 (zcCompletedDifferentialModuleStageSource C ψ i)))

846 (zcCompletedDifferentialModulePreStageMap C ψ i) := by

847 letI : TopologicalSpace

848 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

849 zcCompletedDifferentialPreModuleNaturalTopology C ψ

850 let S := zcCompletedDifferentialPreModuleStageSystem C ψ

851 have hfamily :

852 @Continuous

853 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

854 (ZCCompletedDifferentialPreModuleStageFamily C ψ)

855 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

856 inferInstance

857 (zcCompletedDifferentialPreModuleStageFamilyMap C ψ) :=

858 continuous_induced_dom

859 have hproj := (S.continuous_projection i).comp hfamily

860 change

861 @Continuous

862 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

863 (CrossedDifferentialPreModule

864 (zcCompletedDifferentialModuleStageRing C ψ i)

865 (zcCompletedDifferentialModuleStageSource C ψ i))

866 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) ⊥

867 (zcCompletedDifferentialModulePreStageMap C ψ i) at hproj

868 exact hproj

869

870/--

871The separated completed module carries the quotient topology induced from the finite-stage

872topology on the completed pre-module.

873-/

874@[implicit_reducible]

875def zcSeparatedCompletedDifferentialModuleNaturalTopology :

876 TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

877 TopologicalSpace.coinduced

878 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

879 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

880

881omit [IsTopologicalGroup G] in

882/--

883The quotient map to the separated completed module is continuous for the finite-stage pre-module

884topology and the separated quotient topology.

885-/

886theorem continuous_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology :

887 @Continuous

888 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

889 (ZCSeparatedCompletedDifferentialModule C ψ)

890 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

891 (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)

892 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ :=

893 continuous_coinduced_rng

894

895omit [IsTopologicalGroup G] in

896/--

897The quotient map defining the separated completed module is a quotient map for the finite-stage

898pre-module topology.

899-/

900theorem isQuotientMap_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology :

901 letI : TopologicalSpace

902 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

903 zcCompletedDifferentialPreModuleNaturalTopology C ψ

904 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

905 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

906 Topology.IsQuotientMap (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ := by

907 letI : TopologicalSpace

908 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

909 zcCompletedDifferentialPreModuleNaturalTopology C ψ

910 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

911 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

912 rw [Topology.isQuotientMap_iff]

913 constructor

914 · exact ⟨rfl⟩

915 · exact

916 Submodule.Quotient.mk_surjective

917 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

918

919omit [IsTopologicalGroup G] in

920/--

921Continuity out of the separated completed module can be tested after precomposing with the

922defining quotient map.

923-/

924theorem continuous_zcSeparatedCompletedDifferentialModule_iff_comp_mkQ

925 {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}

926 {A : Type u} [TopologicalSpace A]

927 {f : ZCSeparatedCompletedDifferentialModule C ψ → A} :

928 @Continuous

929 (ZCSeparatedCompletedDifferentialModule C ψ) A

930 (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ) inferInstance f ↔

931 @Continuous

932 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) A

933 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance

934 (fun x => f ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x)) := by

935 letI : TopologicalSpace

936 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

937 zcCompletedDifferentialPreModuleNaturalTopology C ψ

938 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

939 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

940 simpa [Function.comp_def] using

941 (isQuotientMap_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology

942 C ψ).continuous_iff (g := f)

943

944omit [IsTopologicalGroup G] in

945/--

946Each finite-stage projection from the separated completed quotient is continuous for the

947separated quotient topology.

948-/

949theorem continuous_zcSepDiffModuleStageProjAdd_naturalTopology

950 (i : ZCCompletedDifferentialModuleIndex C ψ) :

951 @Continuous

952 (ZCSeparatedCompletedDifferentialModule C ψ)

953 (ZCCompletedDifferentialModuleStage C ψ i)

954 (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)

955 inferInstance

956 (zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i) := by

957 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

958 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

959 letI : TopologicalSpace

960 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

961 zcCompletedDifferentialPreModuleNaturalTopology C ψ

962 rw [continuous_coinduced_dom]

963 change

964 @Continuous

965 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

966 (ZCCompletedDifferentialModuleStage C ψ i)

967 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

968 inferInstance

969 (fun x =>

970 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i

971 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x))

972 letI : TopologicalSpace

973 (CrossedDifferentialPreModule

974 (zcCompletedDifferentialModuleStageRing C ψ i)

975 (zcCompletedDifferentialModuleStageSource C ψ i)) :=

976 ⊥

977 letI : DiscreteTopology

978 (CrossedDifferentialPreModule

979 (zcCompletedDifferentialModuleStageRing C ψ i)

980 (zcCompletedDifferentialModuleStageSource C ψ i)) :=

981 ⟨rfl⟩

982 have hpre :

983 @Continuous

984 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

985 (CrossedDifferentialPreModule

986 (zcCompletedDifferentialModuleStageRing C ψ i)

987 (zcCompletedDifferentialModuleStageSource C ψ i))

988 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

989 inferInstance

990 (zcCompletedDifferentialModulePreStageMap C ψ i) :=

991 continuous_zcCompletedDifferentialModulePreStageMap_naturalTopology C ψ i

992 letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance

993 letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance

994 have hq :

995 Continuous

996 (fun y :

997 CrossedDifferentialPreModule

998 (zcCompletedDifferentialModuleStageRing C ψ i)

999 (zcCompletedDifferentialModuleStageSource C ψ i) =>

1000 (crossedDifferentialRelationSubmodule

1001 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ y) :=

1002 continuous_of_discreteTopology

1003 have hcoord :

1004 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

1005 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i

1006 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x)) =

1007 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

1008 (crossedDifferentialRelationSubmodule

1009 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

1010 (zcCompletedDifferentialModulePreStageMap C ψ i x)) := by

1011 funext x

1012 rw [zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ,

1013 ← zcCompletedDifferentialModulePreStageMap_mkQ]

1014 rw [hcoord]

1015 exact hq.comp hpre

1016

1017omit [IsTopologicalGroup G] in

1018/--

1019The separated finite-stage projection product is continuous for the separated quotient topology.

1020-/

1021theorem continuous_zcSepDiffModuleStageProjProduct_naturalTopology :

1022 @Continuous

1023 (ZCSeparatedCompletedDifferentialModule C ψ)

1024 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,

1025 ZCCompletedDifferentialModuleStage C ψ i)

1026 (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)

1027 inferInstance

1028 (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) := by

1029 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

1030 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

1031 exact

1032 continuous_pi fun i =>

1033 by

1034 simpa [zcSeparatedCompletedDifferentialModuleStageProjectionProduct] using

1035 continuous_zcSepDiffModuleStageProjAdd_naturalTopology C ψ i

1036

1037omit [IsTopologicalGroup G] in

1038/--

1039The separated completed quotient is Hausdorff for the separated finite-stage quotient topology.

1040-/

1041theorem t2Space_zcSeparatedCompletedDifferentialModuleNaturalTopology :

1042 @T2Space

1043 (ZCSeparatedCompletedDifferentialModule C ψ)

1044 (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ) := by

1045 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

1046 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

1047 exact T2Space.of_injective_continuous

1048 (zcSeparatedCompletedDifferentialModuleStageProjectionProduct_injective C ψ)

1049 (continuous_zcSepDiffModuleStageProjProduct_naturalTopology C ψ)

1050

1051omit [IsTopologicalGroup G] in

1052/--

1053In the directed finite-stage situation, the separated quotient topology is exactly the topology

1054induced by all finite-stage separated projections.

1055-/

1056theorem zcSepDiffModuleNaturalTopology_eq_induced_stageProjProduct

1057 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

1058 (hdir : Directed (· ≤ ·)

1059 (id : ZCCompletedDifferentialModuleIndex C ψ →

1060 ZCCompletedDifferentialModuleIndex C ψ)) :

1061 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ =

1062 TopologicalSpace.induced

1063 (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstance := by

1064 ext U

1065 constructor

1066 · intro hU

1067 let Tind : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

1068 TopologicalSpace.induced

1069 (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstance

1070 rw [@isOpen_iff_forall_mem_open

1071 (ZCSeparatedCompletedDifferentialModule C ψ) Tind U]

1072 intro x hxU

1073 refine Submodule.Quotient.induction_on

1074 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

1075 (C := fun x =>

1076 x ∈ U → ∃ t, t ⊆ U ∧ @IsOpen

1077 (ZCSeparatedCompletedDifferentialModule C ψ) Tind t ∧ x ∈ t)

1078 x ?_ hxU

1079 intro a haU

1080 let q :

1081 CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G →

1082 ZCSeparatedCompletedDifferentialModule C ψ :=

1083 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

1084 have hpreOpen :

1085 @IsOpen

1086 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1087 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1088 (q ⁻¹' U) := by

1089 change

1090 @IsOpen

1091 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1092 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1093 (q ⁻¹' U) at hU

1094 exact hU

1095 rcases isOpen_induced_iff.mp hpreOpen with ⟨V, hVopen, hVeq⟩

1096 have haV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ a ∈ V := by

1097 have haU' : a ∈ q ⁻¹' U := haU

1098 rwa [← hVeq] at haU'

1099 let S := zcCompletedDifferentialPreModuleStageSystem C ψ

1100 rcases S.exists_projection_preimage_subset hdir hVopen haV with

1101 ⟨i, W, hWopen, haW, hWV⟩

1102 let t : Set (ZCSeparatedCompletedDifferentialModule C ψ) :=

1103 {z | zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i z =

1104 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q a)}

1105 refine ⟨t, ?_, ?_, ?_⟩

1106 · intro z hz

1107 refine Submodule.Quotient.induction_on

1108 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

1109 (C := fun z => z ∈ t → z ∈ U) z ?_ hz

1110 intro b hb

1111 have hcoord :

1112 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q b) =

1113 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q a) := hb

1114 have hstageRel :

1115 zcCompletedDifferentialModulePreStageMap C ψ i (b - a) ∈

1116 crossedDifferentialRelationSubmodule

1117 (zcCompletedDifferentialModuleStageScalar C ψ i) := by

1118 apply (Submodule.Quotient.mk_eq_zero

1119 (p := crossedDifferentialRelationSubmodule

1120 (zcCompletedDifferentialModuleStageScalar C ψ i))

1121 (x := zcCompletedDifferentialModulePreStageMap C ψ i (b - a))).1

1122 have hq :

1123 (crossedDifferentialRelationSubmodule

1124 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

1125 (zcCompletedDifferentialModulePreStageMap C ψ i (b - a)) = 0 := by

1126 have hbq :

1127 (crossedDifferentialRelationSubmodule

1128 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

1129 (zcCompletedDifferentialModulePreStageMap C ψ i b) =

1130 (crossedDifferentialRelationSubmodule

1131 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

1132 (zcCompletedDifferentialModulePreStageMap C ψ i a) := by

1133 change

1134 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i

1135 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ b) =

1136 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i

1137 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ a)

1138 at hcoord

1139 rw [zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ,

1140 zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ] at hcoord

1141 rw [zcCompletedDifferentialModulePreStageMap_mkQ,

1142 zcCompletedDifferentialModulePreStageMap_mkQ]

1143 exact hcoord

1144 have hzero :

1145 (crossedDifferentialRelationSubmodule

1146 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

1147 (zcCompletedDifferentialModulePreStageMap C ψ i b) -

1148 (crossedDifferentialRelationSubmodule

1149 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

1150 (zcCompletedDifferentialModulePreStageMap C ψ i a) = 0 :=

1151 sub_eq_zero.mpr hbq

1152 simpa [map_sub] using hzero

1153 exact hq

1154 rcases zcCompletedDifferentialModulePreStageMap_relationSubmodule_surjective

1155 C ψ i hstageRel with

1156 ⟨r, hr, hrstage⟩

1157 have hqa : q (b - r) = q b := by

1158 have hrclosed : r ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ :=

1159 crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule C ψ hr

1160 apply (Submodule.Quotient.eq

1161 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)).2

1162 change (b - r) - b ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ

1163 have hdiff : (b - r) - b = -r := by

1164 abel

1165 rw [hdiff]

1166 exact (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).neg_mem hrclosed

1167 have hpre_eq :

1168 zcCompletedDifferentialModulePreStageMap C ψ i (b - r) =

1169 zcCompletedDifferentialModulePreStageMap C ψ i a := by

1170 have hcalc :

1171 zcCompletedDifferentialModulePreStageMap C ψ i (b - a) =

1172 zcCompletedDifferentialModulePreStageMap C ψ i r := hrstage.symm

1173 have hsub :

1174 zcCompletedDifferentialModulePreStageMap C ψ i b -

1175 zcCompletedDifferentialModulePreStageMap C ψ i a =

1176 zcCompletedDifferentialModulePreStageMap C ψ i r := by

1177 simpa [map_sub] using hcalc

1178 rw [map_sub]

1179 rw [← hsub]

1180 abel

1181 have hbW : S.projection i

1182 (zcCompletedDifferentialPreModuleStageFamilyMap C ψ (b - r)) ∈ W := by

1183 change zcCompletedDifferentialModulePreStageMap C ψ i (b - r) ∈ W

1184 rw [hpre_eq]

1185 change zcCompletedDifferentialModulePreStageMap C ψ i a ∈ W at haW

1186 exact haW

1187 have hbV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ (b - r) ∈ V := hWV hbW

1188 have hbU : q (b - r) ∈ U := by

1189 have hbV' :

1190 (b - r) ∈ zcCompletedDifferentialPreModuleStageFamilyMap C ψ ⁻¹' V := hbV

1191 rwa [hVeq] at hbV'

1192 rwa [hqa] at hbU

1193 · letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) := Tind

1194 have hprod :

1195 Continuous (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) :=

1196 continuous_induced_dom

1197 have hcoord :

1198 Continuous (fun z : ZCSeparatedCompletedDifferentialModule C ψ =>

1199 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i z) := by

1200 have hi := (continuous_apply i).comp hprod

1201 change

1202 Continuous

1203 (zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i) at hi

1204 exact hi

1205 haveI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance

1206 exact (isOpen_discrete

1207 ({zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q a)} :

1208 Set (ZCCompletedDifferentialModuleStage C ψ i))).preimage hcoord

1209 · exact rfl

1210 · intro hU

1211 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

1212 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

1213 rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVU⟩

1214 rw [← hVU]

1215 exact hVopen.preimage

1216 (continuous_zcSepDiffModuleStageProjProduct_naturalTopology C ψ)

1217

1218/--

1219The pre-module generator map g \(\mapsto\) dg is continuous for the finite-stage pre-module

1220topology.

1221-/

1222theorem continuous_zcCompletedDifferentialPreModule_single_one_naturalTopology :

1223 @Continuous G

1224 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1225 inferInstance

1226 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1227 (fun g : G => Finsupp.single g (1 : ZCCompletedGroupAlgebra C H)) := by

1228 rw [continuous_induced_rng]

1229 let S := zcCompletedDifferentialPreModuleStageSystem C ψ

1230 let preSingle :

1231 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

1232 G →

1233 CrossedDifferentialPreModule

1234 (zcCompletedDifferentialModuleStageRing C ψ i)

1235 (zcCompletedDifferentialModuleStageSource C ψ i) := fun i g =>

1236 zcCompletedDifferentialModulePreStageMap C ψ i

1237 (Finsupp.single g (1 : ZCCompletedGroupAlgebra C H))

1238 have hpreSingle_continuous :

1239 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

1240 @Continuous G

1241 (CrossedDifferentialPreModule

1242 (zcCompletedDifferentialModuleStageRing C ψ i)

1243 (zcCompletedDifferentialModuleStageSource C ψ i))

1244 inferInstance

1245 ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)

1246 (preSingle i) := by

1247 intro i

1248 have hsource :

1249 Continuous (zcCompletedDifferentialModuleStageSourceProj C ψ i) := by

1250 exact QuotientGroup.continuous_mk

1251 have hsingle :

1252 @Continuous

1253 (zcCompletedDifferentialModuleStageSource C ψ i)

1254 (CrossedDifferentialPreModule

1255 (zcCompletedDifferentialModuleStageRing C ψ i)

1256 (zcCompletedDifferentialModuleStageSource C ψ i))

1257 inferInstance

1258 ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)

1259 (fun q => Finsupp.single q

1260 (1 : zcCompletedDifferentialModuleStageRing C ψ i)) :=

1261 @continuous_of_discreteTopology

1262 (zcCompletedDifferentialModuleStageSource C ψ i)

1263 inferInstance inferInstance

1264 (CrossedDifferentialPreModule

1265 (zcCompletedDifferentialModuleStageRing C ψ i)

1266 (zcCompletedDifferentialModuleStageSource C ψ i))

1267 ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)

1268 (fun q => Finsupp.single q

1269 (1 : zcCompletedDifferentialModuleStageRing C ψ i))

1270 have hcomp :

1271 @Continuous G

1272 (CrossedDifferentialPreModule

1273 (zcCompletedDifferentialModuleStageRing C ψ i)

1274 (zcCompletedDifferentialModuleStageSource C ψ i))

1275 inferInstance

1276 ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)

1277 ((fun q => Finsupp.single q

1278 (1 : zcCompletedDifferentialModuleStageRing C ψ i)) ∘

1279 zcCompletedDifferentialModuleStageSourceProj C ψ i) :=

1280 @Continuous.comp

1281 G

1282 (zcCompletedDifferentialModuleStageSource C ψ i)

1283 (CrossedDifferentialPreModule

1284 (zcCompletedDifferentialModuleStageRing C ψ i)

1285 (zcCompletedDifferentialModuleStageSource C ψ i))

1286 inferInstance inferInstance

1287 ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)

1288 (f := zcCompletedDifferentialModuleStageSourceProj C ψ i)

1289 (g := fun q => Finsupp.single q

1290 (1 : zcCompletedDifferentialModuleStageRing C ψ i))

1291 hsingle hsource

1292 have hfun :

1293 ((fun q => Finsupp.single q

1294 (1 : zcCompletedDifferentialModuleStageRing C ψ i)) ∘

1295 zcCompletedDifferentialModuleStageSourceProj C ψ i) =

1296 preSingle i := by

1297 funext g

1298 simp only [Function.comp_apply, preSingle,

1299 zcCompletedDifferentialModulePreStageMap_single,

1300 zcCompletedGroupAlgebraProjection_one]

1301 exact hfun ▸ hcomp

1302 have hpreSingle_compat : S.CompatibleMaps preSingle := by

1303 intro i j hij

1304 funext g

1305 exact

1306 congrFun

1307 (zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap C ψ i j hij)

1308 (Finsupp.single g (1 : ZCCompletedGroupAlgebra C H))

1309 have hLift : Continuous (S.inverseLimitLift preSingle hpreSingle_compat) :=

1310 S.continuous_inverseLimitLift preSingle hpreSingle_continuous hpreSingle_compat

1311 have hEq :

1312 zcCompletedDifferentialPreModuleStageFamilyMap C ψ ∘

1313 (fun g : G => Finsupp.single g (1 : ZCCompletedGroupAlgebra C H)) =

1314 S.inverseLimitLift preSingle hpreSingle_compat := by

1315 apply S.inverseLimitLift_unique preSingle hpreSingle_compat

1316 intro i

1317 funext g

1318 rfl

1319 rw [hEq]

1320 exact hLift

1321

1322/--

1323The separated universal differential is continuous for the separated finite-stage quotient

1324topology.

1325-/

1326theorem continuous_zcSeparatedUniversalDifferential_naturalTopology :

1327 @Continuous G

1328 (ZCSeparatedCompletedDifferentialModule C ψ)

1329 inferInstance

1330 (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)

1331 (zcSeparatedUniversalDifferential C ψ) := by

1332 letI : TopologicalSpace

1333 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1334 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1335 exact

1336 (continuous_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology C ψ).comp

1337 (continuous_zcCompletedDifferentialPreModule_single_one_naturalTopology C ψ)

1338

1339omit [IsTopologicalGroup G] in

1340/--

1341A pre-quotient linear lift is continuous for the finite-stage pre-module topology when it

1342factors through one finite pre-stage reduction. This is the standard way to discharge the

1343hprelift input in applications where the target data is already finite-stage.

1344-/

1345theorem continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor

1346 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

1347 [TopologicalSpace A]

1348 (delta : G → A)

1349 (i : ZCCompletedDifferentialModuleIndex C ψ)

1350 (L :

1351 CrossedDifferentialPreModule

1352 (zcCompletedDifferentialModuleStageRing C ψ i)

1353 (zcCompletedDifferentialModuleStageSource C ψ i) → A)

1354 (hfactor :

1355 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,

1356 crossedDifferentialModuleLiftLinear

1357 (R := ZCCompletedGroupAlgebra C H) delta x =

1358 L (zcCompletedDifferentialModulePreStageMap C ψ i x)) :

1359 @Continuous

1360 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1361 A

1362 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1363 inferInstance

1364 (crossedDifferentialModuleLiftLinear

1365 (R := ZCCompletedGroupAlgebra C H) delta) := by

1366 letI : TopologicalSpace

1367 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1368 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1369 letI : TopologicalSpace

1370 (CrossedDifferentialPreModule

1371 (zcCompletedDifferentialModuleStageRing C ψ i)

1372 (zcCompletedDifferentialModuleStageSource C ψ i)) :=

1373 ⊥

1374 letI : DiscreteTopology

1375 (CrossedDifferentialPreModule

1376 (zcCompletedDifferentialModuleStageRing C ψ i)

1377 (zcCompletedDifferentialModuleStageSource C ψ i)) :=

1378 ⟨rfl⟩

1379 have hpre :

1380 @Continuous

1381 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1382 (CrossedDifferentialPreModule

1383 (zcCompletedDifferentialModuleStageRing C ψ i)

1384 (zcCompletedDifferentialModuleStageSource C ψ i))

1385 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1386 inferInstance

1387 (zcCompletedDifferentialModulePreStageMap C ψ i) :=

1388 continuous_zcCompletedDifferentialModulePreStageMap_naturalTopology C ψ i

1389 have hL : Continuous L := continuous_of_discreteTopology

1390 have hfun :

1391 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

1392 crossedDifferentialModuleLiftLinear

1393 (R := ZCCompletedGroupAlgebra C H) delta x) =

1394 fun x => L (zcCompletedDifferentialModulePreStageMap C ψ i x) := by

1395 funext x

1396 exact hfactor x

1397 change

1398 @Continuous

1399 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1400 A

1401 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1402 inferInstance

1403 (fun x =>

1404 crossedDifferentialModuleLiftLinear

1405 (R := ZCCompletedGroupAlgebra C H) delta x)

1406 rw [hfun]

1407 exact hL.comp hpre

1408

1409omit [IsTopologicalGroup G] in

1410/--

1411The canonical lift to a finite differential-module stage is continuous for the finite-stage

1412pre-module topology.

1413-/

1414theorem continuous_crossedDifferentialModuleLiftLinear_stageDifferential

1415 (i : ZCCompletedDifferentialModuleIndex C ψ) :

1416 @Continuous

1417 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1418 (ZCCompletedDifferentialModuleStage C ψ i)

1419 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1420 inferInstance

1421 (crossedDifferentialModuleLiftLinear

1422 (R := ZCCompletedGroupAlgebra C H)

1423 (zcCompletedDifferentialModuleStageDifferential C ψ i)) := by

1424 exact

1425 continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor

1426 C ψ

1427 (zcCompletedDifferentialModuleStageDifferential C ψ i)

1428 i

1429 (fun y =>

1430 (crossedDifferentialRelationSubmodule

1431 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ y)

1432 (by

1433 intro x

1434 exact (zcCompletedDifferentialModulePreStageMap_mkQ C ψ i x).symm)

1435

1436/--

1437The raw algebraic crossed-differential relation submodule is closed for the finite-stage

1438topology on the completed pre-module. This closedness condition makes the algebraic quotient

1439separated; the separated quotient construction records this condition structurally.

1440-/

1441def zcCompletedDifferentialModuleRelationSubmoduleClosed : Prop :=

1442 @IsClosed

1443 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1444 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1445 ((crossedDifferentialRelationSubmodule

1446 (zcCompletedGroupAlgebraScalar C ψ) :

1447 Submodule (ZCCompletedGroupAlgebra C H)

1448 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set

1449 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))

1450

1451omit [IsTopologicalGroup G] in

1452/--

1453A useful non-circular closedness criterion. If a Hausdorff/\(T_1\) target receives an injective

1454linear map from the algebraic completed differential module, and the composite from the

1455completed pre-module is continuous for the finite-stage pre-module topology, then the defining

1456crossed-differential relation submodule is closed. In applications the target is usually a

1457finite coordinate module \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\). The formulation isolates

1458the real topological input: continuity of the pre-quotient coordinate map.

1459-/

1460theorem zcDiffModuleRelSubmoduleClosed_of_inj_continuous_comp_mkQ

1461 {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]

1462 [TopologicalSpace M] [T1Space M]

1463 (L :

1464 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] M)

1465 (hLinj : Function.Injective L)

1466 (hcont :

1467 @Continuous

1468 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1469 M

1470 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1471 inferInstance

1472 (fun x =>

1473 L

1474 ((crossedDifferentialRelationSubmodule

1475 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x))) :

1476 zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ := by

1477 letI : TopologicalSpace

1478 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1479 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1480 change IsClosed

1481 ((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :

1482 Submodule (ZCCompletedGroupAlgebra C H)

1483 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1484 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))

1485 have hpreimage :

1486 ((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :

1487 Submodule (ZCCompletedGroupAlgebra C H)

1488 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1489 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =

1490 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

1491 L

1492 ((crossedDifferentialRelationSubmodule

1493 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x)) ⁻¹' ({0} : Set M) := by

1494 ext x

1495 constructor

1496 · intro hx

1497 have hq :

1498 ((crossedDifferentialRelationSubmodule

1499 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x :

1500 ZCCompletedDifferentialModule C ψ) = 0 :=

1501 (Submodule.Quotient.mk_eq_zero

1502 (p := crossedDifferentialRelationSubmodule

1503 (zcCompletedGroupAlgebraScalar C ψ))

1504 (x := x)).2 hx

1505 change

1506 L

1507 ((crossedDifferentialRelationSubmodule

1508 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x) = 0

1509 rw [hq]

1510 exact map_zero L

1511 · intro hx

1512 have hq :

1513 ((crossedDifferentialRelationSubmodule

1514 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x :

1515 ZCCompletedDifferentialModule C ψ) = 0 := by

1516 apply hLinj

1517 simpa using hx

1518 exact

1519 (Submodule.Quotient.mk_eq_zero

1520 (p := crossedDifferentialRelationSubmodule

1521 (zcCompletedGroupAlgebraScalar C ψ))

1522 (x := x)).1 hq

1523 rw [hpreimage]

1524 exact isClosed_singleton.preimage hcont

1525

1526omit [IsTopologicalGroup G] in

1527/--

1528The quotient map from the completed pre-module to the algebraic quotient is continuous for the

1529finite-stage topologies.

1530-/

1531theorem continuous_zcCompletedDifferentialModule_mkQ_naturalTopology :

1532 @Continuous

1533 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1534 (ZCCompletedDifferentialModule C ψ)

1535 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1536 (zcCompletedDifferentialModuleNaturalTopology C ψ)

1537 (crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)).mkQ := by

1538 letI : TopologicalSpace

1539 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1540 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1541 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

1542 zcCompletedDifferentialModuleNaturalTopology C ψ

1543 rw [continuous_induced_rng]

1544 change Continuous

1545 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

1546 fun i : ZCCompletedDifferentialModuleIndex C ψ =>

1547 zcCompletedDifferentialModuleStageProjectionAdd C ψ i

1548 ((crossedDifferentialRelationSubmodule

1549 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x))

1550 refine continuous_pi fun i => ?_

1551 let S := zcCompletedDifferentialPreModuleStageSystem C ψ

1552 letI : TopologicalSpace

1553 (CrossedDifferentialPreModule

1554 (zcCompletedDifferentialModuleStageRing C ψ i)

1555 (zcCompletedDifferentialModuleStageSource C ψ i)) :=

1556 ⊥

1557 letI : DiscreteTopology

1558 (CrossedDifferentialPreModule

1559 (zcCompletedDifferentialModuleStageRing C ψ i)

1560 (zcCompletedDifferentialModuleStageSource C ψ i)) :=

1561 ⟨rfl⟩

1562 have hpre :

1563 @Continuous

1564 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1565 (CrossedDifferentialPreModule

1566 (zcCompletedDifferentialModuleStageRing C ψ i)

1567 (zcCompletedDifferentialModuleStageSource C ψ i))

1568 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance

1569 (zcCompletedDifferentialModulePreStageMap C ψ i) := by

1570 have hfamily :

1571 @Continuous

1572 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1573 (ZCCompletedDifferentialPreModuleStageFamily C ψ)

1574 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance

1575 (zcCompletedDifferentialPreModuleStageFamilyMap C ψ) :=

1576 continuous_induced_dom

1577 have hproj := (S.continuous_projection i).comp hfamily

1578 change

1579 @Continuous

1580 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1581 (CrossedDifferentialPreModule

1582 (zcCompletedDifferentialModuleStageRing C ψ i)

1583 (zcCompletedDifferentialModuleStageSource C ψ i))

1584 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance

1585 (zcCompletedDifferentialModulePreStageMap C ψ i) at hproj

1586 exact hproj

1587 letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance

1588 letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance

1589 have hq :

1590 Continuous

1591 (fun y :

1592 CrossedDifferentialPreModule

1593 (zcCompletedDifferentialModuleStageRing C ψ i)

1594 (zcCompletedDifferentialModuleStageSource C ψ i) =>

1595 (crossedDifferentialRelationSubmodule

1596 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ y) :=

1597 continuous_of_discreteTopology

1598 have hcomp := hq.comp hpre

1599 have hcoord :

1600 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

1601 zcCompletedDifferentialModuleStageProjectionAdd C ψ i

1602 ((crossedDifferentialRelationSubmodule

1603 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x)) =

1604 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

1605 (crossedDifferentialRelationSubmodule

1606 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ

1607 (zcCompletedDifferentialModulePreStageMap C ψ i x)) := by

1608 funext x

1609 rw [zcCompletedDifferentialModuleStageProjectionAdd_apply,

1610 zcCompletedDifferentialModuleStageProjection_mkQ,

1611 ← zcCompletedDifferentialModulePreStageMap_mkQ]

1612 rw [hcoord]

1613 exact hcomp

1614

1615omit [IsTopologicalGroup G] in

1616/--

1617If the finite-stage natural topology on the algebraic quotient is already \(T_1\), then the

1618defining crossed-differential relation submodule is closed in the completed pre-module

1619finite-stage topology. This is the quotient-topology reflection statement: the relation

1620submodule is the preimage of \({0}\) under the continuous algebraic quotient map.

1621-/

1622theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_of_t1_naturalTopology

1623 (hT1 :

1624 @T1Space (ZCCompletedDifferentialModule C ψ)

1625 (zcCompletedDifferentialModuleNaturalTopology C ψ)) :

1626 zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ := by

1627 letI : TopologicalSpace

1628 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1629 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1630 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

1631 zcCompletedDifferentialModuleNaturalTopology C ψ

1632 letI : T1Space (ZCCompletedDifferentialModule C ψ) := hT1

1633 change IsClosed

1634 ((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :

1635 Submodule (ZCCompletedGroupAlgebra C H)

1636 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1637 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))

1638 have hpreimage :

1639 ((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :

1640 Submodule (ZCCompletedGroupAlgebra C H)

1641 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1642 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =

1643 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

1644 (crossedDifferentialRelationSubmodule

1645 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x) ⁻¹'

1646 ({0} : Set (ZCCompletedDifferentialModule C ψ)) := by

1647 ext x

1648 simp only [SetLike.mem_coe, Submodule.mkQ_apply, Set.mem_preimage, Set.mem_singleton_iff,

1649 Submodule.Quotient.mk_eq_zero]

1650 rw [hpreimage]

1651 exact isClosed_singleton.preimage

1652 (continuous_zcCompletedDifferentialModule_mkQ_naturalTopology C ψ)

1653

1654omit [IsTopologicalGroup G] in

1655/--

1656A quotient-level non-circular closedness criterion. If the algebraic completed differential

1657module admits an injective continuous map from its finite-stage natural topology to a \(T_1\)

1658target, then the defining crossed-differential relation submodule is closed in the pre-module

1659finite-stage topology. This packages the topological reflection step through the continuous

1660algebraic quotient map from the pre-module.

1661-/

1662theorem zcDiffModuleRelSubmoduleClosed_of_inj_continuous_naturalTopology

1663 {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]

1664 [TopologicalSpace M] [T1Space M]

1665 (L :

1666 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] M)

1667 (hLinj : Function.Injective L)

1668 (hcont :

1669 @Continuous

1670 (ZCCompletedDifferentialModule C ψ) M

1671 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance

1672 L) :

1673 zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ :=

1674 zcDiffModuleRelSubmoduleClosed_of_inj_continuous_comp_mkQ

1675 C ψ L hLinj

1676 (@Continuous.comp

1677 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1678 (ZCCompletedDifferentialModule C ψ) M

1679 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1680 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance

1681 (f := (crossedDifferentialRelationSubmodule

1682 (zcCompletedGroupAlgebraScalar C ψ)).mkQ)

1683 (g := L) hcont

1684 (continuous_zcCompletedDifferentialModule_mkQ_naturalTopology C ψ))

1685

1686omit [IsTopologicalGroup G] in

1687/--

1688Finite relation-valued reductions put a pre-module element in the finite-stage closure of the

1689completed crossed-differential relation submodule.

1690-/

1691theorem zcDiffModuleFiniteRelationReductions_mem_closure_relSubmodule

1692 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

1693 (hdir : Directed (· ≤ ·)

1694 (id : ZCCompletedDifferentialModuleIndex C ψ →

1695 ZCCompletedDifferentialModuleIndex C ψ))

1696 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1697 (hx : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

1698 zcCompletedDifferentialModulePreStageMap C ψ i x ∈

1699 crossedDifferentialRelationSubmodule

1700 (zcCompletedDifferentialModuleStageScalar C ψ i)) :

1701 x ∈ @closure

1702 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1703 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1704 ((crossedDifferentialRelationSubmodule

1705 (zcCompletedGroupAlgebraScalar C ψ) :

1706 Submodule (ZCCompletedGroupAlgebra C H)

1707 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set

1708 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by

1709 letI : TopologicalSpace

1710 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1711 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1712 rw [mem_closure_iff]

1713 intro U hU hxU

1714 rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVeq⟩

1715 have hxV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ x ∈ V := by

1716 rw [← hVeq] at hxU

1717 exact hxU

1718 let S := zcCompletedDifferentialPreModuleStageSystem C ψ

1719 rcases S.exists_projection_preimage_subset hdir hVopen hxV with

1720 ⟨i, W, hWopen, hxW, hWU⟩

1721 rcases zcCompletedDifferentialModuleFiniteRelationReductions_finiteStageApproximation

1722 C ψ hdir ({i} : Finset (ZCCompletedDifferentialModuleIndex C ψ)) x hx with

1723 ⟨r, hr, hrstage⟩

1724 refine ⟨r, ?_, hr⟩

1725 have hri : zcCompletedDifferentialModulePreStageMap C ψ i r =

1726 zcCompletedDifferentialModulePreStageMap C ψ i x := by

1727 exact hrstage i (by simp only [Finset.mem_singleton])

1728 have hrW :

1729 S.projection i (zcCompletedDifferentialPreModuleStageFamilyMap C ψ r) ∈ W := by

1730 change zcCompletedDifferentialModulePreStageMap C ψ i r ∈ W

1731 rw [hri]

1732 change zcCompletedDifferentialModulePreStageMap C ψ i x ∈ W at hxW

1733 exact hxW

1734 have hrV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ r ∈ V := hWU hrW

1735 rw [← hVeq]

1736 exact hrV

1737

1738omit [IsTopologicalGroup G] in

1739/--

1740Each finite-stage pre-kernel is closed for the finite-stage topology on the completed

1741pre-module.

1742-/

1743theorem isClosed_zcCompletedDifferentialModulePreStageKernel_naturalTopology

1744 (i : ZCCompletedDifferentialModuleIndex C ψ) :

1745 @IsClosed

1746 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1747 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1748 ((zcCompletedDifferentialModulePreStageKernel C ψ i :

1749 Submodule (ZCCompletedGroupAlgebra C H)

1750 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1751 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by

1752 letI : TopologicalSpace

1753 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1754 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1755 let S := zcCompletedDifferentialPreModuleStageSystem C ψ

1756 letI : TopologicalSpace

1757 (CrossedDifferentialPreModule

1758 (zcCompletedDifferentialModuleStageRing C ψ i)

1759 (zcCompletedDifferentialModuleStageSource C ψ i)) :=

1760 ⊥

1761 letI : DiscreteTopology

1762 (CrossedDifferentialPreModule

1763 (zcCompletedDifferentialModuleStageRing C ψ i)

1764 (zcCompletedDifferentialModuleStageSource C ψ i)) :=

1765 ⟨rfl⟩

1766 have hpre :

1767 Continuous (zcCompletedDifferentialModulePreStageMap C ψ i) := by

1768 have hfamily :

1769 @Continuous

1770 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1771 (ZCCompletedDifferentialPreModuleStageFamily C ψ)

1772 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance

1773 (zcCompletedDifferentialPreModuleStageFamilyMap C ψ) :=

1774 continuous_induced_dom

1775 have hproj := (S.continuous_projection i).comp hfamily

1776 change

1777 @Continuous

1778 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1779 (CrossedDifferentialPreModule

1780 (zcCompletedDifferentialModuleStageRing C ψ i)

1781 (zcCompletedDifferentialModuleStageSource C ψ i))

1782 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance

1783 (zcCompletedDifferentialModulePreStageMap C ψ i) at hproj

1784 exact hproj

1785 have hpreimage :

1786 IsClosed

1787 ((zcCompletedDifferentialModulePreStageMap C ψ i) ⁻¹'

1788 (((crossedDifferentialRelationSubmodule

1789 (zcCompletedDifferentialModuleStageScalar C ψ i)) :

1790 Submodule

1791 (zcCompletedDifferentialModuleStageRing C ψ i)

1792 (CrossedDifferentialPreModule

1793 (zcCompletedDifferentialModuleStageRing C ψ i)

1794 (zcCompletedDifferentialModuleStageSource C ψ i))) :

1795 Set (CrossedDifferentialPreModule

1796 (zcCompletedDifferentialModuleStageRing C ψ i)

1797 (zcCompletedDifferentialModuleStageSource C ψ i)))) := by

1798 exact

1799 (isClosed_discrete

1800 (((crossedDifferentialRelationSubmodule

1801 (zcCompletedDifferentialModuleStageScalar C ψ i)) :

1802 Submodule

1803 (zcCompletedDifferentialModuleStageRing C ψ i)

1804 (CrossedDifferentialPreModule

1805 (zcCompletedDifferentialModuleStageRing C ψ i)

1806 (zcCompletedDifferentialModuleStageSource C ψ i))) :

1807 Set (CrossedDifferentialPreModule

1808 (zcCompletedDifferentialModuleStageRing C ψ i)

1809 (zcCompletedDifferentialModuleStageSource C ψ i)))).preimage hpre

1810 have hset :

1811 ((zcCompletedDifferentialModulePreStageKernel C ψ i :

1812 Submodule (ZCCompletedGroupAlgebra C H)

1813 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1814 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =

1815 ((zcCompletedDifferentialModulePreStageMap C ψ i) ⁻¹'

1816 (((crossedDifferentialRelationSubmodule

1817 (zcCompletedDifferentialModuleStageScalar C ψ i)) :

1818 Submodule

1819 (zcCompletedDifferentialModuleStageRing C ψ i)

1820 (CrossedDifferentialPreModule

1821 (zcCompletedDifferentialModuleStageRing C ψ i)

1822 (zcCompletedDifferentialModuleStageSource C ψ i))) :

1823 Set (CrossedDifferentialPreModule

1824 (zcCompletedDifferentialModuleStageRing C ψ i)

1825 (zcCompletedDifferentialModuleStageSource C ψ i)))) := by

1826 ext x

1827 exact

1828 mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule (C := C) (ψ := ψ) (i := i)

1829 (x := x)

1830 simpa [hset] using hpreimage

1831

1832omit [IsTopologicalGroup G] in

1833/--

1834The finite-stage closed relation denominator is closed for the finite-stage pre-module topology.

1835-/

1836theorem isClosed_zcCompletedDifferentialRelationFiniteClosedSubmodule_naturalTopology :

1837 @IsClosed

1838 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1839 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1840 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ :

1841 Submodule (ZCCompletedGroupAlgebra C H)

1842 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1843 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by

1844 letI : TopologicalSpace

1845 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1846 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1847 change IsClosed

1848 ((zcCompletedDifferentialModulePreStageKernelIntersection C ψ :

1849 Submodule (ZCCompletedGroupAlgebra C H)

1850 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1851 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))

1852 rw [zcCompletedDifferentialModulePreStageKernelIntersection]

1853 simpa [Submodule.coe_iInf] using

1854 (isClosed_iInter

1855 (fun i =>

1856 isClosed_zcCompletedDifferentialModulePreStageKernel_naturalTopology

1857 C ψ i))

1858

1859omit [IsTopologicalGroup G] in

1860/--

1861The zero class is closed in the separated completed differential module for the finite-stage

1862quotient topology.

1863-/

1864theorem isClosed_zero_zcSeparatedCompletedDifferentialModuleNaturalTopology :

1865 @IsClosed (ZCSeparatedCompletedDifferentialModule C ψ)

1866 (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)

1867 ({0} : Set (ZCSeparatedCompletedDifferentialModule C ψ)) := by

1868 letI : TopologicalSpace

1869 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1870 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1871 rw [zcSeparatedCompletedDifferentialModuleNaturalTopology, isClosed_coinduced]

1872 have hpreimage :

1873 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ ⁻¹'

1874 ({0} : Set (ZCSeparatedCompletedDifferentialModule C ψ))) =

1875 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ :

1876 Submodule (ZCCompletedGroupAlgebra C H)

1877 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1878 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by

1879 ext x

1880 simp only [Set.mem_preimage, Submodule.mkQ_apply, Set.mem_singleton_iff,

1881 Submodule.Quotient.mk_eq_zero,

1882 SetLike.mem_coe]

1883 rw [hpreimage]

1884 exact isClosed_zcCompletedDifferentialRelationFiniteClosedSubmodule_naturalTopology C ψ

1885

1886omit [IsTopologicalGroup G] in

1887/--

1888The finite-stage closed relation denominator is exactly the closure of the algebraic

1889crossed-differential relation submodule for the finite-stage pre-module topology.

1890-/

1891theorem closure_crossedDifferentialRelationSubmodule_eq_finiteClosedSubmodule

1892 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

1893 (hdir : Directed (· ≤ ·)

1894 (id : ZCCompletedDifferentialModuleIndex C ψ →

1895 ZCCompletedDifferentialModuleIndex C ψ)) :

1896 @closure

1897 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1898 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1899 ((crossedDifferentialRelationSubmodule

1900 (zcCompletedGroupAlgebraScalar C ψ) :

1901 Submodule (ZCCompletedGroupAlgebra C H)

1902 (CrossedDifferentialPreModule

1903 (ZCCompletedGroupAlgebra C H) G)) :

1904 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =

1905 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ :

1906 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by

1907 letI : TopologicalSpace

1908 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1909 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1910 apply Set.Subset.antisymm

1911 · intro x hxcl

1912 change x ∈ zcCompletedDifferentialModulePreStageKernelIntersection C ψ

1913 exact

1914 (mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff (C := C) (ψ := ψ) (x := x)).2

1915 (by

1916 intro i

1917 have hclosed_i :=

1918 isClosed_zcCompletedDifferentialModulePreStageKernel_naturalTopology C ψ i

1919 have hsubset_i :

1920 ((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :

1921 Submodule (ZCCompletedGroupAlgebra C H)

1922 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1923 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) ⊆

1924 ((zcCompletedDifferentialModulePreStageKernel C ψ i :

1925 Submodule (ZCCompletedGroupAlgebra C H)

1926 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1927 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by

1928 intro y hy

1929 exact

1930 crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel

1931 (C := C) (ψ := ψ) i hy

1932 have hxker : x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i :=

1933 closure_minimal hsubset_i hclosed_i hxcl

1934 exact

1935 (mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule (C := C) (ψ := ψ)

1936 (i := i) (x := x)).1 hxker)

1937 · intro x hxhat

1938 have hxstage :

1939 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

1940 zcCompletedDifferentialModulePreStageMap C ψ i x ∈

1941 crossedDifferentialRelationSubmodule

1942 (zcCompletedDifferentialModuleStageScalar C ψ i) :=

1943 (mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff (C := C) (ψ := ψ) (x := x)).1

1944 (by

1945 simpa [zcCompletedDifferentialRelationFiniteClosedSubmodule] using hxhat)

1946 exact

1947 zcDiffModuleFiniteRelationReductions_mem_closure_relSubmodule

1948 C ψ hdir x hxstage

1949

1950omit [IsTopologicalGroup G] in

1951/--

1952A continuous pre-quotient lift to a \(T_1\) target kills the finite-stage closed relation

1953denominator. This is the general descent criterion for maps out of the separated completed

1954universal module.

1955-/

1956theorem crossedDifferentialModuleLiftLinear_kills_finiteClosedSubmodule_of_continuous

1957 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

1958 [TopologicalSpace A] [T1Space A]

1959 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

1960 (hdir : Directed (· ≤ ·)

1961 (id : ZCCompletedDifferentialModuleIndex C ψ →

1962 ZCCompletedDifferentialModuleIndex C ψ))

1963 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)

1964 (hcont :

1965 @Continuous

1966 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

1967 A

1968 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

1969 inferInstance

1970 (crossedDifferentialModuleLiftLinear

1971 (R := ZCCompletedGroupAlgebra C H) delta))

1972 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}

1973 (hx : x ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ) :

1974 crossedDifferentialModuleLiftLinear

1975 (R := ZCCompletedGroupAlgebra C H) delta x = 0 := by

1976 letI : TopologicalSpace

1977 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

1978 zcCompletedDifferentialPreModuleNaturalTopology C ψ

1979 have hxcl :

1980 x ∈ closure

1981 ((crossedDifferentialRelationSubmodule

1982 (zcCompletedGroupAlgebraScalar C ψ) :

1983 Submodule (ZCCompletedGroupAlgebra C H)

1984 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

1985 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by

1986 have hEq :=

1987 closure_crossedDifferentialRelationSubmodule_eq_finiteClosedSubmodule

1988 C ψ hdir

1989 rw [hEq]

1990 exact hx

1991 have hker_closed :

1992 IsClosed

1993 ((fun y : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

1994 crossedDifferentialModuleLiftLinear

1995 (R := ZCCompletedGroupAlgebra C H) delta y) ⁻¹'

1996 ({0} : Set A)) :=

1997 isClosed_singleton.preimage hcont

1998 have hrel_subset_ker :

1999 ((crossedDifferentialRelationSubmodule

2000 (zcCompletedGroupAlgebraScalar C ψ) :

2001 Submodule (ZCCompletedGroupAlgebra C H)

2002 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

2003 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) ⊆

2004 ((fun y : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

2005 crossedDifferentialModuleLiftLinear

2006 (R := ZCCompletedGroupAlgebra C H) delta y) ⁻¹'

2007 ({0} : Set A)) := by

2008 intro y hy

2009 exact

2010 (crossedHomRelationSubmodule_le_ker

2011 (A := A) (zcCompletedGroupAlgebraScalar C ψ)

2012 delta) hy

2013 exact closure_minimal hrel_subset_ker hker_closed hxcl

2014

2015/--

2016The separated universal lift induced by a crossed differential whose pre-quotient lift is

2017continuous for the finite-stage topology.

2018-/

2019def zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

2020 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2021 [TopologicalSpace A] [T1Space A]

2022 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2023 (hdir : Directed (· ≤ ·)

2024 (id : ZCCompletedDifferentialModuleIndex C ψ →

2025 ZCCompletedDifferentialModuleIndex C ψ))

2026 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)

2027 (hcont :

2028 @Continuous

2029 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2030 A

2031 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

2032 inferInstance

2033 (crossedDifferentialModuleLiftLinear

2034 (R := ZCCompletedGroupAlgebra C H) delta)) :

2035 ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A :=

2036 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).liftQ

2037 (crossedDifferentialModuleLiftLinear

2038 (R := ZCCompletedGroupAlgebra C H) delta)

2039 (by

2040 intro x hx

2041 rw [LinearMap.mem_ker]

2042 exact

2043 crossedDifferentialModuleLiftLinear_kills_finiteClosedSubmodule_of_continuous

2044 C ψ hdir delta hcont hx)

2045

2046omit [IsTopologicalGroup G] in

2047/--

2048The separated lift of a continuous crossed-differential prelift sends the separated universal

2049differential of \(g\) to \(\delta(g)\).

2050-/

2051@[simp 900]

2052theorem zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_universal

2053 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2054 [TopologicalSpace A] [T1Space A]

2055 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2056 (hdir : Directed (· ≤ ·)

2057 (id : ZCCompletedDifferentialModuleIndex C ψ →

2058 ZCCompletedDifferentialModuleIndex C ψ))

2059 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)

2060 (hcont :

2061 @Continuous

2062 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2063 A

2064 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

2065 inferInstance

2066 (crossedDifferentialModuleLiftLinear

2067 (R := ZCCompletedGroupAlgebra C H) delta))

2068 (g : G) :

2069 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

2070 C ψ hdir delta hcont

2071 (zcSeparatedUniversalDifferential C ψ g) =

2072 delta g := by

2073 change

2074 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

2075 C ψ hdir delta hcont

2076 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

2077 (Finsupp.single g 1)) =

2078 delta g

2079 rw [zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift,

2080 Submodule.mkQ_apply, Submodule.liftQ_apply]

2081 simp only [crossedDifferentialModuleLiftLinear_single, one_smul]

2082

2083omit [IsTopologicalGroup G] in

2084/--

2085Linear maps out of the separated completed differential module are equal when they agree on all

2086separated universal differentials.

2087-/

2088@[ext]

2089theorem zcSeparatedCompletedDifferentialModuleHom_ext

2090 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2091 {f h : ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A}

2092 (hfh : ∀ g, f (zcSeparatedUniversalDifferential C ψ g) =

2093 h (zcSeparatedUniversalDifferential C ψ g)) :

2094 f = h := by

2095 apply Submodule.linearMap_qext _

2096 apply Finsupp.lhom_ext

2097 intro g r

2098 have hsingle :

2099 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

2100 (Finsupp.single g r) :

2101 ZCSeparatedCompletedDifferentialModule C ψ) =

2102 r • zcSeparatedUniversalDifferential C ψ g := by

2103 rw [← Finsupp.smul_single_one]

2104 rfl

2105 change f ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

2106 (Finsupp.single g r)) =

2107 h ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

2108 (Finsupp.single g r))

2109 simpa [hsingle, map_smul] using congrArg (fun z => r • z) (hfh g)

2110

2111omit [IsTopologicalGroup G] in

2112/--

2113The separated lift of a continuous crossed differential is unique among linear maps with the

2114prescribed values on separated universal differentials.

2115-/

2116theorem zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_unique

2117 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2118 [TopologicalSpace A] [T1Space A]

2119 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2120 (hdir : Directed (· ≤ ·)

2121 (id : ZCCompletedDifferentialModuleIndex C ψ →

2122 ZCCompletedDifferentialModuleIndex C ψ))

2123 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)

2124 (hcont :

2125 @Continuous

2126 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2127 A

2128 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

2129 inferInstance

2130 (crossedDifferentialModuleLiftLinear

2131 (R := ZCCompletedGroupAlgebra C H) delta))

2132 (f : ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A)

2133 (hf : ∀ g, f (zcSeparatedUniversalDifferential C ψ g) = delta g) :

2134 f =

2135 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

2136 C ψ hdir delta hcont := by

2137 apply zcSeparatedCompletedDifferentialModuleHom_ext C ψ

2138 intro g

2139 rw [hf g, zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_universal]

2140

2141/--

2142The separated universal lift is bundled as a continuous linear map for the separated quotient

2143topology.

2144-/

2145def zcSeparatedCompletedDifferentialModuleLiftContinuousLinearMapOfContinuousPrelift

2146 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2147 [TopologicalSpace A] [T1Space A]

2148 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2149 (hdir : Directed (· ≤ ·)

2150 (id : ZCCompletedDifferentialModuleIndex C ψ →

2151 ZCCompletedDifferentialModuleIndex C ψ))

2152 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)

2153 (hcont :

2154 @Continuous

2155 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2156 A

2157 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

2158 inferInstance

2159 (crossedDifferentialModuleLiftLinear

2160 (R := ZCCompletedGroupAlgebra C H) delta)) :

2161 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

2162 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

2163 ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A := by

2164 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

2165 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

2166 refine

2167 { toLinearMap :=

2168 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

2169 C ψ hdir delta hcont

2170 cont := ?_ }

2171 rw [continuous_coinduced_dom]

2172 change

2173 @Continuous

2174 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2175 A

2176 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

2177 inferInstance

2178 (fun x =>

2179 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

2180 C ψ hdir delta hcont

2181 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x))

2182 have hcomp :

2183 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

2184 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

2185 C ψ hdir delta hcont

2186 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x)) =

2187 crossedDifferentialModuleLiftLinear

2188 (R := ZCCompletedGroupAlgebra C H) delta := by

2189 funext x

2190 rw [zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift,

2191 Submodule.mkQ_apply, Submodule.liftQ_apply]

2192 rw [hcomp]

2193 exact hcont

2194

2195omit [IsTopologicalGroup G] in

2196/--

2197The separated completed differential-module lift is evaluated after projection to the relevant

2198finite-stage separated quotient.

2199-/

2200@[simp 900]

2201theorem zcSepDiffModuleLiftContinuousLinearMapOfContinuousPrelift_apply

2202 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2203 [TopologicalSpace A] [T1Space A]

2204 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2205 (hdir : Directed (· ≤ ·)

2206 (id : ZCCompletedDifferentialModuleIndex C ψ →

2207 ZCCompletedDifferentialModuleIndex C ψ))

2208 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)

2209 (hcont :

2210 @Continuous

2211 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2212 A

2213 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

2214 inferInstance

2215 (crossedDifferentialModuleLiftLinear

2216 (R := ZCCompletedGroupAlgebra C H) delta))

2217 (m : ZCSeparatedCompletedDifferentialModule C ψ) :

2218 zcSeparatedCompletedDifferentialModuleLiftContinuousLinearMapOfContinuousPrelift

2219 C ψ hdir delta hcont m =

2220 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

2221 C ψ hdir delta hcont m :=

2222 rfl

2223

2224/--

2225This is the continuous representation theorem for the separated completed module, parameterized

2226by the topological input that turns a continuous crossed differential into a continuous

2227pre-quotient linear lift.

2228-/

2229def zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap

2230 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2231 [TopologicalSpace A] [T1Space A]

2232 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2233 (hdir : Directed (· ≤ ·)

2234 (id : ZCCompletedDifferentialModuleIndex C ψ →

2235 ZCCompletedDifferentialModuleIndex C ψ))

2236 (hprelift :

2237 ∀ (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A),

2238 Continuous delta →

2239 @Continuous

2240 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2241 A

2242 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

2243 inferInstance

2244 (crossedDifferentialModuleLiftLinear

2245 (R := ZCCompletedGroupAlgebra C H) delta)) :

2246 {delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A //

2247 Continuous delta} ≃

2248 (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

2249 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

2250 ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) where

2251 toFun delta :=

2252 zcSeparatedCompletedDifferentialModuleLiftContinuousLinearMapOfContinuousPrelift

2253 C ψ hdir delta.1 (hprelift delta.1 delta.2)

2254 invFun f := by

2255 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

2256 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

2257 exact

2258 ⟨(zcSeparatedUniversalDifferential C ψ).mapLinear f.toLinearMap,

2259 f.cont.comp (continuous_zcSeparatedUniversalDifferential_naturalTopology C ψ)⟩

2260 left_inv delta := by

2261 apply Subtype.ext

2262 apply CrossedHom.ext

2263 intro g

2264 exact

2265 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_universal

2266 C ψ hdir delta.1 (hprelift delta.1 delta.2) g

2267 right_inv f := by

2268 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

2269 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

2270 let delta :=

2271 (zcSeparatedUniversalDifferential C ψ).mapLinear f.toLinearMap

2272 have hcontinuous_delta : Continuous delta :=

2273 f.cont.comp (continuous_zcSeparatedUniversalDifferential_naturalTopology C ψ)

2274 have hlin :

2275 f.toLinearMap =

2276 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

2277 C ψ hdir delta (hprelift delta hcontinuous_delta) := by

2278 apply zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_unique

2279 C ψ hdir

2280 intro g

2281 rfl

2282 apply ContinuousLinearMap.ext

2283 intro m

2284 exact congrFun (congrArg DFunLike.coe hlin.symm) m

2285

2286/--

2287Continuous representation theorem with the finite-stage index nonemptiness and directedness

2288supplied from a continuous homomorphism and the finite quotient-class hypotheses. The only

2289remaining topological input is the pre-quotient lift continuity.

2290-/

2291def zcSepContCrossedDiffEquivCLM

2292 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2293 [TopologicalSpace A] [T1Space A]

2294 [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]

2295 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

2296 (hForm : ProCGroups.FiniteGroupClass.Formation C)

2297 (ψc : ContinuousMonoidHom G H)

2298 (hprelift :

2299 ∀ (delta : ScalarCrossedHom

2300 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A),

2301 Continuous delta →

2302 @Continuous

2303 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2304 A

2305 (zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom)

2306 inferInstance

2307 (crossedDifferentialModuleLiftLinear

2308 (R := ZCCompletedGroupAlgebra C H) delta)) :

2309 {delta : ScalarCrossedHom

2310 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A //

2311 Continuous delta} ≃

2312 (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom) :=

2313 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom

2314 ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →L[ZCCompletedGroupAlgebra C H] A)

2315 := by

2316 letI : Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom) :=

2317 nonempty_zcCompletedDifferentialModuleIndex C hC ψc

2318 exact

2319 zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap

2320 C ψc.toMonoidHom

2321 (directed_zcCompletedDifferentialModuleIndex C hForm hC ψc)

2322 hprelift

2323

2324/--

2325This is the continuous representation theorem for the separated completed module when every

2326continuous crossed differential under consideration has a pre-quotient lift that factors through

2327a finite pre-stage. This packages the finite-stage factorization criterion into the universal

2328property, so the public theorem no longer takes the raw hprelift continuity hypothesis.

2329-/

2330def zcSepCompletedContCrossedDiffEquivContinuousLinearMapOfFiniteStageFactorization

2331 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2332 [TopologicalSpace A] [T1Space A]

2333 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2334 (hdir : Directed (· ≤ ·)

2335 (id : ZCCompletedDifferentialModuleIndex C ψ →

2336 ZCCompletedDifferentialModuleIndex C ψ))

2337 (hfactor :

2338 ∀ (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A),

2339 Continuous delta →

2340 ∃ i : ZCCompletedDifferentialModuleIndex C ψ,

2341 ∃ L :

2342 CrossedDifferentialPreModule

2343 (zcCompletedDifferentialModuleStageRing C ψ i)

2344 (zcCompletedDifferentialModuleStageSource C ψ i) → A,

2345 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,

2346 crossedDifferentialModuleLiftLinear

2347 (R := ZCCompletedGroupAlgebra C H) delta x =

2348 L (zcCompletedDifferentialModulePreStageMap C ψ i x)) :

2349 {delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A //

2350 Continuous delta} ≃

2351 (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=

2352 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ

2353 ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) := by

2354 refine

2355 zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap

2356 C ψ hdir ?_

2357 intro delta hcont

2358 rcases hfactor delta hcont with ⟨i, L, hL⟩

2359 exact

2360 continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor

2361 C ψ delta i L hL

2362

2363/--

2364Continuous representation theorem with finite-stage index data supplied from a continuous

2365homomorphism and raw pre-lift continuity discharged by finite-stage factorization.

2366-/

2367def zcSepContCrossedDiffEquivCLMOfFiniteStage

2368 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2369 [TopologicalSpace A] [T1Space A]

2370 [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]

2371 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

2372 (hForm : ProCGroups.FiniteGroupClass.Formation C)

2373 (ψc : ContinuousMonoidHom G H)

2374 (hfactor :

2375 ∀ (delta : ScalarCrossedHom

2376 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A),

2377 Continuous delta →

2378 ∃ i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom,

2379 ∃ L :

2380 CrossedDifferentialPreModule

2381 (zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i)

2382 (zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i) → A,

2383 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,

2384 crossedDifferentialModuleLiftLinear

2385 (R := ZCCompletedGroupAlgebra C H) delta x =

2386 L (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) :

2387 {delta : ScalarCrossedHom

2388 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A //

2389 Continuous delta} ≃

2390 (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom) :=

2391 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom

2392 ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →L[ZCCompletedGroupAlgebra C H] A)

2393 := by

2394 letI : Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom) :=

2395 nonempty_zcCompletedDifferentialModuleIndex C hC ψc

2396 exact

2397 zcSepCompletedContCrossedDiffEquivContinuousLinearMapOfFiniteStageFactorization

2398 C ψc.toMonoidHom

2399 (directed_zcCompletedDifferentialModuleIndex C hForm hC ψc)

2400 hfactor

2401

2402/--

2403The \(\mathbb{Z}_C\llbracket H\rrbracket\)-action on a finite discrete target factors through

2404one finite coefficient-and-H stage.

2405-/

2406theorem zcCompletedGroupAlgebra_smul_factor_through_finite_stage

2407 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2408 [TopologicalSpace A] [Finite A] [DiscreteTopology A]

2409 [ContinuousSMul (ZCCompletedGroupAlgebra C H) A]

2410 (hForm : ProCGroups.FiniteGroupClass.Formation C) :

2411 ∃ j : ZCCompletedGroupAlgebraIndex C H,

2412 ∃ act : ZCCompletedGroupAlgebraStage C H j → A → A,

2413 ∀ (r : ZCCompletedGroupAlgebra C H) (a : A),

2414 act (zcCompletedGroupAlgebraProjection C H j r) a = r • a := by

2415 classical

2416 letI : Fintype A := Fintype.ofFinite A

2417 letI : ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C :=

2418 hForm.containsTrivialQuotients

2419 letI : Nonempty (ProCIntegerIndex C) :=

2420 ⟨ProCIntegerIndex.terminal (C := C) inferInstance⟩

2421 letI : Nonempty (CompletedGroupAlgebraIndexInClass H C) :=

2422 ⟨_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndexInClass (G := H) C⟩

2423 letI : Nonempty (ZCCompletedGroupAlgebraIndex C H) := inferInstance

2424 letI : Finite (A → A) := Finite.of_fintype (A → A)

2425 let S := zcCompletedGroupAlgebraSystem C H

2426 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, TopologicalSpace (S.X i) :=

2427 S.topologicalSpace

2428 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, CompactSpace (S.X i) := fun i => by

2429 dsimp [S, zcCompletedGroupAlgebraSystem]

2430 change @CompactSpace (ZCCompletedGroupAlgebraStage C H i) ⊥

2431 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩

2432 letI : Finite (ZCCompletedGroupAlgebraStage C H i) :=

2433 finite_modNCompletedGroupAlgebraStageInClass

2434 (n := i.1.modulus) (G := H) C i.2

2435 exact Finite.compactSpace

2436 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, T2Space (S.X i) := fun i => by

2437 dsimp [S, zcCompletedGroupAlgebraSystem]

2438 change @T2Space (ZCCompletedGroupAlgebraStage C H i) ⊥

2439 exact @DiscreteTopology.toT2Space _ ⊥ ⟨rfl⟩

2440 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, TotallyDisconnectedSpace (S.X i) := fun i => by

2441 dsimp [S, zcCompletedGroupAlgebraSystem]

2442 change @TotallyDisconnectedSpace (ZCCompletedGroupAlgebraStage C H i) ⊥

2443 exact @TotallySeparatedSpace.totallyDisconnectedSpace _ ⊥

2444 (@TotallySeparatedSpace.of_discrete _ ⊥ ⟨rfl⟩)

2445 let ρ : ZCCompletedGroupAlgebra C H → A → A := fun r a => r • a

2446 have hρ : Continuous ρ := by

2447 change Continuous (fun r : ZCCompletedGroupAlgebra C H => fun a : A => r • a)

2448 exact continuous_pi fun a => continuous_id.smul continuous_const

2449 rcases S.factors_through_projection_finite

2450 (directed_zcCompletedGroupAlgebraIndex_of_formation C (H := H) hForm)

2451 ρ hρ with

2452 ⟨j, act, _hact_continuous, hact⟩

2453 refine ⟨j, act, ?_⟩

2454 intro r a

2455 have h := congrFun (congrFun hact r) a

2456 simpa [ρ, S, zcCompletedGroupAlgebraSystem] using h.symm

2457

2458omit [IsTopologicalGroup G] in

2459/--

2460A finite discrete target crossed differential has a pre-quotient lift factoring through one

2461finite source/target/coefficient stage.

2462-/

2463theorem crossedDifferentialModuleLiftLinear_factors_finite_discrete

2464 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

2465 [TopologicalSpace A] [Finite A] [DiscreteTopology A]

2466 [ContinuousSMul (ZCCompletedGroupAlgebra C H) A]

2467 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

2468 (hForm : ProCGroups.FiniteGroupClass.Formation C)

2469 (ψc : ContinuousMonoidHom G H)

2470 (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G)

2471 (delta : ScalarCrossedHom

2472 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A)

2473 (hcont : Continuous delta) :

2474 ∃ i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom,

2475 ∃ L :

2476 CrossedDifferentialPreModule

2477 (zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i)

2478 (zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i) → A,

2479 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,

2480 crossedDifferentialModuleLiftLinear

2481 (R := ZCCompletedGroupAlgebra C H) delta x =

2482 L (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x) := by

2483 classical

2484 letI : Fintype A := Fintype.ofFinite A

2485 rcases zcCompletedGroupAlgebra_smul_factor_through_finite_stage

2486 (C := C) (H := H) (A := A) hForm with

2487 ⟨target, act, hact⟩

2488 have hdelta_one : delta 1 = 0 :=

2489 delta.map_one

2490 let W : Set G := {g | delta g = 0}

2491 have hWopen : IsOpen W := by

2492 change IsOpen (delta ⁻¹' ({0} : Set A))

2493 exact (isOpen_discrete _).preimage hcont

2494 have h1W : (1 : G) ∈ W := by

2495 change delta 1 = 0

2496 exact hdelta_one

2497 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hWopen h1W with

2498 ⟨V0, hV0W⟩

2499 let comapSource : OpenNormalSubgroupInClass C G :=

2500 OrderDual.ofDual

2501 (completedGroupAlgebraComapIndexInClass

2502 (G := G) (H := H) C hC ψc target.2)

2503 let source : OpenNormalSubgroupInClass C G :=

2504 ⟨V0.1 ⊓ comapSource.1,

2505 ProCGroups.FiniteGroupClass.Formation.quotient_inf_mem

2506 (C := C) (G := G) hForm V0.1 comapSource.1 V0.2 comapSource.2⟩

2507 let i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom :=

2508 { source := source

2509 target := target

2510 compatible := by

2511 intro g hg

2512 have hgcomap : g ∈ (comapSource.1 : Subgroup G) := hg.2

2513 change ψc.toMonoidHom g ∈

2514 ((((OrderDual.ofDual target.2).1 : OpenNormalSubgroup H) : Subgroup H))

2515 simpa [comapSource, completedGroupAlgebraComapIndexInClass] using hgcomap }

2516 have hsource_delta_zero :

2517 ∀ g : G, g ∈ (source.1 : Subgroup G) → delta g = 0 := by

2518 intro g hg

2519 exact hV0W hg.1

2520 let deltaBar : zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i → A :=

2521 Quotient.lift delta (by

2522 intro a b hab

2523 have hab_source : a⁻¹ * b ∈ (source.1 : Subgroup G) :=

2524 (QuotientGroup.leftRel_apply).1 hab

2525 have hab_zero : delta (a⁻¹ * b) = 0 :=

2526 hsource_delta_zero (a⁻¹ * b) hab_source

2527 have hprod := delta.map_mul a (a⁻¹ * b)

2528 have hrewrite : a * (a⁻¹ * b) = b := by simp only [mul_inv_cancel_left]

2529 have hb : delta b =

2530 delta a + zcCompletedGroupAlgebraScalar C ψc.toMonoidHom a •

2531 delta (a⁻¹ * b) := by

2532 simpa [hrewrite] using hprod

2533 rw [hab_zero, smul_zero, add_zero] at hb

2534 exact hb.symm)

2535 let coeffMap :

2536 zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i →

2537 zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i →+ A :=

2538 fun q =>

2539 { toFun := fun a => act a (deltaBar q)

2540 map_zero' := by

2541 have h := hact (0 : ZCCompletedGroupAlgebra C H) (deltaBar q)

2542 simpa using h

2543 map_add' := by

2544 intro a b

2545 rcases zcCompletedGroupAlgebraProjection_surjective C H target a with ⟨ra, hra⟩

2546 rcases zcCompletedGroupAlgebraProjection_surjective C H target b with ⟨rb, hrb⟩

2547 calc

2548 act (a + b) (deltaBar q)

2549 = act (zcCompletedGroupAlgebraProjection C H target (ra + rb)) (deltaBar q) := by

2550 simp only [ContinuousMonoidHom.coe_toMonoidHom,

2551 zcCompletedGroupAlgebraProjection_add, hra, hrb]

2552 _ = (ra + rb) • deltaBar q := hact (ra + rb) (deltaBar q)

2553 _ = ra • deltaBar q + rb • deltaBar q := add_smul ra rb (deltaBar q)

2554 _ = act a (deltaBar q) + act b (deltaBar q) := by

2555 rw [← hact ra (deltaBar q), ← hact rb (deltaBar q), hra, hrb] }

2556 let Llin :

2557 CrossedDifferentialPreModule

2558 (zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i)

2559 (zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i) →ₗ[ℕ] A :=

2560 Finsupp.lsum ℕ fun q => (coeffMap q).toNatLinearMap

2561 refine ⟨i, (fun y => Llin y), ?_⟩

2562 intro x

2563 refine Finsupp.induction_linear x ?zero ?add ?single

2564 · simp only [crossedDifferentialModuleLiftLinear, map_zero, ContinuousMonoidHom.coe_toMonoidHom,

2565 zcCompletedDifferentialModulePreStageMap]

2566 · intro x y hx hy

2567 simpa only [map_add] using congrArg₂ (· + ·) hx hy

2568 · intro g a

2569 rw [crossedDifferentialModuleLiftLinear_single]

2570 rw [zcCompletedDifferentialModulePreStageMap_single]

2571 change a • delta g =

2572 Llin

2573 (Finsupp.single (zcCompletedDifferentialModuleStageSourceProj C ψc.toMonoidHom i g)

2574 (zcCompletedGroupAlgebraProjection C H i.target a))

2575 rw [Finsupp.lsum_single]

2576 change a • delta g =

2577 act (zcCompletedGroupAlgebraProjection C H target a)

2578 (deltaBar (zcCompletedDifferentialModuleStageSourceProj C ψc.toMonoidHom i g))

2579 simpa [deltaBar, zcCompletedDifferentialModuleStageSourceProj] using

2580 (hact a (delta g)).symm

2581

2582omit [IsTopologicalGroup G] in

2583/--

2584For a profinite target module, continuity of the crossed differential forces continuity of its

2585pre-quotient linear lift for the finite-stage topology.

2586-/

2587theorem continuous_crossedDifferentialModuleLiftLinear_of_profiniteTarget

2588 {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]

2589 [TopologicalSpace M]

2590 [IsTopologicalRing (ZCCompletedGroupAlgebra C H)]

2591 [CompactSpace (ZCCompletedGroupAlgebra C H)]

2592 [IsTopologicalAddGroup M] [ContinuousSMul (ZCCompletedGroupAlgebra C H) M]

2593 [CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M]

2594 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

2595 (hForm : ProCGroups.FiniteGroupClass.Formation C)

2596 (ψc : ContinuousMonoidHom G H)

2597 (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G)

2598 (delta : ScalarCrossedHom

2599 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) M)

2600 (hcont : Continuous delta) :

2601 @Continuous

2602 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2603 M

2604 (zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom)

2605 inferInstance

2606 (crossedDifferentialModuleLiftLinear

2607 (R := ZCCompletedGroupAlgebra C H) delta) := by

2608 classical

2609 letI : ContinuousAdd M := inferInstance

2610 letI : TopologicalSpace

2611 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

2612 zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom

2613 apply _root_.CompletedGroupAlgebra.continuous_of_forall_openSubmodule_quotient_continuous

2614 (R := ZCCompletedGroupAlgebra C H) M

2615 intro W hWopen

2616 let hdisc : _root_.CompletedGroupAlgebra.IsDiscreteModule

2617 (ZCCompletedGroupAlgebra C H) (M ⧸ W) :=

2618 _root_.CompletedGroupAlgebra.quotient_openSubmodule_isDiscreteModule

2619 (ZCCompletedGroupAlgebra C H) M W hWopen

2620 letI : DiscreteTopology (M ⧸ W) := hdisc.2

2621 letI : ContinuousSMul (ZCCompletedGroupAlgebra C H) (M ⧸ W) := hdisc.1.2.2

2622 letI : Fintype (M ⧸ W) :=

2623 Classical.choice

2624 (_root_.CompletedGroupAlgebra.finite_quotient_of_openSubmodule

2625 (ZCCompletedGroupAlgebra C H) M W hWopen)

2626 let deltaQ : ScalarCrossedHom

2627 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) (M ⧸ W) :=

2628 delta.mapLinear (Submodule.mkQ W)

2629 have hqcont : Continuous (Submodule.mkQ W : M → M ⧸ W) := by

2630 change Continuous (Submodule.Quotient.mk (p := W))

2631 exact continuous_quotient_mk'

2632 have hcontQ : Continuous deltaQ := hqcont.comp hcont

2633 rcases crossedDifferentialModuleLiftLinear_factors_finite_discrete

2634 (C := C) (H := H) (A := M ⧸ W) hC hForm ψc hG deltaQ hcontQ with

2635 ⟨i, L, hL⟩

2636 have hEq :

2637 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

2638 Submodule.mkQ W

2639 (crossedDifferentialModuleLiftLinear

2640 (R := ZCCompletedGroupAlgebra C H) delta x)) =

2641 crossedDifferentialModuleLiftLinear

2642 (R := ZCCompletedGroupAlgebra C H) deltaQ := by

2643 funext x

2644 refine Finsupp.induction_linear x ?zero ?add ?single

2645 · simp only [crossedDifferentialModuleLiftLinear, map_zero, deltaQ]

2646 · intro x y hx hy

2647 simp only [map_add, hx, hy]

2648 · intro g a

2649 simp only [crossedDifferentialModuleLiftLinear_single, map_smul]

2650 change a • Submodule.mkQ W (delta g) =

2651 a • Submodule.mkQ W (delta g)

2652 rfl

2653 rw [hEq]

2654 exact

2655 continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor

2656 C ψc.toMonoidHom deltaQ i L hL

2657

2658/--

2659Mathematical profinite-target universal property for \(A_{\psi}(C)\): continuous crossed

2660differentials into a profinite \(\mathbb{Z}_C\llbracket H\rrbracket\)-module are represented by

2661continuous linear maps out of the separated completed Fox module.

2662-/

2663def zcApsiContinuousCrossedDifferentialEquivContinuousLinearMapOfProfiniteTarget

2664 {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]

2665 [TopologicalSpace M]

2666 [IsTopologicalRing (ZCCompletedGroupAlgebra C H)]

2667 [CompactSpace (ZCCompletedGroupAlgebra C H)]

2668 [IsTopologicalAddGroup M] [ContinuousSMul (ZCCompletedGroupAlgebra C H) M]

2669 [CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M]

2670 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

2671 (hForm : ProCGroups.FiniteGroupClass.Formation C)

2672 (ψc : ContinuousMonoidHom G H)

2673 (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G) :

2674 {delta : ScalarCrossedHom

2675 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) M //

2676 Continuous delta} ≃

2677 (letI : TopologicalSpace (ZCApsi C ψc.toMonoidHom) :=

2678 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom

2679 ZCApsi C ψc.toMonoidHom →L[ZCCompletedGroupAlgebra C H] M) := by

2680 letI : T1Space M := inferInstance

2681 letI : ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C :=

2682 hForm.containsTrivialQuotients

2683 letI : Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom) :=

2684 nonempty_zcCompletedDifferentialModuleIndex C hC ψc

2685 exact

2686 zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap

2687 C ψc.toMonoidHom

2688 (directed_zcCompletedDifferentialModuleIndex C hForm hC ψc)

2689 (fun delta hcont =>

2690 continuous_crossedDifferentialModuleLiftLinear_of_profiniteTarget

2691 C hC hForm ψc hG delta hcont)

2692

2693omit [IsTopologicalGroup G] in

2694/--

2695If the completed crossed-differential relation submodule is closed for the finite-stage

2696pre-module topology, then finite relation reductions reflect actual completed relations.

2697-/

2698theorem zcDiffModuleFiniteRelationReductionsReflectRelations_of_isClosed_relSubmodule

2699 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2700 (hdir : Directed (· ≤ ·)

2701 (id : ZCCompletedDifferentialModuleIndex C ψ →

2702 ZCCompletedDifferentialModuleIndex C ψ))

2703 (hclosed :

2704 @IsClosed

2705 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

2706 (zcCompletedDifferentialPreModuleNaturalTopology C ψ)

2707 ((crossedDifferentialRelationSubmodule

2708 (zcCompletedGroupAlgebraScalar C ψ) :

2709 Submodule (ZCCompletedGroupAlgebra C H)

2710 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set

2711 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))) :

2712 zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ := by

2713 intro x hx

2714 letI : TopologicalSpace

2715 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

2716 zcCompletedDifferentialPreModuleNaturalTopology C ψ

2717 have hxcl :

2718 x ∈ closure

2719 ((crossedDifferentialRelationSubmodule

2720 (zcCompletedGroupAlgebraScalar C ψ) :

2721 Submodule (ZCCompletedGroupAlgebra C H)

2722 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set

2723 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :=

2724 zcDiffModuleFiniteRelationReductions_mem_closure_relSubmodule

2725 C ψ hdir x hx

2726 simpa [hclosed.closure_eq] using hxcl

2727

2728omit [IsTopologicalGroup G] in

2729/-- A named version of relation-reflection from closedness of the completed relation submodule. -/

2730theorem zcDiffModuleFiniteRelationReductionsReflectRelations_of_relSubmoduleClosed

2731 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2732 (hdir : Directed (· ≤ ·)

2733 (id : ZCCompletedDifferentialModuleIndex C ψ →

2734 ZCCompletedDifferentialModuleIndex C ψ))

2735 (hclosed : zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ) :

2736 zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ :=

2737 zcDiffModuleFiniteRelationReductionsReflectRelations_of_isClosed_relSubmodule

2738 C ψ hdir hclosed

2739

2740omit [IsTopologicalGroup G] in

2741/-- The pre-quotient separation statement is exactly finite relation-reflection. -/

2742theorem zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations

2743 (C : ProCGroups.FiniteGroupClass.{u}) (ψ : G →* H) :

2744 zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ ↔

2745 zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ := by

2746 constructor

2747 · intro hpre x hx

2748 apply hpre

2749 intro i

2750 exact

2751 (mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule (C := C) (ψ := ψ) (i :=

2752 i) (x := x)).2 (hx i)

2753 · intro hreflect x hx

2754 apply hreflect

2755 intro i

2756 exact

2757 (mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule (C := C) (ψ := ψ) (i :=

2758 i) (x := x)).1 (hx i)

2759

2760omit [IsTopologicalGroup G] in

2761/--

2762Pre-stage separation is equivalently the claim that the crossed-differential relation submodule

2763is exactly the intersection of all finite-stage pre-kernels.

2764-/

2765theorem zcDiffModulePreStageProjsSeparate_iff_relSubmodule_eq_iInf_kernel

2766 (C : ProCGroups.FiniteGroupClass.{u}) (ψ : G →* H) :

2767 zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ ↔

2768 crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =

2769 zcCompletedDifferentialModulePreStageKernelIntersection C ψ := by

2770 constructor

2771 · intro hpre

2772 apply le_antisymm

2773 · intro x hx

2774 rw [zcCompletedDifferentialModulePreStageKernelIntersection, Submodule.mem_iInf]

2775 intro i

2776 exact

2777 crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel

2778 (C := C) (ψ := ψ) i hx

2779 · intro x hx

2780 apply hpre

2781 intro i

2782 have hxi : x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i := by

2783 exact

2784 (Submodule.mem_iInf

2785 (p := fun i : ZCCompletedDifferentialModuleIndex C ψ =>

2786 zcCompletedDifferentialModulePreStageKernel C ψ i)).1

2787 (by

2788 simpa [zcCompletedDifferentialModulePreStageKernelIntersection] using hx) i

2789 simpa using hxi

2790 · intro hEq x hx

2791 have hxint : x ∈ zcCompletedDifferentialModulePreStageKernelIntersection C ψ := by

2792 rw [zcCompletedDifferentialModulePreStageKernelIntersection, Submodule.mem_iInf]

2793 intro i

2794 simpa using hx i

2795 simpa [hEq] using hxint

2796

2797omit [IsTopologicalGroup G] in

2798/-- Pre-quotient finite-stage separation implies separation on the algebraic quotient. -/

2799theorem zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate

2800 (hpre : zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ) :

2801 zcCompletedDifferentialModuleStageProjectionsSeparate C ψ := by

2802 intro a b hab

2803 have hcoord : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

2804 zcCompletedDifferentialModuleStageProjection C ψ i a =

2805 zcCompletedDifferentialModuleStageProjection C ψ i b := by

2806 intro i

2807 simpa [zcCompletedDifferentialModuleStageProjectionProduct,

2808 zcCompletedDifferentialModuleStageProjectionAdd] using congrFun hab i

2809 have hzero :

2810 ∀ z : ZCCompletedDifferentialModule C ψ,

2811 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,

2812 zcCompletedDifferentialModuleStageProjection C ψ i z = 0) → z = 0 := by

2813 intro z

2814 refine Submodule.Quotient.induction_on

2815 (p := crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ))

2816 (C := fun z =>

2817 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,

2818 zcCompletedDifferentialModuleStageProjection C ψ i z = 0) → z = 0)

2819 z ?_

2820 intro x hz

2821 apply (Submodule.Quotient.mk_eq_zero

2822 (p := crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ))

2823 (x := x)).2

2824 apply hpre

2825 intro i

2826 have hi := hz i

2827 change

2828 zcCompletedDifferentialModuleStageProjection C ψ i

2829 ((crossedDifferentialRelationSubmodule

2830 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x) = 0 at hi

2831 rw [zcCompletedDifferentialModuleStageProjection_mkQ] at hi

2832 exact hi

2833 apply sub_eq_zero.mp

2834 apply hzero

2835 intro i

2836 rw [map_sub, hcoord i, sub_self]

2837

2838omit [IsTopologicalGroup G] in

2839/-- Kernel-intersection form of finite-stage separation on the algebraic quotient. -/

2840theorem zcDiffModuleStageProjsSeparate_of_relSubmodule_eq_iInf_kernel

2841 (hker :

2842 crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =

2843 zcCompletedDifferentialModulePreStageKernelIntersection C ψ) :

2844 zcCompletedDifferentialModuleStageProjectionsSeparate C ψ :=

2845 zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate C ψ

2846 ((zcDiffModulePreStageProjsSeparate_iff_relSubmodule_eq_iInf_kernel (C := C) (ψ := ψ)).2 hker)

2847

2848omit [IsTopologicalGroup G] in

2849/--

2850If the finite-stage projection product is injective, then equality of every finite coordinate

2851implies equality in the genuine universal module.

2852-/

2853theorem zcCompletedDifferentialModuleStageProjection_ext_of_separating

2854 (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ)

2855 {a b : ZCCompletedDifferentialModule C ψ}

2856 (h : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,

2857 zcCompletedDifferentialModuleStageProjectionAdd C ψ i a =

2858 zcCompletedDifferentialModuleStageProjectionAdd C ψ i b) :

2859 a = b := by

2860 apply hsep

2861 funext i

2862 exact h i

2863

2864omit [IsTopologicalGroup G] in

2865/--

2866The finite-stage completed topology is Hausdorff once the finite-stage projections separate

2867points.

2868-/

2869theorem t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating

2870 (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :

2871 @T2Space (ZCCompletedDifferentialModule C ψ)

2872 (zcCompletedDifferentialModuleNaturalTopology C ψ) := by

2873 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

2874 zcCompletedDifferentialModuleNaturalTopology C ψ

2875 exact T2Space.of_injective_continuous hsep

2876 (continuous_zcCompletedDifferentialModuleStageProjectionProduct_naturalTopology C ψ)

2877

2878omit [IsTopologicalGroup G] in

2879/-- Kernel-intersection form of the Hausdorff property for the finite-stage completed topology. -/

2880theorem t2Space_zcDiffModuleNaturalTopology_of_relSubmodule_eq_iInf_kernel

2881 (hker :

2882 crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =

2883 zcCompletedDifferentialModulePreStageKernelIntersection C ψ) :

2884 @T2Space (ZCCompletedDifferentialModule C ψ)

2885 (zcCompletedDifferentialModuleNaturalTopology C ψ) :=

2886 t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating C ψ

2887 (zcDiffModuleStageProjsSeparate_of_relSubmodule_eq_iInf_kernel

2888 C ψ hker)

2889

2890omit [IsTopologicalGroup G] in

2891/--

2892If finite-stage projections separate the algebraic quotient, then the defining relation

2893submodule is closed for the finite-stage topology on the completed pre-module.

2894-/

2895theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_of_stageProjsSeparate

2896 (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :

2897 zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ := by

2898 letI : TopologicalSpace

2899 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=

2900 zcCompletedDifferentialPreModuleNaturalTopology C ψ

2901 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

2902 zcCompletedDifferentialModuleNaturalTopology C ψ

2903 letI : T2Space (ZCCompletedDifferentialModule C ψ) :=

2904 t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating C ψ hsep

2905 change IsClosed

2906 ((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :

2907 Submodule (ZCCompletedGroupAlgebra C H)

2908 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

2909 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))

2910 have hpreimage :

2911 (((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :

2912 Submodule (ZCCompletedGroupAlgebra C H)

2913 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :

2914 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))) =

2915 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>

2916 (crossedDifferentialRelationSubmodule

2917 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x) ⁻¹'

2918 ({0} : Set (ZCCompletedDifferentialModule C ψ)) := by

2919 ext x

2920 simp only [SetLike.mem_coe, Submodule.mkQ_apply, Set.mem_preimage, Set.mem_singleton_iff,

2921 Submodule.Quotient.mk_eq_zero]

2922 rw [hpreimage]

2923 exact isClosed_singleton.preimage

2924 (continuous_zcCompletedDifferentialModule_mkQ_naturalTopology C ψ)

2925

2926omit [IsTopologicalGroup G] in

2927/--

2928Finite relation reflection implies closedness of the algebraic crossed-differential relation

2929submodule for the finite-stage pre-module topology.

2930-/

2931theorem zcDiffModuleRelSubmoduleClosed_of_finiteRelationReductionsReflectRelations

2932 (hreflect :

2933 zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ) :

2934 zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ :=

2935 zcCompletedDifferentialModuleRelationSubmoduleClosed_of_stageProjsSeparate C ψ

2936 (zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate C ψ

2937 ((zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations (C := C)

2938 (ψ := ψ)).2 hreflect))

2939

2940omit [IsTopologicalGroup G] in

2941/-- Kernel-intersection formulation of finite relation reflection. -/

2942theorem zcDiffModuleFiniteRelationReductionsReflectRelations_iff_relSubmodule_eq_iInf_kernel

2943 (C : ProCGroups.FiniteGroupClass.{u}) (ψ : G →* H) :

2944 zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ ↔

2945 crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =

2946 zcCompletedDifferentialModulePreStageKernelIntersection C ψ :=

2947 (zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations (C := C) (ψ :=

2948 ψ)).symm.trans

2949 (zcDiffModulePreStageProjsSeparate_iff_relSubmodule_eq_iInf_kernel (C := C) (ψ := ψ))

2950

2951omit [IsTopologicalGroup G] in

2952/--

2953In the directed finite-stage situation, closedness of the completed relation submodule is

2954equivalent to finite-stage separation of the algebraic quotient.

2955-/

2956theorem zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate

2957 {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}

2958 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2959 (hdir : Directed (· ≤ ·)

2960 (id : ZCCompletedDifferentialModuleIndex C ψ →

2961 ZCCompletedDifferentialModuleIndex C ψ)) :

2962 zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ ↔

2963 zcCompletedDifferentialModuleStageProjectionsSeparate C ψ := by

2964 constructor

2965 · intro hclosed

2966 exact

2967 zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate C ψ

2968 ((zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations (C :=

2969 C) (ψ := ψ)).2

2970 (zcDiffModuleFiniteRelationReductionsReflectRelations_of_relSubmoduleClosed

2971 C ψ hdir hclosed))

2972 · intro hsep

2973 exact zcCompletedDifferentialModuleRelationSubmoduleClosed_of_stageProjsSeparate C ψ hsep

2974

2975omit [IsTopologicalGroup G] in

2976/--

2977In the directed finite-stage situation, closedness of the defining relation submodule is

2978equivalent to Hausdorffness of the finite-stage natural topology on the algebraic quotient. This

2979is the mathematical version of the paper-level principle that the source completion/closure has

2980been reflected correctly into the closed quotient exactly when the finite-stage topology on the

2981algebraic universal module is separated.

2982-/

2983theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_iff_t2_naturalTopology

2984 {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}

2985 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]

2986 (hdir : Directed (· ≤ ·)

2987 (id : ZCCompletedDifferentialModuleIndex C ψ →

2988 ZCCompletedDifferentialModuleIndex C ψ)) :

2989 zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ ↔

2990 @T2Space (ZCCompletedDifferentialModule C ψ)

2991 (zcCompletedDifferentialModuleNaturalTopology C ψ) := by

2992 constructor

2993 · intro hclosed

2994 exact

2995 t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating C ψ

2996 ((zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate (C := C) (ψ := ψ) hdir).1 hclosed)

2997 · intro hT2

2998 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

2999 zcCompletedDifferentialModuleNaturalTopology C ψ

3000 letI : T2Space (ZCCompletedDifferentialModule C ψ) := hT2

3001 exact

3002 zcCompletedDifferentialModuleRelationSubmoduleClosed_of_t1_naturalTopology

3003 C ψ (by infer_instance)

3004

3005omit [IsTopologicalGroup G] in

3006/-- Addition is continuous for the finite-stage completed topology. -/

3007theorem continuous_add_zcCompletedDifferentialModuleNaturalTopology :

3008 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

3009 zcCompletedDifferentialModuleNaturalTopology C ψ

3010 Continuous (fun p : ZCCompletedDifferentialModule C ψ ×

3011 ZCCompletedDifferentialModule C ψ => p.1 + p.2) := by

3012 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

3013 zcCompletedDifferentialModuleNaturalTopology C ψ

3014 rw [continuous_induced_rng]

3015 change Continuous

3016 (fun p : ZCCompletedDifferentialModule C ψ ×

3017 ZCCompletedDifferentialModule C ψ =>

3018 fun i : ZCCompletedDifferentialModuleIndex C ψ =>

3019 zcCompletedDifferentialModuleStageProjectionAdd C ψ i (p.1 + p.2))

3020 simpa [map_add] using

3021 (continuous_pi fun i =>

3022 ((continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ i).comp

3023 continuous_fst).add

3024 ((continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ i).comp

3025 continuous_snd))

3026

3027omit [IsTopologicalGroup G] in

3028/-- Negation is continuous for the finite-stage completed topology. -/

3029theorem continuous_neg_zcCompletedDifferentialModuleNaturalTopology :

3030 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

3031 zcCompletedDifferentialModuleNaturalTopology C ψ

3032 Continuous (fun a : ZCCompletedDifferentialModule C ψ => -a) := by

3033 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

3034 zcCompletedDifferentialModuleNaturalTopology C ψ

3035 rw [continuous_induced_rng]

3036 change Continuous

3037 (fun a : ZCCompletedDifferentialModule C ψ =>

3038 fun i : ZCCompletedDifferentialModuleIndex C ψ =>

3039 zcCompletedDifferentialModuleStageProjectionAdd C ψ i (-a))

3040 simpa [map_neg] using

3041 (continuous_pi fun i =>

3042 (continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ i).neg)

3043

3044omit [IsTopologicalGroup G] in

3045/-- The finite-stage completed topology is an additive group topology. -/

3046theorem isTopologicalAddGroup_zcCompletedDifferentialModuleNaturalTopology :

3047 @IsTopologicalAddGroup (ZCCompletedDifferentialModule C ψ)

3048 (zcCompletedDifferentialModuleNaturalTopology C ψ) _ := by

3049 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

3050 zcCompletedDifferentialModuleNaturalTopology C ψ

3051 exact

3052 { continuous_add := by

3053 simpa using continuous_add_zcCompletedDifferentialModuleNaturalTopology C ψ

3054 continuous_neg := by

3055 simpa using continuous_neg_zcCompletedDifferentialModuleNaturalTopology C ψ }

3056

3057/-- The finite-stage differential is continuous as a map out of the source group. -/

3058theorem continuous_zcCompletedDifferentialModuleStageDifferential

3059 (i : ZCCompletedDifferentialModuleIndex C ψ) :

3060 Continuous (zcCompletedDifferentialModuleStageDifferential C ψ i) := by

3061 letI : DiscreteTopology (zcCompletedDifferentialModuleStageSource C ψ i) :=

3062 ProCGroups.ProC.OpenNormalSubgroup.quotientDiscrete (G := G) i.source.1

3063 have hdiff :

3064 Continuous (fun q : zcCompletedDifferentialModuleStageSource C ψ i =>

3065 universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i) q) :=

3066 continuous_of_discreteTopology

3067 have hsource :

3068 Continuous (zcCompletedDifferentialModuleStageSourceProj C ψ i) :=

3069 QuotientGroup.continuous_mk

3070 have hcomp := hdiff.comp hsource

3071 change Continuous (zcCompletedDifferentialModuleStageDifferential C ψ i) at hcomp

3072 exact hcomp

3073

3074/--

3075The universal differential is continuous for the finite-stage completed topology on the

3076algebraic quotient.

3077-/

3078theorem continuous_zcUniversalDifferential_naturalTopology :

3079 @Continuous G (ZCCompletedDifferentialModule C ψ) inferInstance

3080 (zcCompletedDifferentialModuleNaturalTopology C ψ)

3081 (zcUniversalDifferential C ψ) := by

3082 rw [continuous_induced_rng]

3083 change Continuous

3084 (fun g : G =>

3085 fun i : ZCCompletedDifferentialModuleIndex C ψ =>

3086 zcCompletedDifferentialModuleStageProjectionAdd C ψ i

3087 (zcUniversalDifferential C ψ g))

3088 refine continuous_pi fun i => ?_

3089 simpa using continuous_zcCompletedDifferentialModuleStageDifferential C ψ i

3090

3091/--

3092The universal final topology on the algebraic quotient is below the finite-stage completed

3093topology.

3094-/

3095theorem zcUniversalDifferentialFinalTopology_le_naturalTopology :

3096 zcUniversalDifferentialFinalTopology C ψ ≤

3097 zcCompletedDifferentialModuleNaturalTopology C ψ :=

3098 (continuous_zcUniversalDifferential_naturalTopology C ψ).coinduced_le

3099

3100omit [IsTopologicalGroup G] in

3101/--

3102The finite-stage boundary map is continuous for the completed differential-module topology

3103defined by the finite-stage projections.

3104-/

3105theorem continuous_zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap

3106 (i : ZCCompletedDifferentialModuleIndex C ψ) :

3107 Continuous (zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψ i) :=

3108 continuous_of_discreteTopology

3109

3110omit [IsTopologicalGroup G] in

3111/-- The algebraic completed boundary is continuous for the finite-stage completed topology. -/

3112theorem continuous_zcToCompletedGroupAlgebra_naturalTopology

3113 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

3114 (ψc : ContinuousMonoidHom G H) :

3115 @Continuous (ZCCompletedDifferentialModule C ψc.toMonoidHom)

3116 (ZCCompletedGroupAlgebra C H)

3117 (zcCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom) inferInstance

3118 (zcToCompletedGroupAlgebra C ψc.toMonoidHom) := by

3119 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψc.toMonoidHom) :=

3120 zcCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom

3121 have hval : Continuous (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>

3122 ((zcToCompletedGroupAlgebra C ψc.toMonoidHom a : ZCCompletedGroupAlgebra C H) :

3123 (j : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H j)) := by

3124 refine continuous_pi fun j => ?_

3125 let i := zcCompletedDifferentialModuleComapIndex C hC ψc j

3126 have hstage : Continuous (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>

3127 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i

3128 (zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i a)) :=

3129 (continuous_zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap

3130 C ψc.toMonoidHom i).comp

3131 (continuous_zcCompletedDifferentialModuleStageProjection_naturalTopology

3132 C ψc.toMonoidHom i)

3133 have hcoord :

3134 (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>

3135 zcCompletedGroupAlgebraProjection C H j

3136 (zcToCompletedGroupAlgebra C ψc.toMonoidHom a)) =

3137 (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>

3138 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i

3139 (zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i a)) := by

3140 funext a

3141 have h :=

3142 congrArg (fun f =>

3143 f a)

3144 (zcDiffModuleStageBoundaryCompletedLinearMap_comp_stageProj

3145 C ψc.toMonoidHom i)

3146 change

3147 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i

3148 (zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i a) =

3149 zcCompletedGroupAlgebraProjectionLinearMap C H i.target

3150 (zcToCompletedGroupAlgebra C ψc.toMonoidHom a) at h

3151 change

3152 zcCompletedGroupAlgebraProjectionLinearMap C H i.target

3153 (zcToCompletedGroupAlgebra C ψc.toMonoidHom a) =

3154 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i

3155 (zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i a)

3156 exact h.symm

3157 rw [hcoord]

3158 exact hstage

3159 simpa only [Subtype.eta] using

3160 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C H) hval

3161 (fun a => (zcToCompletedGroupAlgebra C ψc.toMonoidHom a).property))

3162

3163omit [IsTopologicalGroup G] in

3164/--

3165Scalar multiplication by \(\mathbb{Z}_C\llbracket H\rrbracket\) is continuous for the

3166finite-stage completed topology.

3167-/

3168theorem continuousSMul_zcCompletedDifferentialModuleNaturalTopology :

3169 @ContinuousSMul (ZCCompletedGroupAlgebra C H)

3170 (ZCCompletedDifferentialModule C ψ)

3171 inferInstance inferInstance (zcCompletedDifferentialModuleNaturalTopology C ψ) := by

3172 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=

3173 zcCompletedDifferentialModuleNaturalTopology C ψ

3174 refine ⟨?_⟩

3175 rw [continuous_induced_rng]

3176 change Continuous

3177 (fun p : ZCCompletedGroupAlgebra C H × ZCCompletedDifferentialModule C ψ =>

3178 fun i : ZCCompletedDifferentialModuleIndex C ψ =>

3179 zcCompletedDifferentialModuleStageProjectionAdd C ψ i (p.1 • p.2))

3180 refine continuous_pi fun i => ?_

3181 letI : TopologicalSpace (zcCompletedDifferentialModuleStageRing C ψ i) := inferInstance

3182 letI : DiscreteTopology (zcCompletedDifferentialModuleStageRing C ψ i) := inferInstance

3183 have hstageAction :

3184 Continuous (fun p : zcCompletedDifferentialModuleStageRing C ψ i ×

3185 ZCCompletedDifferentialModuleStage C ψ i => p.1 • p.2) :=

3186 continuous_of_discreteTopology

3187 have hcoeff :

3188 Continuous (fun a : ZCCompletedGroupAlgebra C H =>

3189 zcCompletedGroupAlgebraProjectionRingHom C H i.target a) :=

3190 continuous_zcCompletedGroupAlgebraProjectionRingHom (C := C) (G := H) i.target

3191 have hmodule :

3192 Continuous (fun a : ZCCompletedDifferentialModule C ψ =>

3193 zcCompletedDifferentialModuleStageProjectionAdd C ψ i a) :=

3194 continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ i

3195 have hpair :

3196 Continuous (fun p : ZCCompletedGroupAlgebra C H ×

3197 ZCCompletedDifferentialModule C ψ =>

3198 (zcCompletedGroupAlgebraProjectionRingHom C H i.target p.1,

3199 zcCompletedDifferentialModuleStageProjectionAdd C ψ i p.2)) :=

3200 (hcoeff.comp continuous_fst).prodMk (hmodule.comp continuous_snd)

3201 have hcomp :

3202 Continuous

3203 ((fun p : zcCompletedDifferentialModuleStageRing C ψ i ×

3204 ZCCompletedDifferentialModuleStage C ψ i => p.1 • p.2) ∘

3205 fun p : ZCCompletedGroupAlgebra C H ×

3206 ZCCompletedDifferentialModule C ψ =>

3207 (zcCompletedGroupAlgebraProjectionRingHom C H i.target p.1,

3208 zcCompletedDifferentialModuleStageProjectionAdd C ψ i p.2)) :=

3209 hstageAction.comp hpair

3210 have hfun :

3211 (fun p : ZCCompletedGroupAlgebra C H × ZCCompletedDifferentialModule C ψ =>

3212 zcCompletedDifferentialModuleStageProjectionAdd C ψ i (p.1 • p.2)) =

3213 ((fun p : zcCompletedDifferentialModuleStageRing C ψ i ×

3214 ZCCompletedDifferentialModuleStage C ψ i => p.1 • p.2) ∘

3215 fun p : ZCCompletedGroupAlgebra C H ×

3216 ZCCompletedDifferentialModule C ψ =>

3217 (zcCompletedGroupAlgebraProjectionRingHom C H i.target p.1,

3218 zcCompletedDifferentialModuleStageProjectionAdd C ψ i p.2)) := by

3219 funext p

3220 change

3221 zcCompletedDifferentialModuleStageProjection C ψ i (p.1 • p.2) =

3222 zcCompletedGroupAlgebraProjectionRingHom C H i.target p.1 •

3223 zcCompletedDifferentialModuleStageProjection C ψ i p.2

3224 rw [map_smul, zcCompletedDifferentialModuleStage_completed_smul]

3225 rw [hfun]

3226 exact hcomp

3227

3228end

3229

3230end FoxDifferential