Source: ProCGroups.CrowellExactSequence.Applications.FiniteRank
1import ProCGroups.CrowellExactSequence.Profinite.BlanchfieldLyndon
2import ProCGroups.FreeProC.FiniteRankSourceData
3import ProCGroups.FiniteStepSolvableQuotients.Abelianization
4import ProCGroups.ProC.InverseLimits.Predicates
6/-!
7# `ProCGroups.CrowellExactSequence.Applications.FiniteRank`
9Crowell exact sequences / Applications / Finite Rank.
11This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed
12coordinate forms.
13-/
15open scoped Topology
17namespace CrowellExactSequence
19open ProCGroups.Abelian
20open ProCGroups.FiniteStepSolvableQuotients
22universe u
24variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
25variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
27/--
28The separated coordinate map for the topological abelianization of a finite-rank free
29pro-\(\Sigma\) group.
30-/
31noncomputable def finiteRank_topologicalAbelianization_sepCoordinateMap
32 {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
34 (C := (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
35 (Fin r) F X) := by
36 letI :
38 (ProCGroups.FiniteGroupClass.sigmaGroup sigma) :=
39 (ProCGroups.FiniteGroupClass.sigmaGroup_fullFormation sigma).containsTrivialQuotients
40 letI : TotallyDisconnectedSpace (TopologicalAbelianization F) :=
43 exact
44 freeProCChosenULift_sepCoordinateMap
45 (H := TopologicalAbelianization F)
46 (C := ProCGroups.FiniteGroupClass.sigmaGroup sigma)
48 (finiteRank_epimorphicallyFreeProCSourceData (F := F) X hFree)
49 (finiteRank_epimorphicallyFreeProCSourceData_basis_card (F := F) X hFree)
50 (TopologicalAbelianization.mkₜ F)
51 (by
52 change Function.Surjective (TopologicalAbelianization.mk F)
53 exact TopologicalAbelianization.surjective_mk F)
55/--
56If the separated abelianized Crowell exact-sequence coordinate vector of a kernel element
57vanishes, the element lies in the second closed derived subgroup.
58-/
59theorem mem_topDerivedTop_two_of_finiteRank_topologicalAbelianization_sepCoordinateMap_eq_zero
60 {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
62 (C := (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
63 (Fin r) F X)
64 {a : F}
65 (haψ : TopologicalAbelianization.mkₜ F a = 1)
66 (hzero :
67 finiteRank_topologicalAbelianization_sepCoordinateMap (F := F) X hFree
70 (TopologicalAbelianization.mkₜ F).toMonoidHom a) = 0) :
71 a ∈ topDerivedTop F 2 := by
72 letI :
74 (ProCGroups.FiniteGroupClass.sigmaGroup sigma) :=
75 (ProCGroups.FiniteGroupClass.sigmaGroup_fullFormation sigma).containsTrivialQuotients
76 letI : TotallyDisconnectedSpace (TopologicalAbelianization F) :=
79 let sourceData := finiteRank_epimorphicallyFreeProCSourceData (F := F) (sigma := sigma) X hFree
80 let hbasis := finiteRank_epimorphicallyFreeProCSourceData_basis_card (F := F) X hFree
81 let C := ProCGroups.FiniteGroupClass.sigmaGroup sigma
82 let ψ : F →ₜ* TopologicalAbelianization F := TopologicalAbelianization.mkₜ F
83 have hψsurj : Function.Surjective ψ := by
84 change Function.Surjective (TopologicalAbelianization.mk F)
85 exact TopologicalAbelianization.surjective_mk F
86 let htarget :=
87 freeProCClosedGeneratedTarget_proC_of_surjective
88 (H := TopologicalAbelianization F) (C := C)
90 sourceData hbasis ψ hψsurj
91 have hDzero :
92 freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
93 (H := TopologicalAbelianization F) (C := C) sourceData hbasis ψ htarget a = 0 := by
94 have happly := hzero
95 dsimp [finiteRank_topologicalAbelianization_sepCoordinateMap, sourceData, hbasis,
96 C, ψ] at happly
97 change
98 freeProCChosenULift_sepCoordinateMap
99 (H := TopologicalAbelianization F) (C := C)
101 sourceData hbasis ψ hψsurj
103 ψ.toMonoidHom a) = 0 at happly
104 have hcoord :=
105 freeProCChosenULift_sepCoordinateMap_universal
106 (H := TopologicalAbelianization F) (C := C)
107 (hC := ProCGroups.FiniteGroupClass.sigmaGroup_fullFormation sigma)
108 sourceData hbasis ψ hψsurj a
109 have hraw := hcoord.symm.trans happly
110 simpa [finiteRank_topologicalAbelianization_sepCoordinateMap, sourceData, hbasis, C, ψ,
111 freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, htarget] using hraw
112 have ha_closed :
113 (⟨a, haψ⟩ : ProCGroups.ProC.ProfiniteKernelSubgroup ψ) ∈
115 freeProC_closedGeneratedFoxVector_kernel_le_closedCommutator
116 (H := TopologicalAbelianization F) (C := C)
118 sourceData hbasis ψ hψsurj htarget
119 ⟨a, haψ⟩ hDzero
120 exact
121 (mem_topDerivedTop_two_iff_mem_closedCommutator_topologicalAbelianizationKernel
122 (G := F) haψ).2 ha_closed
124end CrowellExactSequence