Source: ProCGroups.Completion.FiniteQuotientLifts
1import ProCGroups.Completion.UniversalProperty
2import ProCGroups.ProC.InverseLimits.Predicates
3import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
5/-!
6# Pro C Groups / Completion / Finite Quotient Lifts
8This module proves that unique lifting against finite discrete \(C\)-quotients,
9together with density, implies the full pro-\(C\) completion universal property.
10-/
12open scoped Topology
14namespace ProCGroups.Completion
16universe u
18/--
19A compatible family of continuous homomorphisms to finite stages assembles to a continuous
20homomorphism to the inverse limit.
21-/
22noncomputable def lift_to_inverseLimit_of_compatible_finite_lifts
23 {I : Type u} [Preorder I]
24 (S : ProCGroups.InverseSystems.InverseSystem (I := I))
25 [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
26 {A : Type u} [Group A] [TopologicalSpace A]
27 (φ : ∀ i, A →ₜ* S.X i)
28 (hcompat : S.CompatibleMaps (fun i => φ i)) :
29 A →ₜ* S.inverseLimit :=
30 { toMonoidHom :=
31 { toFun := S.inverseLimitLift (fun i => φ i) hcompat
32 map_one' := by
33 apply S.ext
34 intro i
35 calc
36 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat 1) = φ i 1 := by
37 simpa [Function.comp] using
38 congrFun (S.projection_comp_inverseLimitLift (fun i => φ i) hcompat i) (1 : A)
39 _ = 1 := by simp only [map_one]
40 map_mul' := by
41 intro x y
42 apply S.ext
43 intro i
44 calc
45 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat (x * y)) = φ i (x * y) := by
46 simpa [Function.comp] using
47 congrFun (S.projection_comp_inverseLimitLift (fun i => φ i) hcompat i) (x * y)
48 _ = φ i x * φ i y := by simp only [map_mul]
49 _ =
50 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat x) *
51 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat y) := by
52 have hx :
53 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat x) = φ i x := by
54 simpa [Function.comp] using
55 congrFun (S.projection_comp_inverseLimitLift (fun i => φ i) hcompat i) x
56 have hy :
57 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat y) = φ i y := by
58 simpa [Function.comp] using
59 congrFun (S.projection_comp_inverseLimitLift (fun i => φ i) hcompat i) y
60 rw [← hx, ← hy] }
61 continuous_toFun := S.continuous_inverseLimitLift (fun i => φ i) (fun i => (φ
62 i).continuous_toFun)
63 hcompat }
65/--
66A dense map from a discrete group into a pro-\(C\) group is a pro-\(C\) completion as soon as
67every finite discrete \(C\)-quotient of the source lifts uniquely and continuously across it.
68-/
69theorem isProCCompletion_of_finiteQuotientLifts
70 {C : ProCGroups.FiniteGroupClass.{u}}
71 (hForm : ProCGroups.FiniteGroupClass.Formation C)
72 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
73 {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
74 [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
75 (hGhat : ProCGroups.ProC.HasOpenNormalBasisInClass C (Ghat))
76 {ι : G →ₜ* Ghat}
77 (hιdense : DenseRange ι)
78 (hfinite :
79 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
80 [Finite Q] [DiscreteTopology Q],
81 C Q →
82 ∀ φ : G →ₜ* Q,
83 ∃! φbar : Ghat →ₜ* Q, φbar.comp ι = φ) :
84 IsProCCompletion
85 (C) G Ghat ι := by
86 refine
87 { hasOpenNormalBasisInClass := by simpa using hGhat
88 denseRange := hιdense
89 existsUnique_lift := ?_ }
90 intro H _ _ _ _ _ _ hH ψ
91 let hHproC : ProCGroups.ProC.HasOpenNormalBasisInClass C H := hH
92 let S := ProCGroups.ProC.openNormalSubgroupInClassSystem C H
93 letI : Nonempty (ProCGroups.ProC.OpenNormalSubgroupInClass C H) :=
95 letI : Nonempty (OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H)) := inferInstance
96 letI :
97 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H),
98 DiscreteTopology
99 (H ⧸ ((OrderDual.ofDual U).1 : Subgroup H)) := fun U =>
100 QuotientGroup.discreteTopology
101 (openNormalSubgroup_isOpen (G := H) (OrderDual.ofDual U).1)
102 letI :
103 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H),
104 IsTopologicalGroup
105 (H ⧸ ((OrderDual.ofDual U).1 : Subgroup H)) := fun _ =>
106 topologicalGroup_of_discreteTopology
107 letI :
108 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H),
109 Group (S.X U) := fun U =>
111 (C := C) (G := H) U
112 letI : ProCGroups.InverseSystems.IsGroupSystem S := by
113 dsimp [S]
114 infer_instance
115 letI :
116 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H),
117 DiscreteTopology (S.X U) := fun U => by
119 exact QuotientGroup.discreteTopology
120 (openNormalSubgroup_isOpen (G := H) (OrderDual.ofDual U).1)
121 letI :
122 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H),
123 IsTopologicalGroup (S.X U) := fun _ => by
124 exact topologicalGroup_of_discreteTopology
125 letI :
126 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H),
127 Finite (S.X U) := fun U => by
129 exact C.finite (OrderDual.ofDual U).2
130 letI :
131 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H),
132 T2Space (S.X U) := fun _ => by infer_instance
133 letI : Group S.inverseLimit := by infer_instance
134 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
135 have hStageClass :
136 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H),
137 C (S.X U) := fun U => by
139 exact (OrderDual.ofDual U).2
140 let q :
141 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H), H →ₜ* S.X U := fun U =>
142 { toMonoidHom := ProCGroups.ProC.openNormalSubgroupInClassProj (C := C) (G := H) U
143 continuous_toFun := continuous_quotient_mk' }
144 let qFun :
145 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H), H → S.X U := fun U => q U
146 have hqCompat : S.CompatibleMaps qFun := by
147 intro U V hUV
148 funext h
149 have hc :=
150 congrFun
152 (C := C) (G := H) U V hUV) h
153 change S.map hUV (q V h) = q U h
154 change S.map hUV (q V h) = q U h at hc
155 exact hc
156 let ψcoord :
157 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H), Ghat →ₜ* S.X U := fun U =>
158 Classical.choose (hfinite (hStageClass U) ((q U).comp ψ))
159 let ψcoordFun :
160 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H), Ghat → S.X U := fun U =>
161 ψcoord U
162 have hψcoordSpec :
163 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H),
164 (ψcoord U).comp ι = (q U).comp ψ := by
165 intro U
166 exact (Classical.choose_spec (hfinite (hStageClass U) ((q U).comp ψ))).1
167 have hψcoordUnique :
168 ∀ (U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H))
169 (φbar : Ghat →ₜ* S.X U),
170 φbar.comp ι = (q U).comp ψ →
171 φbar = ψcoord U := by
172 intro U φbar hφbar
173 exact (Classical.choose_spec (hfinite (hStageClass U) ((q U).comp ψ))).2 φbar hφbar
174 have hψcoordCompat : S.CompatibleMaps ψcoordFun := by
175 intro U V hUV
176 have hUV' : ((OrderDual.ofDual V).1 : Subgroup H) ≤ (OrderDual.ofDual U).1 := hUV
177 let qUV : S.X V →ₜ* S.X U :=
178 { toMonoidHom := by
181 (C := C) (G := H) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV'
182 continuous_toFun := S.continuous_map hUV }
183 have hEqHom : qUV.comp (ψcoord V) = ψcoord U := by
184 exact hψcoordUnique U (qUV.comp (ψcoord V)) <| by
185 apply ContinuousMonoidHom.toMonoidHom_injective
186 ext g
187 have hqg :
188 qUV ((q V) (ψ g)) = (q U) (ψ g) := by
189 have hc :=
190 congrFun
192 (C := C) (G := H) U V hUV)
193 (ψ g)
194 change
195 S.map hUV
197 (C := C) (G := H) V (ψ g)) =
199 (C := C) (G := H) U (ψ g) at hc
200 change
201 S.map hUV
203 (C := C) (G := H) V (ψ g)) =
205 (C := C) (G := H) U (ψ g)
206 exact hc
207 calc
208 ((qUV.comp (ψcoord V)).comp ι) g = qUV (ψcoord V (ι g)) := rfl
209 _ = qUV ((q V) (ψ g)) := by
210 exact congrArg qUV (congrArg (fun f : G →ₜ* S.X V => f g) (hψcoordSpec V))
211 _ = (q U) (ψ g) := hqg
212 _ = ((q U).comp ψ) g := rfl
213 funext x
214 exact congrArg (fun f : Ghat →ₜ* S.X U => f x) hEqHom
215 let ψInv : Ghat →ₜ* S.inverseLimit :=
216 lift_to_inverseLimit_of_compatible_finite_lifts S ψcoord hψcoordCompat
217 let eH : H ≃ₜ* S.inverseLimit :=
219 (C := C) (G := H) hForm hHproC
220 have hπeH :
221 ∀ (U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H)) (h : H),
222 S.projection U (eH h) = (q U) h := by
223 intro U h
224 have hproj :=
225 S.projection_inverseLimitLift_apply qFun hqCompat U h
226 change S.projection U (eH h) = q U h at hproj
227 exact hproj
228 let ψbar : Ghat →ₜ* H :=
229 { toMonoidHom := eH.symm.toMonoidHom.comp ψInv.toMonoidHom
230 continuous_toFun := eH.symm.continuous_toFun.comp ψInv.continuous_toFun }
231 have hψbarComp : eH.toMonoidHom.comp ψbar.toMonoidHom = ψInv.toMonoidHom := by
232 apply MonoidHom.ext
233 intro x
234 apply S.ext
235 intro U
236 exact congrArg (fun z : S.inverseLimit => S.projection U z) (eH.apply_symm_apply (ψInv x))
237 have hψbarFac : ψbar.comp ι = ψ := by
238 apply ContinuousMonoidHom.toMonoidHom_injective
239 ext g
240 apply eH.injective
241 apply S.ext
242 intro U
243 calc
244 S.projection U (eH (ψbar (ι g))) = S.projection U (ψInv (ι g)) := by
245 exact congrArg (fun z : S.inverseLimit => S.projection U z)
246 (congrArg (fun f : Ghat →* S.inverseLimit => f (ι g)) hψbarComp)
247 _ = ψcoord U (ι g) := by
248 have hproj :=
249 S.projection_inverseLimitLift_apply ψcoordFun hψcoordCompat U (ι g)
250 change S.projection U (ψInv (ι g)) = ψcoord U (ι g) at hproj
251 exact hproj
252 _ = (q U) (ψ g) := by
253 exact congrArg (fun f : G →ₜ* S.X U => f g) (hψcoordSpec U)
254 _ = S.projection U (eH (ψ g)) := by
255 symm
256 exact hπeH U (ψ g)
257 refine ⟨ψbar, hψbarFac, ?_⟩
258 intro χ hχ
259 apply ContinuousMonoidHom.toMonoidHom_injective
260 apply MonoidHom.ext
261 intro x
262 have hEqFun : (fun z : Ghat => χ z) = fun z : Ghat => ψbar z := by
263 apply DenseRange.equalizer (f := ι) hιdense
264 · exact χ.continuous_toFun
265 · exact ψbar.continuous_toFun
266 · funext g
267 exact congrArg (fun f : G →ₜ* H => f g) (hχ.trans hψbarFac.symm)
268 exact congrArg (fun f : Ghat → H => f x) hEqFun
270end ProCGroups.Completion