Source: ProCGroups.InverseSystems.Quotients
1import Mathlib.Topology.Algebra.ProperAction.Basic
2import ProCGroups.InverseSystems.CompatibilityAndSurjectivity
3import ProCGroups.Topologies.QuotientMaps
5/-!
6# Quotients of group-valued inverse systems
8A compatible family of closed normal stage subgroups induces an inverse system of quotient
9groups and a canonical map from the original limit. This module identifies its kernel and,
10under compact Hausdorff directed-surjective hypotheses, proves that quotienting the inverse
11limit agrees topologically and algebraically with taking the inverse limit of the stage quotients.
12-/
14open scoped Topology
16namespace ProCGroups
17namespace InverseSystems
19universe u v
21namespace InverseSystem
23variable {I : Type u} [Preorder I]
24variable (S : InverseSystem.{u, v} (I := I))
25variable [∀ i, Group (S.X i)] [IsGroupSystem S]
26variable [∀ i, IsTopologicalGroup (S.X i)]
28/-- The transition map of a group-valued inverse system is bundled as a homomorphism. -/
29def transitionHom {i j : I} (hij : i ≤ j) : S.X j →* S.X i where
30 toFun := S.map hij
31 map_one' := IsGroupSystem.map_one (S := S) hij
32 map_mul' := IsGroupSystem.map_mul (S := S) hij
34omit [∀ i, IsTopologicalGroup (S.X i)] in
35/-- The bundled transition homomorphism evaluates to the underlying transition map of `S`. -/
36@[simp] theorem transitionHom_apply {i j : I} (hij : i ≤ j) (x : S.X j) :
37 S.transitionHom hij x = S.map hij x := rfl
39omit [∀ i, IsTopologicalGroup (S.X i)] in
40/-- The bundled transition homomorphism of an inverse system is continuous. -/
41theorem continuous_transitionHom {i j : I} (hij : i ≤ j) :
42 Continuous (S.transitionHom hij) :=
43 S.continuous_map hij
45/-- Closed normal subgroups of the stages, compatible with transition maps. -/
46structure CompatibleClosedNormalSubgroups where
47 /-- The subgroup by which the stage at index `i` will be quotiented. -/
48 N : ∀ i, Subgroup (S.X i)
49 /-- Every selected stage subgroup is normal, so its group quotient is defined. -/
50 normal : ∀ i, (N i).Normal
51 /-- Every selected stage subgroup is closed in the topology of that stage. -/
52 closed : ∀ i, IsClosed ((N i : Subgroup (S.X i)) : Set (S.X i))
53 /--
54 A transition homomorphism sends the subgroup at the later stage into the subgroup at the
55 earlier stage, and hence descends to the corresponding quotients.
56 -/
57 map_le :
58 ∀ {i j : I} (hij : i ≤ j), N j ≤ (N i).comap (S.transitionHom hij)
60namespace CompatibleClosedNormalSubgroups
62variable {S}
63variable (Q : S.CompatibleClosedNormalSubgroups)
65/-- The chosen subgroup is normal. -/
66instance instNormalN (i : I) : (Q.N i).Normal := Q.normal i
68/-- The transition map induced on stage quotients. -/
69def quotientMap {i j : I} (hij : i ≤ j) :
70 S.X j ⧸ Q.N j →* S.X i ⧸ Q.N i :=
71 QuotientGroup.map (N := Q.N j) (M := Q.N i) (f := S.transitionHom hij) (Q.map_le hij)
73omit [∀ i, IsTopologicalGroup (S.X i)] in
74/--
75The induced quotient transition sends the class of `x` modulo `N j` to the class of its
76transition image modulo `N i`.
77-/
78@[simp] theorem quotientMap_mk {i j : I} (hij : i ≤ j) (x : S.X j) :
79 Q.quotientMap hij (QuotientGroup.mk' (Q.N j) x) =
80 QuotientGroup.mk' (Q.N i) (S.map hij x) := by
81 exact QuotientGroup.map_mk' (N := Q.N j) (M := Q.N i)
82 (f := S.transitionHom hij) (Q.map_le hij) x
84omit [∀ i, IsTopologicalGroup (S.X i)] in
85/-- The induced map on stage quotients is continuous. -/
86theorem continuous_quotientMap {i j : I} (hij : i ≤ j) :
87 Continuous (Q.quotientMap hij) := by
88 refine (QuotientGroup.isQuotientMap_mk (N := Q.N j)).continuous_iff.2 ?_
89 change Continuous fun x : S.X j => QuotientGroup.mk' (Q.N i) (S.map hij x)
90 exact QuotientGroup.continuous_mk.comp (S.continuous_map hij)
92/-- The inverse system obtained by quotienting each stage by a compatible closed normal subgroup. -/
93def quotientInverseSystem : InverseSystem (I := I) where
94 X := fun i => S.X i ⧸ Q.N i
95 topologicalSpace := fun i => inferInstance
96 map := fun {_i _j} hij => Q.quotientMap hij
97 continuous_map := fun {_i _j} hij => Q.continuous_quotientMap hij
98 map_id := by
99 intro i
100 funext x
101 refine Quotient.inductionOn' x ?_
102 intro a
103 change QuotientGroup.mk' (Q.N i) (S.map (le_rfl : i ≤ i) a) =
104 QuotientGroup.mk' (Q.N i) a
105 exact congrArg (QuotientGroup.mk' (Q.N i)) (S.map_id_apply i a)
106 map_comp := by
107 intro i j k hij hjk
108 funext x
109 refine Quotient.inductionOn' x ?_
110 intro a
111 change QuotientGroup.mk' (Q.N i) (S.map hij (S.map hjk a)) =
112 QuotientGroup.mk' (Q.N i) (S.map (hij.trans hjk) a)
113 exact congrArg (QuotientGroup.mk' (Q.N i)) (S.map_comp_apply hij hjk a)
115/-- The quotient inverse system has the expected finite-stage quotient groups. -/
116instance quotientInverseSystem_stageGroup (i : I) :
117 Group (Q.quotientInverseSystem.X i) := by
118 change Group (S.X i ⧸ Q.N i)
119 infer_instance
121/-- Each stage quotient carries the quotient topology and its induced topological-group structure. -/
122instance quotientInverseSystem_stageTopologicalGroup (i : I) :
123 IsTopologicalGroup (Q.quotientInverseSystem.X i) := by
124 change IsTopologicalGroup (S.X i ⧸ Q.N i)
125 infer_instance
127/-- The induced quotient transitions preserve the group operations at every stage. -/
128instance quotientInverseSystem_isGroupSystem :
129 IsGroupSystem Q.quotientInverseSystem where
130 map_one := by
131 intro i j hij
132 exact (Q.quotientMap hij).map_one
133 map_mul := by
134 intro i j hij x y
135 exact (Q.quotientMap hij).map_mul x y
136 map_inv := by
137 intro i j hij x
138 exact (Q.quotientMap hij).map_inv x
140/-- The stagewise quotient maps form a morphism from the original system to the quotient system. -/
141def toQuotientInverseSystem : S.Morphism Q.quotientInverseSystem where
142 map := fun i => QuotientGroup.mk' (Q.N i)
143 continuous_map := fun _ => QuotientGroup.continuous_mk
144 comm := by
145 intro i j hij
146 funext x
147 exact (Q.quotientMap_mk hij x).symm
149/-- Kernel of the map from the inverse limit to the inverse limit of stage quotients. -/
150def inverseLimitKernel : Subgroup S.inverseLimit :=
151 ⨅ i, (Q.N i).comap (projectionHom (S := S) i)
153/--
154The intersection of the pullbacks of the normal subgroups `N i` along all limit projections is
155a normal subgroup of the inverse limit.
156-/
157instance inverseLimitKernel_normal : Q.inverseLimitKernel.Normal where
158 conj_mem x hx g := by
159 rw [inverseLimitKernel] at hx ⊢
160 simp only [projectionHom, Subgroup.mem_iInf, Subgroup.mem_comap, MonoidHom.coe_mk,
161 OneHom.coe_mk,
162 projection_apply] at hx ⊢
163 intro i
164 change
165 S.projection i g * S.projection i x * (S.projection i g)⁻¹ ∈ Q.N i
166 exact (Q.normal i).conj_mem (S.projection i x) (hx i) (S.projection i g)
168variable {Q}
170omit [∀ i, IsTopologicalGroup (S.X i)] in
171/--
172Membership in the named kernel is equivalent to vanishing under its defining quotient or
173augmentation map.
174-/
175theorem mem_inverseLimitKernel_iff {x : S.inverseLimit} :
176 x ∈ Q.inverseLimitKernel ↔ ∀ i, S.projection i x ∈ Q.N i := by
177 simp only [inverseLimitKernel, projectionHom, Subgroup.mem_iInf, Subgroup.mem_comap,
178 MonoidHom.coe_mk,
179 OneHom.coe_mk, projection_apply]
181variable (Q)
183/--
184The canonical comparison from the quotient of the inverse limit to the inverse limit of the
185stage quotients.
186-/
187noncomputable def quotientInverseLimitComparison :
188 S.inverseLimit ⧸ Q.inverseLimitKernel →ₜ* Q.quotientInverseSystem.inverseLimit := by
189 let T : InverseSystem (I := I) := Q.quotientInverseSystem
190 let φ : S.inverseLimit →ₜ* T.inverseLimit :=
191 { toMonoidHom :=
192 { toFun := S.limMap Q.toQuotientInverseSystem
193 map_one' := by
194 apply T.ext
195 intro i
196 calc
197 T.projection i (S.limMap Q.toQuotientInverseSystem 1) =
198 Q.toQuotientInverseSystem.map i (S.projection i (1 : S.inverseLimit)) := by
199 exact S.π_limMap_apply Q.toQuotientInverseSystem i 1
200 _ = 1 := by
201 change QuotientGroup.mk' (Q.N i) (S.projection i (1 : S.inverseLimit)) = 1
202 rw [projection_one (S := S) i]
203 simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one]
204 map_mul' := by
205 intro x y
206 apply T.ext
207 intro i
208 calc
209 T.projection i (S.limMap Q.toQuotientInverseSystem (x * y)) =
210 Q.toQuotientInverseSystem.map i (S.projection i (x * y)) := by
211 exact S.π_limMap_apply Q.toQuotientInverseSystem i (x * y)
212 _ =
213 Q.toQuotientInverseSystem.map i (S.projection i x) *
214 Q.toQuotientInverseSystem.map i (S.projection i y) := by
215 change QuotientGroup.mk' (Q.N i) (S.projection i (x * y)) =
216 QuotientGroup.mk' (Q.N i) (S.projection i x) *
217 QuotientGroup.mk' (Q.N i) (S.projection i y)
218 rw [projection_mul (S := S) i x y]
219 simp only [projection_apply, QuotientGroup.mk'_apply, QuotientGroup.mk_mul]
220 _ =
221 T.projection i (S.limMap Q.toQuotientInverseSystem x) *
222 T.projection i (S.limMap Q.toQuotientInverseSystem y) := by
223 rw [← S.π_limMap_apply Q.toQuotientInverseSystem i x,
224 ← S.π_limMap_apply Q.toQuotientInverseSystem i y] }
225 continuous_toFun := S.continuous_limMap Q.toQuotientInverseSystem }
226 refine QuotientGroup.liftₜ Q.inverseLimitKernel φ ?_
227 intro x hx
228 apply T.ext
229 intro i
230 have hxi : S.projection i x ∈ Q.N i := (Q.mem_inverseLimitKernel_iff (x := x)).1 hx i
231 change QuotientGroup.mk' (Q.N i) (S.projection i x) = 1
232 exact (QuotientGroup.eq_one_iff (N := Q.N i) (S.projection i x)).2 hxi
234omit [∀ i, IsTopologicalGroup (S.X i)] in
235/--
236The quotient inverse-limit comparison sends a representative to its compatible family of
237quotient coordinates.
238-/
239@[simp] theorem quotientInverseLimitComparison_mk (x : S.inverseLimit) :
240 Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x) =
241 S.limMap Q.toQuotientInverseSystem x :=
242 by
243 unfold quotientInverseLimitComparison
244 rfl
246omit [∀ i, IsTopologicalGroup (S.X i)] in
247/--
248Projecting the quotient inverse-limit comparison gives the corresponding stage quotient
249representative.
250-/
251@[simp] theorem projection_quotientInverseLimitComparison_mk
252 (i : I) (x : S.inverseLimit) :
253 Q.quotientInverseSystem.projection i
254 (Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x)) =
255 QuotientGroup.mk' (Q.N i) (S.projection i x) := by
256 rw [quotientInverseLimitComparison_mk]
257 rfl
259omit [∀ i, IsTopologicalGroup (S.X i)] in
260/-- The comparison map has trivial kernel. -/
261theorem ker_quotientInverseLimitComparison :
262 Q.quotientInverseLimitComparison.toMonoidHom.ker = ⊥ := by
263 ext a
264 constructor
265 · intro ha
266 refine Quotient.inductionOn' a ?_ ha
267 intro x hx
268 rw [MonoidHom.mem_ker] at hx
269 rw [Subgroup.mem_bot]
270 exact (QuotientGroup.eq_one_iff (N := Q.inverseLimitKernel) x).2 <| by
271 rw [Q.mem_inverseLimitKernel_iff]
272 intro i
273 have hcoord :=
274 congrArg (fun y => Q.quotientInverseSystem.projection i y) hx
275 change QuotientGroup.mk' (Q.N i) (S.projection i x) = 1 at hcoord
276 exact (QuotientGroup.eq_one_iff (N := Q.N i) (S.projection i x)).1 hcoord
277 · intro ha
278 rw [Subgroup.mem_bot] at ha
279 rw [MonoidHom.mem_ker, ha]
280 exact map_one Q.quotientInverseLimitComparison
282omit [∀ i, IsTopologicalGroup (S.X i)] in
283/-- The comparison map is injective: its kernel is exactly the subgroup used in the quotient. -/
284theorem injective_quotientInverseLimitComparison :
285 Function.Injective Q.quotientInverseLimitComparison :=
286 (MonoidHom.ker_eq_bot_iff (f := Q.quotientInverseLimitComparison.toMonoidHom)).mp
287 Q.ker_quotientInverseLimitComparison
289/-- The comparison map is surjective for compact Hausdorff systems over a directed index. -/
290theorem surjective_quotientInverseLimitComparison
291 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
292 (hdir : Directed (· ≤ ·) (id : I → I)) :
293 Function.Surjective Q.quotientInverseLimitComparison := by
294 let T : InverseSystem (I := I) := Q.quotientInverseSystem
295 letI : ∀ i, T2Space (T.X i) := fun i => by
296 dsimp [T, quotientInverseSystem]
297 haveI : IsClosed ((Q.N i : Subgroup (S.X i)) : Set (S.X i)) := Q.closed i
298 exact QuotientGroup.instT2Space
299 have hlimsurj : Function.Surjective (S.limMap Q.toQuotientInverseSystem) :=
300 S.surjective_limMap (T := T) hdir Q.toQuotientInverseSystem
301 (fun i => QuotientGroup.mk'_surjective (Q.N i))
302 intro y
303 rcases hlimsurj y with ⟨x, hx⟩
304 refine ⟨QuotientGroup.mk' Q.inverseLimitKernel x, ?_⟩
305 rw [Q.quotientInverseLimitComparison_mk]
306 exact hx
308/-- The comparison map is bijective for compact Hausdorff systems over a directed index. -/
309theorem bijective_quotientInverseLimitComparison
310 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
311 (hdir : Directed (· ≤ ·) (id : I → I)) :
312 Function.Bijective Q.quotientInverseLimitComparison :=
313 ⟨Q.injective_quotientInverseLimitComparison,
314 Q.surjective_quotientInverseLimitComparison hdir⟩
316/--
317The quotient of an inverse limit by a compatible closed normal family is the inverse limit of
318the stage quotients.
319-/
320noncomputable def quotientInverseLimitContinuousMulEquiv
321 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
322 (hdir : Directed (· ≤ ·) (id : I → I)) :
323 S.inverseLimit ⧸ Q.inverseLimitKernel ≃ₜ* Q.quotientInverseSystem.inverseLimit := by
324 let T : InverseSystem (I := I) := Q.quotientInverseSystem
325 let f := Q.quotientInverseLimitComparison
326 letI : CompactSpace S.inverseLimit := inferInstance
327 letI : CompactSpace (S.inverseLimit ⧸ Q.inverseLimitKernel) := inferInstance
328 letI : ∀ i, T2Space (T.X i) := fun i => by
329 dsimp [T, quotientInverseSystem]
330 haveI : IsClosed ((Q.N i : Subgroup (S.X i)) : Set (S.X i)) := Q.closed i
331 exact QuotientGroup.instT2Space
332 letI : T2Space T.inverseLimit := T.t2Space_inverseLimit
333 exact ContinuousMulEquiv.ofBijectiveCompactToT2
334 f.toMonoidHom f.continuous_toFun (Q.bijective_quotientInverseLimitComparison hdir)
336end CompatibleClosedNormalSubgroups
338end InverseSystem
340end InverseSystems
341end ProCGroups