Yamaguchi Lean 4 Library
Source: ProCGroups.CrowellExactSequence.Profinite.KernelBoundary
ProCGroups/CrowellExactSequence/Profinite/KernelBoundary/Source

Source: ProCGroups.CrowellExactSequence.Profinite.KernelBoundary

1import ProCGroups.CrowellExactSequence.Profinite.SequenceMaps
2import ProCGroups.ProC.Kernels
4/-!
5# Boundary maps from the profinite kernel
7This file constructs the completed and separated boundary maps on the kernel of a profinite
8presentation. It proves that these maps kill commutators and gives continuity criteria ensuring
9that they kill the closure of the commutator subgroup, hence factor through topological
10abelianization.
11-/
13namespace CrowellExactSequence
15noncomputable section
17open scoped BigOperators commutatorElement
18open FoxDifferential
19open ProCGroups.ProC
21universe u
23variable {G H : Type u}
24variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27/-- Kernel elements map multiplicatively to the Fox completed differential module. -/
28def completedKernelBoundaryProCInteger
29 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
30 psi.toMonoidHom.ker →*
31 Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom) where
32 toFun n := Multiplicative.ofAdd
33 (zcUniversalDifferential C psi.toMonoidHom n.1)
34 map_one' := by
35 apply Multiplicative.toAdd.injective
36 exact ScalarCrossedHom.map_one (zcUniversalDifferential C psi.toMonoidHom)
37 map_mul' n₁ n₂ := by
38 apply Multiplicative.toAdd.injective
39 have hmul :=
40 ScalarCrossedHom.map_mul (zcUniversalDifferential C psi.toMonoidHom) n₁.1 n₂.1
41 have hpsi : psi.toMonoidHom n₁.1 = 1 := n₁.2
42 have hadd :
43 zcUniversalDifferential C psi.toMonoidHom ((n₁ * n₂ : psi.toMonoidHom.ker).1) =
44 zcUniversalDifferential C psi.toMonoidHom n₁.1 +
45 zcUniversalDifferential C psi.toMonoidHom n₂.1 := by
46 change
47 zcUniversalDifferential C psi.toMonoidHom (n₁.1 * n₂.1) =
48 zcUniversalDifferential C psi.toMonoidHom n₁.1 +
49 zcUniversalDifferential C psi.toMonoidHom n₂.1
50 rw [hmul, zcCompletedGroupAlgebraScalar_apply, hpsi, map_one, one_smul]
51 exact hadd
53/-- Kernel elements map multiplicatively to the separated completed differential module. -/
54def separatedCompletedKernelBoundaryProCInteger
55 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
56 psi.toMonoidHom.ker →*
57 Multiplicative (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) where
58 toFun n := Multiplicative.ofAdd
59 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1)
60 map_one' := by
61 apply Multiplicative.toAdd.injective
62 change zcSeparatedUniversalDifferential C psi.toMonoidHom 1 = 0
63 rw [← zcCompletedDifferentialModuleToSeparated_universal
64 (C := C) (ψ := psi.toMonoidHom) (g := 1),
65 ScalarCrossedHom.map_one (zcUniversalDifferential C psi.toMonoidHom)]
66 exact
67 (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom).map_zero
68 map_mul' n₁ n₂ := by
69 apply Multiplicative.toAdd.injective
70 have hmul :=
71 ScalarCrossedHom.map_mul
72 (zcSeparatedUniversalDifferential C psi.toMonoidHom) n₁.1 n₂.1
73 have hpsi : psi.toMonoidHom n₁.1 = 1 := n₁.2
74 have hadd :
75 zcSeparatedUniversalDifferential C psi.toMonoidHom ((n₁ * n₂ : psi.toMonoidHom.ker).1) =
76 zcSeparatedUniversalDifferential C psi.toMonoidHom n₁.1 +
77 zcSeparatedUniversalDifferential C psi.toMonoidHom n₂.1 := by
78 change
79 zcSeparatedUniversalDifferential C psi.toMonoidHom (n₁.1 * n₂.1) =
80 zcSeparatedUniversalDifferential C psi.toMonoidHom n₁.1 +
81 zcSeparatedUniversalDifferential C psi.toMonoidHom n₂.1
82 rw [hmul, zcCompletedGroupAlgebraScalar_apply, hpsi, map_one, one_smul]
83 exact hadd
85omit [IsTopologicalGroup G] in
86/--
87Membership in the separated completed kernel-boundary kernel is equivalent to vanishing of the
88corresponding finite-stage coordinate.
89-/
90theorem separatedCompletedKernelBoundaryProCInteger_mem_ker_iff
91 {C : ProCGroups.FiniteGroupClass.{u}} {psi : ContinuousMonoidHom G H}
92 {n : ProfiniteKernelSubgroup psi} :
93 n ∈ (separatedCompletedKernelBoundaryProCInteger
94 (G := G) (H := H) C psi).ker ↔
95 ∀ i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom,
96 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i n.1 = 0 := by
97 constructor
98 · intro hn i
99 have hsep :
100 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
101 change
102 Multiplicative.ofAdd
103 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) =
104 (1 : Multiplicative
105 (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)) at hn
106 have htoAdd :=
107 congrArg
108 (fun x : Multiplicative
109 (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) =>
110 Multiplicative.toAdd x) hn
111 change
112 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = 0 at htoAdd
113 exact htoAdd
114 have hproj := congrArg
115 (fun x : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom =>
116 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i x) hsep
117 rw [zcSeparatedCompletedDifferentialModuleStageProjectionAdd_universal,
118 (zcSeparatedCompletedDifferentialModuleStageProjectionAdd
119 C psi.toMonoidHom i).map_zero] at hproj
120 exact hproj
121 · intro hstage
122 have hsep :
123 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = 0 :=
124 zcSeparatedCompletedDifferentialModuleStageProjectionsSeparate
125 C psi.toMonoidHom
126 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1)
127 (by
128 intro i
129 calc
130 zcSeparatedCompletedDifferentialModuleStageProjectionAdd
131 C psi.toMonoidHom i
132 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) =
133 zcCompletedDifferentialModuleStageDifferential
134 C psi.toMonoidHom i n.1 :=
135 zcSeparatedCompletedDifferentialModuleStageProjectionAdd_universal
136 C psi.toMonoidHom i n.1
137 _ = 0 := hstage i
138 _ =
139 zcSeparatedCompletedDifferentialModuleStageProjectionAdd
140 C psi.toMonoidHom i 0 :=
141 (zcSeparatedCompletedDifferentialModuleStageProjectionAdd
142 C psi.toMonoidHom i).map_zero.symm)
143 change
144 Multiplicative.ofAdd
145 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) =
146 (1 : Multiplicative
147 (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom))
148 simpa [hsep]
150/--
151The separated kernel boundary has closed kernel, because zero can be tested at every finite
152stage and each finite-stage boundary is continuous.
153-/
154theorem isClosed_separatedCompletedKernelBoundaryProCInteger_ker
155 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
156 IsClosed
157 (((separatedCompletedKernelBoundaryProCInteger
158 (G := G) (H := H) C psi).ker :
159 Subgroup (ProfiniteKernelSubgroup psi)) :
160 Set (ProfiniteKernelSubgroup psi)) := by
161 have hker_set :
162 (((separatedCompletedKernelBoundaryProCInteger
163 (G := G) (H := H) C psi).ker :
164 Subgroup (ProfiniteKernelSubgroup psi)) :
165 Set (ProfiniteKernelSubgroup psi)) =
166 ⋂ i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom,
167 (fun n : ProfiniteKernelSubgroup psi =>
168 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i n.1) ⁻¹'
169 ({0} : Set (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i)) := by
170 ext n
171 simp only [Set.mem_iInter, Set.mem_preimage, Set.mem_singleton_iff]
172 exact separatedCompletedKernelBoundaryProCInteger_mem_ker_iff
173 (G := G) (H := H) (C := C) (psi := psi) (n := n)
174 rw [hker_set]
175 refine isClosed_iInter fun i => ?_
176 exact
177 (isClosed_singleton
178 (x := (0 : ZCCompletedDifferentialModuleStage C psi.toMonoidHom i))).preimage
179 ((continuous_zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i).comp
180 continuous_subtype_val)
182omit [IsTopologicalGroup G] in
183/--
184Algebraic part of well-definedness for the separated boundary: ordinary commutators already map
185to zero.
186-/
187theorem separatedCompletedKernelBoundaryProCInteger_commutator_le_ker
188 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
189 commutator (ProfiniteKernelSubgroup psi) <=
190 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker := by
191 refine Subgroup.commutator_le.mpr ?_
192 intro a _ha b _hb
193 change
194 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi)
195 (⁅a, b⁆ : ProfiniteKernelSubgroup psi) = 1
196 rw [map_commutatorElement]
197 exact commutatorElement_eq_one_iff_mul_comm.2
198 (mul_comm
199 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi a)
200 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi b))
202/--
203The separated kernel boundary kills \(\overline{[N,N]}\) without assuming algebraic closedness
204of the raw crossed-differential relation submodule.
205-/
206theorem separatedBoundaryKillsTopologicalCommutatorProCInteger
207 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
208 Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)) <=
209 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker :=
210 Subgroup.topologicalClosure_minimal
211 (s := commutator (ProfiniteKernelSubgroup psi))
212 (t := (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker)
213 (separatedCompletedKernelBoundaryProCInteger_commutator_le_ker
214 (G := G) (H := H) C psi)
215 (isClosed_separatedCompletedKernelBoundaryProCInteger_ker
216 (G := G) (H := H) C psi)
218/--
219If the completed kernel boundary is continuous and its target is \(T_1\), then it vanishes on the
220topological closure of the kernel's commutator subgroup.
221-/
222theorem completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuous
223 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
224 [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
225 [T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)]
226 (hcont :
227 Continuous (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)) :
228 Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)) <=
229 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker := by
230 letI : T1Space (Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom)) := by
231 change T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)
232 infer_instance
233 let f : ProfiniteKernelSubgroup psi →ₜ*
234 Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
235 { toMonoidHom := completedKernelBoundaryProCInteger (G := G) (H := H) C psi
236 continuous_toFun := hcont }
237 intro x hx
238 have hxmk :
240 (ProfiniteKernelSubgroup psi) x = 1 :=
241 ProCGroups.Abelian.TopologicalAbelianization.mk_eq_one_iff.2 hx
242 have hkill :=
245 change (completedKernelBoundaryProCInteger (G := G) (H := H) C psi) x = 1
246 exact hkill
248/--
249Correct topological boundary factorization condition for the genuine \(N^{\mathrm{ab}}(C)\)
250map.
251-/
252abbrev CompletedBoundaryKillsTopologicalCommutatorProCInteger
253 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) : Prop :=
254 Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)) <=
255 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker
257/--
258Continuity of the completed kernel boundary supplies the condition required for it to factor
259through the profinite kernel's topological abelianization.
260-/
261theorem completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuousBoundary
262 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
263 [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
264 [T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)]
265 (hcont :
266 Continuous (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)) :
267 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi :=
268 completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuous
269 (G := G) (H := H) C psi hcont
271omit [IsTopologicalGroup G] in
272/--
273Algebraic part of well-definedness: the kernel boundary kills the ordinary commutator subgroup
274of the profinite kernel. The remaining topological step is to pass from the commutator subgroup
275to its closure.
276-/
277theorem completedKernelBoundaryProCInteger_commutator_le_ker
278 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
279 commutator (ProfiniteKernelSubgroup psi) <=
280 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker := by
281 refine Subgroup.commutator_le.mpr ?_
282 intro a _ha b _hb
283 change
284 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)
285 (⁅a, b⁆ : ProfiniteKernelSubgroup psi) = 1
286 rw [map_commutatorElement]
287 exact commutatorElement_eq_one_iff_mul_comm.2
288 (mul_comm
289 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi a)
290 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi b))
292/-- Topological form of well-definedness from closedness of the kernel of the boundary map. -/
293theorem completedBoundaryKillsTopologicalCommutatorProCInteger_of_closed_ker
294 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
295 (hclosed :
296 IsClosed
297 (((completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker :
298 Subgroup (ProfiniteKernelSubgroup psi)) : Set (ProfiniteKernelSubgroup psi))) :
299 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi :=
300 Subgroup.topologicalClosure_minimal
301 (s := commutator (ProfiniteKernelSubgroup psi))
302 (t := (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker)
303 (completedKernelBoundaryProCInteger_commutator_le_ker
304 (G := G) (H := H) C psi)
305 hclosed
307omit [IsTopologicalGroup G] in
308/--
309Continuity of the universal completed differential on the ambient group implies continuity of
310the kernel boundary.
311-/
312theorem continuous_completedKernelBoundaryZC_of_continuous_zcUnivDiff
313 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
314 [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
315 (hD : Continuous (fun g : G => zcUniversalDifferential C psi.toMonoidHom g)) :
316 Continuous (completedKernelBoundaryProCInteger (G := G) (H := H) C psi) := by
317 change Continuous fun n : ProfiniteKernelSubgroup psi =>
318 Multiplicative.ofAdd (zcUniversalDifferential C psi.toMonoidHom n.1)
319 exact continuous_ofAdd.comp (hD.comp continuous_subtype_val)
321/--
322Well-definedness of \(d_N\) from continuity of the universal completed differential on the
323ambient group.
324-/
325theorem completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff
326 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
327 [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
328 [T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)]
329 (hD : Continuous (fun g : G => zcUniversalDifferential C psi.toMonoidHom g)) :
330 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi :=
331 completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuousBoundary
332 (G := G) (H := H) C psi
333 (continuous_completedKernelBoundaryZC_of_continuous_zcUnivDiff
334 (G := G) (H := H) C psi hD)
336/--
337Finite-coordinate form of the topological well-definedness step for \(d_N\). If a finite
338coordinate system on \(A_{\psi}(C)\) identifies the universal differential on the kernel with a
339continuous coordinate-valued map, then the ordinary commutator-killing identity extends to
340\(\overline{[N,N]}\). In paper language, this is the passage from a continuous coordinate
341formula for \(D|_N\) to the well-defined map \(N^{\mathrm{ab}}(C) \to A_{\psi}(C)\).
342-/
343theorem completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords_fintype
344 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
345 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
346 (hbasis_A :
347 IsPresentedCompletedDifferentialFamilyBasisProCInteger
348 (G := G) (H := H) C psi family)
349 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
350 (Dcoords : ProfiniteKernelSubgroup psi →
351 ZCFreeFoxCoordinates C (X := X) (H := H))
352 (hDcoords_continuous : Continuous Dcoords)
353 (hDcoords :
354 ∀ n : ProfiniteKernelSubgroup psi,
355 Dcoords n =
356 presentedCompletedDifferentialFamilyCoordinatesProCInteger
357 (G := G) (H := H) C psi family hbasis_A
358 (zcUniversalDifferential C psi.toMonoidHom n.1)) :
359 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi := by
360 refine
361 completedBoundaryKillsTopologicalCommutatorProCInteger_of_closed_ker
362 (G := G) (H := H) C psi ?_
363 have hclosed_zero :
364 IsClosed ({0} : Set (ZCFreeFoxCoordinates C (X := X) (H := H))) :=
365 isClosed_singleton
366 have hclosed_preimage :
367 IsClosed
368 (Dcoords ⁻¹' ({0} : Set (ZCFreeFoxCoordinates C (X := X) (H := H)))) :=
369 hclosed_zero.preimage hDcoords_continuous
370 have hker_set :
371 (((completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker :
372 Subgroup (ProfiniteKernelSubgroup psi)) : Set (ProfiniteKernelSubgroup psi)) =
373 Dcoords ⁻¹' ({0} : Set (ZCFreeFoxCoordinates C (X := X) (H := H))) := by
374 ext n
375 change
376 completedKernelBoundaryProCInteger (G := G) (H := H) C psi n = 1 ↔
377 Dcoords n = 0
378 constructor
379 · intro hn
380 have hDzero : zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
381 change Multiplicative.ofAdd
382 (zcUniversalDifferential C psi.toMonoidHom n.1) = 1 at hn
383 have htoAdd :=
384 congrArg
385 (fun x : Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom) =>
386 Multiplicative.toAdd x) hn
387 change zcUniversalDifferential C psi.toMonoidHom n.1 = 0 at htoAdd
388 exact htoAdd
389 rw [hDcoords n, hDzero]
390 exact
391 (presentedCompletedDifferentialFamilyCoordinatesProCInteger
392 (G := G) (H := H) C psi family hbasis_A).map_zero
393 · intro hn
394 have hcoords_zero :
395 presentedCompletedDifferentialFamilyCoordinatesProCInteger
396 (G := G) (H := H) C psi family hbasis_A
397 (zcUniversalDifferential C psi.toMonoidHom n.1) = 0 := by
398 rw [← hDcoords n]
399 exact hn
400 have hDzero : zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
401 apply
402 (presentedCompletedDifferentialFamilyCoordinatesProCInteger
403 (G := G) (H := H) C psi family hbasis_A).injective
404 calc
405 presentedCompletedDifferentialFamilyCoordinatesProCInteger
406 (G := G) (H := H) C psi family hbasis_A
407 (zcUniversalDifferential C psi.toMonoidHom n.1) =
408 0 := hcoords_zero
409 _ =
410 presentedCompletedDifferentialFamilyCoordinatesProCInteger
411 (G := G) (H := H) C psi family hbasis_A 0 :=
412 (presentedCompletedDifferentialFamilyCoordinatesProCInteger
413 (G := G) (H := H) C psi family hbasis_A).map_zero.symm
414 change Multiplicative.ofAdd
415 (zcUniversalDifferential C psi.toMonoidHom n.1) =
416 (1 : Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom))
417 simpa [hDzero]
418 rw [hker_set]
419 exact hclosed_preimage
421/-- Fin-indexed finite-coordinate form of the topological well-definedness step for \(d_N\). -/
422theorem completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords
423 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
424 {r : Nat} (family : Fin r → G)
425 (hbasis_A :
426 IsPresentedCompletedDifferentialFamilyBasisProCInteger
427 (G := G) (H := H) C psi family)
428 [T1Space (Fin r → ZCCompletedGroupAlgebra C H)]
429 (Dcoords : ProfiniteKernelSubgroup psi → Fin r → ZCCompletedGroupAlgebra C H)
430 (hDcoords_continuous : Continuous Dcoords)
431 (hDcoords :
432 ∀ n : ProfiniteKernelSubgroup psi,
433 Dcoords n =
434 presentedCompletedDifferentialFamilyCoordinatesProCInteger
435 (G := G) (H := H) C psi family hbasis_A
436 (zcUniversalDifferential C psi.toMonoidHom n.1)) :
437 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi := by
438 refine
439 completedBoundaryKillsTopologicalCommutatorProCInteger_of_closed_ker
440 (G := G) (H := H) C psi ?_
441 have hclosed_zero :
442 IsClosed ({0} : Set (Fin r → ZCCompletedGroupAlgebra C H)) :=
443 isClosed_singleton
444 have hclosed_preimage :
445 IsClosed (Dcoords ⁻¹' ({0} : Set (Fin r → ZCCompletedGroupAlgebra C H))) :=
446 hclosed_zero.preimage hDcoords_continuous
447 have hker_set :
448 (((completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker :
449 Subgroup (ProfiniteKernelSubgroup psi)) : Set (ProfiniteKernelSubgroup psi)) =
450 Dcoords ⁻¹' ({0} : Set (Fin r → ZCCompletedGroupAlgebra C H)) := by
451 ext n
452 change
453 completedKernelBoundaryProCInteger (G := G) (H := H) C psi n = 1 ↔
454 Dcoords n = 0
455 constructor
456 · intro hn
457 have hDzero : zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
458 change Multiplicative.ofAdd
459 (zcUniversalDifferential C psi.toMonoidHom n.1) = 1 at hn
460 have htoAdd :=
461 congrArg
462 (fun x : Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom) =>
463 Multiplicative.toAdd x) hn
464 change zcUniversalDifferential C psi.toMonoidHom n.1 = 0 at htoAdd
465 exact htoAdd
466 rw [hDcoords n, hDzero]
467 exact
468 (presentedCompletedDifferentialFamilyCoordinatesProCInteger
469 (G := G) (H := H) C psi family hbasis_A).map_zero
470 · intro hn
471 have hcoords_zero :
472 presentedCompletedDifferentialFamilyCoordinatesProCInteger
473 (G := G) (H := H) C psi family hbasis_A
474 (zcUniversalDifferential C psi.toMonoidHom n.1) = 0 := by
475 rw [← hDcoords n]
476 exact hn
477 have hDzero : zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
478 apply
479 (presentedCompletedDifferentialFamilyCoordinatesProCInteger
480 (G := G) (H := H) C psi family hbasis_A).injective
481 calc
482 presentedCompletedDifferentialFamilyCoordinatesProCInteger
483 (G := G) (H := H) C psi family hbasis_A
484 (zcUniversalDifferential C psi.toMonoidHom n.1) =
485 0 := hcoords_zero
486 _ =
487 presentedCompletedDifferentialFamilyCoordinatesProCInteger
488 (G := G) (H := H) C psi family hbasis_A 0 :=
489 (presentedCompletedDifferentialFamilyCoordinatesProCInteger
490 (G := G) (H := H) C psi family hbasis_A).map_zero.symm
491 change Multiplicative.ofAdd
492 (zcUniversalDifferential C psi.toMonoidHom n.1) =
493 (1 : Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom))
494 simpa [hDzero]
495 rw [hker_set]
496 exact hclosed_preimage
498/--
499Finite-coordinate ambient version of the completed-boundary theorem killing the top commutator
500subgroup. This is the form used when a continuous Fox-coordinate formula is constructed on the
501whole source and then restricted to \(\ker \psi\).
502-/
503theorem completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords_fintype
504 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
505 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
506 (hbasis_A :
507 IsPresentedCompletedDifferentialFamilyBasisProCInteger
508 (G := G) (H := H) C psi family)
509 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
510 (Dcoords : G → ZCFreeFoxCoordinates C (X := X) (H := H))
511 (hDcoords_continuous : Continuous Dcoords)
512 (hDcoords :
513 ∀ n : ProfiniteKernelSubgroup psi,
514 Dcoords n.1 =
515 presentedCompletedDifferentialFamilyCoordinatesProCInteger
516 (G := G) (H := H) C psi family hbasis_A
517 (zcUniversalDifferential C psi.toMonoidHom n.1)) :
518 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi := by
519 exact
520 completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords_fintype
521 (G := G) (H := H) C psi family hbasis_A
522 (fun n : ProfiniteKernelSubgroup psi => Dcoords n.1)
523 (hDcoords_continuous.comp continuous_subtype_val)
524 hDcoords
526/--
527\(\operatorname{Fin}\)-indexed ambient-coordinate version of the completed-boundary theorem
528killing the top commutator subgroup for continuous kernel-family coordinates.
529-/
530theorem completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords
531 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
532 {r : Nat} (family : Fin r → G)
533 (hbasis_A :
534 IsPresentedCompletedDifferentialFamilyBasisProCInteger
535 (G := G) (H := H) C psi family)
536 [T1Space (Fin r → ZCCompletedGroupAlgebra C H)]
537 (Dcoords : G → Fin r → ZCCompletedGroupAlgebra C H)
538 (hDcoords_continuous : Continuous Dcoords)
539 (hDcoords :
540 ∀ n : ProfiniteKernelSubgroup psi,
541 Dcoords n.1 =
542 presentedCompletedDifferentialFamilyCoordinatesProCInteger
543 (G := G) (H := H) C psi family hbasis_A
544 (zcUniversalDifferential C psi.toMonoidHom n.1)) :
545 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi := by
546 exact
547 completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords
548 (G := G) (H := H) C psi family hbasis_A
549 (fun n : ProfiniteKernelSubgroup psi => Dcoords n.1)
550 (hDcoords_continuous.comp continuous_subtype_val)
551 hDcoords
553end
555end CrowellExactSequence