Source: CrowellExactSequence/Profinite/ContinuousMagnus/FiniteStageKernel.lean

1import CrowellExactSequence.Profinite.ContinuousMagnus.ClosedGeneratedVector

2import FoxDifferential.Completed.Comparison.FiniteStage

3import FoxDifferential.Completed.Continuous.Naturality

4

5/-

6PUBLIC_PAGE_SNAPSHOT

7generated_at: 2026-05-27T09:47:29+09:00

8lean_source: lean4/CrowellExactSequence/Profinite/ContinuousMagnus/FiniteStageKernel.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

15

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

19

20noncomputable section

21

22open ProCGroups.ProC

23

24universe u

25

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

27variable {ProC : ProCGroupPredicate.{u}}

28

29variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass]

30

31omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in

32/-- Free-group comparison for the concrete closed-generated continuous Fox vector, with the

33right component already identified with the presentation map. -/

34theorem freeFoxDerivVec_eq_freeProCClosedGenFoxVectorZC_comp_lift_mapTarget

35 [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]

36 (hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)

37 (sourceData : FreeProCSourceData ProC)

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

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

40 (htarget :

41 ProC

42 (G :=

43 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

44 (ProC := ProC)

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

46 psi (freeProCChosenULiftFamilyOfBasisCard

47 (ProC := ProC) sourceData hbasis i)) : Subgroup

48 (FoxDifferential.ZCCompletedFoxSemidirect

49 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))

50 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]

51 (η : H →ₜ* K) (w : FreeGroup (ULift.{u} (Fin r))) :

52 FoxDifferential.zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

53 (η.toMonoidHom.comp

54 (psi.toMonoidHom.comp

55 (FreeGroup.lift

56 (freeProCChosenULiftFamilyOfBasisCard

57 (ProC := ProC) sourceData hbasis)))) w =

58 FoxDifferential.zcFreeFoxCoordinatesMap

59 (X := ULift.{u} (Fin r)) ProC.finiteQuotientClass hC η

60 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

61 (H := H) (ProC := ProC) sourceData hbasis psi htarget

62 ((FreeGroup.lift

63 (freeProCChosenULiftFamilyOfBasisCard

64 (ProC := ProC) sourceData hbasis)) w)) := by

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

66 let ι : X → sourceData.carrier :=

67 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis

68 let hfree := freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis

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

70 let hφconv :

71 ProCGroups.FreeProC.FamilyConvergesToOne

72 (G :=

73 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

74 (ProC := ProC) φ : Subgroup

75 (FoxDifferential.ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))

76 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator

77 (ProC := ProC) φ) :=

78 FoxDifferential.freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite

79 (ProC := ProC) φ

80 have hH : ProC (G := H) :=

81 (ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC

82 have hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ := by

83 simpa [φ, ι] using

84 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne

85 (ProC := ProC) sourceData hbasis psi.toMonoidHom

86 have hφHgen :

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

88 simpa [φ, ι] using

89 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective

90 (ProC := ProC) sourceData hbasis psi hpsi

91 have hright :

92 FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated

93 (ProC := ProC) hfree φ htarget hφconv =

94 psi.toMonoidHom := by

95 have hright_lift :=

96 FoxDifferential.freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift

97 (ProC := ProC) X H hfree hH φ htarget hφconv hφHconv hφHgen

98 have hliftHom :=

99 freeProCChosenULiftFamilyOfBasisCard_liftHom_eq_of_surjective

100 (ProC := ProC) sourceData hbasis hH psi hpsi

101 have hlift :

102 hfree.lift hH φ hφHconv hφHgen = psi.toMonoidHom := by

103 simpa [hfree, φ, ι] using congrArg ContinuousMonoidHom.toMonoidHom hliftHom

104 exact hright_lift.trans hlift

105 have hcomp :=

106 FoxDifferential.zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift_mapTarget

107 (ProC := ProC) hfree φ htarget hφconv hC η w

108 simpa [freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, X, ι, hfree, φ,

109 hφconv, hright] using hcomp

110

111omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in

112/-- A finite projection of the concrete closed-generated continuous Fox vector gives zero of the

113corresponding finite Fox derivative vector for a free-group representative. -/

114theorem finiteFoxStageDerivativeVector_eq_zero_of_closedGenFoxVector_proj_eq_zero

115 [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]

116 (hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)

117 (hIso : ProCGroups.FiniteGroupClass.IsomClosed ProC.finiteQuotientClass)

118 (sourceData : FreeProCSourceData ProC)

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

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

121 (htarget :

122 ProC

123 (G :=

124 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

125 (ProC := ProC)

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

127 psi (freeProCChosenULiftFamilyOfBasisCard

128 (ProC := ProC) sourceData hbasis i)) : Subgroup

129 (FoxDifferential.ZCCompletedFoxSemidirect

130 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))

131 (N : Subgroup (FreeGroup (ULift.{u} (Fin r)))) [N.Normal]

132 [TopologicalSpace (FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N)]

133 [IsTopologicalGroup (FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N)]

134 [DiscreteTopology (FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N)]

135 (hCN : ProC.finiteQuotientClass

136 (FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N))

137 (η : H →ₜ* FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N)

138 (hη :

139 (η : H →* FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N).comp

140 ((psi : sourceData.carrier →* H).comp

141 (FreeGroup.lift

142 (freeProCChosenULiftFamilyOfBasisCard

143 (ProC := ProC) sourceData hbasis))) =

144 QuotientGroup.mk' N)

145 (j : ProCGroups.Completion.ProCIntegerIndex ProC.finiteQuotientClass)

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

147 (hproj :

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

149 FoxDifferential.zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass

150 (FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N)

151 (j, FoxDifferential.identityCompletedGroupAlgebraIndexInClassOfMem

152 ProC.finiteQuotientClass

153 (FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N)

154 hIso hCN)

155 ((FoxDifferential.zcFreeFoxCoordinatesMap

156 (X := ULift.{u} (Fin r)) ProC.finiteQuotientClass hC η

157 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

158 (H := H) (ProC := ProC) sourceData hbasis psi htarget

159 ((FreeGroup.lift

160 (freeProCChosenULiftFamilyOfBasisCard

161 (ProC := ProC) sourceData hbasis)) w))) i)) = 0) :

