CrowellExactSequence/Profinite/FiniteRank.lean
1import CrowellExactSequence.Profinite.BlanchfieldLyndon
2import ProCGroups.FiniteStepSolvableQuotients.Abelianization
3import ProCGroups.ProC.GroupPredicates.Standard
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/CrowellExactSequence/Profinite/FiniteRank.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Finite-rank pro-Sigma bridges for the profinite Crowell exact sequence
16This file packages finite-rank free pro-`Σ` groups as `FreeProCSourceData` and exposes the
17abelianization-kernel corollary used by center-freeness applications.
18-/
20open scoped Topology
22namespace CrowellExactSequence
24open ProCGroups.Abelian
25open ProCGroups.FiniteStepSolvableQuotients
27universe u
29variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
31/-- Package a finite-rank free pro-`Σ` group as CES free-source data. -/
32noncomputable def finiteRank_freeProCSourceData
33 {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
34 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
36 (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
37 (Fin r) F X) :
38 FreeProCSourceData (ProCGroups.ProC.proSigmaProC.{u} sigma) where
39 basis := ULift.{u} (Fin r)
40 carrier := F
42 instTopologicalSpace := inferInstance
43 instIsTopologicalGroup := inferInstance
44 inclusion := fun i => X i.down
45 isFree := by
46 simpa [ProCGroups.ProC.proSigmaProC] using
47 hFree.precompEquiv (Equiv.ulift : ULift.{u} (Fin r) ≃ Fin r)
48 proCGroup := by
49 refine
51 simpa [ProCGroups.ProC.proSigmaProC] using hFree.isProC
52 isProCGroup := ?_ }
53 exact hFree.isProC.mono (D :=
54 (ProCGroups.ProC.proSigmaProC.{u} sigma).finiteQuotientClass) (by
55 intro Q _ hQ
56 letI : Finite Q := ProCGroups.FiniteGroupClass.finite hQ
58 (sigma := sigma) (Q := Q)).2 hQ)
60/-- The finite-rank CES source data has the expected basis cardinality. -/
62 {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
63 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
65 (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
66 (Fin r) F X) :
67 Cardinal.mk (finiteRank_freeProCSourceData (F := F) X hFree).basis = r := by
68 simp only [finiteRank_freeProCSourceData, Cardinal.mk_fintype, Fintype.card_ulift,
69 Fintype.card_fin]
71/-- The separated coordinate map for the topological abelianization of a finite-rank free
72pro-`Σ` group. -/
73noncomputable def finiteRank_topologicalAbelianization_sepCoordinateMap
74 {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
75 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
77 (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
78 (Fin r) F X) :=
80 (H := TopologicalAbelianization F)
81 (ProC := ProCGroups.ProC.proSigmaProC.{u} sigma)
82 (finiteRank_freeProCSourceData (F := F) X hFree)
83 (finiteRank_freeProCSourceData_basis_card (F := F) X hFree)
84 (TopologicalAbelianization.mkₜ F)
85 (by
86 change Function.Surjective (TopologicalAbelianization.mk F)
87 exact TopologicalAbelianization.surjective_mk F)
89/-- If the separated abelianized CES coordinate vector of a kernel element vanishes, the element
90lies in the second closed derived subgroup. -/
92 {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
93 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
95 (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
96 (Fin r) F X)
97 {a : F}
98 (haψ : TopologicalAbelianization.mkₜ F a = 1)
99 (hzero :
100 finiteRank_topologicalAbelianization_sepCoordinateMap (F := F) X hFree
102 (ProCGroups.ProC.proSigmaProC.{u} sigma).finiteQuotientClass
103 (TopologicalAbelianization.mkₜ F).toMonoidHom a) = 0) :
104 a ∈ topDerivedTop F 2 := by
105 let sourceData := finiteRank_freeProCSourceData (F := F) (sigma := sigma) X hFree
106 let hbasis := finiteRank_freeProCSourceData_basis_card (F := F) X hFree
107 let ProC := ProCGroups.ProC.proSigmaProC.{u} sigma
108 let ψ : F →ₜ* TopologicalAbelianization F := TopologicalAbelianization.mkₜ F
109 have hψsurj : Function.Surjective ψ := by
110 change Function.Surjective (TopologicalAbelianization.mk F)
111 exact TopologicalAbelianization.surjective_mk F
112 let htarget :=
114 (H := TopologicalAbelianization F) (ProC := ProC) sourceData hbasis ψ hψsurj
115 have hDzero :
117 (H := TopologicalAbelianization F) (ProC := ProC) sourceData hbasis ψ htarget a = 0 := by
118 have happly := hzero
119 dsimp [finiteRank_topologicalAbelianization_sepCoordinateMap, sourceData, hbasis, ProC, ψ] at happly
120 change
122 (H := TopologicalAbelianization F) (ProC := ProC) sourceData hbasis ψ hψsurj
123 (FoxDifferential.zcSeparatedUniversalDifferential ProC.finiteQuotientClass
124 ψ.toMonoidHom a) = 0 at happly
125 rw [freeProCChosenULift_sepCoordinateMap_universal] at happly
126 simpa [finiteRank_topologicalAbelianization_sepCoordinateMap, sourceData, hbasis, ProC, ψ,
127 freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, htarget] using happly
128 have ha_closed :
129 (⟨a, haψ⟩ : ProCGroups.ProC.ProfiniteKernelSubgroup ψ) ∈
132 (H := TopologicalAbelianization F) (ProC := ProC) sourceData hbasis ψ hψsurj htarget
133 ⟨a, haψ⟩ hDzero
134 exact
136 (G := F) haψ).2 ha_closed
138end CrowellExactSequence