Yamaguchi Lean 4 Library
ProCGroups/Categorical/QuotientPullbackEquivalences.lean
ProCGroups/Categorical/QuotientPullbackEquivalences/Source

ProCGroups/Categorical/QuotientPullbackEquivalences.lean

1import ProCGroups.Categorical.ProfinitePullbacks
2import ProCGroups.ProC.Quotients.ClosedNormal
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Categorical/QuotientPullbackEquivalences.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Pullbacks, pushouts, and quotient comparison
15Concrete algebraic and topological pullbacks and pushouts of groups and profinite groups, with comparison maps, universal properties, kernel criteria, and quotient pullback equivalences.
16-/
18namespace Subgroup
20/-- An infimum of normal subgroups is normal. -/
21instance normal_iInf
22 {ι : Type*} {G : Type*} [Group G] (W : ι → Subgroup G)
23 [∀ i, (W i).Normal] :
24 (⨅ i, W i).Normal where
25 conj_mem := by
26 intro n hn g
27 rw [Subgroup.mem_iInf] at hn ⊢
28 intro i
29 exact (show (W i).Normal by infer_instance).conj_mem n (hn i) g
31/-- In a Hausdorff topological group, the join of a compact subgroup with a compact normal subgroup
32is closed. -/
34 {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [T2Space G]
35 (U V : Subgroup G) [V.Normal]
36 (hU : IsCompact (U : Set G)) (hV : IsCompact (V : Set G)) :
37 IsClosed ((U ⊔ V : Subgroup G) : Set G) := by
38 have hmul : Continuous (fun p : G × G => p.1 * p.2) :=
39 continuous_fst.mul continuous_snd
40 have hcompact :
41 IsCompact ((fun p : G × G => p.1 * p.2) '' ((U : Set G) ×ˢ (V : Set G))) :=
42 (hU.prod hV).image hmul
43 have hsup_eq_image :
44 ((U ⊔ V : Subgroup G) : Set G) =
45 (fun p : G × G => p.1 * p.2) '' ((U : Set G) ×ˢ (V : Set G)) := by
46 ext g
47 constructor
48 · intro hg
49 rcases (Subgroup.mem_sup_of_normal_right (s := U) (t := V)).1 hg with
50 ⟨u, hu, v, hv, huv⟩
51 exact ⟨(u, v), ⟨hu, hv⟩, by simp only [huv]⟩
52 · rintro ⟨p, hp, rfl⟩
53 exact (U ⊔ V).mul_mem
54 ((le_sup_left : U ≤ U ⊔ V) hp.1)
55 ((le_sup_right : V ≤ U ⊔ V) hp.2)
56 simpa [hsup_eq_image] using hcompact.isClosed
58/-- In a compact Hausdorff topological group, the join of a closed subgroup with a closed normal
59subgroup is closed. -/
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
70namespace ProCGroups.Categorical
72universe u v
74variable {G : Type u} [Group G]
75variable (U V : Subgroup G) [U.Normal] [V.Normal]
77/-- The quotient map induced by an inclusion of normal subgroups. -/
78def quotientMapOfLE (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
79 G ⧸ M →* G ⧸ N :=
80 QuotientGroup.map M N (MonoidHom.id G) (by
81 intro g hg
82 exact hMN hg)
84/-- Evaluation formula for the quotient map induced by inclusion. -/
85@[simp] theorem quotientMapOfLE_mk (M N : Subgroup G) [M.Normal] [N.Normal]
86 (hMN : M ≤ N) (g : G) :
87 quotientMapOfLE (G := G) M N hMN (QuotientGroup.mk g) = QuotientGroup.mk g :=
88 by
89 let hcomap : M ≤ Subgroup.comap (MonoidHom.id G) N := by
90 simpa using hMN
91 change QuotientGroup.map M N (MonoidHom.id G) hcomap (QuotientGroup.mk g) = QuotientGroup.mk g
92 simp only [QuotientGroup.map_mk, MonoidHom.id_apply]
94/-- Coordinate map from the quotient by an indexed intersection of normal subgroups. -/
95def quotientIInfToCoordinate {ι : Type v} (W : ι → Subgroup G) [∀ i, (W i).Normal]
96 (i : ι) :
97 G ⧸ (⨅ j, W j) →* G ⧸ W i :=
98 quotientMapOfLE (G := G) (⨅ j, W j) (W i) (iInf_le W i)
100@[simp] theorem quotientIInfToCoordinate_mk {ι : Type v}
101 (W : ι → Subgroup G) [∀ i, (W i).Normal] (i : ι) (g : G) :
102 quotientIInfToCoordinate (G := G) W i (QuotientGroup.mk' (⨅ j, W j) g) =
103 QuotientGroup.mk' (W i) g := by
104 simp only [quotientIInfToCoordinate, QuotientGroup.mk'_apply, quotientMapOfLE_mk]
106/-- Quotient classes modulo an indexed intersection are equal when all coordinate quotients are
107equal. For finite families this is the extensional core of the finite-family quotient pullback. -/
108theorem quotient_iInf_isLimit_finite {ι : Type v} [Fintype ι]
109 (W : ι → Subgroup G) [∀ i, (W i).Normal]
110 {x y : G ⧸ (⨅ i, W i)}
111 (hxy : ∀ i, quotientIInfToCoordinate (G := G) W i x =
112 quotientIInfToCoordinate (G := G) W i y) :
113 x = y := by
114 rcases QuotientGroup.mk'_surjective (⨅ i, W i) x with ⟨gx, rfl⟩
115 rcases QuotientGroup.mk'_surjective (⨅ i, W i) y with ⟨gy, rfl⟩
116 apply QuotientGroup.eq.2
117 rw [Subgroup.mem_iInf]
118 intro i
119 have hi := hxy i
120 simpa [quotientIInfToCoordinate] using (QuotientGroup.eq.1 hi)
122/-- Kernel of the quotient map induced by `M ≤ N`, after precomposition with the quotient map
123from `G`. -/
124@[simp] theorem ker_quotientMapOfLE_comp_mk (M N : Subgroup G) [M.Normal] [N.Normal]
125 (hMN : M ≤ N) :
126 ((quotientMapOfLE (G := G) M N hMN).comp (QuotientGroup.mk' M)).ker = N := by
127 ext g
128 simp only [quotientMapOfLE, MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
129 QuotientGroup.map_mk, MonoidHom.id_apply, QuotientGroup.eq_one_iff]
131/-- The left-hand map in the quotient pullback square. -/
132def quotientInfToLeft : G ⧸ (U ⊓ V) →* G ⧸ U :=
133 quotientMapOfLE (G := G) (U ⊓ V) U inf_le_left
135/-- The right-hand map in the quotient pullback square. -/
136def quotientInfToRight : G ⧸ (U ⊓ V) →* G ⧸ V :=
137 quotientMapOfLE (G := G) (U ⊓ V) V inf_le_right
139/-- The bottom-left map in the quotient pullback square. -/
140def quotientToSupLeft : G ⧸ U →* G ⧸ (U ⊔ V) :=
141 quotientMapOfLE (G := G) U (U ⊔ V) le_sup_left
143/-- The bottom-right map in the quotient pullback square. -/
144def quotientToSupRight : G ⧸ V →* G ⧸ (U ⊔ V) :=
145 quotientMapOfLE (G := G) V (U ⊔ V) le_sup_right
147/-- Kernel of the left quotient-to-sup map after precomposition with the quotient map from `G`. -/
149 ((quotientToSupLeft (G := G) U V).comp (QuotientGroup.mk' U)).ker = U ⊔ V := by
152/-- Kernel of the right quotient-to-sup map after precomposition with the quotient map from `G`. -/
154 ((quotientToSupRight (G := G) U V).comp (QuotientGroup.mk' V)).ker = U ⊔ V := by
157/-- The quotient map induced by an inclusion of normal subgroups, viewed as continuous. -/
159 {G : Type u} [Group G] [TopologicalSpace G]
160 (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
161 G ⧸ M →ₜ* G ⧸ N :=
162 QuotientGroup.mapₜ M N (ContinuousMonoidHom.id G) (by
163 intro g hg
164 exact hMN hg)
166/-- Forgetting continuity from `quotientMapOfLECont` recovers `quotientMapOfLE`. -/
168 {G : Type u} [Group G] [TopologicalSpace G]
169 (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
170 (quotientMapOfLECont (G := G) M N hMN).toMonoidHom =
171 quotientMapOfLE (G := G) M N hMN :=
172 by
173 ext g
174 change quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk' M g) =
175 quotientMapOfLE (G := G) M N hMN (QuotientGroup.mk' M g)
177 (QuotientGroup.mapₜ_apply_mk
178 (N := M) (M := N) (f := ContinuousMonoidHom.id G)
179 (hNM := by
180 intro g hg
181 exact hMN hg) g)
183/-- Evaluation of the continuous quotient map induced by inclusion on a quotient class. -/
185 {G : Type u} [Group G] [TopologicalSpace G]
186 (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) (g : G) :
187 quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk g) = QuotientGroup.mk g := by
188 change quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk' M g) =
189 QuotientGroup.mk' N g
190 simpa [quotientMapOfLECont] using
191 (QuotientGroup.mapₜ_apply_mk
192 (N := M) (M := N) (f := ContinuousMonoidHom.id G)
193 (hNM := by
194 intro g hg
195 exact hMN hg) g)
197/-- The canonical map from `G/(U ∩ V)` to the concrete pullback of `G/U` and `G/V` over
198`G/(UV)`. -/
199noncomputable def quotientInfToPullback :
200 G ⧸ (U ⊓ V) →*
201 FiberProduct.carrier (quotientToSupLeft (G := G) U V) (quotientToSupRight (G := G) U V) := by
202 refine FiberProduct.lift
203 (quotientToSupLeft (G := G) U V)
204 (quotientToSupRight (G := G) U V)
205 (quotientInfToLeft (G := G) U V)
206 (quotientInfToRight (G := G) U V) ?_
207 intro x
208 refine Quotient.inductionOn x ?_
209 intro g
210 rfl
212/-- Evaluation formula for the canonical quotient-to-pullback map. -/
213@[simp] theorem quotientInfToPullback_mk (g : G) :
214 quotientInfToPullback (G := G) U V (QuotientGroup.mk g) =
215 ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩ := by
216 rfl
218/-- The first projection of the quotient-to-pullback map is the natural quotient map to `G/U`. -/
220 (FiberProduct.fst _ _).comp
221 (quotientInfToPullback (G := G) U V) =
222 quotientInfToLeft (G := G) U V := by
223 apply MonoidHom.ext
224 intro x
225 refine Quotient.inductionOn' x ?_
226 intro g
227 rfl
229/-- The second projection of the quotient-to-pullback map is the natural quotient map to `G/V`. -/
231 (FiberProduct.snd _ _).comp
232 (quotientInfToPullback (G := G) U V) =
233 quotientInfToRight (G := G) U V := by
234 apply MonoidHom.ext
235 intro x
236 refine Quotient.inductionOn' x ?_
237 intro g
238 rfl
240/-- Injectivity of the canonical quotient-to-pullback map. -/
242 Function.Injective (quotientInfToPullback (G := G) U V) := by
243 intro x y hxy
244 revert hxy
245 refine Quotient.inductionOn₂' x y ?_
246 intro g h hEq
247 apply QuotientGroup.eq.2
248 have hU :
249 QuotientGroup.mk' U g = QuotientGroup.mk' U h := by
251 congrArg (fun z => FiberProduct.fst _ _ z) hEq
252 have hV :
253 QuotientGroup.mk' V g = QuotientGroup.mk' V h := by
255 congrArg (fun z => FiberProduct.snd _ _ z) hEq
256 exact ⟨QuotientGroup.eq.1 hU, QuotientGroup.eq.1 hV⟩
258/-- Surjectivity of the canonical quotient-to-pullback map. -/
260 Function.Surjective (quotientInfToPullback (G := G) U V) := by
261 intro x
262 rcases QuotientGroup.mk'_surjective U x.1.1 with ⟨a, ha⟩
263 rcases QuotientGroup.mk'_surjective V x.1.2 with ⟨b, hb⟩
264 have hsup :
265 QuotientGroup.mk' (U ⊔ V) a = QuotientGroup.mk' (U ⊔ V) b := by
266 calc
267 QuotientGroup.mk' (U ⊔ V) a =
268 quotientToSupLeft (G := G) U V x.1.1 := by
269 rw [← ha]
270 rfl
271 _ = quotientToSupRight (G := G) U V x.1.2 := x.2
272 _ = QuotientGroup.mk' (U ⊔ V) b := by
273 rw [← hb]
274 rfl
275 have hab : a⁻¹ * b ∈ U ⊔ V := QuotientGroup.eq.1 hsup
276 rcases (Subgroup.mem_sup_of_normal_right (s := U) (t := V)).1 hab with
277 ⟨u, hu, v, hv, huv⟩
278 have hb_eq : b = (a * u) * v := by
279 calc
280 b = a * (a⁻¹ * b) := by simp only [mul_inv_cancel_left]
281 _ = a * (u * v) := by rw [← huv]
282 _ = (a * u) * v := by simp only [mul_assoc]
283 have hU : QuotientGroup.mk' U (a * u) = QuotientGroup.mk' U a := by
284 symm
285 apply QuotientGroup.eq.2
286 have hmem : a⁻¹ * (a * u) = u := by simp only [inv_mul_cancel_left]
287 simpa [hmem] using hu
288 have hV : QuotientGroup.mk' V (a * u) = QuotientGroup.mk' V b := by
289 apply QuotientGroup.eq.2
290 have hmem : (a * u)⁻¹ * b = v := by
291 calc
292 (a * u)⁻¹ * b = (a * u)⁻¹ * ((a * u) * v) := by rw [hb_eq]
293 _ = v := by simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
294 rw [hmem]
295 exact hv
296 refine ⟨QuotientGroup.mk' (U ⊓ V) (a * u), ?_⟩
297 apply Subtype.ext
298 apply Prod.ext
299 · calc
301 (QuotientGroup.mk' (U ⊓ V) (a * u))).1.1 =
302 QuotientGroup.mk' U (a * u) := rfl
303 _ = QuotientGroup.mk' U a := hU
304 _ = x.1.1 := ha
305 · calc
307 (QuotientGroup.mk' (U ⊓ V) (a * u))).1.2 =
308 QuotientGroup.mk' V (a * u) := rfl
309 _ = QuotientGroup.mk' V b := hV
310 _ = x.1.2 := hb
312/-- The canonical quotient-to-pullback map is bijective. -/
314 Function.Bijective (quotientInfToPullback (G := G) U V) := by
315 exact ⟨quotientInfToPullback_injective (G := G) U V,
318/-- The quotient square is canonically isomorphic to the pullback. -/
319noncomputable def quotientInfPullbackEquiv :
320 G ⧸ (U ⊓ V) ≃*
321 FiberProduct.carrier (quotientToSupLeft (G := G) U V) (quotientToSupRight (G := G) U V) :=
322 MulEquiv.ofBijective (quotientInfToPullback (G := G) U V)
325/-- The first coordinate of the quotient pullback equivalence is the natural map to `G/U`. -/
327 (FiberProduct.fst _ _).comp (quotientInfPullbackEquiv (G := G) U V).toMonoidHom =
328 quotientInfToLeft (G := G) U V := by
329 change (FiberProduct.fst _ _).comp (quotientInfToPullback (G := G) U V) =
330 quotientInfToLeft (G := G) U V
333/-- The second coordinate of the quotient pullback equivalence is the natural map to `G/V`. -/
335 (FiberProduct.snd _ _).comp (quotientInfPullbackEquiv (G := G) U V).toMonoidHom =
336 quotientInfToRight (G := G) U V := by
337 change (FiberProduct.snd _ _).comp (quotientInfToPullback (G := G) U V) =
338 quotientInfToRight (G := G) U V
341/-- The quotient square is a pullback square. -/
343 IsPullbackSquare
344 (quotientInfToLeft (G := G) U V)
345 (quotientInfToRight (G := G) U V)
346 (quotientToSupLeft (G := G) U V)
347 (quotientToSupRight (G := G) U V) := by
349 (quotientInfToLeft (G := G) U V)
350 (quotientInfToRight (G := G) U V)
351 (quotientToSupLeft (G := G) U V)
352 (quotientToSupRight (G := G) U V)
353 (quotientInfToPullback (G := G) U V)
358section
360variable [TopologicalSpace G]
362section ProfiniteQuotients
364variable [IsTopologicalGroup G]
366omit [U.Normal] in
367/-- In a profinite group, the join of two closed normal subgroups is closed.
368This is the compactness input needed for the lower-right quotient in the quotient-pullback square. -/
369theorem isClosed_sup_of_normal
371 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
372 IsClosed ((U ⊔ V : Subgroup G) : Set G) := by
373 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
374 letI : T2Space G := IsProfiniteGroup.t2Space hG
375 exact Subgroup.isClosed_sup_of_normal U V hUclosed hVclosed
377end ProfiniteQuotients
379/-- The left map in the continuous quotient square . -/
380def quotientInfToLeftCont : G ⧸ (U ⊓ V) →ₜ* G ⧸ U :=
381 quotientMapOfLECont (G := G) (U ⊓ V) U inf_le_left
383/-- The right map in the continuous quotient square . -/
384def quotientInfToRightCont : G ⧸ (U ⊓ V) →ₜ* G ⧸ V :=
385 quotientMapOfLECont (G := G) (U ⊓ V) V inf_le_right
387/-- The bottom-left map in the continuous quotient square . -/
388def quotientToSupLeftCont : G ⧸ U →ₜ* G ⧸ (U ⊔ V) :=
389 quotientMapOfLECont (G := G) U (U ⊔ V) le_sup_left
391/-- The bottom-right map in the continuous quotient square . -/
392def quotientToSupRightCont : G ⧸ V →ₜ* G ⧸ (U ⊔ V) :=
393 quotientMapOfLECont (G := G) V (U ⊔ V) le_sup_right
395/-- Forgetting continuity from the left continuous quotient-square map recovers the
396algebraic map. -/
398 (quotientInfToLeftCont (G := G) U V).toMonoidHom = quotientInfToLeft (G := G) U V :=
399 rfl
401/-- Forgetting continuity from the right continuous quotient-square map recovers the
402algebraic map. -/
404 (quotientInfToRightCont (G := G) U V).toMonoidHom = quotientInfToRight (G := G) U V :=
405 rfl
407/-- Forgetting continuity from the lower-left continuous quotient-square map recovers the
408algebraic map. -/
410 (quotientToSupLeftCont (G := G) U V).toMonoidHom = quotientToSupLeft (G := G) U V :=
411 rfl
413/-- Forgetting continuity from the lower-right continuous quotient-square map recovers the
414algebraic map. -/
416 (quotientToSupRightCont (G := G) U V).toMonoidHom = quotientToSupRight (G := G) U V :=
417 rfl
419/-- Evaluation of the left continuous quotient-square map on a quotient class. -/
420@[simp] theorem quotientInfToLeftCont_mk (g : G) :
421 quotientInfToLeftCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g := by
424/-- Evaluation of the right continuous quotient-square map on a quotient class. -/
425@[simp] theorem quotientInfToRightCont_mk (g : G) :
426 quotientInfToRightCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g := by
429/-- Evaluation of the lower-left continuous quotient-square map on a quotient class. -/
430@[simp] theorem quotientToSupLeftCont_mk (g : G) :
431 quotientToSupLeftCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g := by
434/-- Evaluation of the lower-right continuous quotient-square map on a quotient class. -/
435@[simp] theorem quotientToSupRightCont_mk (g : G) :
436 quotientToSupRightCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g := by
439variable [IsTopologicalGroup G]
441/-- The canonical continuous map from `G/(U ∩ V)` to the concrete continuous pullback of
442`G/U` and `G/V` over `G/(UV)`. -/
444 G ⧸ (U ⊓ V) →ₜ*
445 TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V) (quotientToSupRightCont (G := G) U V) := by
446 refine TopologicalFiberProduct.lift
447 (quotientToSupLeftCont (G := G) U V)
449 (quotientInfToLeftCont (G := G) U V)
450 (quotientInfToRightCont (G := G) U V) ?_
451 intro x
452 refine Quotient.inductionOn x ?_
453 intro g
454 rfl
456omit [IsTopologicalGroup G] in
457/--
458Forgetting continuity from the continuous quotient-to-pullback map recovers the algebraic one.
459-/
461 (quotientInfToContinuousPullback (G := G) U V).toMonoidHom =
462 quotientInfToPullback (G := G) U V := by
463 apply MonoidHom.ext
464 intro x
465 refine Quotient.inductionOn' x ?_
466 intro g
467 exact Subtype.ext <| Prod.ext rfl rfl
469omit [IsTopologicalGroup G] in
470/-- Evaluation formula for the continuous quotient-to-pullback map. -/
471@[simp] theorem quotientInfToContinuousPullback_mk (g : G) :
472 quotientInfToContinuousPullback (G := G) U V (QuotientGroup.mk g) =
473 ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩ := by
474 rfl
476omit [IsTopologicalGroup G] in
477/-- The first projection of the continuous quotient-to-pullback map is the natural quotient map to
478`G/U`. -/
480 (TopologicalFiberProduct.fst _ _).comp (quotientInfToContinuousPullback (G := G) U V) =
481 quotientInfToLeftCont (G := G) U V := by
482 apply ContinuousMonoidHom.ext
483 intro x
484 refine Quotient.inductionOn' x ?_
485 intro g
486 rfl
488omit [IsTopologicalGroup G] in
489/-- The second projection of the continuous quotient-to-pullback map is the natural quotient map to
490`G/V`. -/
492 (TopologicalFiberProduct.snd _ _).comp (quotientInfToContinuousPullback (G := G) U V) =
493 quotientInfToRightCont (G := G) U V := by
494 apply ContinuousMonoidHom.ext
495 intro x
496 refine Quotient.inductionOn' x ?_
497 intro g
498 rfl
500omit [IsTopologicalGroup G] in
501/-- Injectivity of the continuous quotient-to-pullback map on the underlying groups. -/
503 Function.Injective (quotientInfToContinuousPullback (G := G) U V) := by
504 intro x y hxy
505 exact quotientInfToPullback_injective (G := G) U V <| by
506 simpa using hxy
508omit [IsTopologicalGroup G] in
509/-- Surjectivity of the continuous quotient-to-pullback map on the underlying groups. -/
511 Function.Surjective (quotientInfToContinuousPullback (G := G) U V) := by
512 intro x
513 rcases quotientInfToPullback_surjective (G := G) U V x with ⟨y, hy⟩
514 refine ⟨y, ?_⟩
515 simpa using hy
517omit [IsTopologicalGroup G] in
518/-- The continuous quotient-to-pullback map is bijective on the underlying groups. -/
520 Function.Bijective (quotientInfToContinuousPullback (G := G) U V) := by
524/-- The quotient square is canonically isomorphic to the concrete profinite pullback. -/
526 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
527 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
528 G ⧸ (U ⊓ V) ≃ₜ*
529 TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V) (quotientToSupRightCont (G := G) U V) := by
530 let hG : IsProfiniteGroup G :=
531 ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
532 let hInfClosed : IsClosed (((U ⊓ V : Subgroup G) : Set G)) := hUclosed.inter hVclosed
533 let hSupClosed : IsClosed (((U ⊔ V : Subgroup G) : Set G)) :=
534 Subgroup.isClosed_sup_of_normal U V hUclosed hVclosed
535 let hQuotInf : IsProfiniteGroup (G ⧸ (U ⊓ V)) :=
537 let hQuotU : IsProfiniteGroup (G ⧸ U) :=
539 let hQuotV : IsProfiniteGroup (G ⧸ V) :=
541 let hQuotSup : IsProfiniteGroup (G ⧸ (U ⊔ V)) :=
543 let hPull :
545 (TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V) (quotientToSupRightCont (G := G) U V)) :=
546 TopologicalFiberProduct.isProfiniteGroup
547 (quotientToSupLeftCont (G := G) U V)
549 hQuotU hQuotV hQuotSup
550 letI : CompactSpace (G ⧸ (U ⊓ V)) := IsProfiniteGroup.compactSpace hQuotInf
551 letI : T2Space
552 (TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V) (quotientToSupRightCont (G := G) U V)) :=
553 IsProfiniteGroup.t2Space hPull
554 exact ContinuousMulEquiv.ofBijectiveCompactToT2
556 (quotientInfToContinuousPullback (G := G) U V).continuous_toFun
559/-- The quotient pullback equivalence is induced by the canonical comparison map.
560-/
562 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
563 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
565 (G := G) (U := U) (V := V) hUclosed hVclosed).toContinuousMonoidHom =
567 apply ContinuousMonoidHom.ext
568 intro x
569 exact Subtype.ext <| Prod.ext rfl rfl
571/-- Evaluation formula for the continuous quotient pullback equivalence on a quotient class.
572-/
574 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
575 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) (g : G) :
576 quotientInfContinuousPullbackEquiv (G := G) (U := U) (V := V) hUclosed hVclosed
577 (QuotientGroup.mk g) = ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩ := by
578 change quotientInfToContinuousPullback (G := G) U V (QuotientGroup.mk g) = _
581/--
582The first coordinate of the continuous quotient pullback equivalence is the natural map to `G/U`.
583-/
585 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
586 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
587 (TopologicalFiberProduct.fst _ _).comp
589 (G := G) (U := U) (V := V) hUclosed hVclosed).toContinuousMonoidHom =
590 quotientInfToLeftCont (G := G) U V := by
592 (G := G) (U := U) (V := V) hUclosed hVclosed]
595/--
596The second coordinate of the continuous quotient pullback equivalence is the natural map to `G/V`.
597-/
599 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
600 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
601 (TopologicalFiberProduct.snd _ _).comp
603 (G := G) (U := U) (V := V) hUclosed hVclosed).toContinuousMonoidHom =
604 quotientInfToRightCont (G := G) U V := by
606 (G := G) (U := U) (V := V) hUclosed hVclosed]
609/-- The quotient square is a pullback square in the category of profinite groups. -/
611 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
612 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
614 (quotientInfToLeftCont (G := G) U V)
616 (quotientToSupLeftCont (G := G) U V)
617 (quotientToSupRightCont (G := G) U V) := by
619 (quotientInfToLeftCont (G := G) U V)
621 (quotientToSupLeftCont (G := G) U V)
623 (quotientInfContinuousPullbackEquiv (G := G) (U := U) (V := V) hUclosed hVclosed)
624 (quotientInfContinuousPullbackEquiv_fst (G := G) (U := U) (V := V) hUclosed hVclosed)
625 (quotientInfContinuousPullbackEquiv_snd (G := G) (U := U) (V := V) hUclosed hVclosed)
627namespace QuotientPullback
629omit [TopologicalSpace G] [IsTopologicalGroup G] in
630@[simp] theorem infToLeft_mk (g : G) :
631 quotientInfToLeft (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g :=
632 rfl
634omit [TopologicalSpace G] [IsTopologicalGroup G] in
635@[simp] theorem infToRight_mk (g : G) :
636 quotientInfToRight (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g :=
637 rfl
639omit [TopologicalSpace G] [IsTopologicalGroup G] in
640@[simp] theorem leftToSup_mk (g : G) :
641 quotientToSupLeft (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g :=
642 rfl
644omit [TopologicalSpace G] [IsTopologicalGroup G] in
645@[simp] theorem rightToSup_mk (g : G) :
646 quotientToSupRight (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk g :=
647 rfl
649omit [TopologicalSpace G] [IsTopologicalGroup G] in
650@[simp] theorem comparison_apply_mk (g : G) :
651 quotientInfToPullback (G := G) U V (QuotientGroup.mk g) =
652 ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩ :=
655omit [TopologicalSpace G] [IsTopologicalGroup G] in
657 Function.Bijective (quotientInfToPullback (G := G) U V) :=
660omit [TopologicalSpace G] [IsTopologicalGroup G] in
661/-- Namespaced form of the algebraic quotient-pullback theorem. -/
662theorem isPullback :
663 IsPullbackSquare
664 (quotientInfToLeft (G := G) U V)
665 (quotientInfToRight (G := G) U V)
666 (quotientToSupLeft (G := G) U V)
667 (quotientToSupRight (G := G) U V) :=
668 quotientInf_isPullback (G := G) (U := U) (V := V)
670theorem hasProfiniteTestPullbackProperty
671 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
672 (hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
674 (quotientInfToLeftCont (G := G) U V)
676 (quotientToSupLeftCont (G := G) U V)
677 (quotientToSupRightCont (G := G) U V) :=
678 quotientInf_hasProfiniteTestPullbackProperty (G := G) (U := U) (V := V) hUclosed hVclosed
680end QuotientPullback
682end
683end ProCGroups.Categorical