162 FoxDifferential.finiteFoxStageDerivativeVector

163 (X := ULift.{u} (Fin r)) N j.modulus w = 0 := by

164 have hcompare :=

165 freeFoxDerivVec_eq_freeProCClosedGenFoxVectorZC_comp_lift_mapTarget

166 (H := H) (ProC := ProC) hC sourceData hbasis psi hpsi htarget η w

167 have hcompare' :

168 FoxDifferential.zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

169 (QuotientGroup.mk' N) w =

170 FoxDifferential.zcFreeFoxCoordinatesMap

171 (X := ULift.{u} (Fin r)) ProC.finiteQuotientClass hC η

172 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

173 (H := H) (ProC := ProC) sourceData hbasis psi htarget

174 ((FreeGroup.lift

175 (freeProCChosenULiftFamilyOfBasisCard

176 (ProC := ProC) sourceData hbasis)) w)) := by

177 simpa [hη] using hcompare

178 have hproj' :

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

180 FoxDifferential.zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass

181 (FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N)

182 (j, FoxDifferential.identityCompletedGroupAlgebraIndexInClassOfMem

183 ProC.finiteQuotientClass

184 (FoxDifferential.zcFiniteStageTarget (ULift.{u} (Fin r)) N)

185 hIso hCN)

186 (FoxDifferential.zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass

187 (QuotientGroup.mk' N) w i)) = 0 := by

188 simpa [hcompare'] using hproj

189 exact

190 FoxDifferential.finiteFoxStageDerivativeVector_eq_zero_of_zcFreeFoxDerivVec_identityProj_eq_zero

191 (C := ProC.finiteQuotientClass) (X := ULift.{u} (Fin r)) N hIso hCN j hproj'

192

193omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in

194/-- Local constancy of a finite target/coefficent projection of the concrete closed-generated

195continuous Fox vector. -/

196theorem exists_openNormalSubgroupInClass_eq_on_right_coset_closedGenFoxVector_proj

197 [ProC.HasFiniteQuotientFinite]

198 (hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)

199 (sourceData : FreeProCSourceData ProC)

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

201 (psi : ContinuousMonoidHom sourceData.carrier H)

202 (htarget :

203 ProC

204 (G :=

205 (FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget

206 (ProC := ProC)

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

208 psi (freeProCChosenULiftFamilyOfBasisCard

209 (ProC := ProC) sourceData hbasis i)) : Subgroup

210 (FoxDifferential.ZCCompletedFoxSemidirect

211 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))

212 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]

213 (η : H →ₜ* K)

214 (j : FoxDifferential.ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass K)

215 (g₀ : sourceData.carrier) :

216 ∃ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass sourceData.carrier,

217 ∀ g : sourceData.carrier,

218 g * g₀⁻¹ ∈ (U.1 : Subgroup sourceData.carrier) →

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

220 FoxDifferential.zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass K j

221 ((FoxDifferential.zcFreeFoxCoordinatesMap

222 (X := ULift.{u} (Fin r)) ProC.finiteQuotientClass hC η

223 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

224 (H := H) (ProC := ProC) sourceData hbasis psi htarget g)) i)) =

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

226 FoxDifferential.zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass K j

227 ((FoxDifferential.zcFreeFoxCoordinatesMap

228 (X := ULift.{u} (Fin r)) ProC.finiteQuotientClass hC η

229 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

230 (H := H) (ProC := ProC) sourceData hbasis psi htarget g₀)) i)) := by

231 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=

232 ⟨by

233 intro Q _ hQ

234 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩

235 let f : sourceData.carrier →

236 (ULift.{u} (Fin r) →

237 FoxDifferential.ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass K j) :=

