Source: ProCGroups.Categorical.QuotientPullbackEquivalences
1import ProCGroups.Categorical.ProfinitePullbacks
2import ProCGroups.ProC.Quotients.ClosedNormal
4/-!
5# Pro C Groups / Categorical / Quotient Pullback Equivalences
7This module identifies the quotient by an intersection with the concrete
8fiber product of the two quotient maps to the quotient by their supremum, in
9both the algebraic and continuous settings.
10-/
12namespace ProCGroups
14namespace Subgroup
16/-- An infimum of normal subgroups is normal. -/
17instance normal_iInf
18 {ι : Type*} {G : Type*} [Group G] (W : ι → Subgroup G)
19 [∀ i, (W i).Normal] :
20 (⨅ i, W i).Normal where
21 conj_mem := by
22 intro n hn g
23 rw [Subgroup.mem_iInf] at hn ⊢
24 intro i
25 exact (show (W i).Normal by infer_instance).conj_mem n (hn i) g
27/--
28In a Hausdorff topological group, the join of a compact subgroup with a compact normal subgroup
29is closed.
30-/
31theorem isClosed_sup_of_isCompact_of_normal_right
32 {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [T2Space G]
33 (U V : Subgroup G) [V.Normal]
34 (hU : IsCompact (U : Set G)) (hV : IsCompact (V : Set G)) :
35 IsClosed ((U ⊔ V : Subgroup G) : Set G) := by
36 have hmul : Continuous (fun p : G × G => p.1 * p.2) :=
37 continuous_fst.mul continuous_snd
38 have hcompact :
39 IsCompact ((fun p : G × G => p.1 * p.2) '' ((U : Set G) ×ˢ (V : Set G))) :=
40 (hU.prod hV).image hmul
41 have hsup_eq_image :
42 ((U ⊔ V : Subgroup G) : Set G) =
43 (fun p : G × G => p.1 * p.2) '' ((U : Set G) ×ˢ (V : Set G)) := by
44 ext g
45 constructor
46 · intro hg
47 rcases (Subgroup.mem_sup_of_normal_right (s := U) (t := V)).1 hg with
48 ⟨u, hu, v, hv, huv⟩
49 exact ⟨(u, v), ⟨hu, hv⟩, by simp only [huv]⟩
50 · rintro ⟨p, hp, rfl⟩
51 exact (U ⊔ V).mul_mem
52 ((le_sup_left : U ≤ U ⊔ V) hp.1)
53 ((le_sup_right : V ≤ U ⊔ V) hp.2)
54 simpa [hsup_eq_image] using hcompact.isClosed
56/--
57In a compact Hausdorff topological group, the join of a closed subgroup with a closed normal
58subgroup is closed.
59-/
60theorem isClosed_sup_of_normal
61 {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [CompactSpace G]
62 [T2Space G]
63 (U V : Subgroup G) [V.Normal]
64 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
65 IsClosed ((U ⊔ V : Subgroup G) : Set G) :=
66 isClosed_sup_of_isCompact_of_normal_right U V hUclosed.isCompact hVclosed.isCompact
68end Subgroup
70end ProCGroups
72namespace ProCGroups.Categorical
74universe u v
76variable {G : Type u} [Group G]
77variable (U V : Subgroup G) [U.Normal] [V.Normal]
79/-- The quotient map induced by an inclusion of normal subgroups. -/
80def quotientMapOfLE (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
81 G ⧸ M →* G ⧸ N :=
82 QuotientGroup.map M N (MonoidHom.id G) (by
83 intro g hg
84 exact hMN hg)
86/-- The quotient map induced by an inclusion sends a coset to its image coset. -/
87@[simp] theorem quotientMapOfLE_mk (M N : Subgroup G) [M.Normal] [N.Normal]
88 (hMN : M ≤ N) (g : G) :
89 quotientMapOfLE (G := G) M N hMN (QuotientGroup.mk g) = QuotientGroup.mk g :=
90 by
91 let hcomap : M ≤ Subgroup.comap (MonoidHom.id G) N := by
92 simpa using hMN
93 change QuotientGroup.map M N (MonoidHom.id G) hcomap (QuotientGroup.mk g) = QuotientGroup.mk g
94 simp only [QuotientGroup.map_mk, MonoidHom.id_apply]
96/-- Coordinate map from the quotient by an indexed intersection of normal subgroups. -/
97def quotientIInfToCoordinate {ι : Type v} (W : ι → Subgroup G) [∀ i, (W i).Normal]
98 (i : ι) :
99 G ⧸ (⨅ j, W j) →* G ⧸ W i :=
100 quotientMapOfLE (G := G) (⨅ j, W j) (W i) (iInf_le W i)
102/--
103The map from the quotient by the infimum to a coordinate quotient sends a representative to its
104coordinate coset.
105-/
106@[simp] theorem quotientIInfToCoordinate_mk {ι : Type v}
107 (W : ι → Subgroup G) [∀ i, (W i).Normal] (i : ι) (g : G) :
108 quotientIInfToCoordinate (G := G) W i (QuotientGroup.mk' (⨅ j, W j) g) =
109 QuotientGroup.mk' (W i) g := by
110 simp only [quotientIInfToCoordinate, QuotientGroup.mk'_apply, quotientMapOfLE_mk]
112/--
113Quotient classes modulo an indexed intersection are equal when all coordinate quotients are
114equal.
115-/
116theorem quotient_iInf_isLimit {ι : Type v}
117 (W : ι → Subgroup G) [∀ i, (W i).Normal]
118 {x y : G ⧸ (⨅ i, W i)}
119 (hxy : ∀ i, quotientIInfToCoordinate (G := G) W i x =
120 quotientIInfToCoordinate (G := G) W i y) :
121 x = y := by
122 rcases QuotientGroup.mk'_surjective (⨅ i, W i) x with ⟨gx, rfl⟩
123 rcases QuotientGroup.mk'_surjective (⨅ i, W i) y with ⟨gy, rfl⟩
124 apply QuotientGroup.eq.2
125 rw [Subgroup.mem_iInf]
126 intro i
127 have hi := hxy i
128 simpa [quotientIInfToCoordinate] using (QuotientGroup.eq.1 hi)
131/--
132Kernel of the quotient map induced by M \(\le\) N, after precomposition with the quotient map
133from \(G\).
134-/
135@[simp] theorem ker_quotientMapOfLE_comp_mk (M N : Subgroup G) [M.Normal] [N.Normal]
136 (hMN : M ≤ N) :
137 ((quotientMapOfLE (G := G) M N hMN).comp (QuotientGroup.mk' M)).ker = N := by
138 ext g
139 simp only [quotientMapOfLE, MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk',
140 Function.comp_apply,
141 QuotientGroup.map_mk, MonoidHom.id_apply, QuotientGroup.eq_one_iff]
143/-- The left-hand map in the quotient pullback square. -/
144def quotientInfToLeft : G ⧸ (U ⊓ V) →* G ⧸ U :=
145 quotientMapOfLE (G := G) (U ⊓ V) U inf_le_left
147/-- The right-hand map in the quotient pullback square. -/
148def quotientInfToRight : G ⧸ (U ⊓ V) →* G ⧸ V :=
149 quotientMapOfLE (G := G) (U ⊓ V) V inf_le_right
151/-- The bottom-left map in the quotient pullback square. -/
152def quotientToSupLeft : G ⧸ U →* G ⧸ (U ⊔ V) :=
153 quotientMapOfLE (G := G) U (U ⊔ V) le_sup_left
155/-- The bottom-right map in the quotient pullback square. -/
156def quotientToSupRight : G ⧸ V →* G ⧸ (U ⊔ V) :=
157 quotientMapOfLE (G := G) V (U ⊔ V) le_sup_right
159/-- Kernel of the left quotient-to-sup map after precomposition with the quotient map from \(G\). -/
160@[simp] theorem ker_quotientToSupLeft_comp_mk :
161 ((quotientToSupLeft (G := G) U V).comp (QuotientGroup.mk' U)).ker = U ⊔ V := by
162 simp only [quotientToSupLeft, ker_quotientMapOfLE_comp_mk]
164/--
165This lemma identifies the kernel of the right quotient-to-sup map after precomposition with the
166quotient map from \(G\).
167-/
168@[simp] theorem ker_quotientToSupRight_comp_mk :
169 ((quotientToSupRight (G := G) U V).comp (QuotientGroup.mk' V)).ker = U ⊔ V := by
170 simp only [quotientToSupRight, ker_quotientMapOfLE_comp_mk]
172/-- The quotient map induced by an inclusion of normal subgroups is viewed as continuous. -/
173def quotientMapOfLECont
174 {G : Type u} [Group G] [TopologicalSpace G]
175 (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
176 G ⧸ M →ₜ* G ⧸ N :=
177 QuotientGroup.mapₜ M N (ContinuousMonoidHom.id G) (by
178 intro g hg
179 exact hMN hg)
181/--
182The quotient map sends the class of an element to the class of its image under the underlying
183group homomorphism.
184-/
185@[simp] theorem quotientMapOfLECont_toMonoidHom
186 {G : Type u} [Group G] [TopologicalSpace G]
187 (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
188 (quotientMapOfLECont (G := G) M N hMN).toMonoidHom =
189 quotientMapOfLE (G := G) M N hMN :=
190 by
191 ext g
192 change quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk' M g) =
193 quotientMapOfLE (G := G) M N hMN (QuotientGroup.mk' M g)
194 simpa [quotientMapOfLECont, quotientMapOfLE] using
195 (QuotientGroup.mapₜ_apply_mk
196 (N := M) (M := N) (f := ContinuousMonoidHom.id G)
197 (hNM := by
198 intro g hg
199 exact hMN hg) g)
201/-- Evaluation of the continuous quotient map induced by inclusion on a quotient class. -/
202@[simp] theorem quotientMapOfLECont_mk
203 {G : Type u} [Group G] [TopologicalSpace G]
204 (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) (g : G) :
205 quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk g) = QuotientGroup.mk g := by
206 change quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk' M g) =
207 QuotientGroup.mk' N g
208 simpa [quotientMapOfLECont] using
209 (QuotientGroup.mapₜ_apply_mk
210 (N := M) (M := N) (f := ContinuousMonoidHom.id G)
211 (hNM := by
212 intro g hg
213 exact hMN hg) g)
215/--
216The canonical map from \(G/(U \cap V)\) to the concrete pullback of \(G/U\) and \(G/V\) over
217\(G/(UV)\).
218-/
219noncomputable def quotientInfToPullback :
220 G ⧸ (U ⊓ V) →*
221 FiberProduct.carrier (quotientToSupLeft (G := G) U V) (quotientToSupRight (G := G) U V) := by
222 refine FiberProduct.lift
223 (quotientToSupLeft (G := G) U V)
224 (quotientToSupRight (G := G) U V)
225 (quotientInfToLeft (G := G) U V)
226 (quotientInfToRight (G := G) U V) ?_
227 intro x
228 refine Quotient.inductionOn x ?_
229 intro g
230 rfl
232/-- The quotient-to-pullback map sends a coset to the corresponding pair of quotient cosets. -/
233@[simp] theorem quotientInfToPullback_mk (g : G) :
234 quotientInfToPullback (G := G) U V (QuotientGroup.mk g) =
235 ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩ := by
236 rfl
238/-- The first projection of the quotient-to-pullback map is the natural quotient map to \(G/U\). -/
239@[simp] theorem pullbackFst_quotientInfToPullback :
240 (FiberProduct.fst _ _).comp
241 (quotientInfToPullback (G := G) U V) =
242 quotientInfToLeft (G := G) U V := by
243 apply MonoidHom.ext
244 intro x
245 refine Quotient.inductionOn' x ?_
246 intro g
247 rfl
249/-- The second projection of the quotient-to-pullback map is the natural quotient map to \(G/V\). -/
250@[simp] theorem pullbackSnd_quotientInfToPullback :
251 (FiberProduct.snd _ _).comp
252 (quotientInfToPullback (G := G) U V) =
253 quotientInfToRight (G := G) U V := by
254 apply MonoidHom.ext
255 intro x
256 refine Quotient.inductionOn' x ?_
257 intro g
258 rfl
260/--
261The canonical map from \(G/(U \cap V)\) to the pullback of \(G/U\) and \(G/V\) over \(G/(UV)\)
262is injective.
263-/
264theorem quotientInfToPullback_injective :
265 Function.Injective (quotientInfToPullback (G := G) U V) := by
266 intro x y hxy
267 revert hxy
268 refine Quotient.inductionOn₂' x y ?_
269 intro g h hEq
270 apply QuotientGroup.eq.2
271 have hU :
272 QuotientGroup.mk' U g = QuotientGroup.mk' U h := by
273 exact congrArg (fun z => z.1.1) hEq
274 have hV :
275 QuotientGroup.mk' V g = QuotientGroup.mk' V h := by
276 exact congrArg (fun z => z.1.2) hEq
277 exact ⟨QuotientGroup.eq.1 hU, QuotientGroup.eq.1 hV⟩
279/--
280The canonical map from the quotient by \(U \cap V\) to the pullback of the quotients by \(U\)
281and \(V\) is surjective.
282-/
283theorem quotientInfToPullback_surjective :
284 Function.Surjective (quotientInfToPullback (G := G) U V) := by
285 intro x
286 rcases QuotientGroup.mk'_surjective U x.1.1 with ⟨a, ha⟩
287 rcases QuotientGroup.mk'_surjective V x.1.2 with ⟨b, hb⟩
288 have hsup :
289 QuotientGroup.mk' (U ⊔ V) a = QuotientGroup.mk' (U ⊔ V) b := by
290 calc
291 QuotientGroup.mk' (U ⊔ V) a =
292 quotientToSupLeft (G := G) U V x.1.1 := by
293 rw [← ha]
294 rfl
295 _ = quotientToSupRight (G := G) U V x.1.2 := x.2
296 _ = QuotientGroup.mk' (U ⊔ V) b := by
297 rw [← hb]
298 rfl
299 have hab : a⁻¹ * b ∈ U ⊔ V := QuotientGroup.eq.1 hsup
300 rcases (Subgroup.mem_sup_of_normal_right (s := U) (t := V)).1 hab with
301 ⟨u, hu, v, hv, huv⟩
302 have hb_eq : b = (a * u) * v := by
303 calc
304 b = a * (a⁻¹ * b) := by simp only [mul_inv_cancel_left]
305 _ = a * (u * v) := by rw [← huv]
306 _ = (a * u) * v := by simp only [mul_assoc]
307 have hU : QuotientGroup.mk' U (a * u) = QuotientGroup.mk' U a := by
308 symm
309 apply QuotientGroup.eq.2
310 have hmem : a⁻¹ * (a * u) = u := by simp only [inv_mul_cancel_left]
311 simpa [hmem] using hu
312 have hV : QuotientGroup.mk' V (a * u) = QuotientGroup.mk' V b := by
313 apply QuotientGroup.eq.2
314 have hmem : (a * u)⁻¹ * b = v := by
315 calc
316 (a * u)⁻¹ * b = (a * u)⁻¹ * ((a * u) * v) := by rw [hb_eq]
317 _ = v := by simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
318 rw [hmem]
319 exact hv
320 refine ⟨QuotientGroup.mk' (U ⊓ V) (a * u), ?_⟩
321 apply Subtype.ext
322 apply Prod.ext
323 · calc
324 (quotientInfToPullback (G := G) U V
325 (QuotientGroup.mk' (U ⊓ V) (a * u))).1.1 =
326 QuotientGroup.mk' U (a * u) := rfl
327 _ = QuotientGroup.mk' U a := hU
328 _ = x.1.1 := ha
329 · calc
330 (quotientInfToPullback (G := G) U V
331 (QuotientGroup.mk' (U ⊓ V) (a * u))).1.2 =
332 QuotientGroup.mk' V (a * u) := rfl
333 _ = QuotientGroup.mk' V b := hV
334 _ = x.1.2 := hb
336/-- The canonical quotient-to-pullback map is bijective. -/
337theorem quotientInfToPullback_bijective :
338 Function.Bijective (quotientInfToPullback (G := G) U V) := by
339 exact ⟨quotientInfToPullback_injective (G := G) U V,
340 quotientInfToPullback_surjective (G := G) U V⟩
342/-- The quotient square is canonically isomorphic to the pullback. -/
343noncomputable def quotientInfPullbackEquiv :
344 G ⧸ (U ⊓ V) ≃*
345 FiberProduct.carrier (quotientToSupLeft (G := G) U V) (quotientToSupRight (G := G) U V) :=
346 MulEquiv.ofBijective (quotientInfToPullback (G := G) U V)
347 (quotientInfToPullback_bijective (G := G) U V)
349/-- The first coordinate of the quotient pullback equivalence is the natural map to \(G/U\). -/
350@[simp] theorem quotientInfPullbackEquiv_fst :
351 (FiberProduct.fst _ _).comp (quotientInfPullbackEquiv (G := G) U V).toMonoidHom =
352 quotientInfToLeft (G := G) U V := by
353 change (FiberProduct.fst _ _).comp (quotientInfToPullback (G := G) U V) =
354 quotientInfToLeft (G := G) U V
355 exact pullbackFst_quotientInfToPullback (G := G) U V
357/-- The second coordinate of the quotient pullback equivalence is the natural map to \(G/V\). -/
358@[simp] theorem quotientInfPullbackEquiv_snd :
359 (FiberProduct.snd _ _).comp (quotientInfPullbackEquiv (G := G) U V).toMonoidHom =
360 quotientInfToRight (G := G) U V := by
361 change (FiberProduct.snd _ _).comp (quotientInfToPullback (G := G) U V) =
362 quotientInfToRight (G := G) U V
363 exact pullbackSnd_quotientInfToPullback (G := G) U V
365/-- The quotient square is a pullback square. -/
366theorem quotientInf_isPullback :
367 CategoryTheory.IsPullback
368 (GrpCat.ofHom (quotientInfToLeft (G := G) U V))
369 (GrpCat.ofHom (quotientInfToRight (G := G) U V))
370 (GrpCat.ofHom (quotientToSupLeft (G := G) U V))
371 (GrpCat.ofHom (quotientToSupRight (G := G) U V)) := by
372 apply
373 (FiberProduct.isPullback
374 (quotientToSupLeft (G := G) U V)
375 (quotientToSupRight (G := G) U V)).of_iso'
376 (quotientInfPullbackEquiv (G := G) U V).toGrpIso
377 (CategoryTheory.Iso.refl _) (CategoryTheory.Iso.refl _)
378 (CategoryTheory.Iso.refl _)
379 · apply GrpCat.hom_ext
380 exact quotientInfPullbackEquiv_fst (G := G) U V
381 · apply GrpCat.hom_ext
382 exact quotientInfPullbackEquiv_snd (G := G) U V
383 · simp
384 · simp
386section
388variable [TopologicalSpace G]
390/-- The left map in the continuous quotient square. -/
391def quotientInfToLeftCont : G ⧸ (U ⊓ V) →ₜ* G ⧸ U :=
392 quotientMapOfLECont (G := G) (U ⊓ V) U inf_le_left
394/-- The right map in the continuous quotient square. -/
395def quotientInfToRightCont : G ⧸ (U ⊓ V) →ₜ* G ⧸ V :=
396 quotientMapOfLECont (G := G) (U ⊓ V) V inf_le_right
398/-- The bottom-left map in the continuous quotient square. -/
399def quotientToSupLeftCont : G ⧸ U →ₜ* G ⧸ (U ⊔ V) :=
400 quotientMapOfLECont (G := G) U (U ⊔ V) le_sup_left
402/-- The bottom-right map in the continuous quotient square. -/
403def quotientToSupRightCont : G ⧸ V →ₜ* G ⧸ (U ⊔ V) :=
404 quotientMapOfLECont (G := G) V (U ⊔ V) le_sup_right
406/--
407Forgetting continuity from the left continuous quotient-square map recovers the algebraic map.
408-/
409@[simp] theorem quotientInfToLeftCont_toMonoidHom :
410 (quotientInfToLeftCont (G := G) U V).toMonoidHom = quotientInfToLeft (G := G) U V :=
411 rfl
413/-- Forgetting continuity from the right continuous quotient-square map recovers the
414algebraic map. -/
415@[simp] theorem quotientInfToRightCont_toMonoidHom :
416 (quotientInfToRightCont (G := G) U V).toMonoidHom = quotientInfToRight (G := G) U V :=
417 rfl
419/--
420Forgetting continuity from the lower-left continuous quotient-square map recovers the algebraic
421map.
422-/
423@[simp] theorem quotientToSupLeftCont_toMonoidHom :
424 (quotientToSupLeftCont (G := G) U V).toMonoidHom = quotientToSupLeft (G := G) U V :=
425 rfl
427/--
428Forgetting continuity from the lower-right continuous quotient-square map recovers the algebraic
429map.
430-/
431@[simp] theorem quotientToSupRightCont_toMonoidHom :
432 (quotientToSupRightCont (G := G) U V).toMonoidHom = quotientToSupRight (G := G) U V :=
433 rfl
435/-- Evaluation of the left continuous quotient-square map on a quotient class. -/
436@[simp] theorem quotientInfToLeftCont_mk (g : G) :
437 quotientInfToLeftCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g := by
438 simp only [quotientInfToLeftCont, quotientMapOfLECont_mk]
440/-- Evaluation of the right continuous quotient-square map on a quotient class. -/
441@[simp] theorem quotientInfToRightCont_mk (g : G) :
442 quotientInfToRightCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g := by
443 simp only [quotientInfToRightCont, quotientMapOfLECont_mk]
445/-- Evaluation of the lower-left continuous quotient-square map on a quotient class. -/
446@[simp] theorem quotientToSupLeftCont_mk (g : G) :
447 quotientToSupLeftCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g := by
448 simp only [quotientToSupLeftCont, quotientMapOfLECont_mk]
450/-- Evaluation of the lower-right continuous quotient-square map on a quotient class. -/
451@[simp] theorem quotientToSupRightCont_mk (g : G) :
452 quotientToSupRightCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g := by
453 simp only [quotientToSupRightCont, quotientMapOfLECont_mk]
455variable [IsTopologicalGroup G]
457/--
458The canonical continuous map from \(G/(U \cap V)\) to the concrete continuous pullback of
459\(G/U\) and \(G/V\) over \(G/(UV)\).
460-/
461def quotientInfToContinuousPullback :
462 G ⧸ (U ⊓ V) →ₜ*
463 TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V)
464 (quotientToSupRightCont (G := G) U V) := by
465 refine TopologicalFiberProduct.lift
466 (quotientToSupLeftCont (G := G) U V)
467 (quotientToSupRightCont (G := G) U V)
468 (quotientInfToLeftCont (G := G) U V)
469 (quotientInfToRightCont (G := G) U V) ?_
470 intro x
471 refine Quotient.inductionOn x ?_
472 intro g
473 rfl
475omit [IsTopologicalGroup G] in
476/--
477Forgetting continuity from the continuous quotient-to-pullback map recovers the algebraic one.
478-/
479@[simp] theorem quotientInfToContinuousPullback_toMonoidHom :
480 (quotientInfToContinuousPullback (G := G) U V).toMonoidHom =
481 quotientInfToPullback (G := G) U V := by
482 apply MonoidHom.ext
483 intro x
484 refine Quotient.inductionOn' x ?_
485 intro g
486 exact Subtype.ext <| Prod.ext rfl rfl
488omit [IsTopologicalGroup G] in
489/-- Evaluation formula for the continuous quotient-to-pullback map. -/
490@[simp] theorem quotientInfToContinuousPullback_mk (g : G) :
491 quotientInfToContinuousPullback (G := G) U V (QuotientGroup.mk g) =
492 ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩ := by
493 rfl
495omit [IsTopologicalGroup G] in
496/-- The first projection of the continuous quotient-to-pullback map is the natural quotient map to
497`G/U`. -/
498@[simp] theorem pullbackFstCont_quotientInfToContinuousPullback :
499 (TopologicalFiberProduct.fst _ _).comp (quotientInfToContinuousPullback (G := G) U V) =
500 quotientInfToLeftCont (G := G) U V := by
501 apply ContinuousMonoidHom.ext
502 intro x
503 refine Quotient.inductionOn' x ?_
504 intro g
505 rfl
507omit [IsTopologicalGroup G] in
508/-- The second projection of the continuous quotient-to-pullback map is the natural quotient map to
509`G/V`. -/
510@[simp] theorem pullbackSndCont_quotientInfToContinuousPullback :
511 (TopologicalFiberProduct.snd _ _).comp (quotientInfToContinuousPullback (G := G) U V) =
512 quotientInfToRightCont (G := G) U V := by
513 apply ContinuousMonoidHom.ext
514 intro x
515 refine Quotient.inductionOn' x ?_
516 intro g
517 rfl
519omit [IsTopologicalGroup G] in
520/-- Injectivity of the continuous quotient-to-pullback map on the underlying groups. -/
521theorem quotientInfToContinuousPullback_injective :
522 Function.Injective (quotientInfToContinuousPullback (G := G) U V) := by
523 intro x y hxy
524 apply quotientInfToPullback_injective (G := G) U V
525 apply Subtype.ext
526 apply Prod.ext
527 · exact congrArg (fun z => z.1.1) hxy
528 · exact congrArg (fun z => z.1.2) hxy
530omit [IsTopologicalGroup G] in
531/-- Surjectivity of the continuous quotient-to-pullback map on the underlying groups. -/
532theorem quotientInfToContinuousPullback_surjective :
533 Function.Surjective (quotientInfToContinuousPullback (G := G) U V) := by
534 intro x
535 rcases quotientInfToPullback_surjective (G := G) U V x with ⟨y, hy⟩
536 refine ⟨y, ?_⟩
537 apply Subtype.ext
538 apply Prod.ext
539 · exact congrArg (fun z => z.1.1) hy
540 · exact congrArg (fun z => z.1.2) hy
542omit [IsTopologicalGroup G] in
543/-- The continuous quotient-to-pullback map is bijective on the underlying groups. -/
544theorem quotientInfToContinuousPullback_bijective :
545 Function.Bijective (quotientInfToContinuousPullback (G := G) U V) := by
546 exact ⟨quotientInfToContinuousPullback_injective (G := G) U V,
547 quotientInfToContinuousPullback_surjective (G := G) U V⟩
549/-- The quotient square is canonically isomorphic to the concrete continuous fiber product. -/
550noncomputable def quotientInfContinuousPullbackEquiv
551 [CompactSpace G] [T2Space G]
552 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
553 G ⧸ (U ⊓ V) ≃ₜ*
554 TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V)
555 (quotientToSupRightCont (G := G) U V) := by
556 letI : IsClosed (U : Set G) := hUclosed
557 letI : IsClosed (V : Set G) := hVclosed
558 exact ContinuousMulEquiv.ofBijectiveCompactToT2
559 (quotientInfToContinuousPullback (G := G) U V)
560 (quotientInfToContinuousPullback (G := G) U V).continuous_toFun
561 (quotientInfToContinuousPullback_bijective (G := G) U V)
563/-- The quotient pullback equivalence is induced by the canonical comparison map. -/
564@[simp] theorem quotientInfContinuousPullbackEquiv_toContinuousMonoidHom
565 [CompactSpace G] [T2Space G]
566 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
567 ContinuousMonoidHom.toContinuousMonoidHom (quotientInfContinuousPullbackEquiv
568 (G := G) (U := U) (V := V) hUclosed hVclosed) =
569 quotientInfToContinuousPullback (G := G) U V := by
570 apply ContinuousMonoidHom.ext
571 intro x
572 exact Subtype.ext <| Prod.ext rfl rfl
574/-- Evaluation formula for the continuous quotient pullback equivalence on a quotient class.
575-/
576@[simp] theorem quotientInfContinuousPullbackEquiv_mk
577 [CompactSpace G] [T2Space G]
578 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) (g : G) :
579 quotientInfContinuousPullbackEquiv (G := G) (U := U) (V := V) hUclosed hVclosed
580 (QuotientGroup.mk g) = ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩ := by
581 change quotientInfToContinuousPullback (G := G) U V (QuotientGroup.mk g) = _
582 exact quotientInfToContinuousPullback_mk (G := G) U V g
584/--
585The first coordinate of the continuous quotient pullback equivalence is the natural map to `G/U`.
586-/
587@[simp] theorem quotientInfContinuousPullbackEquiv_fst
588 [CompactSpace G] [T2Space G]
589 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
590 (TopologicalFiberProduct.fst _ _).comp
591 (ContinuousMonoidHom.toContinuousMonoidHom (quotientInfContinuousPullbackEquiv
592 (G := G) (U := U) (V := V) hUclosed hVclosed)) =
593 quotientInfToLeftCont (G := G) U V := by
594 rw [quotientInfContinuousPullbackEquiv_toContinuousMonoidHom
595 (G := G) (U := U) (V := V) hUclosed hVclosed]
596 exact pullbackFstCont_quotientInfToContinuousPullback (G := G) U V
598/--
599The second coordinate of the continuous quotient pullback equivalence is the natural map to `G/V`.
600-/
601@[simp] theorem quotientInfContinuousPullbackEquiv_snd
602 [CompactSpace G] [T2Space G]
603 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
604 (TopologicalFiberProduct.snd _ _).comp
605 (ContinuousMonoidHom.toContinuousMonoidHom (quotientInfContinuousPullbackEquiv
606 (G := G) (U := U) (V := V) hUclosed hVclosed)) =
607 quotientInfToRightCont (G := G) U V := by
608 rw [quotientInfContinuousPullbackEquiv_toContinuousMonoidHom
609 (G := G) (U := U) (V := V) hUclosed hVclosed]
610 exact pullbackSndCont_quotientInfToContinuousPullback (G := G) U V
612/-- For closed normal subgroups of a compact Hausdorff topological group, the quotient square
613has the universal
614property when tested against profinite source groups. -/
615theorem quotientInf_hasProfiniteTestPullbackProperty
616 [CompactSpace G] [T2Space G]
617 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
618 HasProfiniteTestPullbackProperty
619 (quotientInfToLeftCont (G := G) U V)
620 (quotientInfToRightCont (G := G) U V)
621 (quotientToSupLeftCont (G := G) U V)
622 (quotientToSupRightCont (G := G) U V) := by
623 exact hasProfiniteTestPullbackProperty_of_equiv_toConcretePullback
624 (quotientInfToLeftCont (G := G) U V)
625 (quotientInfToRightCont (G := G) U V)
626 (quotientToSupLeftCont (G := G) U V)
627 (quotientToSupRightCont (G := G) U V)
628 (quotientInfContinuousPullbackEquiv (G := G) (U := U) (V := V) hUclosed hVclosed)
629 (quotientInfContinuousPullbackEquiv_fst (G := G) (U := U) (V := V) hUclosed hVclosed)
630 (quotientInfContinuousPullbackEquiv_snd (G := G) (U := U) (V := V) hUclosed hVclosed)
632end
633end ProCGroups.Categorical