CrowellExactSequence/Profinite/ContinuousMagnus/ClosedGeneratedVector.lean
1import CrowellExactSequence.Profinite.FreeProCSourceData
2import FoxDifferential.Completed.Continuous.Free.Continuity
3import FoxDifferential.Completed.Continuous.TopologicalGeneration
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/CrowellExactSequence/Profinite/ContinuousMagnus/ClosedGeneratedVector.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Continuous Magnus criterion over pro-C integer coefficients
16This file is internal to the proof that the displayed
17`d_N : N^ab(C) -> A_psi(C)` is injective. Its conclusions are stated back in terms of the
18completed Fox differential on the genuine kernel, not as a second exact sequence.
19-/
21namespace CrowellExactSequence
23noncomputable section
25open ProCGroups.ProC
27universe u
29variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30variable {ProC : ProCGroupPredicate.{u}}
32variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass]
34/-- The closed-generated continuous Fox derivative vector attached to a finite chosen free
35pro-`C` basis and a presentation map. -/
37 (sourceData : FreeProCSourceData ProC)
38 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
39 (psi : ContinuousMonoidHom sourceData.carrier H)
40 (htarget :
41 ProC
42 (G :=
44 (ProC := ProC)
45 (fun i : ULift.{u} (Fin r) =>
47 (ProC := ProC) sourceData hbasis i)) : Subgroup
49 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))) :
50 sourceData.carrier →
52 ProC.finiteQuotientClass (X := ULift.{u} (Fin r)) (H := H) :=
53 let hfree :=
54 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
55 let φ : ULift.{u} (Fin r) → H := fun i =>
56 psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)
57 let hφconv :
58 ProCGroups.FreeProC.FamilyConvergesToOne
59 (G :=
61 (ProC := ProC) φ : Subgroup
63 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))
65 (ProC := ProC) φ) :=
67 (ProC := ProC) φ
69 (ProC := ProC) hfree φ htarget hφconv
71omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
72/-- An abstract kernel word for the chosen finite free basis gives a genuine cycle point in the
73closed-generated Fox graph target. This is the algebraic source of the completed cycle-lifting
74step: before passing to closures, every relation word `w` with target value `1` contributes
75`(D w, 1)` to the closed-generated graph. -/
77 (sourceData : FreeProCSourceData ProC)
78 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
79 (psi : ContinuousMonoidHom sourceData.carrier H)
80 {w : FreeGroup (ULift.{u} (Fin r))}
81 (hw :
82 FreeGroup.lift
83 (fun i : ULift.{u} (Fin r) =>
85 (ProC := ProC) sourceData hbasis i)) w = 1) :
86 ({ left :=
87 FoxDifferential.zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
88 (FreeGroup.lift
89 (fun i : ULift.{u} (Fin r) =>
91 (ProC := ProC) sourceData hbasis i))) w,
92 right := (1 : H) } :
93 FoxDifferential.ZCCompletedFoxSemidirect ProC.finiteQuotientClass
94 (ULift.{u} (Fin r)) H) ∈
96 (ProC := ProC)
97 (fun i : ULift.{u} (Fin r) =>
99 (ProC := ProC) sourceData hbasis i)) : Subgroup
100 (FoxDifferential.ZCCompletedFoxSemidirect ProC.finiteQuotientClass
101 (ULift.{u} (Fin r)) H)) := by
102 exact
104 (ProC := ProC)
105 (fun i : ULift.{u} (Fin r) =>
107 (ProC := ProC) sourceData hbasis i))
108 hw
110omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
111/-- The right component of the closed-generated Fox graph attached to the chosen lifted finite
112basis is the original presentation map.
114This is the target-coordinate half of the paper graph identity. It is independent of the left
115Fox-coordinate calculation: the right component and `psi` are continuous homomorphisms from the
116same free pro-`C` group, and they agree on the chosen free generators. -/
118 [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
119 (sourceData : FreeProCSourceData ProC)
120 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
121 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
122 (htarget :
123 ProC
124 (G :=
126 (ProC := ProC)
127 (fun i : ULift.{u} (Fin r) =>
129 (ProC := ProC) sourceData hbasis i)) : Subgroup
131 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))) :
133 (ProC := ProC)
134 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
135 (fun i : ULift.{u} (Fin r) =>
136 psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))
137 htarget
139 (ProC := ProC)
140 (fun i : ULift.{u} (Fin r) =>
141 psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))) =
142 psi.toMonoidHom := by
143 let X : Type u := ULift.{u} (Fin r)
144 let ι : X → sourceData.carrier :=
145 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
146 let hfree := freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
147 let φ : X → H := fun i => psi (ι i)
148 let hφconv :
149 ProCGroups.FreeProC.FamilyConvergesToOne
150 (G :=
152 (ProC := ProC) φ : Subgroup
153 (FoxDifferential.ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
155 (ProC := ProC) φ) :=
157 (ProC := ProC) φ
158 have hH : ProC (G := H) :=
160 have hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ := by
161 simpa [φ, ι] using
163 (ProC := ProC) sourceData hbasis psi.toMonoidHom
164 have hφHgen :
165 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
166 simpa [φ, ι] using
168 (ProC := ProC) sourceData hbasis psi hpsi
169 simpa [X, ι, hfree, φ, hφconv] using
171 (ProC := ProC) X H hfree hH φ htarget hφconv hφHconv hφHgen psi
172 (by intro i; rfl)
174omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
175/-- The closed-generated continuous Fox derivative vector is a crossed differential with respect
176to the original presentation map, once the presentation is surjective. -/
178 [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
179 (sourceData : FreeProCSourceData ProC)
180 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
181 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
182 (htarget :
183 ProC
184 (G :=
186 (ProC := ProC)
187 (fun i : ULift.{u} (Fin r) =>
189 (ProC := ProC) sourceData hbasis i)) : Subgroup
191 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))) :
193 (FoxDifferential.zcCompletedGroupAlgebraScalar
194 ProC.finiteQuotientClass psi.toMonoidHom)
196 (H := H) (ProC := ProC) sourceData hbasis psi htarget) := by
197 let X : Type u := ULift.{u} (Fin r)
198 let ι : X → sourceData.carrier :=
199 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
200 let hfree := freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
201 let φ : X → H := fun i => psi (ι i)
202 let hφconv :
203 ProCGroups.FreeProC.FamilyConvergesToOne
204 (G :=
206 (ProC := ProC) φ : Subgroup
207 (FoxDifferential.ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
209 (ProC := ProC) φ) :=
211 (ProC := ProC) φ
212 have hH : ProC (G := H) :=
214 have hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ := by
215 simpa [φ, ι] using
217 (ProC := ProC) sourceData hbasis psi.toMonoidHom
218 have hφHgen :
219 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
220 simpa [φ, ι] using
222 (ProC := ProC) sourceData hbasis psi hpsi
223 have hright :
225 (ProC := ProC) hfree φ htarget hφconv =
226 psi.toMonoidHom := by
227 simpa [X, ι, hfree, φ, hφconv] using
229 (H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget
230 have hD :=
232 (ProC := ProC) hfree φ htarget hφconv
233 simpa [freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, X, ι, φ,
234 hfree, hφconv, hright] using hD
236omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
237/-- The closed-generated continuous Fox derivative vector is continuous. -/
239 (sourceData : FreeProCSourceData ProC)
240 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
241 (psi : ContinuousMonoidHom sourceData.carrier H)
242 (htarget :
243 ProC
244 (G :=
246 (ProC := ProC)
247 (fun i : ULift.{u} (Fin r) =>
249 (ProC := ProC) sourceData hbasis i)) : Subgroup
251 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))) :
252 Continuous
254 (H := H) (ProC := ProC) sourceData hbasis psi htarget) := by
255 let hfree :=
256 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
257 let φ : ULift.{u} (Fin r) → H := fun i =>
258 psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)
259 let hφconv :
260 ProCGroups.FreeProC.FamilyConvergesToOne
261 (G :=
263 (ProC := ProC) φ : Subgroup
265 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))
267 (ProC := ProC) φ) :=
269 (ProC := ProC) φ
270 simpa [freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, hfree, φ, hφconv] using
272 (ProC := ProC) (ULift.{u} (Fin r)) H hfree φ htarget hφconv
274omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
275/-- Universal completed Magnus-kernel reduction for the closed-generated continuous Fox vector.
277After this theorem, the remaining paper statement is exactly the concrete continuous Magnus
278kernel for the completed Fox derivative vector. -/
280 [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
281 (sourceData : FreeProCSourceData ProC)
282 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
283 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
284 (htarget :
285 ProC
286 (G :=
288 (ProC := ProC)
289 (fun i : ULift.{u} (Fin r) =>
291 (ProC := ProC) sourceData hbasis i)) : Subgroup
293 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))
294 (hDker :
295 ∀ n : ProfiniteKernelSubgroup psi,
297 (H := H) (ProC := ProC) sourceData hbasis psi htarget n.1 = 0 →
298 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
299 ∀ n : ProfiniteKernelSubgroup psi,
300 FoxDifferential.zcUniversalDifferential
301 ProC.finiteQuotientClass psi.toMonoidHom n.1 = 0 →
302 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi) := by
303 exact
304 FoxDifferential.zcUniversalDifferential_kernel_le_closedCommutator_of_crossedDifferential
305 ProC.finiteQuotientClass psi
307 (H := H) (ProC := ProC) sourceData hbasis psi htarget)
309 (H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget)
310 hDker
312end
314end CrowellExactSequence