238 fun g i =>

239 FoxDifferential.zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass K j

240 ((FoxDifferential.zcFreeFoxCoordinatesMap

241 (X := ULift.{u} (Fin r)) ProC.finiteQuotientClass hC η

242 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

243 (H := H) (ProC := ProC) sourceData hbasis psi htarget g)) i)

244 have hf : Continuous f := by

245 have hD :

246 Continuous

247 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

248 (H := H) (ProC := ProC) sourceData hbasis psi htarget) :=

249 continuous_freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

250 (H := H) (ProC := ProC) sourceData hbasis psi htarget

251 have hmap :

252 Continuous (fun g : sourceData.carrier =>

253 FoxDifferential.zcFreeFoxCoordinatesMap

254 (X := ULift.{u} (Fin r)) ProC.finiteQuotientClass hC η

255 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

256 (H := H) (ProC := ProC) sourceData hbasis psi htarget g)) :=

257 (FoxDifferential.continuous_zcFreeFoxCoordinatesMap

258 ProC.finiteQuotientClass hC η).comp hD

259 refine continuous_pi fun i => ?_

260 change Continuous (fun g : sourceData.carrier =>

261 ((FoxDifferential.zcFreeFoxCoordinatesMap

262 (X := ULift.{u} (Fin r)) ProC.finiteQuotientClass hC η

263 (freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger

264 (H := H) (ProC := ProC) sourceData hbasis psi htarget g)) i).1 j)

265 exact (continuous_apply j).comp

266 (continuous_subtype_val.comp ((continuous_apply i).comp hmap))

267 have hdisc :

268 DiscreteTopology

269 (ULift.{u} (Fin r) →

270 FoxDifferential.ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass K j) := by

271 infer_instance

272 letI :

273 DiscreteTopology

274 (ULift.{u} (Fin r) →

275 FoxDifferential.ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass K j) := hdisc

276 simpa [f] using

277 ProCGroups.ProC.IsProCGroup.exists_openNormalSubgroupInClass_eq_on_right_coset_of_continuous_discrete

278 (C := ProC.finiteQuotientClass) sourceData.proCGroup.isProCGroup f hf g₀

279

280omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in

281/-- The chosen lifted finite free basis surjects onto every finite open-normal quotient of the

282free pro-`C` source. -/

283theorem freeProCChosenULiftFamilyOfBasisCard_quotient_lift_surjective

284 (sourceData : FreeProCSourceData ProC)

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

286 (V : OpenNormalSubgroupInClass ProC.finiteQuotientClass sourceData.carrier) :

287 Function.Surjective

288 ((QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier)).comp

289 (FreeGroup.lift

290 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis))) := by

291 classical

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

293 let ι : X → sourceData.carrier :=

294 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis

295 let Q : Type u := sourceData.carrier ⧸ (V.1 : Subgroup sourceData.carrier)

296 letI : DiscreteTopology Q :=

297 QuotientGroup.discreteTopology V.1.toOpenSubgroup.isOpen'

298 let g : X → Q :=

299 fun i => QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier) (ι i)

300 have hsource :

301 ProCGroups.Generation.TopologicallyGenerates

302 (G := sourceData.carrier) (Set.range ι) := by

303 simpa [X, ι] using

304 freeProCChosenULiftFamilyOfBasisCard_generates (ProC := ProC) sourceData hbasis

305 have hquot_image :

306 ProCGroups.Generation.TopologicallyGenerates

307 (G := Q)

308 ((QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier)) '' Set.range ι) :=

309 ProCGroups.Generation.topologicallyGenerates_quotient_image

310 (G := sourceData.carrier) (N := (V.1 : Subgroup sourceData.carrier)) hsource

311 have hrange :

312 (QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier)) '' Set.range ι =

313 Set.range g := by

314 ext y

315 constructor

316 · rintro ⟨x, ⟨i, rfl⟩, rfl⟩

317 exact ⟨i, rfl⟩

318 · rintro ⟨i, rfl⟩

319 exact ⟨ι i, ⟨i, rfl⟩, rfl⟩

320 have hg :

321 ProCGroups.Generation.TopologicallyGenerates (G := Q) (Set.range g) := by

322 rw [← hrange]

323 exact hquot_image

324 have hsurj :

325 Function.Surjective (FreeGroup.lift g) :=

326 ProCGroups.FiniteGeneration.freeGroup_lift_surjective_of_topologicallyGenerates_discrete

327 (G := Q) g hg

328 have hlift :

329 FreeGroup.lift g =

330 (QuotientGroup.mk' (V.1 : Subgroup sourceData.carrier)).comp

331 (FreeGroup.lift ι) := by

332 apply FreeGroup.ext_hom

333 intro i

334 rw [FreeGroup.lift_apply_of, MonoidHom.comp_apply, FreeGroup.lift_apply_of]

335 simpa [hlift, X, ι] using hsurj

336

337end

338

339end CrowellExactSequence