FoxDifferential/Completed/Continuous/Universal/NaturalTopology.lean
1import FoxDifferential.Completed.Continuous.Universal.System
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Continuous/Universal/NaturalTopology.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Continuous crossed differentials
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.Completion
21open ProCGroups.ProC
23universe u
25variable (C : ProCGroups.FiniteGroupClass.{u})
26variable {G H : Type u}
27variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29variable (ψ : G →* H)
31/-- The additive finite-stage projection from the algebraic completed differential module. -/
33 (i : ZCCompletedDifferentialModuleIndex C ψ) :
34 ZCCompletedDifferentialModule C ψ →+
35 ZCCompletedDifferentialModuleStage C ψ i :=
36 (zcCompletedDifferentialModuleStageProjection C ψ i).toAddMonoidHom
38omit [IsTopologicalGroup G] in
39@[simp]
41 (i : ZCCompletedDifferentialModuleIndex C ψ)
42 (a : ZCCompletedDifferentialModule C ψ) :
44 zcCompletedDifferentialModuleStageProjection C ψ i a :=
45 rfl
47omit [IsTopologicalGroup G] in
48@[simp]
50 (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
52 (zcUniversalDifferential C ψ g) =
53 zcCompletedDifferentialModuleStageDifferential C ψ i g :=
56/-- The product of all finite source/target/coefficient projections of the algebraic quotient. -/
59 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
60 ZCCompletedDifferentialModuleStage C ψ i :=
61 fun a i => zcCompletedDifferentialModuleStageProjectionAdd C ψ i a
63omit [IsTopologicalGroup G] in
64@[simp]
66 (a : ZCCompletedDifferentialModule C ψ)
67 (i : ZCCompletedDifferentialModuleIndex C ψ) :
70 rfl
72/-- The finite-stage completed topology on the algebraic completed differential module.
74This topology is named deliberately: it is not installed as a global instance. -/
76 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
77 TopologicalSpace.induced
78 (zcCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstance
80omit [IsTopologicalGroup G] in
81/-- The product map defining the finite-stage completed topology is continuous. -/
83 @Continuous (ZCCompletedDifferentialModule C ψ)
84 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
86 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
88 continuous_induced_dom
90omit [IsTopologicalGroup G] in
91/-- Each finite-stage projection is continuous for the finite-stage completed topology. -/
93 (i : ZCCompletedDifferentialModuleIndex C ψ) :
94 @Continuous (ZCCompletedDifferentialModule C ψ)
95 (ZCCompletedDifferentialModuleStage C ψ i)
96 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
97 (zcCompletedDifferentialModuleStageProjectionAdd C ψ i) := by
98 have hprod :=
100 simpa [zcCompletedDifferentialModuleStageProjectionProduct, Function.comp_def] using
101 (@Continuous.comp
103 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
106 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance inferInstance
108 (g := fun x => x i)
109 (continuous_apply i) hprod)
111omit [IsTopologicalGroup G] in
113 (i : ZCCompletedDifferentialModuleIndex C ψ) :
114 @Continuous (ZCCompletedDifferentialModule C ψ)
116 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
117 (zcCompletedDifferentialModuleStageProjection C ψ i) := by
118 simpa using
121/-- A named predicate for the algebraic separation still needed to make the natural topology
123def zcCompletedDifferentialModuleStageProjectionsSeparate : Prop :=
124 Function.Injective (zcCompletedDifferentialModuleStageProjectionProduct C ψ)
126/-- A pre-quotient formulation of finite-stage separation: the only finite formal
128crossed-differential relations. -/
130 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
131 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
133 (R := ZCCompletedGroupAlgebra C H)
134 (zcCompletedDifferentialModuleStageDifferential C ψ i) x = 0) →
137/-- The kernel on the pre-module cut out by one finite source/target/coefficient stage. -/
139 (i : ZCCompletedDifferentialModuleIndex C ψ) :
140 Submodule (ZCCompletedGroupAlgebra C H)
141 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
142 LinearMap.ker
144 (R := ZCCompletedGroupAlgebra C H)
147omit [IsTopologicalGroup G] in
148@[simp]
150 (i : ZCCompletedDifferentialModuleIndex C ψ)
151 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
152 x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i ↔
154 (R := ZCCompletedGroupAlgebra C H)
155 (zcCompletedDifferentialModuleStageDifferential C ψ i) x = 0 :=
156 Iff.rfl
158omit [IsTopologicalGroup G] in
159/-- Membership in a finite pre-stage kernel is equivalently membership of the explicit
162 (i : ZCCompletedDifferentialModuleIndex C ψ)
163 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
164 x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i ↔
165 zcCompletedDifferentialModulePreStageMap C ψ i x ∈
167 (zcCompletedDifferentialModuleStageScalar C ψ i) := by
168 constructor
169 · intro hx
170 have hq :
172 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
173 (zcCompletedDifferentialModulePreStageMap C ψ i x) = 0 := by
175 exact hx
176 exact
177 (Submodule.Quotient.mk_eq_zero
180 (x := zcCompletedDifferentialModulePreStageMap C ψ i x)).1 hq
181 · intro hx
182 have hq :
184 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
185 (zcCompletedDifferentialModulePreStageMap C ψ i x) = 0 :=
186 (Submodule.Quotient.mk_eq_zero
189 (x := zcCompletedDifferentialModulePreStageMap C ψ i x)).2 hx
192 exact hq
194omit [IsTopologicalGroup G] in
195/-- Every defining crossed-differential relation is killed by every finite stage. -/
197 (i : ZCCompletedDifferentialModuleIndex C ψ) :
199 zcCompletedDifferentialModulePreStageKernel C ψ i := by
200 simpa [zcCompletedDifferentialModulePreStageKernel] using
202 (A := ZCCompletedDifferentialModuleStage C ψ i)
207omit [IsTopologicalGroup G] in
208/-- The explicit finite pre-stage map sends completed crossed-differential relations to finite
209crossed-differential relations. -/
211 (i : ZCCompletedDifferentialModuleIndex C ψ)
212 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}
213 (hx : x ∈ crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)) :
214 zcCompletedDifferentialModulePreStageMap C ψ i x ∈
216 (zcCompletedDifferentialModuleStageScalar C ψ i) :=
218 C ψ i x).1
220 (C := C) (ψ := ψ) i hx)
222/-- The common finite-stage kernel on the pre-module. -/
224 Submodule (ZCCompletedGroupAlgebra C H)
225 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
226 ⨅ i : ZCCompletedDifferentialModuleIndex C ψ,
229omit [IsTopologicalGroup G] in
230/-- The common finite-stage kernel can be read as the condition that every explicit finite
233 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
235 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
236 zcCompletedDifferentialModulePreStageMap C ψ i x ∈
238 (zcCompletedDifferentialModuleStageScalar C ψ i) := by
239 rw [zcCompletedDifferentialModulePreStageKernelIntersection, Submodule.mem_iInf]
240 constructor
241 · intro hx i
242 exact
244 C ψ i x).1 (hx i)
245 · intro hx i
246 exact
248 C ψ i x).2 (hx i)
250/-- The finite-stage closed relation submodule defining the separated completed
251`ψ`-differential module. -/
253 Submodule (ZCCompletedGroupAlgebra C H)
254 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
257/-- The separated completed `ψ`-differential module.
260abbrev ZCSeparatedCompletedDifferentialModule : Type u :=
264/-- Paper-facing Crowell module `A_ψ(C)`.
267not the algebraic quotient `ZCCompletedDifferentialModule`. -/
271omit [IsTopologicalGroup G] in
272/-- Algebraic crossed-differential relations vanish in the finite-stage separated quotient. -/
275 (zcCompletedGroupAlgebraScalar C ψ) ≤
277 intro x hx
280 intro i
283/-- The universal differential into the separated completed quotient. -/
284def zcSeparatedUniversalDifferential (g : G) :
287 (Finsupp.single g 1)
289omit [IsTopologicalGroup G] in
290/-- The separated universal differential satisfies the crossed product rule. -/
291theorem zcSeparatedUniversalDifferential_mul (g h : G) :
292 zcSeparatedUniversalDifferential C ψ (g * h) =
293 zcSeparatedUniversalDifferential C ψ g +
294 zcCompletedGroupAlgebraScalar C ψ g •
295 zcSeparatedUniversalDifferential C ψ h := by
296 have hzero :
299 (zcCompletedGroupAlgebraScalar C ψ) g h) = 0 := by
300 exact
301 (Submodule.Quotient.mk_eq_zero
304 (zcCompletedGroupAlgebraScalar C ψ) g h)).2
307 (zcCompletedGroupAlgebraScalar C ψ) g h))
308 have hzero' :
309 zcSeparatedUniversalDifferential C ψ (g * h) -
310 (zcSeparatedUniversalDifferential C ψ g +
312 (zcCompletedGroupAlgebraScalar C ψ g • Finsupp.single h 1)) = 0 := by
313 simpa [zcSeparatedUniversalDifferential, crossedDifferentialRelationElement] using hzero
314 have hsmul :
316 (zcCompletedGroupAlgebraScalar C ψ g • Finsupp.single h 1) =
317 zcCompletedGroupAlgebraScalar C ψ g •
318 zcSeparatedUniversalDifferential C ψ h := by
319 simpa [zcSeparatedUniversalDifferential, Submodule.mkQ_apply] using
320 (Submodule.Quotient.mk_smul
322 (r := zcCompletedGroupAlgebraScalar C ψ g)
323 (x := Finsupp.single h 1))
324 have hzero'' :
325 zcSeparatedUniversalDifferential C ψ (g * h) -
326 (zcSeparatedUniversalDifferential C ψ g +
327 zcCompletedGroupAlgebraScalar C ψ g •
328 zcSeparatedUniversalDifferential C ψ h) = 0 := by
329 rw [hsmul] at hzero'
330 exact hzero'
331 exact sub_eq_zero.mp hzero''
333omit [IsTopologicalGroup G] in
334/-- The separated universal differential is a crossed differential. -/
338 (zcSeparatedUniversalDifferential C ψ) := by
339 intro g h
340 exact zcSeparatedUniversalDifferential_mul C ψ g h
342omit [IsTopologicalGroup G] in
343/-- Commutator formula for the separated universal differential when the right factor lies in the
344kernel of the target homomorphism. -/
346 (g h : G) (hh : ψ h = 1) :
347 zcSeparatedUniversalDifferential C ψ ⁅g, h⁆ =
348 (zcGroupLike C H (ψ g) - 1) •
349 zcSeparatedUniversalDifferential C ψ h := by
350 let δ := zcSeparatedUniversalDifferential C ψ
351 let coeff := zcCompletedGroupAlgebraScalar C ψ
352 have hcross :
353 IsCrossedDifferential coeff δ :=
355 have hcomm := IsCrossedDifferential.commutator hcross g h
356 have hconj : ψ (g * h * g⁻¹) = 1 := by
358 have hcommKer : ψ ⁅g, h⁆ = 1 := by
360 calc
361 δ ⁅g, h⁆ =
362 δ g + zcGroupLike C H (ψ g) • δ h - δ g - δ h := by
363 simpa only [δ, coeff, zcCompletedGroupAlgebraScalar_apply, hconj,
365 _ = zcGroupLike C H (ψ g) • δ h - δ h := by
366 abel
367 _ = (zcGroupLike C H (ψ g) - 1) • δ h := by
368 rw [sub_smul, one_smul]
370omit [IsTopologicalGroup G] in
371/-- A representative is zero in the separated quotient exactly when all finite reductions are
374 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
375 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x =
376 (0 : ZCSeparatedCompletedDifferentialModule C ψ) ↔
377 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
378 zcCompletedDifferentialModulePreStageMap C ψ i x ∈
380 (zcCompletedDifferentialModuleStageScalar C ψ i) := by
381 constructor
382 · intro hx
383 exact
385 ((Submodule.Quotient.mk_eq_zero
387 (x := x)).1 hx)
388 · intro hx
389 exact
390 (Submodule.Quotient.mk_eq_zero
392 (x := x)).2
395/-- Finite-stage projection from the separated completed quotient. -/
397 (i : ZCCompletedDifferentialModuleIndex C ψ) :
399 ZCCompletedDifferentialModuleStage C ψ i :=
402 (R := ZCCompletedGroupAlgebra C H)
404 (by
405 intro x hx
406 rw [LinearMap.mem_ker]
407 have hxstage :
408 zcCompletedDifferentialModulePreStageMap C ψ i x ∈
410 (zcCompletedDifferentialModuleStageScalar C ψ i) :=
412 (by
413 simpa [zcCompletedDifferentialRelationFiniteClosedSubmodule] using hx) i
414 have hq :
416 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
417 (zcCompletedDifferentialModulePreStageMap C ψ i x) = 0 :=
418 (Submodule.Quotient.mk_eq_zero
421 (x := zcCompletedDifferentialModulePreStageMap C ψ i x)).2 hxstage
422 rw [zcCompletedDifferentialModulePreStageMap_mkQ] at hq
423 exact hq)
425omit [IsTopologicalGroup G] in
426@[simp]
428 (i : ZCCompletedDifferentialModuleIndex C ψ)
429 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
431 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x) =
433 (R := ZCCompletedGroupAlgebra C H)
434 (zcCompletedDifferentialModuleStageDifferential C ψ i) x := by
435 rw [zcSeparatedCompletedDifferentialModuleStageProjectionAdd, Submodule.mkQ_apply,
436 Submodule.liftQ_apply]
438omit [IsTopologicalGroup G] in
439@[simp]
441 (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
443 (zcSeparatedUniversalDifferential C ψ g) =
444 zcCompletedDifferentialModuleStageDifferential C ψ i g := by
447 simp only [crossedDifferentialModuleLiftLinear_single, one_smul]
449/-- The product of all finite-stage projections from the separated completed quotient. -/
452 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
453 ZCCompletedDifferentialModuleStage C ψ i :=
454 fun a i => zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a
456omit [IsTopologicalGroup G] in
457@[simp]
459 (a : ZCSeparatedCompletedDifferentialModule C ψ)
460 (i : ZCCompletedDifferentialModuleIndex C ψ) :
463 rfl
465omit [IsTopologicalGroup G] in
466/-- The finite-stage projections separate points of the separated completed quotient. -/
468 ∀ x : ZCSeparatedCompletedDifferentialModule C ψ,
469 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
470 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x = 0) →
471 x = 0 := by
472 intro x
473 refine Submodule.Quotient.induction_on
475 (C := fun x =>
476 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
477 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x = 0) →
478 x = 0)
479 x ?_
480 intro y hy
481 apply
482 (Submodule.Quotient.mk_eq_zero
484 (x := y)).2
485 exact
487 (by
488 intro i
489 have hlin :
491 (R := ZCCompletedGroupAlgebra C H)
492 (zcCompletedDifferentialModuleStageDifferential C ψ i) y = 0 := by
493 simpa using hy i
494 have hq :
496 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
497 (zcCompletedDifferentialModulePreStageMap C ψ i y) = 0 := by
499 exact hlin
500 exact
501 (Submodule.Quotient.mk_eq_zero
504 (x := zcCompletedDifferentialModulePreStageMap C ψ i y)).1 hq)
506omit [IsTopologicalGroup G] in
507/-- The finite-stage projection product is injective on the separated completed quotient. -/
509 Function.Injective
511 intro x y hxy
512 apply sub_eq_zero.mp
514 intro i
515 have hi :
517 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i y := by
518 simpa [zcSeparatedCompletedDifferentialModuleStageProjectionProduct] using congrFun hxy i
519 rw [map_sub, hi, sub_self]
521omit [IsTopologicalGroup G] in
522/-- Extensionality for the separated completed quotient by finite-stage projections. -/
524 {a b : ZCSeparatedCompletedDifferentialModule C ψ}
525 (h : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
528 a = b :=
530 (funext h)
532/-- The natural map from the algebraic quotient to the finite-stage separated quotient. -/
534 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
537 (zcCompletedGroupAlgebraScalar C ψ)).liftQ
539 (by
540 intro x hx
541 rw [LinearMap.mem_ker]
542 exact
543 (Submodule.Quotient.mk_eq_zero
545 (x := x)).2
548omit [IsTopologicalGroup G] in
549@[simp]
550theorem zcCompletedDifferentialModuleToSeparated_universal (g : G) :
552 (zcUniversalDifferential C ψ g) =
553 zcSeparatedUniversalDifferential C ψ g := by
554 simp only [zcCompletedDifferentialModuleToSeparated, zcUniversalDifferential, universalCrossedDifferential,
555 Submodule.mkQ_apply, Submodule.liftQ_apply, zcSeparatedUniversalDifferential]
557omit [IsTopologicalGroup G] in
558/-- The pre-quotient completed boundary kills the finite-stage closed relation submodule.
560This is the descent input for the separated boundary
561`A_psi(C)_sep -> Z_C[[H]]`. -/
564 (ψc : ContinuousMonoidHom G H)
565 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}
566 (hx : x ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψc.toMonoidHom) :
568 (R := ZCCompletedGroupAlgebra C H)
569 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x = 0 := by
571 intro j
572 let i := zcCompletedDifferentialModuleComapIndex C hC ψc j
573 have hxall :
574 ∀ i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom,
575 zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x ∈
577 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i) := by
579 exact
581 C ψc.toMonoidHom x).1 hx
582 have hxstage :
583 zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x ∈
585 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i) :=
586 hxall i
587 have hstage_zero :
588 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
590 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
591 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) = 0 := by
592 have hq :
594 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
595 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x) = 0 :=
596 (Submodule.Quotient.mk_eq_zero
598 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i))
599 (x := zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)).2 hxstage
601 have hcompat :=
602 congrArg
603 (fun f =>
604 f
606 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x))
608 C ψc.toMonoidHom i)
609 have hstage_proj :
610 zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i
612 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x) =
614 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
615 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x) := by
618 (zcCompletedDifferentialModulePreStageMap_mkQ C ψc.toMonoidHom i x).symm
619 have hboundary_quot :
620 zcToCompletedGroupAlgebra C ψc.toMonoidHom
622 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x) =
624 (R := ZCCompletedGroupAlgebra C H)
625 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x := by
626 rfl
627 have hproj_eq :
630 (R := ZCCompletedGroupAlgebra C H)
631 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x) =
632 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
634 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
635 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) := by
636 calc
639 (R := ZCCompletedGroupAlgebra C H)
640 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x) =
641 zcCompletedGroupAlgebraProjection C H i.target
642 (zcToCompletedGroupAlgebra C ψc.toMonoidHom
644 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x)) := by
645 rw [hboundary_quot]
646 simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedDifferentialModuleComapIndex, i]
647 _ =
648 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
649 (zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i
651 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x)) := by
652 simpa [LinearMap.comp_apply] using hcompat.symm
653 _ =
654 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
656 (zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
657 (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) := by
658 rw [hstage_proj]
659 rw [hproj_eq, hstage_zero]
660 simp only [zcCompletedGroupAlgebraProjection_zero]
662/-- The completed boundary descends to the separated completed differential module. -/
665 (ψc : ContinuousMonoidHom G H) :
666 ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
667 ZCCompletedGroupAlgebra C H :=
668 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψc.toMonoidHom).liftQ
670 (R := ZCCompletedGroupAlgebra C H)
671 (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom))
672 (by
673 intro x hx
674 rw [LinearMap.mem_ker]
676 C hC ψc hx)
678omit [IsTopologicalGroup G] in
679@[simp]
682 (ψc : ContinuousMonoidHom G H)
683 (g : G) :
685 (zcSeparatedUniversalDifferential C ψc.toMonoidHom g) =
686 zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom g := by
688 zcSeparatedUniversalDifferential, Submodule.mkQ_apply, Submodule.liftQ_apply]
689 simp only [ContinuousMonoidHom.coe_toMonoidHom, crossedDifferentialModuleLiftLinear_single, smul_eq_mul,
690 one_mul]
692omit [IsTopologicalGroup G] in
695 (ψc : ContinuousMonoidHom G H) :
696 (zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC ψc).comp
697 (zcCompletedDifferentialModuleToSeparated C ψc.toMonoidHom) =
698 zcToCompletedGroupAlgebra C ψc.toMonoidHom := by
699 apply zcCompletedDifferentialModuleHom_ext C ψc.toMonoidHom
700 intro g
701 rw [LinearMap.comp_apply, zcCompletedDifferentialModuleToSeparated_universal,
705/-- Algebraic relation-reflection form of finite-stage separation: if every finite
707crossed-differential relation, then the original element is already in the raw completed
708crossed-differential relation submodule.
710This is an algebraic `ZCCompletedDifferentialModule` compatibility predicate, not an input for the
711final separated profinite Crowell middle term. -/
713 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
714 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
715 zcCompletedDifferentialModulePreStageMap C ψ i x ∈
717 (zcCompletedDifferentialModuleStageScalar C ψ i)) →
720/-- The finite-stage topology on the completed pre-module, before quotienting by the
721crossed-differential relations. -/
723 TopologicalSpace (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
724 TopologicalSpace.induced
725 (zcCompletedDifferentialPreModuleStageFamilyMap C ψ) inferInstance
727omit [IsTopologicalGroup G] in
728/-- Each finite pre-stage reduction is continuous for the finite-stage topology on the completed
729pre-module. -/
731 (i : ZCCompletedDifferentialModuleIndex C ψ) :
732 @Continuous
738 (⊥ : TopologicalSpace
741 (zcCompletedDifferentialModuleStageSource C ψ i)))
742 (zcCompletedDifferentialModulePreStageMap C ψ i) := by
743 letI : TopologicalSpace
744 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
746 let S := zcCompletedDifferentialPreModuleStageSystem C ψ
747 have hfamily :
748 @Continuous
752 inferInstance
754 continuous_induced_dom
755 have hproj := (S.continuous_projection i).comp hfamily
756 simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using hproj
758/-- The quotient topology on the separated completed module induced from the finite-stage
759topology on the completed pre-module. -/
761 TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
762 TopologicalSpace.coinduced
766omit [IsTopologicalGroup G] in
767/-- The quotient map to the separated completed module is continuous for the finite-stage
768pre-module topology and the separated quotient topology. -/
770 @Continuous
775 (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ :=
776 continuous_coinduced_rng
778omit [IsTopologicalGroup G] in
779/-- The quotient map defining the separated completed module is a quotient map for the
782 letI : TopologicalSpace
783 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
785 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
787 Topology.IsQuotientMap (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ := by
788 letI : TopologicalSpace
789 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
791 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
793 rw [Topology.isQuotientMap_iff]
794 constructor
795 · exact
796 Submodule.Quotient.mk_surjective
798 · intro s
799 rfl
801omit [IsTopologicalGroup G] in
802/-- Continuity out of the separated completed module can be tested after precomposing with the
803defining quotient map. -/
805 {A : Type u} [TopologicalSpace A]
806 (f : ZCSeparatedCompletedDifferentialModule C ψ → A) :
807 @Continuous
809 (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ) inferInstance f ↔
810 @Continuous
811 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) A
812 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance
813 (fun x => f ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x)) := by
814 letI : TopologicalSpace
815 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
817 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
819 simpa [Function.comp_def] using
821 C ψ).continuous_iff (g := f)
823omit [IsTopologicalGroup G] in
824/-- Each finite-stage projection from the separated completed quotient is continuous for the
825separated quotient topology. -/
827 (i : ZCCompletedDifferentialModuleIndex C ψ) :
828 @Continuous
832 inferInstance
833 (zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i) := by
834 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
836 letI : TopologicalSpace
837 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
839 rw [continuous_coinduced_dom]
840 change
841 @Continuous
845 inferInstance
846 (fun x =>
848 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x))
849 letI : TopologicalSpace
852 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
853 ⊥
854 letI : DiscreteTopology
857 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
858 ⟨rfl⟩
859 have hpre :
860 @Continuous
866 inferInstance
867 (zcCompletedDifferentialModulePreStageMap C ψ i) :=
869 letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
870 letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
871 have hq :
872 Continuous
873 (fun y :
876 (zcCompletedDifferentialModuleStageSource C ψ i) =>
878 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ y) :=
879 continuous_of_discreteTopology
880 have hcoord :
881 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
883 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x)) =
884 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
886 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
887 (zcCompletedDifferentialModulePreStageMap C ψ i x)) := by
888 funext x
891 rw [hcoord]
892 exact hq.comp hpre
894omit [IsTopologicalGroup G] in
895/-- The separated finite-stage projection product is continuous for the separated quotient
896topology. -/
898 @Continuous
900 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
903 inferInstance
905 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
907 exact
908 continuous_pi fun i =>
909 by
913omit [IsTopologicalGroup G] in
914/-- The separated completed quotient is Hausdorff for the separated finite-stage quotient
915topology. -/
917 @T2Space
920 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
922 exact T2Space.of_injective_continuous
926omit [IsTopologicalGroup G] in
927/-- In the directed finite-stage situation, the separated quotient topology is exactly the
930 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
931 (hdir : Directed (· ≤ ·)
932 (id : ZCCompletedDifferentialModuleIndex C ψ →
935 TopologicalSpace.induced
936 (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstance := by
937 ext U
938 constructor
939 · intro hU
940 let Tind : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
941 TopologicalSpace.induced
942 (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstance
943 rw [@isOpen_iff_forall_mem_open
944 (ZCSeparatedCompletedDifferentialModule C ψ) Tind U]
945 intro x hxU
946 refine Submodule.Quotient.induction_on
948 (C := fun x =>
949 x ∈ U → ∃ t, t ⊆ U ∧ @IsOpen
950 (ZCSeparatedCompletedDifferentialModule C ψ) Tind t ∧ x ∈ t)
951 x ?_ hxU
952 intro a haU
953 let q :
957 have hpreOpen :
958 @IsOpen
961 (q ⁻¹' U) := by
962 simpa [q, zcSeparatedCompletedDifferentialModuleNaturalTopology] using hU
963 rcases isOpen_induced_iff.mp hpreOpen with ⟨V, hVopen, hVeq⟩
964 have haV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ a ∈ V := by
965 have haU' : a ∈ q ⁻¹' U := haU
966 rwa [← hVeq] at haU'
967 let S := zcCompletedDifferentialPreModuleStageSystem C ψ
968 rcases S.exists_projection_preimage_subset hdir hVopen haV with
969 ⟨i, W, hWopen, haW, hWV⟩
970 let t : Set (ZCSeparatedCompletedDifferentialModule C ψ) :=
971 {z | zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i z =
973 refine ⟨t, ?_, ?_, ?_⟩
974 · intro z hz
975 refine Submodule.Quotient.induction_on
977 (C := fun z => z ∈ t → z ∈ U) z ?_ hz
978 intro b hb
979 have hcoord :
980 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q b) =
981 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q a) := hb
982 have hstageRel :
983 zcCompletedDifferentialModulePreStageMap C ψ i (b - a) ∈
985 (zcCompletedDifferentialModuleStageScalar C ψ i) := by
986 apply (Submodule.Quotient.mk_eq_zero
989 (x := zcCompletedDifferentialModulePreStageMap C ψ i (b - a))).1
990 have hq :
992 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
993 (zcCompletedDifferentialModulePreStageMap C ψ i (b - a)) = 0 := by
994 have hbq :
996 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
997 (zcCompletedDifferentialModulePreStageMap C ψ i b) =
999 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
1000 (zcCompletedDifferentialModulePreStageMap C ψ i a) := by
1003 simpa [q] using hcoord
1004 have hzero :
1006 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
1007 (zcCompletedDifferentialModulePreStageMap C ψ i b) -
1009 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
1010 (zcCompletedDifferentialModulePreStageMap C ψ i a) = 0 :=
1011 sub_eq_zero.mpr hbq
1012 simpa [map_sub] using hzero
1013 exact hq
1015 C ψ i hstageRel with
1016 ⟨r, hr, hrstage⟩
1017 have hqa : q (b - r) = q b := by
1018 have hrclosed : r ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ :=
1020 apply (Submodule.Quotient.eq
1022 change (b - r) - b ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ
1023 have hdiff : (b - r) - b = -r := by
1024 abel
1025 rw [hdiff]
1026 exact (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).neg_mem hrclosed
1027 have hpre_eq :
1028 zcCompletedDifferentialModulePreStageMap C ψ i (b - r) =
1029 zcCompletedDifferentialModulePreStageMap C ψ i a := by
1030 have hcalc :
1031 zcCompletedDifferentialModulePreStageMap C ψ i (b - a) =
1032 zcCompletedDifferentialModulePreStageMap C ψ i r := hrstage.symm
1033 have hsub :
1034 zcCompletedDifferentialModulePreStageMap C ψ i b -
1035 zcCompletedDifferentialModulePreStageMap C ψ i a =
1036 zcCompletedDifferentialModulePreStageMap C ψ i r := by
1037 simpa [map_sub] using hcalc
1038 rw [map_sub]
1039 rw [← hsub]
1040 abel
1041 have hbW : S.projection i
1042 (zcCompletedDifferentialPreModuleStageFamilyMap C ψ (b - r)) ∈ W := by
1043 change zcCompletedDifferentialModulePreStageMap C ψ i (b - r) ∈ W
1044 rw [hpre_eq]
1045 simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using haW
1046 have hbV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ (b - r) ∈ V := hWV hbW
1047 have hbU : q (b - r) ∈ U := by
1048 have hbV' :
1049 (b - r) ∈ zcCompletedDifferentialPreModuleStageFamilyMap C ψ ⁻¹' V := hbV
1050 rwa [hVeq] at hbV'
1051 rwa [hqa] at hbU
1052 · letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) := Tind
1053 have hprod :
1054 Continuous (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) :=
1055 continuous_induced_dom
1056 have hcoord :
1057 Continuous (fun z : ZCSeparatedCompletedDifferentialModule C ψ =>
1058 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i z) := by
1060 (continuous_apply i).comp hprod
1061 haveI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
1062 exact (isOpen_discrete
1063 ({zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q a)} :
1064 Set (ZCCompletedDifferentialModuleStage C ψ i))).preimage hcoord
1065 · exact rfl
1066 · intro hU
1067 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
1069 rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVU⟩
1070 rw [← hVU]
1071 exact hVopen.preimage
1074/-- The pre-module generator map `g ↦ dg` is continuous for the finite-stage pre-module
1075topology. -/
1077 @Continuous G
1079 inferInstance
1081 (fun g : G => Finsupp.single g (1 : ZCCompletedGroupAlgebra C H)) := by
1082 rw [continuous_induced_rng]
1083 let S := zcCompletedDifferentialPreModuleStageSystem C ψ
1084 let preSingle :
1085 ∀ i : ZCCompletedDifferentialModuleIndex C ψ, G → S.X i := fun i g =>
1087 (Finsupp.single g (1 : ZCCompletedGroupAlgebra C H))
1088 have hpreSingle_continuous : ∀ i, Continuous (preSingle i) := by
1089 intro i
1090 letI : TopologicalSpace
1093 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
1094 ⊥
1095 letI : DiscreteTopology
1098 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
1099 ⟨rfl⟩
1100 have hsource :
1101 Continuous (zcCompletedDifferentialModuleStageSourceProj C ψ i) := by
1102 simpa [zcCompletedDifferentialModuleStageSourceProj] using
1103 (continuous_quotient_mk' : Continuous (fun g : G =>
1104 QuotientGroup.mk' (i.source.1 : Subgroup G) g))
1105 have hsingle :
1106 Continuous (fun q : zcCompletedDifferentialModuleStageSource C ψ i =>
1107 Finsupp.single q (1 : zcCompletedDifferentialModuleStageRing C ψ i)) :=
1108 continuous_of_discreteTopology
1109 simpa [preSingle, zcCompletedDifferentialModulePreStageMap_single] using
1110 hsingle.comp hsource
1111 have hpreSingle_compat : S.CompatibleMaps preSingle := by
1112 intro i j hij
1113 funext g
1114 exact
1115 congrFun
1117 (Finsupp.single g (1 : ZCCompletedGroupAlgebra C H))
1118 have hLift : Continuous (S.inverseLimitLift preSingle hpreSingle_compat) :=
1119 S.continuous_inverseLimitLift preSingle hpreSingle_continuous hpreSingle_compat
1120 have hEq :
1122 (fun g : G => Finsupp.single g (1 : ZCCompletedGroupAlgebra C H)) =
1123 S.inverseLimitLift preSingle hpreSingle_compat := by
1124 apply S.inverseLimitLift_unique preSingle hpreSingle_compat
1125 intro i
1126 funext g
1127 rfl
1128 rw [hEq]
1129 exact hLift
1131/-- The separated universal differential is continuous for the separated finite-stage quotient
1132topology. -/
1134 @Continuous G
1136 inferInstance
1138 (zcSeparatedUniversalDifferential C ψ) := by
1139 letI : TopologicalSpace
1140 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1142 exact
1146omit [IsTopologicalGroup G] in
1147/-- A pre-quotient linear lift is continuous for the finite-stage pre-module topology when it
1151 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1152 [TopologicalSpace A]
1153 (delta : G → A)
1154 (i : ZCCompletedDifferentialModuleIndex C ψ)
1155 (L :
1158 (zcCompletedDifferentialModuleStageSource C ψ i) → A)
1159 (hfactor :
1160 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
1162 (R := ZCCompletedGroupAlgebra C H) delta x =
1163 L (zcCompletedDifferentialModulePreStageMap C ψ i x)) :
1164 @Continuous
1166 A
1168 inferInstance
1170 (R := ZCCompletedGroupAlgebra C H) delta) := by
1171 letI : TopologicalSpace
1172 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1174 letI : TopologicalSpace
1177 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
1178 ⊥
1179 letI : DiscreteTopology
1182 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
1183 ⟨rfl⟩
1184 have hpre :
1185 @Continuous
1191 inferInstance
1192 (zcCompletedDifferentialModulePreStageMap C ψ i) :=
1194 have hL : Continuous L := continuous_of_discreteTopology
1195 have hfun :
1196 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
1198 (R := ZCCompletedGroupAlgebra C H) delta x) =
1199 fun x => L (zcCompletedDifferentialModulePreStageMap C ψ i x) := by
1200 funext x
1201 exact hfactor x
1202 change
1203 @Continuous
1205 A
1207 inferInstance
1208 (fun x =>
1210 (R := ZCCompletedGroupAlgebra C H) delta x)
1211 rw [hfun]
1212 exact hL.comp hpre
1214omit [IsTopologicalGroup G] in
1215/-- The canonical lift to a finite differential-module stage is continuous for the finite-stage
1216pre-module topology. -/
1218 (i : ZCCompletedDifferentialModuleIndex C ψ) :
1219 @Continuous
1223 inferInstance
1225 (R := ZCCompletedGroupAlgebra C H)
1226 (zcCompletedDifferentialModuleStageDifferential C ψ i)) := by
1227 exact
1229 C ψ
1231 i
1232 (fun y =>
1234 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ y)
1235 (by
1236 intro x
1237 exact (zcCompletedDifferentialModulePreStageMap_mkQ C ψ i x).symm)
1239/-- The raw algebraic crossed-differential relation submodule is closed for the finite-stage
1240topology on the completed pre-module. This closedness condition makes the algebraic quotient
1241separated; the separated quotient construction records this condition structurally. -/
1242def zcCompletedDifferentialModuleRelationSubmoduleClosed : Prop :=
1243 @IsClosed
1247 (zcCompletedGroupAlgebraScalar C ψ) :
1248 Submodule (ZCCompletedGroupAlgebra C H)
1249 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set
1252omit [IsTopologicalGroup G] in
1253/-- A useful non-circular closedness criterion. If a Hausdorff/T1 target receives an injective
1254linear map from the algebraic completed differential module, and the composite from the completed
1256crossed-differential relation submodule is closed.
1259isolates the real topological input: continuity of the pre-quotient coordinate map. -/
1261 {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
1262 [TopologicalSpace M] [T1Space M]
1263 (L :
1264 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] M)
1265 (hLinj : Function.Injective L)
1266 (hcont :
1267 @Continuous
1269 M
1271 inferInstance
1272 (fun x =>
1273 L
1275 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x))) :
1277 letI : TopologicalSpace
1278 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1280 change IsClosed
1282 Submodule (ZCCompletedGroupAlgebra C H)
1283 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1284 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))
1285 have hpreimage :
1287 Submodule (ZCCompletedGroupAlgebra C H)
1288 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1289 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =
1290 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
1291 L
1293 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x)) ⁻¹' ({0} : Set M) := by
1294 ext x
1295 constructor
1296 · intro hx
1297 have hq :
1299 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x :
1300 ZCCompletedDifferentialModule C ψ) = 0 :=
1301 (Submodule.Quotient.mk_eq_zero
1304 (x := x)).2 hx
1305 change
1306 L
1308 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x) = 0
1309 rw [hq]
1311 · intro hx
1312 have hq :
1314 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x :
1315 ZCCompletedDifferentialModule C ψ) = 0 := by
1316 apply hLinj
1317 simpa using hx
1318 exact
1319 (Submodule.Quotient.mk_eq_zero
1322 (x := x)).1 hq
1323 rw [hpreimage]
1324 exact isClosed_singleton.preimage hcont
1326omit [IsTopologicalGroup G] in
1327/-- The quotient map from the completed pre-module to the algebraic quotient is continuous for the
1330 @Continuous
1335 (crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)).mkQ := by
1336 letI : TopologicalSpace
1337 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1339 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
1341 rw [continuous_induced_rng]
1342 change Continuous
1343 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
1344 fun i : ZCCompletedDifferentialModuleIndex C ψ =>
1347 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x))
1348 refine continuous_pi fun i => ?_
1349 let S := zcCompletedDifferentialPreModuleStageSystem C ψ
1350 letI : TopologicalSpace
1353 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
1354 ⊥
1355 letI : DiscreteTopology
1358 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
1359 ⟨rfl⟩
1360 have hpre :
1361 @Continuous
1366 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance
1367 (zcCompletedDifferentialModulePreStageMap C ψ i) := by
1368 have hfamily :
1369 @Continuous
1372 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance
1374 continuous_induced_dom
1375 have hproj := (S.continuous_projection i).comp hfamily
1376 simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using hproj
1377 letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
1378 letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
1379 have hq :
1380 Continuous
1381 (fun y :
1384 (zcCompletedDifferentialModuleStageSource C ψ i) =>
1386 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ y) :=
1387 continuous_of_discreteTopology
1388 have hcomp := hq.comp hpre
1389 have hcoord :
1390 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
1393 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x)) =
1394 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
1396 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
1397 (zcCompletedDifferentialModulePreStageMap C ψ i x)) := by
1398 funext x
1402 rw [hcoord]
1403 exact hcomp
1405omit [IsTopologicalGroup G] in
1406/-- If the finite-stage natural topology on the algebraic quotient is already T1,
1407then the defining crossed-differential relation submodule is closed in the completed pre-module
1410This is the quotient-topology reflection statement: the relation submodule is the preimage
1411of `{0}` under the continuous algebraic quotient map. -/
1413 (hT1 :
1414 @T1Space (ZCCompletedDifferentialModule C ψ)
1417 letI : TopologicalSpace
1418 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1420 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
1422 letI : T1Space (ZCCompletedDifferentialModule C ψ) := hT1
1423 change IsClosed
1425 Submodule (ZCCompletedGroupAlgebra C H)
1426 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1427 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))
1428 have hpreimage :
1430 Submodule (ZCCompletedGroupAlgebra C H)
1431 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1432 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =
1433 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
1435 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x) ⁻¹'
1436 ({0} : Set (ZCCompletedDifferentialModule C ψ)) := by
1437 ext x
1438 simp only [SetLike.mem_coe, Submodule.mkQ_apply, Set.mem_preimage, Set.mem_singleton_iff,
1439 Submodule.Quotient.mk_eq_zero]
1440 rw [hpreimage]
1441 exact isClosed_singleton.preimage
1444omit [IsTopologicalGroup G] in
1445/-- A quotient-level non-circular closedness criterion. If the algebraic completed differential
1446module admits an injective continuous map from its finite-stage natural topology to a T1 target,
1447then the defining crossed-differential relation submodule is closed in the pre-module finite-stage
1448topology.
1450This packages the topological reflection step through the continuous algebraic quotient map
1451from the pre-module. -/
1453 {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
1454 [TopologicalSpace M] [T1Space M]
1455 (L :
1456 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] M)
1457 (hLinj : Function.Injective L)
1458 (hcont :
1459 @Continuous
1460 (ZCCompletedDifferentialModule C ψ) M
1461 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
1462 L) :
1465 C ψ L hLinj
1466 (@Continuous.comp
1468 (ZCCompletedDifferentialModule C ψ) M
1470 (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
1472 (zcCompletedGroupAlgebraScalar C ψ)).mkQ)
1473 (g := L) hcont
1476omit [IsTopologicalGroup G] in
1477/-- Finite relation-valued reductions put a pre-module element in the finite-stage closure of the
1478completed crossed-differential relation submodule. -/
1480 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
1481 (hdir : Directed (· ≤ ·)
1482 (id : ZCCompletedDifferentialModuleIndex C ψ →
1484 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
1485 (hx : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
1486 zcCompletedDifferentialModulePreStageMap C ψ i x ∈
1488 (zcCompletedDifferentialModuleStageScalar C ψ i)) :
1489 x ∈ @closure
1493 (zcCompletedGroupAlgebraScalar C ψ) :
1494 Submodule (ZCCompletedGroupAlgebra C H)
1495 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set
1496 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
1497 letI : TopologicalSpace
1498 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1500 rw [mem_closure_iff]
1501 intro U hU hxU
1502 rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVeq⟩
1503 have hxV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ x ∈ V := by
1504 rw [← hVeq] at hxU
1505 exact hxU
1506 let S := zcCompletedDifferentialPreModuleStageSystem C ψ
1507 rcases S.exists_projection_preimage_subset hdir hVopen hxV with
1508 ⟨i, W, hWopen, hxW, hWU⟩
1510 C ψ hdir ({i} : Finset (ZCCompletedDifferentialModuleIndex C ψ)) x hx with
1511 ⟨r, hr, hrstage⟩
1512 refine ⟨r, ?_, hr⟩
1513 have hri : zcCompletedDifferentialModulePreStageMap C ψ i r =
1514 zcCompletedDifferentialModulePreStageMap C ψ i x := by
1515 exact hrstage i (by simp only [Finset.mem_singleton])
1516 have hrW :
1517 S.projection i (zcCompletedDifferentialPreModuleStageFamilyMap C ψ r) ∈ W := by
1518 change zcCompletedDifferentialModulePreStageMap C ψ i r ∈ W
1519 rw [hri]
1520 simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using hxW
1521 have hrV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ r ∈ V := hWU hrW
1522 rw [← hVeq]
1523 exact hrV
1525omit [IsTopologicalGroup G] in
1526/-- Each finite-stage pre-kernel is closed for the finite-stage topology on the completed
1527pre-module. -/
1529 (i : ZCCompletedDifferentialModuleIndex C ψ) :
1530 @IsClosed
1534 Submodule (ZCCompletedGroupAlgebra C H)
1535 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1536 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
1537 letI : TopologicalSpace
1538 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1540 let S := zcCompletedDifferentialPreModuleStageSystem C ψ
1541 letI : TopologicalSpace
1544 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
1545 ⊥
1546 letI : DiscreteTopology
1549 (zcCompletedDifferentialModuleStageSource C ψ i)) :=
1550 ⟨rfl⟩
1551 have hpre :
1552 Continuous (zcCompletedDifferentialModulePreStageMap C ψ i) := by
1553 have hfamily :
1554 @Continuous
1557 (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance
1559 continuous_induced_dom
1560 have hproj := (S.continuous_projection i).comp hfamily
1561 simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using hproj
1562 have hpreimage :
1563 IsClosed
1564 ((zcCompletedDifferentialModulePreStageMap C ψ i) ⁻¹'
1566 (zcCompletedDifferentialModuleStageScalar C ψ i)) :
1567 Submodule
1571 (zcCompletedDifferentialModuleStageSource C ψ i))) :
1574 (zcCompletedDifferentialModuleStageSource C ψ i)))) := by
1575 exact
1576 (isClosed_discrete
1578 (zcCompletedDifferentialModuleStageScalar C ψ i)) :
1579 Submodule
1583 (zcCompletedDifferentialModuleStageSource C ψ i))) :
1586 (zcCompletedDifferentialModuleStageSource C ψ i)))).preimage hpre
1587 have hset :
1589 Submodule (ZCCompletedGroupAlgebra C H)
1590 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1591 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =
1592 ((zcCompletedDifferentialModulePreStageMap C ψ i) ⁻¹'
1594 (zcCompletedDifferentialModuleStageScalar C ψ i)) :
1595 Submodule
1599 (zcCompletedDifferentialModuleStageSource C ψ i))) :
1602 (zcCompletedDifferentialModuleStageSource C ψ i)))) := by
1603 ext x
1604 exact
1606 C ψ i x
1607 simpa [hset] using hpreimage
1609omit [IsTopologicalGroup G] in
1610/-- The finite-stage closed relation denominator is closed for the finite-stage pre-module
1611topology. -/
1613 @IsClosed
1617 Submodule (ZCCompletedGroupAlgebra C H)
1618 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1619 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
1620 letI : TopologicalSpace
1621 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1623 change IsClosed
1625 Submodule (ZCCompletedGroupAlgebra C H)
1626 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1627 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))
1629 simpa [Submodule.coe_iInf] using
1630 (isClosed_iInter
1631 (fun i =>
1633 C ψ i))
1635omit [IsTopologicalGroup G] in
1636/-- The zero class is closed in the separated completed differential module for the finite-stage
1637quotient topology. -/
1639 @IsClosed (ZCSeparatedCompletedDifferentialModule C ψ)
1641 ({0} : Set (ZCSeparatedCompletedDifferentialModule C ψ)) := by
1642 letI : TopologicalSpace
1643 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1645 rw [zcSeparatedCompletedDifferentialModuleNaturalTopology, isClosed_coinduced]
1646 have hpreimage :
1647 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ ⁻¹'
1648 ({0} : Set (ZCSeparatedCompletedDifferentialModule C ψ))) =
1650 Submodule (ZCCompletedGroupAlgebra C H)
1651 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1652 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
1653 ext x
1654 simp only [Set.mem_preimage, Submodule.mkQ_apply, Set.mem_singleton_iff, Submodule.Quotient.mk_eq_zero,
1655 SetLike.mem_coe]
1656 rw [hpreimage]
1659omit [IsTopologicalGroup G] in
1660/-- The finite-stage closed relation denominator is exactly the closure of the algebraic
1663 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
1664 (hdir : Directed (· ≤ ·)
1665 (id : ZCCompletedDifferentialModuleIndex C ψ →
1667 @closure
1671 (zcCompletedGroupAlgebraScalar C ψ) :
1672 Submodule (ZCCompletedGroupAlgebra C H)
1674 (ZCCompletedGroupAlgebra C H) G)) :
1675 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =
1677 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
1678 letI : TopologicalSpace
1679 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1681 apply Set.Subset.antisymm
1682 · intro x hxcl
1683 change x ∈ zcCompletedDifferentialModulePreStageKernelIntersection C ψ
1684 exact
1686 (by
1687 intro i
1688 have hclosed_i :=
1690 have hsubset_i :
1692 Submodule (ZCCompletedGroupAlgebra C H)
1693 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1694 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) ⊆
1696 Submodule (ZCCompletedGroupAlgebra C H)
1697 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1698 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
1699 intro y hy
1700 exact
1702 (C := C) (ψ := ψ) i hy
1703 have hxker : x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i :=
1704 closure_minimal hsubset_i hclosed_i hxcl
1705 exact
1707 C ψ i x).1 hxker)
1708 · intro x hxhat
1709 have hxstage :
1710 ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
1711 zcCompletedDifferentialModulePreStageMap C ψ i x ∈
1713 (zcCompletedDifferentialModuleStageScalar C ψ i) :=
1715 (by
1716 simpa [zcCompletedDifferentialRelationFiniteClosedSubmodule] using hxhat)
1717 exact
1719 C ψ hdir x hxstage
1721omit [IsTopologicalGroup G] in
1722/-- A continuous pre-quotient lift to a T1 target kills the finite-stage closed relation
1723denominator. This is the general descent criterion for maps out of the separated completed
1724universal module. -/
1726 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1727 [TopologicalSpace A] [T1Space A]
1728 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
1729 (hdir : Directed (· ≤ ·)
1730 (id : ZCCompletedDifferentialModuleIndex C ψ →
1732 (delta : G → A)
1733 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
1734 (hcont :
1735 @Continuous
1737 A
1739 inferInstance
1741 (R := ZCCompletedGroupAlgebra C H) delta))
1742 {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}
1743 (hx : x ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ) :
1745 (R := ZCCompletedGroupAlgebra C H) delta x = 0 := by
1746 letI : TopologicalSpace
1747 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
1749 have hxcl :
1750 x ∈ closure
1752 (zcCompletedGroupAlgebraScalar C ψ) :
1753 Submodule (ZCCompletedGroupAlgebra C H)
1754 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1755 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
1756 have hEq :=
1758 C ψ hdir
1759 rw [hEq]
1760 exact hx
1761 have hker_closed :
1762 IsClosed
1763 ((fun y : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
1765 (R := ZCCompletedGroupAlgebra C H) delta y) ⁻¹'
1766 ({0} : Set A)) :=
1767 isClosed_singleton.preimage hcont
1768 have hrel_subset_ker :
1770 (zcCompletedGroupAlgebraScalar C ψ) :
1771 Submodule (ZCCompletedGroupAlgebra C H)
1772 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
1773 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) ⊆
1774 ((fun y : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
1776 (R := ZCCompletedGroupAlgebra C H) delta y) ⁻¹'
1777 ({0} : Set A)) := by
1778 intro y hy
1779 exact
1781 (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdelta) hy
1782 exact closure_minimal hrel_subset_ker hker_closed hxcl
1784/-- The separated universal lift induced by a crossed differential whose pre-quotient lift is
1787 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1788 [TopologicalSpace A] [T1Space A]
1789 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
1790 (hdir : Directed (· ≤ ·)
1791 (id : ZCCompletedDifferentialModuleIndex C ψ →
1793 (delta : G → A)
1794 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
1795 (hcont :
1796 @Continuous
1798 A
1800 inferInstance
1802 (R := ZCCompletedGroupAlgebra C H) delta)) :
1803 ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A :=
1806 (R := ZCCompletedGroupAlgebra C H) delta)
1807 (by
1808 intro x hx
1809 rw [LinearMap.mem_ker]
1810 exact
1812 C ψ hdir delta hdelta hcont hx)
1814omit [IsTopologicalGroup G] in
1815@[simp 900]
1817 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1818 [TopologicalSpace A] [T1Space A]
1819 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
1820 (hdir : Directed (· ≤ ·)
1821 (id : ZCCompletedDifferentialModuleIndex C ψ →
1823 (delta : G → A)
1824 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
1825 (hcont :
1826 @Continuous
1828 A
1830 inferInstance
1832 (R := ZCCompletedGroupAlgebra C H) delta))
1833 (g : G) :
1835 C ψ hdir delta hdelta hcont
1836 (zcSeparatedUniversalDifferential C ψ g) =
1837 delta g := by
1839 zcSeparatedUniversalDifferential, Submodule.mkQ_apply, Submodule.liftQ_apply]
1840 simp only [crossedDifferentialModuleLiftLinear_single, one_smul]
1842omit [IsTopologicalGroup G] in
1843@[ext]
1845 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1846 {f h : ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A}
1847 (hfh : ∀ g, f (zcSeparatedUniversalDifferential C ψ g) =
1848 h (zcSeparatedUniversalDifferential C ψ g)) :
1849 f = h := by
1850 apply Submodule.linearMap_qext _
1851 apply Finsupp.lhom_ext
1852 intro g r
1853 have hsingle :
1855 (Finsupp.single g r) :
1857 r • zcSeparatedUniversalDifferential C ψ g := by
1858 rw [← Finsupp.smul_single_one]
1859 rfl
1860 change f ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
1861 (Finsupp.single g r)) =
1862 h ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
1863 (Finsupp.single g r))
1866omit [IsTopologicalGroup G] in
1868 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1869 [TopologicalSpace A] [T1Space A]
1870 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
1871 (hdir : Directed (· ≤ ·)
1872 (id : ZCCompletedDifferentialModuleIndex C ψ →
1874 (delta : G → A)
1875 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
1876 (hcont :
1877 @Continuous
1879 A
1881 inferInstance
1883 (R := ZCCompletedGroupAlgebra C H) delta))
1884 (f : ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A)
1885 (hf : ∀ g, f (zcSeparatedUniversalDifferential C ψ g) = delta g) :
1886 f =
1888 C ψ hdir delta hdelta hcont := by
1890 intro g
1893/-- The separated universal lift bundled as a continuous linear map for the separated quotient
1894topology. -/
1896 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1897 [TopologicalSpace A] [T1Space A]
1898 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
1899 (hdir : Directed (· ≤ ·)
1900 (id : ZCCompletedDifferentialModuleIndex C ψ →
1902 (delta : G → A)
1903 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
1904 (hcont :
1905 @Continuous
1907 A
1909 inferInstance
1911 (R := ZCCompletedGroupAlgebra C H) delta)) :
1912 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
1914 ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A := by
1915 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
1917 refine
1918 { toLinearMap :=
1920 C ψ hdir delta hdelta hcont
1921 cont := ?_ }
1922 rw [continuous_coinduced_dom]
1923 change
1924 @Continuous
1926 A
1928 inferInstance
1929 (fun x =>
1931 C ψ hdir delta hdelta hcont
1932 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x))
1933 have hcomp :
1934 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
1936 C ψ hdir delta hdelta hcont
1937 ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x)) =
1939 (R := ZCCompletedGroupAlgebra C H) delta := by
1940 funext x
1942 Submodule.mkQ_apply, Submodule.liftQ_apply]
1943 rw [hcomp]
1944 exact hcont
1946omit [IsTopologicalGroup G] in
1947@[simp 900]
1949 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1950 [TopologicalSpace A] [T1Space A]
1951 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
1952 (hdir : Directed (· ≤ ·)
1953 (id : ZCCompletedDifferentialModuleIndex C ψ →
1955 (delta : G → A)
1956 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
1957 (hcont :
1958 @Continuous
1960 A
1962 inferInstance
1964 (R := ZCCompletedGroupAlgebra C H) delta))
1965 (m : ZCSeparatedCompletedDifferentialModule C ψ) :
1967 C ψ hdir delta hdelta hcont m =
1969 C ψ hdir delta hdelta hcont m :=
1970 rfl
1972/-- Continuous representation theorem for the separated completed module, parameterized by the
1973topological input that turns a continuous crossed differential into a continuous pre-quotient
1974linear lift. -/
1976 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1977 [TopologicalSpace A] [T1Space A]
1978 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
1979 (hdir : Directed (· ≤ ·)
1980 (id : ZCCompletedDifferentialModuleIndex C ψ →
1982 (hprelift :
1983 ∀ (delta : G → A),
1984 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta →
1985 Continuous delta →
1986 @Continuous
1988 A
1990 inferInstance
1992 (R := ZCCompletedGroupAlgebra C H) delta)) :
1993 {delta : G → A //
1994 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta ∧
1995 Continuous delta} ≃
1996 (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
1998 ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) where
1999 toFun delta :=
2001 C ψ hdir delta.1 delta.2.1 (hprelift delta.1 delta.2.1 delta.2.2)
2002 invFun f := by
2003 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
2005 exact ⟨fun g => f (zcSeparatedUniversalDifferential C ψ g), by
2006 constructor
2007 · intro g h
2008 change f (zcSeparatedUniversalDifferential C ψ (g * h)) =
2009 f (zcSeparatedUniversalDifferential C ψ g) +
2010 zcCompletedGroupAlgebraScalar C ψ g •
2011 f (zcSeparatedUniversalDifferential C ψ h)
2013 simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul]
2014 · exact f.cont.comp (continuous_zcSeparatedUniversalDifferential_naturalTopology C ψ)⟩
2015 left_inv delta := by
2016 apply Subtype.ext
2017 funext g
2018 exact
2020 C ψ hdir delta.1 delta.2.1
2021 (hprelift delta.1 delta.2.1 delta.2.2) g
2022 right_inv f := by
2023 letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
2025 apply ContinuousLinearMap.ext
2026 intro m
2027 have hdelta :
2029 (fun g => f (zcSeparatedUniversalDifferential C ψ g)) := by
2030 intro g h
2031 change f (zcSeparatedUniversalDifferential C ψ (g * h)) =
2032 f (zcSeparatedUniversalDifferential C ψ g) +
2033 zcCompletedGroupAlgebraScalar C ψ g •
2034 f (zcSeparatedUniversalDifferential C ψ h)
2036 simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul]
2037 have hcontinuous_delta :
2038 Continuous (fun g => f (zcSeparatedUniversalDifferential C ψ g)) :=
2039 f.cont.comp (continuous_zcSeparatedUniversalDifferential_naturalTopology C ψ)
2040 have hlin :
2041 f.toLinearMap =
2043 C ψ hdir
2044 (fun g => f (zcSeparatedUniversalDifferential C ψ g))
2045 hdelta
2046 (hprelift
2047 (fun g => f (zcSeparatedUniversalDifferential C ψ g))
2048 hdelta hcontinuous_delta) := by
2050 C ψ hdir
2051 intro g
2052 rfl
2053 exact congrFun (congrArg DFunLike.coe hlin.symm) m
2055/-- Continuous representation theorem with the finite-stage index nonemptiness and directedness
2057remaining topological input is the pre-quotient lift continuity. -/
2059 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
2060 [TopologicalSpace A] [T1Space A]
2063 (hForm : ProCGroups.FiniteGroupClass.Formation C)
2064 (ψc : ContinuousMonoidHom G H)
2065 (hprelift :
2066 ∀ (delta : G → A),
2067 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta →
2068 Continuous delta →
2069 @Continuous
2071 A
2072 (zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom)
2073 inferInstance
2075 (R := ZCCompletedGroupAlgebra C H) delta)) :
2076 {delta : G → A //
2077 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta ∧
2078 Continuous delta} ≃
2079 (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom) :=
2080 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom
2081 ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →L[ZCCompletedGroupAlgebra C H] A) := by
2082 letI : Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom) :=
2084 exact
2086 C ψc.toMonoidHom
2087 (directed_zcCompletedDifferentialModuleIndex C hForm hC ψc)
2088 hprelift
2090/-- Continuous representation theorem for the separated completed module when every continuous
2092pre-stage. This packages the finite-stage factorization criterion into the universal property, so
2093the public theorem no longer takes the raw `hprelift` continuity hypothesis. -/
2095 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
2096 [TopologicalSpace A] [T1Space A]
2097 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
2098 (hdir : Directed (· ≤ ·)
2099 (id : ZCCompletedDifferentialModuleIndex C ψ →
2101 (hfactor :
2102 ∀ (delta : G → A),
2103 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta →
2104 Continuous delta →
2105 ∃ i : ZCCompletedDifferentialModuleIndex C ψ,
2106 ∃ L :
2109 (zcCompletedDifferentialModuleStageSource C ψ i) → A,
2110 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
2112 (R := ZCCompletedGroupAlgebra C H) delta x =
2113 L (zcCompletedDifferentialModulePreStageMap C ψ i x)) :
2114 {delta : G → A //
2115 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta ∧
2116 Continuous delta} ≃
2117 (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
2119 ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) := by
2120 refine
2122 C ψ hdir ?_
2123 intro delta hdelta hcont
2124 rcases hfactor delta hdelta hcont with ⟨i, L, hL⟩
2125 exact
2127 C ψ delta i L hL
2129/-- Continuous representation theorem with finite-stage index data supplied from a continuous
2132 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
2133 [TopologicalSpace A] [T1Space A]
2136 (hForm : ProCGroups.FiniteGroupClass.Formation C)
2137 (ψc : ContinuousMonoidHom G H)
2138 (hfactor :
2139 ∀ (delta : G → A),
2140 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta →
2141 Continuous delta →
2142 ∃ i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom,
2143 ∃ L :
2145 (zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i)
2146 (zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i) → A,
2147 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
2149 (R := ZCCompletedGroupAlgebra C H) delta x =
2150 L (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) :
2151 {delta : G → A //
2152 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta ∧
2153 Continuous delta} ≃
2154 (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom) :=
2155 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom
2156 ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →L[ZCCompletedGroupAlgebra C H] A) := by
2157 letI : Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom) :=
2159 exact
2161 C ψc.toMonoidHom
2162 (directed_zcCompletedDifferentialModuleIndex C hForm hC ψc)
2163 hfactor
2165/-- The `Z_C[[H]]`-action on a finite discrete target factors through one finite
2166coefficient-and-`H` stage. -/
2168 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
2169 [TopologicalSpace A] [Fintype A] [DiscreteTopology A]
2170 [ContinuousSMul (ZCCompletedGroupAlgebra C H) A]
2171 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
2172 ∃ j : ZCCompletedGroupAlgebraIndex C H,
2173 ∃ act : ZCCompletedGroupAlgebraStage C H j → A → A,
2174 ∀ (r : ZCCompletedGroupAlgebra C H) (a : A),
2175 act (zcCompletedGroupAlgebraProjection C H j r) a = r • a := by
2176 classical
2177 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly C) :=
2180 hForm.containsTrivialQuotients
2181 letI : Nonempty (ProCIntegerIndex C) :=
2182 ⟨ProCIntegerIndex.terminal (C := C) inferInstance⟩
2183 letI : Nonempty (CompletedGroupAlgebraIndexInClass H C) :=
2184 ⟨_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndexInClass (G := H) C⟩
2185 letI : Nonempty (ZCCompletedGroupAlgebraIndex C H) := inferInstance
2186 letI : Finite (A → A) := Finite.of_fintype (A → A)
2187 let S := zcCompletedGroupAlgebraSystem C H
2188 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, TopologicalSpace (S.X i) := fun _ => by
2189 dsimp [S, zcCompletedGroupAlgebraSystem]
2190 infer_instance
2191 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, CompactSpace (S.X i) := fun i => by
2192 dsimp [S, zcCompletedGroupAlgebraSystem]
2193 infer_instance
2194 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, T2Space (S.X i) := fun i => by
2195 dsimp [S, zcCompletedGroupAlgebraSystem]
2196 infer_instance
2197 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, TotallyDisconnectedSpace (S.X i) := fun i => by
2198 dsimp [S, zcCompletedGroupAlgebraSystem]
2199 infer_instance
2200 let ρ : ZCCompletedGroupAlgebra C H → A → A := fun r a => r • a
2201 have hρ : Continuous ρ := by
2202 change Continuous (fun r : ZCCompletedGroupAlgebra C H => fun a : A => r • a)
2203 exact continuous_pi fun a => continuous_id.smul continuous_const
2204 rcases S.factors_through_projection_finite
2205 (directed_zcCompletedGroupAlgebraIndex_of_formation C (H := H) hForm)
2206 ρ hρ with
2207 ⟨j, act, _hact_continuous, hact⟩
2208 refine ⟨j, act, ?_⟩
2209 intro r a
2210 have h := congrFun (congrFun hact r) a
2211 simpa [ρ, S, zcCompletedGroupAlgebraSystem] using h.symm
2213omit [IsTopologicalGroup G] in
2214/-- A finite discrete target crossed differential has a pre-quotient lift factoring through one
2217 {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
2218 [TopologicalSpace A] [Fintype A] [DiscreteTopology A]
2219 [ContinuousSMul (ZCCompletedGroupAlgebra C H) A]
2221 (hForm : ProCGroups.FiniteGroupClass.Formation C)
2222 (ψc : ContinuousMonoidHom G H)
2223 (hG : ProCGroups.ProC.IsProCGroup C G)
2224 (delta : G → A)
2225 (hdelta : IsCrossedDifferential
2226 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta)
2227 (hcont : Continuous delta) :
2228 ∃ i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom,
2229 ∃ L :
2231 (zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i)
2232 (zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i) → A,
2233 ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
2235 (R := ZCCompletedGroupAlgebra C H) delta x =
2236 L (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x) := by
2237 classical
2239 (C := C) (H := H) (A := A) hForm with
2240 ⟨target, act, hact⟩
2241 have hdelta_one : delta 1 = 0 := by
2242 have h := hdelta 1 1
2244 have h' := congrArg (fun z : A => z - delta 1) h
2245 have hzero : 0 = delta 1 := by
2246 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
2247 simpa using hzero.symm
2248 let W : Set G := {g | delta g = 0}
2249 have hWopen : IsOpen W := by
2250 change IsOpen (delta ⁻¹' ({0} : Set A))
2251 exact (isOpen_discrete _).preimage hcont
2252 have h1W : (1 : G) ∈ W := by
2253 simpa [W] using hdelta_one
2254 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hWopen h1W with
2255 ⟨V0, hV0W⟩
2256 let comapSource : OpenNormalSubgroupInClass C G :=
2257 OrderDual.ofDual
2258 (completedGroupAlgebraComapIndexInClass
2259 (G := G) (H := H) C hC ψc target.2)
2260 let source : OpenNormalSubgroupInClass C G :=
2261 ⟨V0.1 ⊓ comapSource.1,
2263 (C := C) (G := G) hForm V0.1 comapSource.1 V0.2 comapSource.2⟩
2264 let i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom :=
2265 { source := source
2266 target := target
2267 compatible := by
2268 intro g hg
2269 have hgcomap : g ∈ (comapSource.1 : Subgroup G) := hg.2
2270 change ψc.toMonoidHom g ∈
2271 ((((OrderDual.ofDual target.2).1 : OpenNormalSubgroup H) : Subgroup H))
2272 simpa [comapSource, completedGroupAlgebraComapIndexInClass] using hgcomap }
2273 have hsource_delta_zero :
2274 ∀ g : G, g ∈ (source.1 : Subgroup G) → delta g = 0 := by
2275 intro g hg
2276 exact hV0W hg.1
2277 let deltaBar : zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i → A :=
2278 Quotient.lift delta (by
2279 intro a b hab
2280 have hab_source : a⁻¹ * b ∈ (source.1 : Subgroup G) :=
2281 (QuotientGroup.leftRel_apply).1 hab
2282 have hab_zero : delta (a⁻¹ * b) = 0 :=
2283 hsource_delta_zero (a⁻¹ * b) hab_source
2284 have hprod := hdelta a (a⁻¹ * b)
2285 have hrewrite : a * (a⁻¹ * b) = b := by simp only [mul_inv_cancel_left]
2286 have hb : delta b =
2287 delta a + zcCompletedGroupAlgebraScalar C ψc.toMonoidHom a •
2288 delta (a⁻¹ * b) := by
2289 simpa [hrewrite] using hprod
2290 rw [hab_zero, smul_zero, add_zero] at hb
2291 exact hb.symm)
2292 let coeffMap :
2293 zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i →
2294 zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i →+ A :=
2295 fun q =>
2296 { toFun := fun a => act a (deltaBar q)
2297 map_zero' := by
2298 have h := hact (0 : ZCCompletedGroupAlgebra C H) (deltaBar q)
2299 simpa using h
2300 map_add' := by
2301 intro a b
2302 rcases zcCompletedGroupAlgebraProjection_surjective C H target a with ⟨ra, hra⟩
2303 rcases zcCompletedGroupAlgebraProjection_surjective C H target b with ⟨rb, hrb⟩
2304 calc
2305 act (a + b) (deltaBar q)
2306 = act (zcCompletedGroupAlgebraProjection C H target (ra + rb)) (deltaBar q) := by
2307 simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedGroupAlgebraProjection_add, hra, hrb]
2308 _ = (ra + rb) • deltaBar q := hact (ra + rb) (deltaBar q)
2309 _ = ra • deltaBar q + rb • deltaBar q := add_smul ra rb (deltaBar q)
2310 _ = act a (deltaBar q) + act b (deltaBar q) := by
2311 rw [← hact ra (deltaBar q), ← hact rb (deltaBar q), hra, hrb] }
2312 let Llin :
2314 (zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i)
2315 (zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i) →ₗ[ℕ] A :=
2316 Finsupp.lsum ℕ fun q => (coeffMap q).toNatLinearMap
2317 refine ⟨i, (fun y => Llin y), ?_⟩
2318 intro x
2320 · simp only [crossedDifferentialModuleLiftLinear, map_zero, ContinuousMonoidHom.coe_toMonoidHom,
2322 · intro x y hx hy
2324 · intro g a
2327 change a • delta g =
2328 Llin
2329 (Finsupp.single (zcCompletedDifferentialModuleStageSourceProj C ψc.toMonoidHom i g)
2330 (zcCompletedGroupAlgebraProjection C H i.target a))
2331 rw [Finsupp.lsum_single]
2332 change a • delta g =
2333 act (zcCompletedGroupAlgebraProjection C H target a)
2334 (deltaBar (zcCompletedDifferentialModuleStageSourceProj C ψc.toMonoidHom i g))
2335 simpa [deltaBar, zcCompletedDifferentialModuleStageSourceProj] using
2336 (hact a (delta g)).symm
2338omit [IsTopologicalGroup G] in
2339/-- For a profinite target module, continuity of the crossed differential forces continuity of
2342 {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
2343 [TopologicalSpace M]
2345 (hForm : ProCGroups.FiniteGroupClass.Formation C)
2346 (ψc : ContinuousMonoidHom G H)
2347 (hG : ProCGroups.ProC.IsProCGroup C G)
2348 (hM : _root_.CompletedGroupAlgebra.IsProfiniteModule
2349 (ZCCompletedGroupAlgebra C H) M)
2350 (delta : G → M)
2351 (hdelta : IsCrossedDifferential
2352 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta)
2353 (hcont : Continuous delta) :
2354 @Continuous
2356 M
2357 (zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom)
2358 inferInstance
2360 (R := ZCCompletedGroupAlgebra C H) delta) := by
2361 classical
2362 letI : IsTopologicalAddGroup M := hM.2.1
2363 letI : ContinuousAdd M := inferInstance
2364 letI : TopologicalSpace
2365 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
2366 zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom
2367 apply _root_.CompletedGroupAlgebra.continuous_of_forall_openSubmodule_quotient_continuous
2368 (R := ZCCompletedGroupAlgebra C H) M hM
2369 intro W hWopen
2370 let hdisc : _root_.CompletedGroupAlgebra.IsDiscreteModule
2371 (ZCCompletedGroupAlgebra C H) (M ⧸ W) :=
2372 _root_.CompletedGroupAlgebra.quotient_openSubmodule_isDiscreteModule
2373 (ZCCompletedGroupAlgebra C H) M hM W hWopen
2374 letI : DiscreteTopology (M ⧸ W) := hdisc.2
2375 letI : ContinuousSMul (ZCCompletedGroupAlgebra C H) (M ⧸ W) := hdisc.1.2.2
2376 letI : Fintype (M ⧸ W) :=
2377 Classical.choice
2378 (_root_.CompletedGroupAlgebra.finite_quotient_of_openSubmodule
2379 (ZCCompletedGroupAlgebra C H) M hM W hWopen)
2380 let deltaQ : G → M ⧸ W := fun g => Submodule.mkQ W (delta g)
2381 have hdeltaQ : IsCrossedDifferential
2382 (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) deltaQ :=
2383 IsCrossedDifferential.map_linear hdelta (Submodule.mkQ W)
2384 have hqcont : Continuous (Submodule.mkQ W : M → M ⧸ W) := by
2385 change Continuous (Submodule.Quotient.mk (p := W))
2386 exact continuous_quotient_mk'
2387 have hcontQ : Continuous deltaQ := hqcont.comp hcont
2389 (C := C) (H := H) (A := M ⧸ W) hC hForm ψc hG deltaQ hdeltaQ hcontQ with
2390 ⟨i, L, hL⟩
2391 have hEq :
2392 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
2393 Submodule.mkQ W
2395 (R := ZCCompletedGroupAlgebra C H) delta x)) =
2397 (R := ZCCompletedGroupAlgebra C H) deltaQ := by
2398 funext x
2400 · simp only [crossedDifferentialModuleLiftLinear, map_zero, Submodule.mkQ_apply, deltaQ]
2401 · intro x y hx hy
2403 · intro g a
2404 simp only [crossedDifferentialModuleLiftLinear_single, map_smul, Submodule.mkQ_apply, deltaQ]
2405 rw [hEq]
2406 exact
2408 C ψc.toMonoidHom deltaQ i L hL
2410/-- Paper-facing profinite-target universal property for `A_ψ(C)`: continuous crossed
2411differentials into a profinite `Z_C[[H]]`-module are represented by continuous linear maps out of
2412the separated completed Fox module. -/
2414 {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
2415 [TopologicalSpace M]
2417 (hForm : ProCGroups.FiniteGroupClass.Formation C)
2418 (ψc : ContinuousMonoidHom G H)
2419 (hG : ProCGroups.ProC.IsProCGroup C G)
2420 (hM : _root_.CompletedGroupAlgebra.IsProfiniteModule
2421 (ZCCompletedGroupAlgebra C H) M) :
2422 {delta : G → M //
2423 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta ∧
2424 Continuous delta} ≃
2426 zcSeparatedCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom
2427 ZCApsi C ψc.toMonoidHom →L[ZCCompletedGroupAlgebra C H] M) := by
2428 letI : T1Space M := _root_.CompletedGroupAlgebra.IsProfiniteModule.t1Space hM
2430 hForm.containsTrivialQuotients
2431 letI : Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom) :=
2433 exact
2435 C ψc.toMonoidHom
2436 (directed_zcCompletedDifferentialModuleIndex C hForm hC ψc)
2437 (fun delta hdelta hcont =>
2439 C hC hForm ψc hG hM delta hdelta hcont)
2441omit [IsTopologicalGroup G] in
2442/-- If the completed crossed-differential relation submodule is closed for the finite-stage
2445 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
2446 (hdir : Directed (· ≤ ·)
2447 (id : ZCCompletedDifferentialModuleIndex C ψ →
2449 (hclosed :
2450 @IsClosed
2454 (zcCompletedGroupAlgebraScalar C ψ) :
2455 Submodule (ZCCompletedGroupAlgebra C H)
2456 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set
2457 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))) :
2459 intro x hx
2460 letI : TopologicalSpace
2461 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
2463 have hxcl :
2464 x ∈ closure
2466 (zcCompletedGroupAlgebraScalar C ψ) :
2467 Submodule (ZCCompletedGroupAlgebra C H)
2468 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set
2469 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :=
2471 C ψ hdir x hx
2472 simpa [hclosed.closure_eq] using hxcl
2474omit [IsTopologicalGroup G] in
2475/-- A named version of relation-reflection from closedness of the completed relation submodule. -/
2477 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
2478 (hdir : Directed (· ≤ ·)
2479 (id : ZCCompletedDifferentialModuleIndex C ψ →
2481 (hclosed : zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ) :
2484 C ψ hdir hclosed
2486omit [IsTopologicalGroup G] in
2487/-- The pre-quotient separation statement is exactly finite relation-reflection. -/
2491 constructor
2492 · intro hpre x hx
2493 apply hpre
2494 intro i
2495 exact
2497 C ψ i x).2 (hx i)
2498 · intro hreflect x hx
2499 apply hreflect
2500 intro i
2501 exact
2503 C ψ i x).1 (hx i)
2505omit [IsTopologicalGroup G] in
2506/-- Pre-stage separation is equivalently the assertion that the crossed-differential relation
2512 constructor
2513 · intro hpre
2514 apply le_antisymm
2515 · intro x hx
2516 rw [zcCompletedDifferentialModulePreStageKernelIntersection, Submodule.mem_iInf]
2517 intro i
2518 exact
2520 (C := C) (ψ := ψ) i hx
2521 · intro x hx
2522 apply hpre
2523 intro i
2524 have hxi : x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i := by
2525 exact
2526 (Submodule.mem_iInf
2527 (p := fun i : ZCCompletedDifferentialModuleIndex C ψ =>
2529 (by
2530 simpa [zcCompletedDifferentialModulePreStageKernelIntersection] using hx) i
2531 simpa using hxi
2532 · intro hEq x hx
2533 have hxint : x ∈ zcCompletedDifferentialModulePreStageKernelIntersection C ψ := by
2534 rw [zcCompletedDifferentialModulePreStageKernelIntersection, Submodule.mem_iInf]
2535 intro i
2536 simpa using hx i
2537 simpa [hEq] using hxint
2539omit [IsTopologicalGroup G] in
2540/-- Pre-quotient finite-stage separation implies separation on the algebraic quotient. -/
2542 (hpre : zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ) :
2544 intro a b hab
2545 have hcoord : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
2547 zcCompletedDifferentialModuleStageProjection C ψ i b := by
2548 intro i
2550 zcCompletedDifferentialModuleStageProjectionAdd] using congrFun hab i
2551 have hzero :
2552 ∀ z : ZCCompletedDifferentialModule C ψ,
2553 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
2554 zcCompletedDifferentialModuleStageProjection C ψ i z = 0) → z = 0 := by
2555 intro z
2556 refine Submodule.Quotient.induction_on
2558 (C := fun z =>
2559 (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
2560 zcCompletedDifferentialModuleStageProjection C ψ i z = 0) → z = 0)
2561 z ?_
2562 intro x hz
2563 apply (Submodule.Quotient.mk_eq_zero
2565 (x := x)).2
2566 apply hpre
2567 intro i
2568 have hi := hz i
2569 simpa [zcCompletedDifferentialModuleStageProjection_mkQ] using hi
2570 apply sub_eq_zero.mp
2571 apply hzero
2572 intro i
2573 rw [map_sub, hcoord i, sub_self]
2575omit [IsTopologicalGroup G] in
2576/-- Kernel-intersection form of finite-stage separation on the algebraic quotient. -/
2578 (hker :
2584 C ψ).2 hker)
2586omit [IsTopologicalGroup G] in
2587/-- If the finite-stage projection product is injective, then equality of every finite coordinate
2588implies equality in the genuine universal module. -/
2591 {a b : ZCCompletedDifferentialModule C ψ}
2592 (h : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
2595 a = b := by
2596 apply hsep
2597 funext i
2598 exact h i
2600omit [IsTopologicalGroup G] in
2601/-- The finite-stage completed topology is Hausdorff once the finite-stage projections separate
2602points. -/
2604 (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :
2605 @T2Space (ZCCompletedDifferentialModule C ψ)
2606 (zcCompletedDifferentialModuleNaturalTopology C ψ) := by
2607 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
2609 exact T2Space.of_injective_continuous hsep
2612omit [IsTopologicalGroup G] in
2613/-- Kernel-intersection form of the Hausdorff property for the finite-stage completed topology. -/
2615 (hker :
2618 @T2Space (ZCCompletedDifferentialModule C ψ)
2622 C ψ hker)
2624omit [IsTopologicalGroup G] in
2625/-- If finite-stage projections separate the algebraic quotient, then the defining relation submodule is
2628 (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :
2630 letI : TopologicalSpace
2631 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
2633 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
2635 letI : T2Space (ZCCompletedDifferentialModule C ψ) :=
2637 change IsClosed
2639 Submodule (ZCCompletedGroupAlgebra C H)
2640 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
2641 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))
2642 have hpreimage :
2644 Submodule (ZCCompletedGroupAlgebra C H)
2645 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
2646 Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))) =
2647 (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
2649 (zcCompletedGroupAlgebraScalar C ψ)).mkQ x) ⁻¹'
2650 ({0} : Set (ZCCompletedDifferentialModule C ψ)) := by
2651 ext x
2652 simp only [SetLike.mem_coe, Submodule.mkQ_apply, Set.mem_preimage, Set.mem_singleton_iff,
2653 Submodule.Quotient.mk_eq_zero]
2654 rw [hpreimage]
2655 exact isClosed_singleton.preimage
2658omit [IsTopologicalGroup G] in
2659/-- Finite relation reflection implies closedness of the algebraic crossed-differential relation
2662 (hreflect :
2668 C ψ).2 hreflect))
2670omit [IsTopologicalGroup G] in
2671/-- Kernel-intersection formulation of finite relation reflection. -/
2677 C ψ).symm.trans
2679 C ψ)
2681omit [IsTopologicalGroup G] in
2682/-- In the directed finite-stage situation, closedness of the completed relation submodule is
2685 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
2686 (hdir : Directed (· ≤ ·)
2687 (id : ZCCompletedDifferentialModuleIndex C ψ →
2691 constructor
2692 · intro hclosed
2693 exact
2696 C ψ).2
2698 C ψ hdir hclosed))
2699 · intro hsep
2702omit [IsTopologicalGroup G] in
2703/-- In the directed finite-stage situation, closedness of the defining relation submodule is
2706This is the formal version of the paper-level principle that the source completion/closure has
2708algebraic universal module is separated. -/
2710 [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
2711 (hdir : Directed (· ≤ ·)
2712 (id : ZCCompletedDifferentialModuleIndex C ψ →
2715 @T2Space (ZCCompletedDifferentialModule C ψ)
2716 (zcCompletedDifferentialModuleNaturalTopology C ψ) := by
2717 constructor
2718 · intro hclosed
2719 exact
2722 C ψ hdir).1 hclosed)
2723 · intro hT2
2724 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
2726 letI : T2Space (ZCCompletedDifferentialModule C ψ) := hT2
2727 exact
2729 C ψ (by infer_instance)
2731omit [IsTopologicalGroup G] in
2732/-- Addition is continuous for the finite-stage completed topology. -/
2734 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
2736 Continuous (fun p : ZCCompletedDifferentialModule C ψ ×
2737 ZCCompletedDifferentialModule C ψ => p.1 + p.2) := by
2738 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
2740 rw [continuous_induced_rng]
2741 change Continuous
2742 (fun p : ZCCompletedDifferentialModule C ψ ×
2744 fun i : ZCCompletedDifferentialModuleIndex C ψ =>
2745 zcCompletedDifferentialModuleStageProjectionAdd C ψ i (p.1 + p.2))
2747 (continuous_pi fun i =>
2751 continuous_snd))
2753omit [IsTopologicalGroup G] in
2754/-- Negation is continuous for the finite-stage completed topology. -/
2756 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
2758 Continuous (fun a : ZCCompletedDifferentialModule C ψ => -a) := by
2759 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
2761 rw [continuous_induced_rng]
2762 change Continuous
2763 (fun a : ZCCompletedDifferentialModule C ψ =>
2764 fun i : ZCCompletedDifferentialModuleIndex C ψ =>
2765 zcCompletedDifferentialModuleStageProjectionAdd C ψ i (-a))
2766 simpa [map_neg] using
2767 (continuous_pi fun i =>
2770omit [IsTopologicalGroup G] in
2771/-- The finite-stage completed topology is an additive group topology. -/
2773 @IsTopologicalAddGroup (ZCCompletedDifferentialModule C ψ)
2774 (zcCompletedDifferentialModuleNaturalTopology C ψ) _ := by
2775 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
2777 exact
2778 { continuous_add := by
2779 simpa using continuous_add_zcCompletedDifferentialModuleNaturalTopology C ψ
2780 continuous_neg := by
2781 simpa using continuous_neg_zcCompletedDifferentialModuleNaturalTopology C ψ }
2783/-- The finite-stage differential is continuous as a map out of the source group. -/
2785 (i : ZCCompletedDifferentialModuleIndex C ψ) :
2786 Continuous (zcCompletedDifferentialModuleStageDifferential C ψ i) := by
2787 letI : ContinuousMul G := (inferInstanceAs (IsTopologicalGroup G)).toContinuousMul
2788 letI : DiscreteTopology (zcCompletedDifferentialModuleStageSource C ψ i) :=
2789 ProCGroups.ProC.OpenNormalSubgroup.quotientDiscrete (G := G) i.source.1
2790 have hdiff :
2791 Continuous (fun q : zcCompletedDifferentialModuleStageSource C ψ i =>
2793 continuous_of_discreteTopology
2796 hdiff.comp
2797 (continuous_quotient_mk' : Continuous (fun g : G =>
2798 QuotientGroup.mk' (i.source.1 : Subgroup G) g))
2800/-- The universal differential is continuous for the finite-stage completed topology on the
2801algebraic quotient. -/
2803 @Continuous G (ZCCompletedDifferentialModule C ψ) inferInstance
2805 (zcUniversalDifferential C ψ) := by
2806 rw [continuous_induced_rng]
2807 change Continuous
2808 (fun g : G =>
2809 fun i : ZCCompletedDifferentialModuleIndex C ψ =>
2811 (zcUniversalDifferential C ψ g))
2812 refine continuous_pi fun i => ?_
2813 simpa using continuous_zcCompletedDifferentialModuleStageDifferential C ψ i
2815/-- The universal final topology on the algebraic quotient is below the finite-stage completed
2816topology. -/
2820 (continuous_zcUniversalDifferential_naturalTopology C ψ).coinduced_le
2822omit [IsTopologicalGroup G] in
2823/-- The finite-stage boundary map is continuous. -/
2825 [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
2826 (i : ZCCompletedDifferentialModuleIndex C ψ) :
2827 Continuous (zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψ i) :=
2828 continuous_of_discreteTopology
2830omit [IsTopologicalGroup G] in
2831/-- The algebraic completed boundary is continuous for the finite-stage completed topology. -/
2833 [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
2835 (ψc : ContinuousMonoidHom G H) :
2836 @Continuous (ZCCompletedDifferentialModule C ψc.toMonoidHom)
2837 (ZCCompletedGroupAlgebra C H)
2838 (zcCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom) inferInstance
2839 (zcToCompletedGroupAlgebra C ψc.toMonoidHom) := by
2840 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψc.toMonoidHom) :=
2841 zcCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom
2842 have hval : Continuous (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>
2843 ((zcToCompletedGroupAlgebra C ψc.toMonoidHom a : ZCCompletedGroupAlgebra C H) :
2844 (j : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H j)) := by
2845 refine continuous_pi fun j => ?_
2846 let i := zcCompletedDifferentialModuleComapIndex C hC ψc j
2847 have hstage : Continuous (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>
2848 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
2849 (zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i a)) :=
2851 C ψc.toMonoidHom i).comp
2853 C ψc.toMonoidHom i)
2854 have hcoord :
2855 (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>
2857 (zcToCompletedGroupAlgebra C ψc.toMonoidHom a)) =
2858 (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>
2859 zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
2860 (zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i a)) := by
2861 funext a
2862 have h :=
2863 congrArg (fun f =>
2864 f a)
2866 C ψc.toMonoidHom i)
2867 simpa [LinearMap.comp_apply, i] using h.symm
2868 rw [hcoord]
2869 exact hstage
2870 simpa only [Subtype.eta] using
2871 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C H) hval
2872 (fun a => (zcToCompletedGroupAlgebra C ψc.toMonoidHom a).property))
2874omit [IsTopologicalGroup G] in
2875/-- Scalar multiplication by `Z_C[[H]]` is continuous for the finite-stage completed topology. -/
2877 [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] :
2878 @ContinuousSMul (ZCCompletedGroupAlgebra C H)
2880 inferInstance inferInstance (zcCompletedDifferentialModuleNaturalTopology C ψ) := by
2881 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
2883 refine ⟨?_⟩
2884 rw [continuous_induced_rng]
2885 change Continuous
2886 (fun p : ZCCompletedGroupAlgebra C H × ZCCompletedDifferentialModule C ψ =>
2887 fun i : ZCCompletedDifferentialModuleIndex C ψ =>
2888 zcCompletedDifferentialModuleStageProjectionAdd C ψ i (p.1 • p.2))
2889 refine continuous_pi fun i => ?_
2890 letI : TopologicalSpace (zcCompletedDifferentialModuleStageRing C ψ i) := inferInstance
2891 letI : DiscreteTopology (zcCompletedDifferentialModuleStageRing C ψ i) := inferInstance
2892 have hstageAction :
2893 Continuous (fun p : zcCompletedDifferentialModuleStageRing C ψ i ×
2894 ZCCompletedDifferentialModuleStage C ψ i => p.1 • p.2) :=
2895 continuous_of_discreteTopology
2896 have hcoeff :
2897 Continuous (fun a : ZCCompletedGroupAlgebra C H =>
2898 zcCompletedGroupAlgebraProjectionRingHom C H i.target a) :=
2899 continuous_zcCompletedGroupAlgebraProjectionRingHom (C := C) (G := H) i.target
2900 have hmodule :
2901 Continuous (fun a : ZCCompletedDifferentialModule C ψ =>
2902 zcCompletedDifferentialModuleStageProjectionAdd C ψ i a) :=
2904 have hcoord :
2905 Continuous (fun p : ZCCompletedGroupAlgebra C H ×
2907 zcCompletedGroupAlgebraProjectionRingHom C H i.target p.1 •
2908 zcCompletedDifferentialModuleStageProjectionAdd C ψ i p.2) :=
2909 hstageAction.comp (hcoeff.comp continuous_fst |>.prodMk (hmodule.comp continuous_snd))
2911 zcCompletedDifferentialModuleStage_completed_smul] using hcoord
2913end
2915end FoxDifferential