Yamaguchi Lean 4 Library
CrowellExactSequence/Profinite/ContinuousMagnus/KernelClosedCommutator.lean
CrowellExactSequence/Profinite/ContinuousMagnus/KernelClosedCommutator/Source

CrowellExactSequence/Profinite/ContinuousMagnus/KernelClosedCommutator.lean

1import CrowellExactSequence.Discrete.MagnusComparison
2import CrowellExactSequence.Profinite.ContinuousMagnus.FiniteStageKernel
3import ProCGroups.ProC.OpenNormalSubgroups.ClosedCommutator
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/CrowellExactSequence/Profinite/ContinuousMagnus/KernelClosedCommutator.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Profinite Crowell exact sequence
16Crowell-specific material is kept separate from general Fox calculus: relation modules, kernel boundaries, Blanchfield-Lyndon maps, and discrete/profinite exactness statements are assembled here.
17-/
18namespace CrowellExactSequence
20noncomputable section
22open ProCGroups.ProC
24universe u
26variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27variable {ProC : ProCGroupPredicate.{u}}
29variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass]
32/-- Concrete continuous Magnus kernel for the closed-generated completed Fox vector.
34This is the paper's injectivity step for
35`d_N : N^ab(C) -> Z_C[[H]]^r`: a kernel element killed by the continuous Fox derivative vector
36already lies in `closure([N,N])`. -/
38 [T2Space H]
39 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
40 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
41 [ProC.DeterminedByFiniteQuotients]
42 (sourceData : FreeProCSourceData ProC)
43 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
44 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
45 (htarget :
46 ProC
47 (G :=
49 (ProC := ProC)
50 (fun i : ULift.{u} (Fin r) =>
52 (ProC := ProC) sourceData hbasis i)) : Subgroup
54 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))) :
57 (H := H) (ProC := ProC) sourceData hbasis psi htarget n.1 = 0 →
59 classical
60 let X : Type u := ULift.{u} (Fin r)
61 let ι : X → sourceData.carrier :=
62 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
63 letI : CompactSpace sourceData.carrier := ProCGroup.compactSpace ProC sourceData.carrier
64 letI : ProCGroup ProC (ProfiniteKernelSubgroup psi) :=
66 (G := sourceData.carrier) (H := H) ProC psi
67 intro n hnD
68 refine
69 ProCGroup.mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator
70 (G := ProfiniteKernelSubgroup psi) ProC ?_
71 intro U
72 let Nclosed : ClosedSubgroup sourceData.carrier :=
75 (C := ProC.finiteQuotientClass)
76 (G := sourceData.carrier) sourceData.proCGroup.isProCGroup
77 Nclosed U.1.toOpenSubgroup with
78 ⟨V₀, hV₀U⟩
79 have hV₀U_sub :
81 m.1 ∈ (V₀.1 : Subgroup sourceData.carrier) → m ∈ (U.1 : Subgroup (ProfiniteKernelSubgroup psi)) := by
82 intro m hm
83 exact hV₀U (by
84 change m.1 ∈ (V₀.1 : Subgroup sourceData.carrier)
85 exact hm)
86 let hfopen : IsOpenMap psi :=
88 let W₀ : OpenNormalSubgroupInClass ProC.finiteQuotientClass H :=
89 OpenNormalSubgroupInClass.mapOpenNormal_of_formation
90 (C := ProC.finiteQuotientClass) (G := sourceData.carrier)
91 ProC.finiteQuotientFormation psi hfopen hpsi V₀
92 let Q₀ : Type u := sourceData.carrier ⧸ (V₀.1 : Subgroup sourceData.carrier)
93 let K₀ : Type u := H ⧸ (W₀.1 : Subgroup H)
94 letI : Finite Q₀ := ProC.finiteQuotientFormation.finiteOnly V₀.2
95 letI : Finite K₀ := ProC.finiteQuotientFormation.finiteOnly W₀.2
96 letI : DiscreteTopology K₀ :=
97 QuotientGroup.discreteTopology W₀.1.toOpenSubgroup.isOpen'
98 let qH₀ : H →ₜ* K₀ :=
99 OpenNormalSubgroupInClass.quotientProj
100 (C := ProC.finiteQuotientClass) W₀
101 have hV₀W₀ :
102 (V₀.1 : Subgroup sourceData.carrier) ≤
103 (W₀.1 : Subgroup H).comap psi.toMonoidHom := by
104 intro g hg
105 change psi g ∈ (W₀.1 : Subgroup H)
106 change psi g ∈
107 ((OpenNormalSubgroup.map psi hfopen hpsi V₀.1 : OpenNormalSubgroup H) :
108 Subgroup H)
109 exact (Subgroup.mem_map).2 ⟨g, hg, rfl⟩
110 let α₀ : FreeGroup X →* Q₀ :=
111 (QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier)).comp
112 (FreeGroup.lift ι)
113 let β : Q₀ →* K₀ :=
114 QuotientGroup.map
115 (N := (V₀.1 : Subgroup sourceData.carrier))
116 (M := (W₀.1 : Subgroup H))
117 (f := psi.toMonoidHom) hV₀W₀
118 have hα₀_surj : Function.Surjective α₀ := by
119 simpa [α₀, X, ι] using
121 (ProC := ProC) sourceData hbasis V₀
122 have hβ_surj : Function.Surjective β := by
123 intro y
124 rcases QuotientGroup.mk'_surjective (W₀.1 : Subgroup H) y with ⟨h, rfl⟩
125 rcases hpsi h with ⟨g, rfl⟩
126 exact ⟨QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) g, rfl⟩
127 have hCker : ProC.finiteQuotientClass β.ker :=
128 ProC.finiteQuotientHereditary.subgroupClosed β.ker V₀.2
129 letI : Finite β.ker := ProC.finiteQuotientFormation.finiteOnly hCker
131 (C := ProC.finiteQuotientClass)
132 ProC.finiteQuotientFormation ProC.finiteQuotientHereditary hCker with
133 ⟨j, hpow⟩
134 let ψstage : FreeGroup X →* K₀ := β.comp α₀
135 let Nstage : Subgroup (FreeGroup X) := ψstage.ker
136 let Qstage : Type u := FoxDifferential.zcFiniteStageTarget X Nstage
137 letI : TopologicalSpace Qstage := ⊥
138 letI : DiscreteTopology Qstage := ⟨rfl⟩
139 letI : IsTopologicalGroup Qstage := inferInstance
140 have hψstage_surj : Function.Surjective ψstage := by
141 intro k
142 rcases hβ_surj k with ⟨q, rfl⟩
143 rcases hα₀_surj q with ⟨w, rfl⟩
144 exact ⟨w, rfl⟩
145 let e : Qstage ≃* K₀ :=
146 QuotientGroup.quotientKerEquivOfSurjective ψstage hψstage_surj
147 have hCstage : ProC.finiteQuotientClass Qstage :=
148 ProC.finiteQuotientIsomClosed ⟨e.symm⟩ W₀.2
149 let eSymm : K₀ →ₜ* Qstage :=
150 { toMonoidHom := e.symm.toMonoidHom
151 continuous_toFun := continuous_of_discreteTopology }
152 let η : H →ₜ* Qstage :=
153 eSymm.comp qH₀
154 have he_apply (w : FreeGroup X) :
155 e (QuotientGroup.mk' Nstage w) = ψstage w := by
156 change QuotientGroup.quotientKerEquivOfSurjective ψstage hψstage_surj
157 (QuotientGroup.mk' ψstage.ker w) = ψstage w
158 rfl
159 have hη :
160 (η : H →* Qstage).comp
161 ((psi : sourceData.carrier →* H).comp (FreeGroup.lift ι)) =
162 QuotientGroup.mk' Nstage := by
163 apply MonoidHom.ext
164 intro w
165 apply e.injective
166 change e (η (psi ((FreeGroup.lift ι) w))) =
167 e (QuotientGroup.mk' Nstage w)
168 rw [he_apply]
169 change e (e.symm (qH₀ (psi ((FreeGroup.lift ι) w)))) = β (α₀ w)
170 rw [e.apply_symm_apply]
171 change QuotientGroup.mk' (W₀.1 : Subgroup H) (psi ((FreeGroup.lift ι) w)) =
172 β (QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) ((FreeGroup.lift ι) w))
173 rw [QuotientGroup.map_mk']
174 rfl
176 ProC.finiteQuotientClass Qstage :=
178 ProC.finiteQuotientClass Qstage ProC.finiteQuotientIsomClosed hCstage)
180 (H := H) (ProC := ProC) ProC.finiteQuotientHereditary
181 sourceData hbasis psi htarget η J n.1 with
182 ⟨Vloc, hloc⟩
183 let Vfinal : OpenNormalSubgroupInClass ProC.finiteQuotientClass sourceData.carrier :=
184 OpenNormalSubgroupInClass.inf
185 (C := ProC.finiteQuotientClass) (G := sourceData.carrier)
186 ProC.finiteQuotientFormation V₀ Vloc
187 let αfinal : FreeGroup X →*
188 sourceData.carrier ⧸ (Vfinal.1 : Subgroup sourceData.carrier) :=
189 (QuotientGroup.mk' (Vfinal.1 : Subgroup sourceData.carrier)).comp
190 (FreeGroup.lift ι)
191 have hαfinal_surj : Function.Surjective αfinal := by
192 simpa [αfinal, X, ι] using
194 (ProC := ProC) sourceData hbasis Vfinal
195 rcases hαfinal_surj
196 (QuotientGroup.mk' (Vfinal.1 : Subgroup sourceData.carrier) n.1) with
197 ⟨w, hwfinal⟩
198 have hfinal_le_V₀ :
199 (Vfinal.1 : Subgroup sourceData.carrier) ≤ (V₀.1 : Subgroup sourceData.carrier) := by
200 intro g hg
201 change g ∈ ((V₀.1 ⊓ Vloc.1 : OpenNormalSubgroup sourceData.carrier) : Subgroup sourceData.carrier) at hg
202 exact hg.1
203 have hfinal_le_Vloc :
204 (Vfinal.1 : Subgroup sourceData.carrier) ≤ (Vloc.1 : Subgroup sourceData.carrier) := by
205 intro g hg
206 change g ∈ ((V₀.1 ⊓ Vloc.1 : OpenNormalSubgroup sourceData.carrier) : Subgroup sourceData.carrier) at hg
207 exact hg.2
208 have hα₀w :
209 α₀ w = QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) n.1 := by
210 let τ : sourceData.carrier ⧸ (Vfinal.1 : Subgroup sourceData.carrier) →*
211 sourceData.carrier ⧸ (V₀.1 : Subgroup sourceData.carrier) :=
212 QuotientGroup.map
213 (N := (Vfinal.1 : Subgroup sourceData.carrier))
214 (M := (V₀.1 : Subgroup sourceData.carrier))
215 (f := MonoidHom.id sourceData.carrier) hfinal_le_V₀
216 have hτ := congrArg τ hwfinal
217 simpa [τ, αfinal, α₀] using hτ
218 have hdiff_final :
219 ((FreeGroup.lift ι) w) * n.1⁻¹ ∈
220 (Vfinal.1 : Subgroup sourceData.carrier) := by
221 have hwq :
222 QuotientGroup.mk' (Vfinal.1 : Subgroup sourceData.carrier)
223 ((FreeGroup.lift ι) w) =
224 QuotientGroup.mk' (Vfinal.1 : Subgroup sourceData.carrier) n.1 := by
225 simpa [αfinal] using hwfinal
226 simpa [div_eq_mul_inv] using
227 (QuotientGroup.eq_iff_div_mem
228 (N := (Vfinal.1 : Subgroup sourceData.carrier))).1 hwq
229 have hdiff_loc :
230 ((FreeGroup.lift ι) w) * n.1⁻¹ ∈
231 (Vloc.1 : Subgroup sourceData.carrier) :=
232 hfinal_le_Vloc hdiff_final
233 have hproj_n :
234 (fun i : X =>
236 Qstage J
237 ((FoxDifferential.zcFreeFoxCoordinatesMap
238 (X := X) ProC.finiteQuotientClass ProC.finiteQuotientHereditary η
240 (H := H) (ProC := ProC) sourceData hbasis psi htarget n.1)) i)) = 0 := by
241 funext i
242 simp only [hnD, FoxDifferential.zcFreeFoxCoordinatesMap_apply, Pi.zero_apply, map_zero,
244 have hproj_w :
245 (fun i : X =>
247 Qstage J
248 ((FoxDifferential.zcFreeFoxCoordinatesMap
249 (X := X) ProC.finiteQuotientClass ProC.finiteQuotientHereditary η
251 (H := H) (ProC := ProC) sourceData hbasis psi htarget
252 ((FreeGroup.lift ι) w))) i)) = 0 := by
253 have heq := hloc ((FreeGroup.lift ι) w) hdiff_loc
254 exact (by
255 simpa [X, ι, J] using
256 heq.trans (by
257 simpa [X, ι, J] using hproj_n))
258 have hder :
260 (X := X) Nstage j.modulus w = 0 :=
262 (H := H) (ProC := ProC) ProC.finiteQuotientHereditary
263 ProC.finiteQuotientIsomClosed sourceData hbasis psi hpsi htarget
264 Nstage hCstage η hη j hproj_w
265 have hwker : w ∈ (β.comp α₀).ker := by
266 change β (α₀ w) = 1
267 rw [hα₀w]
268 change QuotientGroup.mk' (W₀.1 : Subgroup H) (psi n.1) = 1
269 exact (QuotientGroup.eq_one_iff
270 (N := (W₀.1 : Subgroup H)) (psi n.1)).2 (by
271 have hnpsi : psi n.1 = 1 := by
272 change psi n.1 = 1
273 exact n.2
274 rw [hnpsi]
275 exact (W₀.1 : Subgroup H).one_mem)
276 have hcommβ :
277 (⟨α₀ w, by
278 change β (α₀ w) = 1
279 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
280 commutator β.ker :=
282 (X := X) α₀ β j.modulus j.positive hpow hwker
283 (by simpa [Nstage, ψstage] using hder)
284 let κ : ProfiniteKernelSubgroup psi →* β.ker :=
285 { toFun := fun m =>
286 ⟨QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) m.1, by
287 change β (QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) m.1) = 1
288 change QuotientGroup.mk' (W₀.1 : Subgroup H) (psi m.1) = 1
289 exact (QuotientGroup.eq_one_iff
290 (N := (W₀.1 : Subgroup H)) (psi m.1)).2 (by
291 have hmpsi : psi m.1 = 1 := by
292 change psi m.1 = 1
293 exact m.2
294 rw [hmpsi]
295 exact (W₀.1 : Subgroup H).one_mem)⟩
296 map_one' := by
297 apply Subtype.ext
298 simp only [OneMemClass.coe_one, QuotientGroup.mk'_apply, QuotientGroup.mk_one]
299 map_mul' := by
300 intro a b
301 apply Subtype.ext
302 simp only [Subgroup.coe_mul, map_mul, QuotientGroup.mk'_apply, MulMemClass.mk_mul_mk]}
303 have hκ_surj : Function.Surjective κ := by
304 intro y
305 rcases QuotientGroup.mk'_surjective
306 (V₀.1 : Subgroup sourceData.carrier) y.1 with
307 ⟨g, hg⟩
308 have hψgW : psi g ∈ (W₀.1 : Subgroup H) := by
309 have hβg : β (QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) g) = 1 := by
310 have hyβ : β y.1 = 1 := by
311 change β y.1 = 1
312 exact y.2
313 simpa [hg] using hyβ
314 change QuotientGroup.mk' (W₀.1 : Subgroup H) (psi g) = 1 at hβg
315 exact (QuotientGroup.eq_one_iff
316 (N := (W₀.1 : Subgroup H)) (psi g)).1 hβg
317 have hψgWmap :
318 psi g ∈
319 ((OpenNormalSubgroup.map psi hfopen hpsi V₀.1 : OpenNormalSubgroup H) :
320 Subgroup H) := by
321 simpa [W₀] using hψgW
322 rcases (Subgroup.mem_map).1 hψgWmap with ⟨v, hvV₀, hvψ⟩
324 ⟨g * v⁻¹, by
325 change psi (g * v⁻¹) = 1
326 rw [map_mul, map_inv]
327 have hvψ' : psi v = psi g := hvψ
328 rw [hvψ', mul_inv_cancel]⟩
329 refine ⟨m, ?_⟩
330 apply Subtype.ext
331 change QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) (g * v⁻¹) = y.1
332 rw [← hg]
333 have hvq :
334 QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) v = 1 :=
335 (QuotientGroup.eq_one_iff
336 (N := (V₀.1 : Subgroup sourceData.carrier)) v).2 hvV₀
337 rw [map_mul, map_inv, hvq]
338 simp only [QuotientGroup.mk'_apply, inv_one, mul_one]
339 have hκkerU :
340 κ.ker ≤ (U.1 : Subgroup (ProfiniteKernelSubgroup psi)) := by
341 intro m hm
342 have hq : QuotientGroup.mk' (V₀.1 : Subgroup sourceData.carrier) m.1 = 1 := by
343 exact congrArg Subtype.val hm
344 exact hV₀U_sub m
345 ((QuotientGroup.eq_one_iff
346 (N := (V₀.1 : Subgroup sourceData.carrier)) m.1).1 hq)
347 have hκn_eq :
348 κ n =
349 (⟨α₀ w, by
350 change β (α₀ w) = 1
351 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) := by
352 apply Subtype.ext
353 exact hα₀w.symm
354 have hκn_comm : κ n ∈ commutator β.ker := by
355 simpa [hκn_eq] using hcommβ
356 have hquotU :
357 QuotientGroup.mk' (U.1 : Subgroup (ProfiniteKernelSubgroup psi)) n ∈
360 κ hκ_surj (U.1 : Subgroup (ProfiniteKernelSubgroup psi)) hκkerU hκn_comm
361 exact ⟨U, le_rfl, hquotU⟩
363end
365end CrowellExactSequence