Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Continuous.Magnus.KernelClosedCommutator
ProCGroups/FoxDifferential/Completed/Continuous/Magnus/KernelClosedCommutator/Source

Source: ProCGroups.FoxDifferential.Completed.Continuous.Magnus.KernelClosedCommutator

1import ProCGroups.FoxDifferential.Completed.Comparison.MagnusKernel
2import ProCGroups.FoxDifferential.Completed.Continuous.Magnus.FiniteStageKernel
3import ProCGroups.ProC.OpenNormalSubgroups.ClosedCommutator
4import ProCGroups.FreeProC.FiniteBasis
5import ProCGroups.FoxDifferential.Completed.Continuous.Magnus.ClosedGeneratedVector
7/-!
8# Fox Differential / Completed / Continuous Magnus / Kernel Closed Commutator
10This module identifies the kernel of the completed Magnus map with the closed
11commutator subgroup of the presentation kernel, using the finite-stage kernel
12comparison and the pro-\(C\) closed-commutator criterion.
13-/
15namespace CrowellExactSequence
17noncomputable section
19open ProCGroups.ProC
22universe u
24variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
25variable {C : ProCGroups.FiniteGroupClass.{u}}
30/--
31Concrete continuous Magnus kernel for the closed-generated completed Fox vector. It gives the
32injectivity step for \(d_N : N^{\mathrm{ab}}(C) \to \mathbb{Z}_C\llbracket H\rrbracket^{r}\):
33an element killed by the continuous Fox derivative vector already lies in \(\overline{[N,N]}\).
34-/
35theorem freeProC_closedGeneratedFoxVector_kernel_le_closedCommutator
36 [CompactSpace H]
37 [T2Space H]
38 [TotallyDisconnectedSpace H]
40 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
41 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
42 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
43 (htarget :
44 HasOpenNormalBasisInClass C
46 (C := C)
47 (fun i : ULift.{u} (Fin r) =>
48 psi (freeProCChosenULiftFamilyOfBasisCard
49 (C := C) sourceData hbasis i)) : Subgroup
51 C (ULift.{u} (Fin r)) H))) :
52 ∀ n : ProfiniteKernelSubgroup psi,
53 freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
54 (H := H) (C := C) sourceData hbasis psi htarget n.1 = 0 →
55 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi) := by
56 classical
57 let X : Type u := ULift.{u} (Fin r)
58 let ι : X → sourceData.carrier :=
59 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
60 letI : IsClosed
61 ((ProfiniteKernelSubgroup psi : Subgroup sourceData.carrier) :
62 Set sourceData.carrier) :=
63 isClosed_profiniteKernelSubgroup psi
64 letI : CompactSpace (ProfiniteKernelSubgroup psi) :=
65 (show IsClosed
66 ((ProfiniteKernelSubgroup psi : Subgroup sourceData.carrier) :
67 Set sourceData.carrier) from inferInstance).isClosedEmbedding_subtypeVal.compactSpace
68 have hKernel : HasOpenNormalBasisInClass C (ProfiniteKernelSubgroup psi) :=
69 HasOpenNormalBasisInClass.profiniteKernelSubgroup
70 hC.hereditary sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi
71 intro n hnD
72 refine
73 mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator
74 (G := ProfiniteKernelSubgroup psi)
75 hC.melnikovFormation.formation hKernel ?_
76 intro U
77 let Nclosed : ClosedSubgroup sourceData.carrier :=
78 ⟨ProfiniteKernelSubgroup psi, isClosed_profiniteKernelSubgroup psi⟩
79 rcases exists_openNormalSubgroupInClass_inter_closedSubgroup_le
80 (C := C)
81 (G := sourceData.carrier) sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass
82 Nclosed U.1.toOpenSubgroup with
83 ⟨V₀, hV₀U⟩
84 have hV₀U_sub :
85 ∀ m : ProfiniteKernelSubgroup psi,
86 m.1 ∈ (V₀.1 : Subgroup sourceData.carrier) →
87 m ∈ (U.1 : Subgroup (ProfiniteKernelSubgroup psi)) := by
88 intro m hm
89 exact hV₀U (by
90 change m.1 ∈ (V₀.1 : Subgroup sourceData.carrier)
91 exact hm)
92 let hfopen : IsOpenMap psi :=
94 let W₀ : OpenNormalSubgroupInClass C H :=
95 OpenNormalSubgroupInClass.mapOpenNormal_of_formation
96 (C := C) (G := sourceData.carrier)
97 hC.melnikovFormation.formation psi hfopen hpsi V₀
98 let Q₀ : Type u := sourceData.carrier ⧸ (V₀.1 : Subgroup sourceData.carrier)
99 let K₀ : Type u := H ⧸ (W₀.1 : Subgroup H)
100 letI : Finite Q₀ := C.finite V₀.2
101 letI : Finite K₀ := C.finite W₀.2
102 letI : DiscreteTopology K₀ :=
103 QuotientGroup.discreteTopology W₀.1.toOpenSubgroup.isOpen'
104 let qH₀ : H →ₜ* K₀ :=
105 OpenNormalSubgroupInClass.quotientProj
106 (C := C) W₀
107 have hV₀W₀ :
108 (V₀.1 : Subgroup sourceData.carrier) ≤
109 (W₀.1 : Subgroup H).comap psi.toMonoidHom := by
110 intro g hg
111 change psi g ∈ (W₀.1 : Subgroup H)
112 change psi g ∈
113 ((OpenNormalSubgroup.map psi hfopen hpsi V₀.1 : OpenNormalSubgroup H) :
114 Subgroup H)
115 exact (Subgroup.mem_map).2 ⟨g, hg, rfl⟩
116 let α₀ : FreeGroup X →* Q₀ :=
117 (QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier)).comp
118 (FreeGroup.lift ι)
119 let β : Q₀ →* K₀ :=
120 QuotientGroup.map
121 (N := (V₀.1 : Subgroup sourceData.carrier))
122 (M := (W₀.1 : Subgroup H))
123 (f := psi.toMonoidHom) hV₀W₀
124 have hα₀_surj : Function.Surjective α₀ := by
125 simpa [α₀, X, ι] using
126 freeProCChosenULiftFamilyOfBasisCard_quotient_lift_surjective
127 (C := C) sourceData hbasis V₀
128 have hβ_surj : Function.Surjective β := by
129 intro y
130 rcases QuotientGroup.mk'_surjective (W₀.1 : Subgroup H) y with ⟨h, rfl⟩
131 rcases hpsi h with ⟨g, rfl⟩
132 exact ⟨QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) g, rfl⟩
133 have hCker : C β.ker :=
134 hC.hereditary.subgroupClosed β.ker V₀.2
135 letI : Finite β.ker := C.finite hCker
137 (C := C)
138 hC.melnikovFormation.formation hC.hereditary hCker with
139 ⟨j, hpow⟩
140 let ψstage : FreeGroup X →* K₀ := β.comp α₀
141 let Nstage : Subgroup (FreeGroup X) := ψstage.ker
142 let Qstage : Type u := FoxDifferential.zcFiniteStageTarget X Nstage
143 letI : TopologicalSpace Qstage := ⊥
144 letI : DiscreteTopology Qstage := ⟨rfl⟩
145 letI : IsTopologicalGroup Qstage := inferInstance
146 have hψstage_surj : Function.Surjective ψstage := by
147 intro k
148 rcases hβ_surj k with ⟨q, rfl⟩
149 rcases hα₀_surj q with ⟨w, rfl⟩
150 exact ⟨w, rfl⟩
151 let e : Qstage ≃* K₀ :=
152 QuotientGroup.quotientKerEquivOfSurjective ψstage hψstage_surj
153 have hCstage : C Qstage :=
154 hC.isomClosed ⟨e.symm⟩ W₀.2
155 let eSymm : K₀ →ₜ* Qstage :=
156 { toMonoidHom := e.symm.toMonoidHom
157 continuous_toFun := continuous_of_discreteTopology }
158 let η : H →ₜ* Qstage :=
159 eSymm.comp qH₀
160 have he_apply (w : FreeGroup X) :
161 e (QuotientGroup.mk' Nstage w) = ψstage w := by
162 change QuotientGroup.quotientKerEquivOfSurjective ψstage hψstage_surj
163 (QuotientGroup.mk' ψstage.ker w) = ψstage w
164 rfl
165 have hη :
166 (η : H →* Qstage).comp
167 ((psi : sourceData.carrier →* H).comp (FreeGroup.lift ι)) =
168 QuotientGroup.mk' Nstage := by
169 apply MonoidHom.ext
170 intro w
171 apply e.injective
172 change e (η (psi ((FreeGroup.lift ι) w))) =
173 e (QuotientGroup.mk' Nstage w)
174 rw [he_apply]
175 change e (e.symm (qH₀ (psi ((FreeGroup.lift ι) w)))) = β (α₀ w)
176 rw [e.apply_symm_apply]
177 change QuotientGroup.mk' (W₀.1 : Subgroup H) (psi ((FreeGroup.lift ι) w)) =
178 β (QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) ((FreeGroup.lift ι) w))
179 rw [QuotientGroup.map_mk']
180 rfl
182 C Qstage :=
184 C Qstage hC.isomClosed hCstage)
185 rcases exists_openNormalSubgroupInClass_eq_on_right_coset_closedGenFoxVector_proj
186 (H := H) (C := C) hC.hereditary
187 sourceData hbasis psi htarget η J n.1 with
188 ⟨Vloc, hloc⟩
189 let Vfinal : OpenNormalSubgroupInClass C sourceData.carrier :=
190 OpenNormalSubgroupInClass.inf
191 (C := C) (G := sourceData.carrier)
192 hC.melnikovFormation.formation V₀ Vloc
193 let αfinal : FreeGroup X →*
194 sourceData.carrier ⧸ (Vfinal.1 : Subgroup sourceData.carrier) :=
195 (QuotientGroup.mk' (Vfinal.1 : Subgroup sourceData.carrier)).comp
196 (FreeGroup.lift ι)
197 have hαfinal_surj : Function.Surjective αfinal := by
198 simpa [αfinal, X, ι] using
199 freeProCChosenULiftFamilyOfBasisCard_quotient_lift_surjective
200 (C := C) sourceData hbasis Vfinal
201 rcases hαfinal_surj
202 (QuotientGroup.mk' (Vfinal.1 : Subgroup sourceData.carrier) n.1) with
203 ⟨w, hwfinal⟩
204 have hfinal_le_V₀ :
205 (Vfinal.1 : Subgroup sourceData.carrier) ≤ (V₀.1 : Subgroup sourceData.carrier) := by
206 intro g hg
207 change g ∈
208 ((V₀.1 ⊓ Vloc.1 : OpenNormalSubgroup sourceData.carrier) :
209 Subgroup sourceData.carrier) at hg
210 exact hg.1
211 have hfinal_le_Vloc :
212 (Vfinal.1 : Subgroup sourceData.carrier) ≤ (Vloc.1 : Subgroup sourceData.carrier) := by
213 intro g hg
214 change g ∈
215 ((V₀.1 ⊓ Vloc.1 : OpenNormalSubgroup sourceData.carrier) :
216 Subgroup sourceData.carrier) at hg
217 exact hg.2
218 have hα₀w :
219 α₀ w = QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) n.1 := by
220 let τ : sourceData.carrier ⧸ (Vfinal.1 : Subgroup sourceData.carrier) →*
221 sourceData.carrier ⧸ (V₀.1 : Subgroup sourceData.carrier) :=
222 QuotientGroup.map
223 (N := (Vfinal.1 : Subgroup sourceData.carrier))
224 (M := (V₀.1 : Subgroup sourceData.carrier))
225 (f := MonoidHom.id sourceData.carrier) hfinal_le_V₀
226 have hτ := congrArg τ hwfinal
227 simpa [τ, αfinal, α₀] using hτ
228 have hdiff_final :
229 ((FreeGroup.lift ι) w) * n.1⁻¹ ∈
230 (Vfinal.1 : Subgroup sourceData.carrier) := by
231 have hwq :
232 QuotientGroup.mk' (Vfinal.1 : Subgroup sourceData.carrier)
233 ((FreeGroup.lift ι) w) =
234 QuotientGroup.mk' (Vfinal.1 : Subgroup sourceData.carrier) n.1 := by
235 simpa [αfinal] using hwfinal
236 simpa [div_eq_mul_inv] using
237 (QuotientGroup.eq_iff_div_mem
238 (N := (Vfinal.1 : Subgroup sourceData.carrier))).1 hwq
239 have hdiff_loc :
240 ((FreeGroup.lift ι) w) * n.1⁻¹ ∈
241 (Vloc.1 : Subgroup sourceData.carrier) :=
242 hfinal_le_Vloc hdiff_final
243 have hproj_n :
244 (fun i : X =>
246 Qstage J
248 (X := X) C hC.hereditary η
249 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
250 (H := H) (C := C) sourceData hbasis psi htarget n.1)) i)) = 0 := by
251 funext i
252 simp only [hnD, FoxDifferential.zcFreeFoxCoordinatesMap_apply, Pi.zero_apply, map_zero,
254 have hproj_w :
255 (fun i : X =>
257 Qstage J
259 (X := X) C hC.hereditary η
260 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
261 (H := H) (C := C) sourceData hbasis psi htarget
262 ((FreeGroup.lift ι) w))) i)) = 0 := by
263 have heq := hloc ((FreeGroup.lift ι) w) hdiff_loc
264 exact (by
265 simpa [X, ι, J] using
266 heq.trans (by
267 simpa [X, ι, J] using hproj_n))
268 have hder :
270 (X := X) Nstage j.modulus w = 0 :=
271 foxAlgebraicStageDerivativeVector_eq_zero_of_closedGenFoxVector_proj_eq_zero
272 (H := H) (C := C) hC.melnikovFormation.formation hC.hereditary
273 hC.isomClosed sourceData hbasis psi hpsi htarget
274 (N := Nstage) hCstage η hη j hproj_w
275 have hwker : w ∈ (β.comp α₀).ker := by
276 change β (α₀ w) = 1
277 rw [hα₀w]
278 change QuotientGroup.mk' (W₀.1 : Subgroup H) (psi n.1) = 1
279 exact (QuotientGroup.eq_one_iff
280 (N := (W₀.1 : Subgroup H)) (psi n.1)).2 (by
281 have hnpsi : psi n.1 = 1 := by
282 exact n.2
283 rw [hnpsi]
284 exact (W₀.1 : Subgroup H).one_mem)
285 have hcommβ :
286 (⟨α₀ w, by
287 change β (α₀ w) = 1
288 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
289 commutator β.ker :=
290 mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero_finite
291 (X := X) α₀ β j.modulus j.positive hpow hwker
292 (by simpa [Nstage, ψstage] using hder)
293 let κ : ProfiniteKernelSubgroup psi →* β.ker :=
294 { toFun := fun m =>
295 ⟨QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) m.1, by
296 change β (QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) m.1) = 1
297 change QuotientGroup.mk' (W₀.1 : Subgroup H) (psi m.1) = 1
298 exact (QuotientGroup.eq_one_iff
299 (N := (W₀.1 : Subgroup H)) (psi m.1)).2 (by
300 have hmpsi : psi m.1 = 1 := by
301 exact m.2
302 rw [hmpsi]
303 exact (W₀.1 : Subgroup H).one_mem)⟩
304 map_one' := by
305 apply Subtype.ext
306 simp only [OneMemClass.coe_one, QuotientGroup.mk'_apply, QuotientGroup.mk_one]
307 map_mul' := by
308 intro a b
309 apply Subtype.ext
310 simp only [Subgroup.coe_mul, map_mul, QuotientGroup.mk'_apply, MulMemClass.mk_mul_mk]}
311 have hκ_surj : Function.Surjective κ := by
312 intro y
313 rcases QuotientGroup.mk'_surjective
314 (V₀.1 : Subgroup sourceData.carrier) y.1 with
315 ⟨g, hg⟩
316 have hψgW : psi g ∈ (W₀.1 : Subgroup H) := by
317 have hβg : β (QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) g) = 1 := by
318 have hyβ : β y.1 = 1 := by
319 exact y.2
320 simpa [hg] using hyβ
321 change QuotientGroup.mk' (W₀.1 : Subgroup H) (psi g) = 1 at hβg
322 exact (QuotientGroup.eq_one_iff
323 (N := (W₀.1 : Subgroup H)) (psi g)).1 hβg
324 have hψgWmap :
325 psi g ∈
326 ((OpenNormalSubgroup.map psi hfopen hpsi V₀.1 : OpenNormalSubgroup H) :
327 Subgroup H) := by
328 change psi g ∈
329 ((OpenNormalSubgroup.map psi hfopen hpsi V₀.1 : OpenNormalSubgroup H) :
330 Subgroup H) at hψgW
331 exact hψgW
332 rcases (Subgroup.mem_map).1 hψgWmap with ⟨v, hvV₀, hvψ⟩
333 let m : ProfiniteKernelSubgroup psi :=
334 ⟨g * v⁻¹, by
335 change psi (g * v⁻¹) = 1
336 rw [map_mul, map_inv]
337 have hvψ' : psi v = psi g := hvψ
338 rw [hvψ', mul_inv_cancel]⟩
339 refine ⟨m, ?_⟩
340 apply Subtype.ext
341 change QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) (g * v⁻¹) = y.1
342 rw [← hg]
343 have hvq :
344 QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) v = 1 :=
345 (QuotientGroup.eq_one_iff
346 (N := (V₀.1 : Subgroup sourceData.carrier)) v).2 hvV₀
347 rw [map_mul, map_inv, hvq]
348 simp only [QuotientGroup.mk'_apply, inv_one, mul_one]
349 have hκkerU :
350 κ.ker ≤ (U.1 : Subgroup (ProfiniteKernelSubgroup psi)) := by
351 intro m hm
352 have hq : QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) m.1 = 1 := by
353 exact congrArg Subtype.val hm
354 exact hV₀U_sub m
355 ((QuotientGroup.eq_one_iff
356 (N := (V₀.1 : Subgroup sourceData.carrier)) m.1).1 hq)
357 have hκn_eq :
358 κ n =
359 (⟨α₀ w, by
360 change β (α₀ w) = 1
361 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) := by
362 apply Subtype.ext
363 exact hα₀w.symm
364 have hκn_comm : κ n ∈ commutator β.ker := by
365 simpa [hκn_eq] using hcommβ
366 have hquotU :
367 QuotientGroup.mk' (U.1 : Subgroup (ProfiniteKernelSubgroup psi)) n ∈
368 commutator (ProfiniteKernelSubgroup psi ⧸ (U.1 : Subgroup (ProfiniteKernelSubgroup psi))) :=
369 quotient_mk_mem_commutator_of_surjective_image_mem_commutator
370 κ hκ_surj (U.1 : Subgroup (ProfiniteKernelSubgroup psi)) hκkerU hκn_comm
371 exact ⟨U, le_rfl, hquotU⟩
373end
375end CrowellExactSequence