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

Source: ProCGroups.CrowellExactSequence.Profinite.KernelInjectivity

1import ProCGroups.CrowellExactSequence.Profinite.KernelBoundary
3/-!
4# Injectivity criteria from the profinite kernel
6This file factors the completed Crowell boundary through the topological abelianization of the
7kernel. It proves that the resulting boundary is annihilated by the completed differential map
8and records the Magnus-kernel criteria used to establish injectivity in the profinite sequence.
9-/
11namespace CrowellExactSequence
13noncomputable section
15open ProCGroups.ProC
17universe u
19variable {G H : Type u}
20variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
21variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
23/--
24Boundary from the topological kernel abelianization to \(A_{\psi}(C)\), assuming the displayed
25boundary kills \(\overline{[N,N]}\).
26-/
27def profiniteKernelAbelianizationBoundaryHomProCInteger
28 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
29 (hwell_dN :
30 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
31 ProfiniteKernelAbelianization psi →*
32 Multiplicative (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom) :=
33 QuotientGroup.lift
34 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)))
35 (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)
36 hwell_dN
38/-- Additive boundary from the topological kernel abelianization to \(A_{\psi}(C)\). -/
39def profiniteKernelAbelianizationBoundaryAddProCInteger
40 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
41 (hwell_dN :
42 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
43 ProfiniteKernelAbelianizationAdd psi →+
45 (profiniteKernelAbelianizationBoundaryHomProCInteger
46 (G := G) (H := H) C psi hwell_dN).toAdditiveLeft
48/--
49The \(\mathbb{Z}_C\)-coefficient boundary map is obtained from the profinite kernel
50abelianization boundary construction.
51-/
52@[simp]
53theorem profiniteKernelAbelianizationBoundaryAddProCInteger_of
54 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
55 (hwell_dN :
56 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
57 (n : ProfiniteKernelSubgroup psi) :
58 profiniteKernelAbelianizationBoundaryAddProCInteger
59 (G := G) (H := H) C psi hwell_dN
60 (Additive.ofMul
61 (QuotientGroup.mk'
62 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
63 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 := by
64 rfl
66/--
67Separated boundary from the topological kernel abelianization to the finite-stage separated
68completed differential module. Unlike the algebraic target, this map is well-defined without a
69separate closedness or continuity hypothesis.
70-/
71def profiniteKernelAbelianizationBoundaryHomProCIntegerSep
72 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
73 ProfiniteKernelAbelianization psi →*
74 Multiplicative
76 QuotientGroup.lift
77 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)))
78 (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi)
79 (separatedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
81/-- Additive separated boundary from the topological kernel abelianization. -/
82def profiniteKernelAbelianizationBoundaryAddProCIntegerSep
83 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
84 ProfiniteKernelAbelianizationAdd psi →+
86 (profiniteKernelAbelianizationBoundaryHomProCIntegerSep
87 (G := G) (H := H) C psi).toAdditiveLeft
89/--
90The separated \(\mathbb{Z}_C\)-coefficient boundary map is obtained from the profinite kernel
91abelianization boundary construction.
92-/
93@[simp]
94theorem profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of
95 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
96 (n : ProfiniteKernelSubgroup psi) :
97 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
98 (G := G) (H := H) C psi
99 (Additive.ofMul
100 (QuotientGroup.mk'
101 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
103 rfl
105/--
106The map from the completed differential module to its separated quotient carries the
107kernel-abelianization boundary to its separated version.
108-/
109theorem zcDiffModuleToSep_profKerAbBoundaryAddZC
110 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
111 (hwell_dN :
112 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
113 (x : ProfiniteKernelAbelianizationAdd psi) :
115 (profiniteKernelAbelianizationBoundaryAddProCInteger
116 (G := G) (H := H) C psi hwell_dN x) =
117 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
118 (G := G) (H := H) C psi x := by
119 change
120 (fun y : ProfiniteKernelAbelianization psi =>
122 (profiniteKernelAbelianizationBoundaryAddProCInteger
123 (G := G) (H := H) C psi hwell_dN (Additive.ofMul y)) =
124 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
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
131 (profiniteKernelAbelianizationBoundaryAddProCInteger
132 (G := G) (H := H) C psi hwell_dN
133 (Additive.ofMul
134 (QuotientGroup.mk'
135 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
136 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
137 (G := G) (H := H) C psi
138 (Additive.ofMul
139 (QuotientGroup.mk'
140 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))
141 rw [profiniteKernelAbelianizationBoundaryAddProCInteger_of,
142 profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of,
145/--
146The completed Crowell differential map vanishes on the image of the profinite-kernel
147abelianization boundary.
148-/
149theorem presentedCompletedToZC_profiniteKernelAbelianizationBoundaryAdd
150 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
151 (hwell_dN :
152 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
153 (x : ProfiniteKernelAbelianizationAdd psi) :
154 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
155 (profiniteKernelAbelianizationBoundaryAddProCInteger
156 (G := G) (H := H) C psi hwell_dN x) =
157 0 := by
158 change
159 (fun y : ProfiniteKernelAbelianization psi =>
160 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
161 (profiniteKernelAbelianizationBoundaryAddProCInteger
162 (G := G) (H := H) C psi hwell_dN (Additive.ofMul y)) = 0)
163 (Additive.toMul x)
164 refine QuotientGroup.induction_on (Additive.toMul x) ?_
165 intro n
166 change
167 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
168 (profiniteKernelAbelianizationBoundaryAddProCInteger
169 (G := G) (H := H) C psi hwell_dN
170 (Additive.ofMul
171 (QuotientGroup.mk'
172 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
173 0
174 rw [profiniteKernelAbelianizationBoundaryAddProCInteger_of,
175 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d_of_mem_ker]
177/--
178Magnus-kernel criterion form of injectivity for the genuine topological kernel boundary. In
179paper language this is the step \(ker(D|_N) = \overline{[N,N]} \mapsto d_N: N^{\mathrm{ab}}(C)
180\to A_{\psi}(C)\) is injective.
181-/
182theorem profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
183 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
184 (hwell_dN :
185 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
186 (hker :
187 ∀ n : ProfiniteKernelSubgroup psi,
188 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
189 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
190 Function.Injective
191 (profiniteKernelAbelianizationBoundaryAddProCInteger
192 (G := G) (H := H) C psi hwell_dN) := by
193 intro x y hxy
194 suffices x - y = 0 by exact sub_eq_zero.mp this
195 let F :=
196 profiniteKernelAbelianizationBoundaryAddProCInteger
197 (G := G) (H := H) C psi hwell_dN
198 have hmap : F (x - y) = 0 := by
199 rw [map_sub, hxy, sub_self]
200 have hzero_of_map_zero :
201 ∀ z : ProfiniteKernelAbelianizationAdd psi, F z = 0 → z = 0 := by
202 intro z hz
203 apply Additive.toMul.injective
204 change (Additive.toMul z : ProfiniteKernelAbelianization psi) = 1
205 revert hz
206 change
207 (fun q : ProfiniteKernelAbelianization psi =>
208 F (Additive.ofMul q) = 0 → q = 1) (Additive.toMul z)
209 refine QuotientGroup.induction_on (Additive.toMul z) ?_
210 intro n hn
211 change
212 QuotientGroup.mk'
213 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n = 1
214 exact (QuotientGroup.eq_one_iff
215 (N := Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n).2
216 (by
217 have hnD :
218 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := by
219 calc
221 F
222 (Additive.ofMul
223 (QuotientGroup.mk'
224 (Subgroup.topologicalClosure
225 (commutator (ProfiniteKernelSubgroup psi))) n)) :=
226 (profiniteKernelAbelianizationBoundaryAddProCInteger_of
227 (G := G) (H := H) C psi hwell_dN n).symm
228 _ = 0 := hn
229 simpa [Subgroup.closedCommutator] using hker n hnD)
230 exact hzero_of_map_zero (x - y) hmap
232/-- Magnus-kernel criterion form of injectivity for the separated topological kernel boundary. -/
233theorem profKerAbBoundaryAddZCSep_inj_of_kernel_le_closedCommutator
234 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
235 (hker :
236 ∀ n : ProfiniteKernelSubgroup psi,
238 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
239 Function.Injective
240 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
241 (G := G) (H := H) C psi) := by
242 intro x y hxy
243 suffices x - y = 0 by exact sub_eq_zero.mp this
244 let F :=
245 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
246 (G := G) (H := H) C psi
247 have hmap : F (x - y) = 0 := by
248 rw [map_sub, hxy, sub_self]
249 have hzero_of_map_zero :
250 ∀ z : ProfiniteKernelAbelianizationAdd psi, F z = 0 → z = 0 := by
251 intro z hz
252 apply Additive.toMul.injective
253 change (Additive.toMul z : ProfiniteKernelAbelianization psi) = 1
254 revert hz
255 change
256 (fun q : ProfiniteKernelAbelianization psi =>
257 F (Additive.ofMul q) = 0 → q = 1) (Additive.toMul z)
258 refine QuotientGroup.induction_on (Additive.toMul z) ?_
259 intro n hn
260 change
261 QuotientGroup.mk'
262 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n = 1
263 exact (QuotientGroup.eq_one_iff
264 (N := Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n).2
265 (by
266 have hnD :
268 C psi.toMonoidHom n.1 = 0 := by
269 calc
271 F
272 (Additive.ofMul
273 (QuotientGroup.mk'
274 (Subgroup.topologicalClosure
275 (commutator (ProfiniteKernelSubgroup psi))) n)) :=
276 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of
277 (G := G) (H := H) C psi n).symm
278 _ = 0 := hn
279 simpa [Subgroup.closedCommutator] using hker n hnD)
280 exact hzero_of_map_zero (x - y) hmap
282/--
283Injectivity of the genuine topological kernel boundary is exactly the Magnus-kernel criterion
284in the reverse direction. In paper language this says that once \(d_N: N^{\mathrm{ab}}(C) \to
285A_{\psi}(C)\) is known to be injective, an element of ker \(\psi\) whose completed Fox
286differential vanishes is already in \(\overline{[N,N]}\).
287-/
288theorem kernel_le_closedCommutator_of_profKerAbBoundaryAddZC_inj
289 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
290 (hwell_dN :
291 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
292 (hinj :
293 Function.Injective
294 (profiniteKernelAbelianizationBoundaryAddProCInteger
295 (G := G) (H := H) C psi hwell_dN)) :
296 ∀ n : ProfiniteKernelSubgroup psi,
297 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
298 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi) := by
299 intro n hn
300 let F :=
301 profiniteKernelAbelianizationBoundaryAddProCInteger
302 (G := G) (H := H) C psi hwell_dN
303 have hzero :
304 F
305 (Additive.ofMul
306 (QuotientGroup.mk'
307 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
308 F 0 := by
309 rw [profiniteKernelAbelianizationBoundaryAddProCInteger_of]
310 calc
311 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 := hn
312 _ = F 0 := F.map_zero.symm
313 have hclass :
314 Additive.ofMul
315 (QuotientGroup.mk'
316 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n) =
317 0 :=
318 hinj hzero
319 have hmk :
320 QuotientGroup.mk'
321 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n = 1 := by
322 simpa using congrArg Additive.toMul hclass
323 exact (QuotientGroup.eq_one_iff
324 (N := Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n).1 hmk
326/--
327Injectivity of \(d_N: N^{\mathrm{ab}}(C) \to A_{\psi}(C)\) is equivalent to the continuous
328Magnus-kernel criterion.
329-/
330theorem profKerAbBoundaryAddZC_inj_iff_kernel_le_closedCommutator
331 {C : ProCGroups.FiniteGroupClass.{u}} {psi : ContinuousMonoidHom G H}
332 (hwell_dN :
333 CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
334 Function.Injective
335 (profiniteKernelAbelianizationBoundaryAddProCInteger
336 (G := G) (H := H) C psi hwell_dN) ↔
337 ∀ n : ProfiniteKernelSubgroup psi,
338 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
339 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi) := by
340 constructor
341 · exact
342 kernel_le_closedCommutator_of_profKerAbBoundaryAddZC_inj
343 (G := G) (H := H) C psi hwell_dN
344 · exact
345 profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
346 (G := G) (H := H) C psi hwell_dN
348/--
349Continuous-boundary version of the Magnus-kernel injectivity criterion. This packages the two
350paper steps that \(d_N\) is well-defined and that \(\ker D|_N \leq \overline{[N,N]}\):
351continuity of the completed universal differential supplies well-definedness, and the kernel
352criterion supplies injectivity of the resulting genuine boundary map.
353-/
354theorem profKerAbBoundaryAddZC_inj_of_continuous_zcUnivDiff_kernel_le_closedCommutator
355 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
356 [TopologicalSpace (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom)]
358 (hD : Continuous
359 (fun g : G => FoxDifferential.zcUniversalDifferential C psi.toMonoidHom g))
360 (hker :
361 ∀ n : ProfiniteKernelSubgroup psi,
362 FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
363 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
364 let hwell_dN :=
365 completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff
366 (G := G) (H := H) C psi hD
367 Function.Injective
368 (profiniteKernelAbelianizationBoundaryAddProCInteger
369 (G := G) (H := H) C psi hwell_dN) := by
370 let hwell_dN :=
371 completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff
372 (G := G) (H := H) C psi hD
373 exact
374 profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
375 (G := G) (H := H) C psi hwell_dN hker
377end
379end CrowellExactSequence