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

1import ProCGroups.FreeProC.FiniteBasis

2import ProCGroups.FoxDifferential.Completed.Continuous.Free.Continuity

3import ProCGroups.FoxDifferential.Completed.Continuous.TopologicalGeneration

5/-!

6# Fox Differential / Completed / Continuous Magnus / Closed Generated Vector

8This module bundles the completed Fox derivative vector as a scalar crossed

9homomorphism, first over pro-\(C\) integers and then over the presented

10coefficient ring. It also records the closed-generation and Magnus-reduction

11identities used by the completed Magnus injectivity argument.

12-/

14namespace CrowellExactSequence

16noncomputable section

18open ProCGroups.ProC

19open FoxDifferential

21universe u

23variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

24variable {C : ProCGroups.FiniteGroupClass.{u}}

26variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]

28section ProfiniteTarget

30variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

32/--

33The closed-generated continuous Fox derivative vector attached to a finite chosen free

34pro-\(C\) basis and a presentation map.

35-/

36def freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

37 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

38 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)

39 (psi : ContinuousMonoidHom sourceData.carrier H)

40 (htarget :

41 ProCGroups.ProC.HasOpenNormalBasisInClass C

42 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

43 (C := C)

44 (fun i : ULift.{u} (Fin r) =>

45 psi (freeProCChosenULiftFamilyOfBasisCard

46 (C := C) sourceData hbasis i)) : Subgroup

47 (FoxDifferential.ZCCompletedFoxSemidirect

48 C (ULift.{u} (Fin r)) H))) :

49 FoxDifferential.ScalarCrossedHom

50 (FoxDifferential.zcCompletedGroupAlgebraScalar C

51 (FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated

52 (C := C)

53 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)

54 (fun i : ULift.{u} (Fin r) =>

55 psi (freeProCChosenULiftFamilyOfBasisCard

56 (C := C) sourceData hbasis i))

57 htarget

58 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite

59 (C := C)

60 (fun i : ULift.{u} (Fin r) =>

61 psi (freeProCChosenULiftFamilyOfBasisCard

62 (C := C) sourceData hbasis i)))))

63 (FoxDifferential.ZCFreeFoxCoordinates

64 C (X := ULift.{u} (Fin r)) (H := H)) :=

65 let hfree :=

66 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis

67 let φ : ULift.{u} (Fin r) → H := fun i =>

68 psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i)

69 let hφconv :

70 ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups

71 (G :=

72 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

73 (C := C) φ : Subgroup

74 (FoxDifferential.ZCCompletedFoxSemidirect

75 C (ULift.{u} (Fin r)) H)))

76 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator

77 (C := C) φ) :=

78 FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite

79 (C := C) φ

80 FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated

81 (C := C) hfree φ htarget hφconv

83end ProfiniteTarget

85omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in

86/--

87An abstract kernel word for the chosen finite free basis gives a genuine cycle point in the

88closed-generated Fox graph target. This is the algebraic source of the completed cycle-lifting

89step: before passing to closures, every relation word \(w\) with target value \(1\) contributes

90\((D w, 1)\) to the closed-generated graph.

91-/

92theorem freeProC_closedGeneratedTarget_mem_of_freeGroupFoxDerivativeVector_kernel

93 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

94 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)

95 (psi : ContinuousMonoidHom sourceData.carrier H)

96 {w : FreeGroup (ULift.{u} (Fin r))}

97 (hw :

98 FreeGroup.lift

99 (fun i : ULift.{u} (Fin r) =>

100 psi (freeProCChosenULiftFamilyOfBasisCard

101 (C := C) sourceData hbasis i)) w = 1) :

102 ({ left :=

103 FoxDifferential.zcFreeGroupFoxDerivativeVector C

104 (FreeGroup.lift

105 (fun i : ULift.{u} (Fin r) =>

106 psi (freeProCChosenULiftFamilyOfBasisCard

107 (C := C) sourceData hbasis i))) w,

108 right := (1 : H) } :

109 FoxDifferential.ZCCompletedFoxSemidirect C

110 (ULift.{u} (Fin r)) H) ∈

111 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

112 (C := C)

