Source: ProCGroups.Completion.UniversalProperty
1import ProCGroups.ProC.InverseLimits.Predicates
3/-!
4# Pro C Groups / Completion / Universal Property
6This module defines the universal property of a pro-\(C\) completion and proves
7the resulting lift, uniqueness, comparison, and canonical-equivalence results.
8-/
10open scoped Topology
12namespace ProCGroups.Completion
14universe u v
16variable {C : ProCGroups.FiniteGroupClass}
18/-- An abstract pro-\(C\) completion of a topological group. -/
19structure IsProCCompletion
21 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
22 (Ghat : Type u) [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
23 [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
24 (ι : G →ₜ* Ghat) : Prop where
25 /--
26 Open normal subgroups with quotients in `C` form a neighborhood basis at one in the completed
27 group.
28 -/
29 hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C Ghat
30 /-- The image of the original group under the completion map is dense in `Ghat`. -/
31 denseRange : DenseRange ι
32 /--
33 Every continuous homomorphism from `G` to a pro-`C` target extends uniquely to a continuous
34 homomorphism from `Ghat`.
35 -/
36 existsUnique_lift :
37 ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
38 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H],
40 ∀ (φ : G →ₜ* H), ∃! φbar : Ghat →ₜ* H, φbar.comp ι = φ
42namespace IsProCCompletion
44variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
45variable {Ghat : Type u} [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
46variable [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
47variable {ι : G →ₜ* Ghat}
49/--
50A continuous homomorphism from the source group to a pro-\(C\) target factors uniquely through
51the pro-\(C\) completion.
52-/
53noncomputable def lift
54 (hι : IsProCCompletion C G Ghat ι)
55 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
56 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
57 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H)) (φ : G →ₜ* H) :
58 Ghat →ₜ* H :=
59 Classical.choose (ExistsUnique.exists (hι.existsUnique_lift hH φ))
61/--
62The universal-property lift is continuous and extends the given homomorphism along the
63completion map.
64-/
65theorem lift_spec
66 (hι : IsProCCompletion C G Ghat ι)
67 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
68 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
69 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H)) (φ : G →ₜ* H) :
70 (hι.lift hH φ).comp ι = φ :=
71 Classical.choose_spec (ExistsUnique.exists (hι.existsUnique_lift hH φ))
73/-- The universal-property lift is the unique continuous map extending the given homomorphism. -/
74theorem lift_unique
75 (hι : IsProCCompletion C G Ghat ι)
76 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
77 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
78 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H)) (φ : G →ₜ* H)
79 {f : Ghat →ₜ* H} (hfac : f.comp ι = φ) :
80 f = hι.lift hH φ :=
81 (hι.existsUnique_lift hH φ).unique hfac (hι.lift_spec hH φ)
83/--
84Continuous homomorphisms out of a pro-\(C\) completion are determined by their composites with
85the dense source map.
86-/
87theorem hom_ext
88 (hι : IsProCCompletion C G Ghat ι)
89 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
90 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
91 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
92 {f g : Ghat →ₜ* H}
93 (hfg : f.comp ι = g.comp ι) :
94 f = g :=
95 (hι.existsUnique_lift hH (f.comp ι)).unique rfl hfg.symm
97/-- The lift of the completion map to the completion itself is the identity. -/
98@[simp] theorem lift_self_eq_id
99 (hι : IsProCCompletion C G Ghat ι) :
100 hι.lift hι.hasOpenNormalBasisInClass ι = ContinuousMonoidHom.id Ghat := by
101 symm
102 exact hι.lift_unique hι.hasOpenNormalBasisInClass ι rfl
104variable {Ghat₂ : Type u} [Group Ghat₂] [TopologicalSpace Ghat₂] [IsTopologicalGroup Ghat₂]
105variable [CompactSpace Ghat₂] [T2Space Ghat₂] [TotallyDisconnectedSpace Ghat₂]
106variable {ι₂ : G →ₜ* Ghat₂}
108/-- The canonical comparison map between two pro-\(C\) completions of the same group. -/
109noncomputable def comparison
110 (h₁ : IsProCCompletion C G Ghat ι)
111 (h₂ : IsProCCompletion C G Ghat₂ ι₂) : Ghat →ₜ* Ghat₂ :=
112 h₁.lift h₂.hasOpenNormalBasisInClass ι₂
114/--
115The comparison map between two pro-\(C\) completions agrees with the second completion map on
116the source.
117-/
118theorem comparison_spec
119 (h₁ : IsProCCompletion C G Ghat ι)
120 (h₂ : IsProCCompletion C G Ghat₂ ι₂) :
121 (h₁.comparison h₂).comp ι = ι₂ :=
122 h₁.lift_spec h₂.hasOpenNormalBasisInClass ι₂
124/-- The two comparison maps between pro-\(C\) completions compose to the identity. -/
125@[simp 900] theorem comparison_comp_eq_id
126 (h₁ : IsProCCompletion C G Ghat ι)
127 (h₂ : IsProCCompletion C G Ghat₂ ι₂) :
128 (h₂.comparison h₁).comp (h₁.comparison h₂) = ContinuousMonoidHom.id Ghat := by
129 let e12 : Ghat →ₜ* Ghat₂ := h₁.comparison h₂
130 let e21 : Ghat₂ →ₜ* Ghat := h₂.comparison h₁
131 have he12 : e12.comp ι = ι₂ := h₁.comparison_spec h₂
132 have he21 : e21.comp ι₂ = ι := h₂.comparison_spec h₁
133 have hfac : (e21.comp e12).comp ι = ι := by
134 ext x
135 have h12 : e12 (ι x) = ι₂ x := congrArg (fun f : G →ₜ* Ghat₂ => f x) he12
136 have h21 : e21 (ι₂ x) = ι x := congrArg (fun f : G →ₜ* Ghat => f x) he21
137 simpa [MonoidHom.comp_apply, h12] using h21
138 calc
139 e21.comp e12 = h₁.lift h₁.hasOpenNormalBasisInClass ι :=
140 h₁.lift_unique h₁.hasOpenNormalBasisInClass ι hfac
141 _ = ContinuousMonoidHom.id Ghat := h₁.lift_self_eq_id
143/--
144The canonical multiplicative homeomorphism between two pro-\(C\) completions of the same
145topological group.
146-/
147noncomputable def continuousMulEquiv
148 (h₁ : IsProCCompletion C G Ghat ι)
149 (h₂ : IsProCCompletion C G Ghat₂ ι₂) : Ghat ≃ₜ* Ghat₂ :=
150 let f : Ghat →ₜ* Ghat₂ := h₁.comparison h₂
151 let g : Ghat₂ →ₜ* Ghat := h₂.comparison h₁
152 { toMulEquiv :=
153 { toFun := f
154 invFun := g
155 left_inv := by
156 intro x
157 have hgf : g.comp f = ContinuousMonoidHom.id Ghat := h₁.comparison_comp_eq_id h₂
158 exact congrArg (fun h : Ghat →ₜ* Ghat => h x) hgf
159 right_inv := by
160 intro x
161 have hfg : f.comp g = ContinuousMonoidHom.id Ghat₂ := h₂.comparison_comp_eq_id h₁
162 exact congrArg (fun h : Ghat₂ →ₜ* Ghat₂ => h x) hfg
163 map_mul' := f.map_mul }
164 continuous_toFun := f.continuous_toFun
165 continuous_invFun := g.continuous_toFun }
167/--
168The canonical equivalence between pro-\(C\) completions sends one completion map to the other.
169-/
170@[simp] theorem continuousMulEquiv_apply_completionMap
171 (h₁ : IsProCCompletion C G Ghat ι)
172 (h₂ : IsProCCompletion C G Ghat₂ ι₂) (x : G) :
173 h₁.continuousMulEquiv h₂ (ι x) = ι₂ x := by
174 simpa [continuousMulEquiv, comparison] using
175 congrArg (fun f : G →ₜ* Ghat₂ => f x) (h₁.comparison_spec h₂)
177/--
178The inverse canonical equivalence between pro-\(C\) completions sends the second completion map
179back to the first.
180-/
181@[simp] theorem continuousMulEquiv_symm_apply_completionMap
182 (h₁ : IsProCCompletion C G Ghat ι)
183 (h₂ : IsProCCompletion C G Ghat₂ ι₂) (x : G) :
184 (h₁.continuousMulEquiv h₂).symm (ι₂ x) = ι x := by
185 change h₂.comparison h₁ (ι₂ x) = ι x
186 exact congrArg (fun f : G →ₜ* Ghat => f x) (h₂.comparison_spec h₁)
188end IsProCCompletion
190end ProCGroups.Completion