CrowellExactSequence/Profinite/KernelBoundary.lean
1import CrowellExactSequence.Profinite.SequenceMaps
2import ProCGroups.ProC.Kernels
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/CrowellExactSequence/Profinite/KernelBoundary.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Kernel boundary
15The target is the Fox universal completed differential module
16`ZCCompletedDifferentialModule C psi.toMonoidHom`.
17-/
19namespace CrowellExactSequence
21noncomputable section
23open scoped BigOperators
24open FoxDifferential
25open ProCGroups.ProC
27universe u
29variable {G H : Type u}
30variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/-- Kernel elements map multiplicatively to the Fox completed differential module. -/
35 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
36 psi.toMonoidHom.ker →*
37 Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom) where
38 toFun n := Multiplicative.ofAdd
39 (zcUniversalDifferential C psi.toMonoidHom n.1)
40 map_one' := by
41 apply Multiplicative.toAdd.injective
42 exact zcUniversalDifferential_one C psi.toMonoidHom
43 map_mul' n₁ n₂ := by
44 apply Multiplicative.toAdd.injective
45 have hmul := zcUniversalDifferential_mul C psi.toMonoidHom n₁.1 n₂.1
46 have hpsi : psi n₁.1 = 1 := n₁.2
47 have hcoef :
48 zcGroupLike C H (psi n₁.1) = 1 := by
49 rw [hpsi]
50 exact map_one (zcGroupLike C H)
51 have hadd :
52 zcUniversalDifferential C psi.toMonoidHom ((n₁ * n₂ : psi.toMonoidHom.ker).1) =
53 zcUniversalDifferential C psi.toMonoidHom n₁.1 +
54 zcUniversalDifferential C psi.toMonoidHom n₂.1 := by
55 simpa [zcCompletedGroupAlgebraScalar_apply, hpsi, hcoef, one_smul] using hmul
56 simpa using hadd
58/-- Kernel elements map multiplicatively to the separated completed differential module. -/
60 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
61 psi.toMonoidHom.ker →*
62 Multiplicative (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) where
63 toFun n := Multiplicative.ofAdd
64 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1)
65 map_one' := by
66 apply Multiplicative.toAdd.injective
67 change zcSeparatedUniversalDifferential C psi.toMonoidHom 1 = 0
69 (C := C) (ψ := psi.toMonoidHom) (g := 1),
72 map_mul' n₁ n₂ := by
73 apply Multiplicative.toAdd.injective
74 have hmul := zcSeparatedUniversalDifferential_mul C psi.toMonoidHom n₁.1 n₂.1
75 have hpsi : psi n₁.1 = 1 := n₁.2
76 have hcoef :
77 zcGroupLike C H (psi n₁.1) = 1 := by
78 rw [hpsi]
79 exact map_one (zcGroupLike C H)
80 have hadd :
81 zcSeparatedUniversalDifferential C psi.toMonoidHom ((n₁ * n₂ : psi.toMonoidHom.ker).1) =
82 zcSeparatedUniversalDifferential C psi.toMonoidHom n₁.1 +
83 zcSeparatedUniversalDifferential C psi.toMonoidHom n₂.1 := by
84 simpa [zcCompletedGroupAlgebraScalar_apply, hpsi, hcoef, one_smul] using hmul
85 simpa using hadd
87omit [IsTopologicalGroup G] in
89 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
90 (n : ProfiniteKernelSubgroup psi) :
93 ∀ i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom,
94 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i n.1 = 0 := by
95 constructor
96 · intro hn i
97 have hsep :
98 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
99 change
100 Multiplicative.ofAdd
101 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) =
102 (1 : Multiplicative
103 (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)) at hn
104 simpa using
105 congrArg
106 (fun x : Multiplicative
107 (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) =>
108 Multiplicative.toAdd x) hn
109 simpa using congrArg
110 (fun x : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom =>
111 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i x) hsep
112 · intro hstage
113 have hsep :
114 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = 0 :=
116 C psi.toMonoidHom
117 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1)
118 (by intro i; simpa using hstage i)
119 change
120 Multiplicative.ofAdd
121 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) =
122 (1 : Multiplicative
123 (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom))
124 simpa [hsep]
126/-- The separated kernel boundary has closed kernel, because zero can be tested at every finite
129 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
130 IsClosed
133 Subgroup (ProfiniteKernelSubgroup psi)) :
134 Set (ProfiniteKernelSubgroup psi)) := by
135 have hker_set :
138 Subgroup (ProfiniteKernelSubgroup psi)) :
139 Set (ProfiniteKernelSubgroup psi)) =
140 ⋂ i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom,
141 (fun n : ProfiniteKernelSubgroup psi =>
142 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i n.1) ⁻¹'
143 ({0} : Set (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i)) := by
144 ext n
145 simp only [Set.mem_iInter, Set.mem_preimage, Set.mem_singleton_iff]
147 (G := G) (H := H) C psi n
148 rw [hker_set]
149 refine isClosed_iInter fun i => ?_
150 exact
151 (isClosed_singleton (x := (0 : ZCCompletedDifferentialModuleStage C psi.toMonoidHom i))).preimage
152 ((continuous_zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i).comp
153 continuous_subtype_val)
155omit [IsTopologicalGroup G] in
156/-- Algebraic part of well-definedness for the separated boundary: ordinary commutators already
157map to zero. -/
159 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
160 commutator (ProfiniteKernelSubgroup psi) <=
161 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker := by
162 refine Subgroup.commutator_le.mpr ?_
163 intro a _ha b _hb
164 change (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi) ⁅a, b⁆ = 1
165 rw [map_commutatorElement]
166 exact commutatorElement_eq_one_iff_mul_comm.2
167 (mul_comm
168 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi a)
169 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi b))
171/-- The separated kernel boundary kills `closure([N,N])` without assuming algebraic closedness of
172the raw crossed-differential relation submodule. -/
174 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
175 Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)) <=
176 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker :=
177 Subgroup.topologicalClosure_minimal
178 (s := commutator (ProfiniteKernelSubgroup psi))
179 (t := (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker)
181 (G := G) (H := H) C psi)
183 (G := G) (H := H) C psi)
186 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
187 [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
188 [T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)]
189 (hcont :
190 Continuous (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)) :
191 Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)) <=
192 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker := by
193 letI : T1Space (Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom)) := by
194 change T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)
195 infer_instance
196 let f : ProfiniteKernelSubgroup psi →ₜ*
197 Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
198 { toMonoidHom := completedKernelBoundaryProCInteger (G := G) (H := H) C psi
199 continuous_toFun := hcont }
200 intro x hx
201 have hxmk :
203 (ProfiniteKernelSubgroup psi) x = 1 :=
204 ProCGroups.Abelian.TopologicalAbelianization.mk_eq_one_iff.2 hx
205 have hkill :=
206 congrArg (fun y => ProCGroups.Abelian.TopologicalAbelianization.lift f y) hxmk
207 simpa [f, MonoidHom.mem_ker] using hkill
209/-- Correct topological boundary factorization condition for the genuine `N^ab(C)` map. -/
211 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) : Prop :=
212 Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)) <=
213 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker
216 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
217 [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
218 [T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)]
219 (hcont :
220 Continuous (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)) :
221 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi :=
223 (G := G) (H := H) C psi hcont
225omit [IsTopologicalGroup G] in
226/-- Algebraic part of well-definedness: the kernel boundary kills the ordinary commutator
227subgroup of the profinite kernel. The remaining topological step is to pass from the commutator
228subgroup to its closure. -/
230 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
231 commutator (ProfiniteKernelSubgroup psi) <=
232 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker := by
233 refine Subgroup.commutator_le.mpr ?_
234 intro a _ha b _hb
235 change (completedKernelBoundaryProCInteger (G := G) (H := H) C psi) ⁅a, b⁆ = 1
236 rw [map_commutatorElement]
237 exact commutatorElement_eq_one_iff_mul_comm.2
238 (mul_comm
239 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi a)
240 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi b))
242/-- Topological form of well-definedness from closedness of the kernel of the boundary map. -/
244 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
245 (hclosed :
246 IsClosed
247 (((completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker :
248 Subgroup (ProfiniteKernelSubgroup psi)) : Set (ProfiniteKernelSubgroup psi))) :
249 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi :=
250 Subgroup.topologicalClosure_minimal
251 (s := commutator (ProfiniteKernelSubgroup psi))
252 (t := (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker)
254 (G := G) (H := H) C psi)
255 hclosed
257omit [IsTopologicalGroup G] in
258/-- Continuity of the kernel boundary follows from continuity of the universal completed
259differential on the ambient group. -/
261 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
262 [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
263 (hD : Continuous (fun g : G => zcUniversalDifferential C psi.toMonoidHom g)) :
264 Continuous (completedKernelBoundaryProCInteger (G := G) (H := H) C psi) := by
265 change Continuous fun n : ProfiniteKernelSubgroup psi =>
266 Multiplicative.ofAdd (zcUniversalDifferential C psi.toMonoidHom n.1)
267 exact continuous_ofAdd.comp (hD.comp continuous_subtype_val)
269/-- Well-definedness of `d_N` from continuity of the universal completed differential on the
270ambient group. -/
272 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
273 [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
274 [T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)]
275 (hD : Continuous (fun g : G => zcUniversalDifferential C psi.toMonoidHom g)) :
276 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi :=
278 (G := G) (H := H) C psi
280 (G := G) (H := H) C psi hD)
282/-- Finite-coordinate form of the topological well-definedness step for `d_N`.
285with a continuous coordinate-valued map, then the ordinary commutator-killing identity extends to
286`closure([N,N])`. In paper language, this is the passage from a continuous coordinate formula
287for `D|_N` to the well-defined map `N^ab(C) -> A_psi(C)`. -/
289 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
290 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
291 (hbasis_A :
293 (G := G) (H := H) C psi family)
294 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
295 (Dcoords : ProfiniteKernelSubgroup psi →
296 ZCFreeFoxCoordinates C (X := X) (H := H))
297 (hDcoords_continuous : Continuous Dcoords)
298 (hDcoords :
299 ∀ n : ProfiniteKernelSubgroup psi,
300 Dcoords n =
302 (G := G) (H := H) C psi family hbasis_A
303 (zcUniversalDifferential C psi.toMonoidHom n.1)) :
304 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi := by
305 refine
307 (G := G) (H := H) C psi ?_
308 have hclosed_zero :
309 IsClosed ({0} : Set (ZCFreeFoxCoordinates C (X := X) (H := H))) :=
310 isClosed_singleton
311 have hclosed_preimage :
312 IsClosed
313 (Dcoords ⁻¹' ({0} : Set (ZCFreeFoxCoordinates C (X := X) (H := H)))) :=
314 hclosed_zero.preimage hDcoords_continuous
315 have hker_set :
316 (((completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker :
317 Subgroup (ProfiniteKernelSubgroup psi)) : Set (ProfiniteKernelSubgroup psi)) =
318 Dcoords ⁻¹' ({0} : Set (ZCFreeFoxCoordinates C (X := X) (H := H))) := by
319 ext n
320 change
321 completedKernelBoundaryProCInteger (G := G) (H := H) C psi n = 1 ↔
322 Dcoords n = 0
323 constructor
324 · intro hn
325 have hDzero : zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
326 change Multiplicative.ofAdd
327 (zcUniversalDifferential C psi.toMonoidHom n.1) = 1 at hn
328 simpa using
329 congrArg
330 (fun x : Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom) =>
331 Multiplicative.toAdd x) hn
332 rw [hDcoords n, hDzero]
334 · intro hn
335 have hcoords_zero :
337 (G := G) (H := H) C psi family hbasis_A
338 (zcUniversalDifferential C psi.toMonoidHom n.1) = 0 := by
339 rw [← hDcoords n]
340 exact hn
341 have hDzero : zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
342 apply
344 (G := G) (H := H) C psi family hbasis_A).injective
345 simpa using hcoords_zero
346 change Multiplicative.ofAdd
347 (zcUniversalDifferential C psi.toMonoidHom n.1) =
348 (1 : Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom))
349 simpa [hDzero]
350 rw [hker_set]
351 exact hclosed_preimage
353/-- `Fin`-indexed finite-coordinate form of the topological well-definedness step for `d_N`. -/
355 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
356 {r : Nat} (family : Fin r → G)
357 (hbasis_A :
359 (G := G) (H := H) C psi family)
360 [T1Space (Fin r → ZCCompletedGroupAlgebra C H)]
361 (Dcoords : ProfiniteKernelSubgroup psi → Fin r → ZCCompletedGroupAlgebra C H)
362 (hDcoords_continuous : Continuous Dcoords)
363 (hDcoords :
364 ∀ n : ProfiniteKernelSubgroup psi,
365 Dcoords n =
367 (G := G) (H := H) C psi family hbasis_A
368 (zcUniversalDifferential C psi.toMonoidHom n.1)) :
369 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi := by
370 refine
372 (G := G) (H := H) C psi ?_
373 have hclosed_zero :
374 IsClosed ({0} : Set (Fin r → ZCCompletedGroupAlgebra C H)) :=
375 isClosed_singleton
376 have hclosed_preimage :
377 IsClosed (Dcoords ⁻¹' ({0} : Set (Fin r → ZCCompletedGroupAlgebra C H))) :=
378 hclosed_zero.preimage hDcoords_continuous
379 have hker_set :
380 (((completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker :
381 Subgroup (ProfiniteKernelSubgroup psi)) : Set (ProfiniteKernelSubgroup psi)) =
382 Dcoords ⁻¹' ({0} : Set (Fin r → ZCCompletedGroupAlgebra C H)) := by
383 ext n
384 change
385 completedKernelBoundaryProCInteger (G := G) (H := H) C psi n = 1 ↔
386 Dcoords n = 0
387 constructor
388 · intro hn
389 have hDzero : zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
390 change Multiplicative.ofAdd
391 (zcUniversalDifferential C psi.toMonoidHom n.1) = 1 at hn
392 simpa using
393 congrArg
394 (fun x : Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom) =>
395 Multiplicative.toAdd x) hn
396 rw [hDcoords n, hDzero]
398 · intro hn
399 have hcoords_zero :
401 (G := G) (H := H) C psi family hbasis_A
402 (zcUniversalDifferential C psi.toMonoidHom n.1) = 0 := by
403 rw [← hDcoords n]
404 exact hn
405 have hDzero : zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
406 apply
408 (G := G) (H := H) C psi family hbasis_A).injective
409 simpa using hcoords_zero
410 change Multiplicative.ofAdd
411 (zcUniversalDifferential C psi.toMonoidHom n.1) =
412 (1 : Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom))
413 simpa [hDzero]
414 rw [hker_set]
415 exact hclosed_preimage
417/-- Ambient-coordinate version of
419This is the form used when a continuous Fox-coordinate formula is constructed on the whole source
422 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
423 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
424 (hbasis_A :
426 (G := G) (H := H) C psi family)
427 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
428 (Dcoords : G → ZCFreeFoxCoordinates C (X := X) (H := H))
429 (hDcoords_continuous : Continuous Dcoords)
430 (hDcoords :
431 ∀ n : ProfiniteKernelSubgroup psi,
432 Dcoords n.1 =
434 (G := G) (H := H) C psi family hbasis_A
435 (zcUniversalDifferential C psi.toMonoidHom n.1)) :
436 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi := by
437 exact
439 (G := G) (H := H) C psi family hbasis_A
440 (fun n : ProfiniteKernelSubgroup psi => Dcoords n.1)
441 (hDcoords_continuous.comp continuous_subtype_val)
442 hDcoords
444/-- `Fin`-indexed ambient-coordinate version of
447 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
448 {r : Nat} (family : Fin r → G)
449 (hbasis_A :
451 (G := G) (H := H) C psi family)
452 [T1Space (Fin r → ZCCompletedGroupAlgebra C H)]
453 (Dcoords : G → Fin r → ZCCompletedGroupAlgebra C H)
454 (hDcoords_continuous : Continuous Dcoords)
455 (hDcoords :
456 ∀ n : ProfiniteKernelSubgroup psi,
457 Dcoords n.1 =
459 (G := G) (H := H) C psi family hbasis_A
460 (zcUniversalDifferential C psi.toMonoidHom n.1)) :
461 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi := by
462 exact
464 (G := G) (H := H) C psi family hbasis_A
465 (fun n : ProfiniteKernelSubgroup psi => Dcoords n.1)
466 (hDcoords_continuous.comp continuous_subtype_val)
467 hDcoords
469end
471end CrowellExactSequence