CrowellExactSequence/Profinite/KernelInjectivity.lean
1import CrowellExactSequence.Profinite.KernelBoundary
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CrowellExactSequence/Profinite/KernelInjectivity.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Profinite kernel boundary
14This file contains the genuine boundary
15`d_N : N^ab(C) -> A_psi(C)` and the continuous-Magnus injectivity criterion for it.
16-/
18namespace CrowellExactSequence
20noncomputable section
22open ProCGroups.ProC
24universe u
26variable {G H : Type u}
27variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30/-- Boundary from the genuine topological kernel abelianization to `A_psi(C)`, assuming the
31displayed boundary kills `closure([N,N])`. -/
33 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
34 (hwell_dN :
35 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
36 ProfiniteKernelAbelianization psi →*
37 Multiplicative (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom) :=
38 QuotientGroup.lift
39 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)))
40 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)
41 hwell_dN
43/-- Additive boundary from the genuine topological kernel abelianization to `A_psi(C)`. -/
45 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
46 (hwell_dN :
47 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
49 FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom :=
51 (G := G) (H := H) C psi hwell_dN).toAdditiveLeft
53@[simp]
55 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
56 (hwell_dN :
57 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
58 (n : ProfiniteKernelSubgroup psi) :
60 (G := G) (H := H) C psi hwell_dN
61 (Additive.ofMul
62 (QuotientGroup.mk'
63 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
64 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 := by
65 rfl
67/-- Separated boundary from the genuine topological kernel abelianization to the finite-stage
68separated completed differential module. Unlike the algebraic target, this map is well-defined
69without a separate closedness or continuity hypothesis. -/
71 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
72 ProfiniteKernelAbelianization psi →*
73 Multiplicative
74 (FoxDifferential.ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
75 QuotientGroup.lift
76 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)))
77 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi)
78 (separatedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
80/-- Additive separated boundary from the genuine topological kernel abelianization. -/
82 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
84 FoxDifferential.ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
86 (G := G) (H := H) C psi).toAdditiveLeft
88/-- Pro-`C` notation for the separated topological kernel boundary. -/
90 (ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H) :
91 ProCKernelAbelianizationAdd ProC psi →+
93 ProC.finiteQuotientClass psi.toMonoidHom :=
95 (G := G) (H := H) ProC.finiteQuotientClass psi
97@[simp]
99 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
100 (n : ProfiniteKernelSubgroup psi) :
102 (G := G) (H := H) C psi
103 (Additive.ofMul
104 (QuotientGroup.mk'
105 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
106 FoxDifferential.zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 := by
107 rfl
110 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
111 (hwell_dN :
112 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
113 (x : ProfiniteKernelAbelianizationAdd psi) :
114 FoxDifferential.zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom
116 (G := G) (H := H) C psi hwell_dN x) =
118 (G := G) (H := H) C psi x := by
119 change
120 (fun y : ProfiniteKernelAbelianization psi =>
121 FoxDifferential.zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom
123 (G := G) (H := H) C psi hwell_dN (Additive.ofMul y)) =
125 (G := G) (H := H) C psi (Additive.ofMul y))
126 (Additive.toMul x)
127 refine QuotientGroup.induction_on (Additive.toMul x) ?_
128 intro n
129 change
130 FoxDifferential.zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom
132 (G := G) (H := H) C psi hwell_dN
133 (Additive.ofMul
134 (QuotientGroup.mk'
135 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
137 (G := G) (H := H) C psi
138 (Additive.ofMul
139 (QuotientGroup.mk'
140 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))
146 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
147 (hwell_dN :
148 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
149 (x : ProfiniteKernelAbelianizationAdd psi) :
150 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
152 (G := G) (H := H) C psi hwell_dN x) =
153 0 := by
154 change
155 (fun y : ProfiniteKernelAbelianization psi =>
156 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
158 (G := G) (H := H) C psi hwell_dN (Additive.ofMul y)) = 0)
159 (Additive.toMul x)
160 refine QuotientGroup.induction_on (Additive.toMul x) ?_
161 intro n
162 change
163 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
165 (G := G) (H := H) C psi hwell_dN
166 (Additive.ofMul
167 (QuotientGroup.mk'
168 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
169 0
173/-- Magnus-kernel criterion form of injectivity for the genuine topological kernel boundary.
175In paper language this is the step
178 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
179 (hwell_dN :
180 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
181 (hker :
182 ∀ n : ProfiniteKernelSubgroup psi,
183 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
184 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
185 Function.Injective
187 (G := G) (H := H) C psi hwell_dN) := by
188 intro x y hxy
189 suffices x - y = 0 by exact sub_eq_zero.mp this
190 let F :=
192 (G := G) (H := H) C psi hwell_dN
193 have hmap : F (x - y) = 0 := by
194 rw [map_sub, hxy, sub_self]
195 have hzero_of_map_zero :
196 ∀ z : ProfiniteKernelAbelianizationAdd psi, F z = 0 → z = 0 := by
197 intro z hz
198 apply Additive.toMul.injective
199 change (Additive.toMul z : ProfiniteKernelAbelianization psi) = 1
200 revert hz
201 change
202 (fun q : ProfiniteKernelAbelianization psi =>
203 F (Additive.ofMul q) = 0 → q = 1) (Additive.toMul z)
204 refine QuotientGroup.induction_on (Additive.toMul z) ?_
205 intro n hn
206 change
207 QuotientGroup.mk'
208 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n = 1
209 exact (QuotientGroup.eq_one_iff
210 (N := Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n).2
211 (by
212 simpa [Subgroup.closedCommutator, F] using
213 hker n (by simpa [F] using hn))
214 exact hzero_of_map_zero (x - y) hmap
216/-- Magnus-kernel criterion form of injectivity for the separated topological kernel boundary. -/
218 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
219 (hker :
220 ∀ n : ProfiniteKernelSubgroup psi,
221 FoxDifferential.zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = 0 →
222 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
223 Function.Injective
225 (G := G) (H := H) C psi) := by
226 intro x y hxy
227 suffices x - y = 0 by exact sub_eq_zero.mp this
228 let F :=
230 (G := G) (H := H) C psi
231 have hmap : F (x - y) = 0 := by
232 rw [map_sub, hxy, sub_self]
233 have hzero_of_map_zero :
234 ∀ z : ProfiniteKernelAbelianizationAdd psi, F z = 0 → z = 0 := by
235 intro z hz
236 apply Additive.toMul.injective
237 change (Additive.toMul z : ProfiniteKernelAbelianization psi) = 1
238 revert hz
239 change
240 (fun q : ProfiniteKernelAbelianization psi =>
241 F (Additive.ofMul q) = 0 → q = 1) (Additive.toMul z)
242 refine QuotientGroup.induction_on (Additive.toMul z) ?_
243 intro n hn
244 change
245 QuotientGroup.mk'
246 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n = 1
247 exact (QuotientGroup.eq_one_iff
248 (N := Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n).2
249 (by
250 simpa [Subgroup.closedCommutator, F] using
251 hker n (by simpa [F] using hn))
252 exact hzero_of_map_zero (x - y) hmap
254/-- Injectivity of the genuine topological kernel boundary is exactly the Magnus-kernel
255criterion in the reverse direction.
257In paper language this says that once
259Fox differential vanishes is already in `closure([N,N])`. -/
261 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
262 (hwell_dN :
263 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
264 (hinj :
265 Function.Injective
267 (G := G) (H := H) C psi hwell_dN)) :
268 ∀ n : ProfiniteKernelSubgroup psi,
269 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
270 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi) := by
271 intro n hn
272 let F :=
274 (G := G) (H := H) C psi hwell_dN
275 have hzero :
276 F
277 (Additive.ofMul
278 (QuotientGroup.mk'
279 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
280 F 0 := by
282 simpa [F] using hn
283 have hclass :
284 Additive.ofMul
285 (QuotientGroup.mk'
286 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n) =
287 0 :=
288 hinj hzero
289 have hmk :
290 QuotientGroup.mk'
291 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n = 1 := by
292 simpa using congrArg Additive.toMul hclass
293 exact (QuotientGroup.eq_one_iff
294 (N := Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n).1 hmk
296/-- Paper-language form: injectivity of
297`d_N : N^ab(C) -> A_psi(C)` is equivalent to the continuous Magnus-kernel criterion. -/
299 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
300 (hwell_dN :
301 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
302 Function.Injective
304 (G := G) (H := H) C psi hwell_dN) ↔
305 ∀ n : ProfiniteKernelSubgroup psi,
306 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
307 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi) := by
308 constructor
309 · exact
311 (G := G) (H := H) C psi hwell_dN
312 · exact
314 (G := G) (H := H) C psi hwell_dN
316/-- Continuous-boundary version of the Magnus-kernel injectivity criterion.
319continuity of the completed universal differential supplies well-definedness, and the kernel
320criterion supplies injectivity of the resulting genuine boundary map. -/
322 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
323 [TopologicalSpace (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom)]
324 [T1Space (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom)]
325 (hD : Continuous
326 (fun g : G => FoxDifferential.zcUniversalDifferential C psi.toMonoidHom g))
327 (hker :
328 ∀ n : ProfiniteKernelSubgroup psi,
329 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
330 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
331 let hwell_dN :=
333 (G := G) (H := H) C psi hD
334 Function.Injective
336 (G := G) (H := H) C psi hwell_dN) := by
337 let hwell_dN :=
339 (G := G) (H := H) C psi hD
340 exact
342 (G := G) (H := H) C psi hwell_dN hker
344end
346end CrowellExactSequence