Yamaguchi Lean 4 Library
ProCGroups/Completion/FiniteQuotientLifts.lean
ProCGroups/Completion/FiniteQuotientLifts/Source

ProCGroups/Completion/FiniteQuotientLifts.lean

1import ProCGroups.Completion.UniversalProperty
2import ProCGroups.ProC.GroupPredicates.Basic
3import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/Completion/FiniteQuotientLifts.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pro-C completion and finite quotient systems
16Organizes finite quotient systems, completion maps, finite-target factorization, and the universal property of pro-C completion.
17-/
19open scoped Topology
21namespace ProCGroups.Completion
23universe u
25/-- Unique lifting property against finite discrete `C`-quotients of the source. -/
27 (C : ProCGroups.FiniteGroupClass.{u})
28 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29 {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
30 (ι : G →ₜ* Ghat) : Prop :=
31 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
32 [Finite Q] [DiscreteTopology Q],
33 C Q →
34 ∀ φ : G →ₜ* Q,
35 ∃! φbar : Ghat →ₜ* Q, φbar.comp ι = φ
37/-- A compatible family of continuous homomorphisms to finite stages assembles to a continuous
38homomorphism to the inverse limit. -/
40 {I : Type u} [Preorder I]
42 [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
43 [∀ i, IsTopologicalGroup (S.X i)]
44 {A : Type u} [Group A] [TopologicalSpace A]
45 (φ : ∀ i, A →ₜ* S.X i)
46 (hcompat : S.CompatibleMaps (fun i => φ i)) :
47 A →ₜ* S.inverseLimit :=
48 { toMonoidHom :=
49 { toFun := S.inverseLimitLift (fun i => φ i) hcompat
50 map_one' := by
51 apply S.ext
52 intro i
53 calc
54 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat 1) = φ i 1 := by
55 simpa [Function.comp] using
56 congrFun (S.projection_comp_inverseLimitLift (fun i => φ i) hcompat i) (1 : A)
57 _ = 1 := by simp only [map_one]
58 map_mul' := by
59 intro x y
60 apply S.ext
61 intro i
62 calc
63 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat (x * y)) = φ i (x * y) := by
64 simpa [Function.comp] using
65 congrFun (S.projection_comp_inverseLimitLift (fun i => φ i) hcompat i) (x * y)
66 _ = φ i x * φ i y := by simp only [map_mul]
67 _ =
68 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat x) *
69 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat y) := by
70 have hx :
71 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat x) = φ i x := by
72 simpa [Function.comp] using
73 congrFun (S.projection_comp_inverseLimitLift (fun i => φ i) hcompat i) x
74 have hy :
75 S.projection i (S.inverseLimitLift (fun i => φ i) hcompat y) = φ i y := by
76 simpa [Function.comp] using
77 congrFun (S.projection_comp_inverseLimitLift (fun i => φ i) hcompat i) y
78 rw [← hx, ← hy] }
79 continuous_toFun := S.continuous_inverseLimitLift (fun i => φ i) (fun i => (φ i).continuous_toFun)
80 hcompat }
82/-- A dense map from a discrete group into a pro-`C` group is a pro-`C` completion as soon as
83every finite discrete `C`-quotient of the source lifts uniquely and continuously across it. -/
85 {C : ProCGroups.FiniteGroupClass.{u}}
87 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
88 [DiscreteTopology G]
89 {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
90 (hGhat : ProCGroups.ProC.IsProCGroup C Ghat)
91 {ι : G →ₜ* Ghat}
92 (hιdense : DenseRange ι)
93 (hfinite :
94 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
95 [Finite Q] [DiscreteTopology Q],
96 C Q →
97 ∀ φ : G →ₜ* Q,
98 ∃! φbar : Ghat →ₜ* Q, φbar.comp ι = φ) :
101 refine
102 { isProC := by simpa using hGhat
103 denseRange := hιdense
105 intro H _ _ _ hH ψ
106 let hHproC : ProCGroups.ProC.IsProCGroup C H := by
107 simpa using hH
110 ProCGroups.ProC.IsProCGroup.openNormalSubgroupInClass_nonempty hHproC
111 letI : Nonempty (OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H)) := inferInstance
112 letI :
114 Group (S.X U) := fun U => by
116 infer_instance
118 dsimp [S]
119 infer_instance
120 letI :
122 IsTopologicalGroup (S.X U) := fun U => by
124 infer_instance
125 letI :
127 Finite (S.X U) := fun U => by
129 exact hForm.finiteOnly (OrderDual.ofDual U).2
130 letI :
132 DiscreteTopology (S.X U) := fun U => by
134 exact QuotientGroup.discreteTopology
135 (openNormalSubgroup_isOpen (G := H) (OrderDual.ofDual U).1)
136 letI : CompactSpace H := ProCGroups.ProC.IsProCGroup.compactSpace hHproC
137 letI : T2Space H := ProCGroups.ProC.IsProCGroup.t2Space hHproC
138 letI :
140 T2Space (S.X U) := fun _ => by infer_instance
141 letI : Group S.inverseLimit := by infer_instance
142 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
143 let q :
144 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H), H →ₜ* S.X U := fun U =>
145 { toMonoidHom := ProCGroups.ProC.openNormalSubgroupInClassProj (C := C) (G := H) U
146 continuous_toFun := continuous_quotient_mk' }
147 let qFun :
148 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H), H → S.X U := fun U => q U
149 have hqCompat : S.CompatibleMaps qFun := by
150 simpa [q, qFun, S] using
152 let ψcoord :
153 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H), Ghat →ₜ* S.X U := fun U =>
154 Classical.choose (hfinite (OrderDual.ofDual U).2 ((q U).comp ψ))
155 let ψcoordFun :
156 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H), Ghat → S.X U := fun U =>
157 ψcoord U
158 have hψcoordSpec :
160 (ψcoord U).comp ι = (q U).comp ψ := by
161 intro U
162 exact (Classical.choose_spec (hfinite (OrderDual.ofDual U).2 ((q U).comp ψ))).1
163 have hψcoordUnique :
165 (φbar : Ghat →ₜ* S.X U),
166 φbar.comp ι = (q U).comp ψ →
167 φbar = ψcoord U := by
168 intro U φbar hφbar
169 exact (Classical.choose_spec (hfinite (OrderDual.ofDual U).2 ((q U).comp ψ))).2 φbar hφbar
170 have hψcoordCompat : S.CompatibleMaps ψcoordFun := by
171 intro U V hUV
172 have hUV' : ((OrderDual.ofDual V).1 : Subgroup H) ≤ (OrderDual.ofDual U).1 := hUV
173 let qUV : S.X V →ₜ* S.X U :=
174 { toMonoidHom := by
177 (C := C) (G := H) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV'
178 continuous_toFun := S.continuous_map hUV }
179 have hEqHom : qUV.comp (ψcoord V) = ψcoord U := by
180 exact hψcoordUnique U (qUV.comp (ψcoord V)) <| by
181 apply ContinuousMonoidHom.toMonoidHom_injective
182 ext g
183 have hqg :
184 qUV ((q V) (ψ g)) = (q U) (ψ g) := by
185 simpa [q, S] using
186 congrFun
188 (ψ g)
189 calc
190 ((qUV.comp (ψcoord V)).comp ι) g = qUV (ψcoord V (ι g)) := rfl
191 _ = qUV ((q V) (ψ g)) := by
192 exact congrArg qUV (congrArg (fun f : G →ₜ* S.X V => f g) (hψcoordSpec V))
193 _ = (q U) (ψ g) := hqg
194 _ = ((q U).comp ψ) g := rfl
195 funext x
196 exact congrArg (fun f : Ghat →ₜ* S.X U => f x) hEqHom
197 let ψInv : Ghat →ₜ* S.inverseLimit :=
199 let eH : H ≃ₜ* S.inverseLimit :=
201 (C := C) (G := H) hForm hHproC
202 have hπeH :
203 ∀ (U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C H)) (h : H),
204 S.projection U (eH h) = (q U) h := by
205 intro U h
207 using congrFun (S.projection_comp_inverseLimitLift qFun hqCompat U) h
208 let ψbar : Ghat →ₜ* H :=
209 { toMonoidHom := eH.symm.toMonoidHom.comp ψInv.toMonoidHom
210 continuous_toFun := eH.symm.continuous_toFun.comp ψInv.continuous_toFun }
211 have hψbarComp : eH.toMonoidHom.comp ψbar.toMonoidHom = ψInv.toMonoidHom := by
212 apply MonoidHom.ext
213 intro x
214 apply S.ext
215 intro U
216 exact congrArg (fun z : S.inverseLimit => S.projection U z) (eH.apply_symm_apply (ψInv x))
217 have hψbarFac : ψbar.comp ι = ψ := by
218 apply ContinuousMonoidHom.toMonoidHom_injective
219 ext g
220 apply eH.injective
221 apply S.ext
222 intro U
223 calc
224 S.projection U (eH (ψbar (ι g))) = S.projection U (ψInv (ι g)) := by
225 exact congrArg (fun z : S.inverseLimit => S.projection U z)
226 (congrArg (fun f : Ghat →* S.inverseLimit => f (ι g)) hψbarComp)
227 _ = ψcoord U (ι g) := by
228 simpa [ψcoordFun, Function.comp] using
229 congrFun (S.projection_comp_inverseLimitLift ψcoordFun hψcoordCompat U) (ι g)
230 _ = (q U) (ψ g) := by
231 exact congrArg (fun f : G →ₜ* S.X U => f g) (hψcoordSpec U)
232 _ = S.projection U (eH (ψ g)) := by
233 symm
234 exact hπeH U (ψ g)
235 refine ⟨ψbar, hψbarFac, ?_⟩
236 intro χ hχ
237 apply ContinuousMonoidHom.toMonoidHom_injective
238 apply MonoidHom.ext
239 intro x
240 have hEqFun : (fun z : Ghat => χ z) = fun z : Ghat => ψbar z := by
241 apply DenseRange.equalizer (f := ι) hιdense
242 · exact χ.continuous_toFun
243 · exact ψbar.continuous_toFun
244 · funext g
245 exact congrArg (fun f : G →ₜ* H => f g) (hχ.trans hψbarFac.symm)
246 exact congrArg (fun f : Ghat → H => f x) hEqFun
248/-- Finite discrete quotient lifts extend uniquely to any pro-`C` target. -/
250 {C : ProCGroups.FiniteGroupClass.{u}}
252 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
253 [DiscreteTopology G]
254 {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
255 (hGhat : ProCGroups.ProC.IsProCGroup C Ghat)
256 {ι : G →ₜ* Ghat}
257 (hιdense : DenseRange ι)
258 (hfinite :
259 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
260 [Finite Q] [DiscreteTopology Q],
261 C Q →
262 ∀ φ : G →ₜ* Q,
263 ∃! φbar : Ghat →ₜ* Q, φbar.comp ι = φ)
264 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
266 (ψ : G →ₜ* H) :
267 ∃! ψbar : Ghat →ₜ* H, ψbar.comp ι = ψ :=
269 (C := C) hForm hGhat hιdense hfinite).existsUnique_lift hH ψ
271/-- Name exposing the exact strength of the finite discrete quotient lifting hypothesis. -/
273 {C : ProCGroups.FiniteGroupClass.{u}}
275 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
276 [DiscreteTopology G]
277 {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
278 (hGhat : ProCGroups.ProC.IsProCGroup C Ghat)
279 {ι : G →ₜ* Ghat}
280 (hιdense : DenseRange ι)
281 (hfinite : HasUniqueFiniteDiscreteQuotientLifts C (G := G) (Ghat := Ghat) ι) :
285 (C := C) hForm hGhat hιdense hfinite
287end ProCGroups.Completion