113 (fun i : ULift.{u} (Fin r) =>

114 psi (freeProCChosenULiftFamilyOfBasisCard

115 (C := C) sourceData hbasis i)) : Subgroup

116 (FoxDifferential.ZCCompletedFoxSemidirect C

117 (ULift.{u} (Fin r)) H)) := by

118 exact

119 FoxDifferential.freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel

120 (C := C)

121 (fun i : ULift.{u} (Fin r) =>

122 psi (freeProCChosenULiftFamilyOfBasisCard

123 (C := C) sourceData hbasis i))

124 hw

125

126section ProfiniteTarget

127

128variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

129

130omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in

131/--

132The right component of the closed-generated Fox graph attached to the chosen lifted finite

133basis is the original presentation map; the two continuous homomorphisms agree on every chosen

134free generator.

135-/

136theorem freeProCCompletedFoxRightHomViaClosedGeneratedProCInteger_eq

137 (hForm : ProCGroups.FiniteGroupClass.Formation C)

138 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

139 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)

140 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)

141 (htarget :

142 ProCGroups.ProC.HasOpenNormalBasisInClass C

143 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

144 (C := C)

145 (fun i : ULift.{u} (Fin r) =>

146 psi (freeProCChosenULiftFamilyOfBasisCard

147 (C := C) sourceData hbasis i)) : Subgroup

148 (FoxDifferential.ZCCompletedFoxSemidirect

149 C (ULift.{u} (Fin r)) H))) :

150 FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated

151 (C := C)

152 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)

153 (fun i : ULift.{u} (Fin r) =>

154 psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))

155 htarget

156 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite

157 (C := C)

158 (fun i : ULift.{u} (Fin r) =>

159 psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))) =

160 psi.toMonoidHom := by

161 let X : Type u := ULift.{u} (Fin r)

162 let ι : X → sourceData.carrier :=

163 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis

164 let hfree := freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis

165 let φ : X → H := fun i => psi (ι i)

166 let hφconv :

167 ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups

168 (G :=

169 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

170 (C := C) φ : Subgroup

171 (FoxDifferential.ZCCompletedFoxSemidirect C X H)))

172 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator

173 (C := C) φ) :=

174 FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite

175 (C := C) φ

176 have hH : ProCGroups.ProC.HasOpenNormalBasisInClass C H :=

177 ProCGroups.ProC.HasOpenNormalBasisInClass.of_surjective

178 hForm sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi

179 have hφHconv : ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups (G := H) φ := by

180 simpa [φ, ι] using

181 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups

182 (C := C) sourceData hbasis psi.toMonoidHom

183 have hφHgen :

184 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by

185 simpa [φ, ι] using

186 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective

187 (C := C) sourceData hbasis psi hpsi

188 simpa [X, ι, hfree, φ, hφconv] using

189 FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom

190 (C := C) X H hfree hH φ htarget hφconv hφHconv hφHgen psi

191 (by intro i; rfl)

192

193omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in

194/-- The closed-generated continuous Fox derivative vector, bundled with the

195original presentation map as its coefficient homomorphism. -/

196def freeProCCompletedFoxDerivativeVectorForPresentation

197 (hForm : ProCGroups.FiniteGroupClass.Formation C)

198 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

199 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)

200 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)

201 (htarget :

202 ProCGroups.ProC.HasOpenNormalBasisInClass C

203 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

204 (C := C)

205 (fun i : ULift.{u} (Fin r) =>

206 psi (freeProCChosenULiftFamilyOfBasisCard

207 (C := C) sourceData hbasis i)) : Subgroup

208 (FoxDifferential.ZCCompletedFoxSemidirect

209 C (ULift.{u} (Fin r)) H))) :

210 FoxDifferential.ScalarCrossedHom

211 (FoxDifferential.zcCompletedGroupAlgebraScalar

212 C psi.toMonoidHom)

213 (FoxDifferential.ZCFreeFoxCoordinates

214 C (X := ULift.{u} (Fin r)) (H := H)) where

215 toFun :=

216 freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

217 (H := H) (C := C) sourceData hbasis psi htarget

218 map_mul' := by

219 intro g h

220 let X : Type u := ULift.{u} (Fin r)

221 let ι : X → sourceData.carrier :=

222 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis

223 let hfree :=

224 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree

225 (C := C) sourceData hbasis

226 let φ : X → H := fun i => psi (ι i)

227 let hφconv :

228 ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups

229 (G :=

230 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

231 (C := C) φ : Subgroup

232 (FoxDifferential.ZCCompletedFoxSemidirect C X H)))

233 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator

234 (C := C) φ) :=

235 FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite

236 (C := C) φ

237 have hright :

238 FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated

239 (C := C) hfree φ htarget hφconv =

240 psi.toMonoidHom := by

241 simpa [X, ι, hfree, φ, hφconv] using

242 freeProCCompletedFoxRightHomViaClosedGeneratedProCInteger_eq

243 (H := H) (C := C) hForm sourceData hbasis psi hpsi htarget

244 have hD :=

245 (FoxDifferential.freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated

246 (C := C) hfree φ htarget hφconv).map_mul g h

247 rw [← hright]

248 exact hD

249

250omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in

251/-- The closed-generated continuous Fox derivative vector is continuous. -/

252theorem continuous_freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

253 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

254 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)

255 (psi : ContinuousMonoidHom sourceData.carrier H)

256 (htarget :

257 ProCGroups.ProC.HasOpenNormalBasisInClass C

258 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

259 (C := C)

260 (fun i : ULift.{u} (Fin r) =>

261 psi (freeProCChosenULiftFamilyOfBasisCard

262 (C := C) sourceData hbasis i)) : Subgroup

263 (FoxDifferential.ZCCompletedFoxSemidirect

264 C (ULift.{u} (Fin r)) H))) :

265 Continuous

266 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

267 (H := H) (C := C) sourceData hbasis psi htarget) := by

268 let hfree :=

269 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis

270 let φ : ULift.{u} (Fin r) → H := fun i =>

271 psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i)

272 let hφconv :

273 ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups

274 (G :=

275 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

276 (C := C) φ : Subgroup

277 (FoxDifferential.ZCCompletedFoxSemidirect

278 C (ULift.{u} (Fin r)) H)))

279 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator

280 (C := C) φ) :=

281 FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite

282 (C := C) φ

283 simpa [freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, hfree, φ, hφconv] using

284 FoxDifferential.continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated

285 (C := C) (ULift.{u} (Fin r)) H hfree φ htarget hφconv

286

287omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in

288/--

289Universal completed Magnus-kernel reduction for the closed-generated continuous Fox vector.

290After this reduction, the remaining paper statement is exactly the concrete continuous Magnus

291kernel for the completed Fox derivative vector.

292-/

293theorem freeProC_zcUnivDiff_kernel_le_closedCommutator_of_closedGenFoxVector

294 (hForm : ProCGroups.FiniteGroupClass.Formation C)

295 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)

296 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)

297 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)

298 (htarget :

299 ProCGroups.ProC.HasOpenNormalBasisInClass C

300 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

301 (C := C)

302 (fun i : ULift.{u} (Fin r) =>

303 psi (freeProCChosenULiftFamilyOfBasisCard

304 (C := C) sourceData hbasis i)) : Subgroup

305 (FoxDifferential.ZCCompletedFoxSemidirect

306 C (ULift.{u} (Fin r)) H)))

307 (hDker :

308 ∀ n : ProfiniteKernelSubgroup psi,

309 freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

310 (H := H) (C := C) sourceData hbasis psi htarget n.1 = 0 →

311 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :

312 ∀ n : ProfiniteKernelSubgroup psi,

313 FoxDifferential.zcUniversalDifferential

314 C psi.toMonoidHom n.1 = 0 →

315 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi) := by

316 exact

317 FoxDifferential.zcUniversalDifferential_kernel_le_closedCommutator_of_crossedDifferential

318 C psi

319 (freeProCCompletedFoxDerivativeVectorForPresentation

320 (H := H) (C := C) hForm sourceData hbasis psi hpsi htarget)

321 hDker

322

323end ProfiniteTarget

324

325end

326

327end CrowellExactSequence