Source: ProCGroups.Topologies.QuotientMaps
1import Mathlib.Topology.Algebra.Group.Quotient
2import ProCGroups.Topologies.ContinuousMulEquiv
4/-!
5# Continuous maps between group quotients
7This file develops algebraic and continuous equivalences induced by surjective homomorphisms,
8lifts and maps between quotient groups, congruences between quotients, and restrictions to
9preimages of subgroups.
10-/
12open scoped Topology
14universe u v
16namespace ProCGroups
18namespace QuotientGroup
20section Algebra
22variable {G : Type u} {H : Type v} [Group G] [Group H]
24/--
25The comap of a quotient subgroup is determined by the representative-level map when the kernel
26condition holds.
27-/
28theorem comap_eq_of_map_eq_of_ker_le
29 (f : G →* H) {N : Subgroup G} {M : Subgroup H}
30 (hmap : N.map f = M) (hker : f.ker ≤ N) :
31 M.comap f = N := by
32 calc
33 M.comap f = (N.map f).comap f := by simp only [hmap]
34 _ = N ⊔ f.ker := by simpa using (Subgroup.comap_map_eq (f := f) (H := N))
35 _ = N := sup_eq_left.2 hker
37/--
38Under the kernel condition, the induced quotient map has trivial kernel for the corresponding
39representative-level map.
40-/
41private theorem map_ker_eq_bot_of_map_eq_of_ker_le
42 (f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
43 (hNM : N ≤ M.comap f) (hmap : N.map f = M) (hker : f.ker ≤ N) :
44 (QuotientGroup.map (N := N) (M := M) (f := f) hNM).ker = ⊥ := by
45 have hcomap : M.comap f = N := comap_eq_of_map_eq_of_ker_le f hmap hker
46 calc
47 (QuotientGroup.map (N := N) (M := M) (f := f) hNM).ker =
48 Subgroup.map (QuotientGroup.mk' N) (Subgroup.comap f M) := by
49 simpa using QuotientGroup.ker_map (N := N) (M := M) (f := f) hNM
50 _ = Subgroup.map (QuotientGroup.mk' N) N := by simp only [hcomap,
51 _root_.QuotientGroup.map_mk'_self]
52 _ = ⊥ := by
53 refine (Subgroup.map_eq_bot_iff (f := QuotientGroup.mk' N) (H := N)).2 ?_
54 intro x hx
55 simpa using hx
57/--
58A surjective homomorphism induces an isomorphism on quotients whenever it maps the source normal
59subgroup onto the target normal subgroup and its kernel is contained in the source normal
60subgroup.
61-/
62noncomputable def mapMulEquivOfSurjective
63 (f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
64 (hf : Function.Surjective f) (hmap : N.map f = M) (hker : f.ker ≤ N) :
65 G ⧸ N ≃* H ⧸ M := by
66 have hNM : N ≤ M.comap f := by
67 intro x hx
68 change f x ∈ M
69 simpa [hmap] using (show f x ∈ N.map f from ⟨x, hx, rfl⟩)
70 let φ : G ⧸ N →* H ⧸ M :=
71 QuotientGroup.map (N := N) (M := M) (f := f) hNM
72 have hsurj : Function.Surjective φ := by
73 intro y
74 obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective M y
75 rcases hf h with ⟨g, rfl⟩
76 exact ⟨QuotientGroup.mk' N g, rfl⟩
77 have hkerφ : φ.ker = ⊥ := by
78 dsimp [φ]
79 exact map_ker_eq_bot_of_map_eq_of_ker_le (f := f) hNM hmap hker
80 have hinj : Function.Injective φ :=
81 (MonoidHom.ker_eq_bot_iff (f := φ)).1 hkerφ
82 exact MulEquiv.ofBijective φ ⟨hinj, hsurj⟩
84/-- A surjective homomorphism induces the expected multiplicative equivalence on quotient groups. -/
85@[simp] theorem mapMulEquivOfSurjective_apply_mk
86 (f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
87 (hf : Function.Surjective f) (hmap : N.map f = M) (hker : f.ker ≤ N) (g : G) :
88 mapMulEquivOfSurjective (G := G) (H := H) f hf hmap hker (QuotientGroup.mk' N g) =
89 QuotientGroup.mk' M (f g) := by
90 rfl
92end Algebra
94section Topology
96variable {G : Type u} {H : Type v}
97variable [Group G] [TopologicalSpace G]
98variable [Group H] [TopologicalSpace H]
100/-- The lifted continuous quotient map is induced by the quotient universal property. -/
101def liftₜ
102 (N : Subgroup G) [N.Normal] (f : G →ₜ* H)
103 (hN : N ≤ f.toMonoidHom.ker) :
104 G ⧸ N →ₜ* H := by
105 let φ : G ⧸ N →* H := QuotientGroup.lift N f.toMonoidHom hN
106 have hcomp : Continuous (fun x : G => φ (QuotientGroup.mk' N x)) := by
107 simpa [φ, QuotientGroup.lift_mk'] using f.continuous_toFun
108 have hcont : Continuous φ :=
109 (QuotientGroup.isQuotientMap_mk (G := G) (N := N)).continuous_iff.2 hcomp
110 exact
111 { toMonoidHom := φ
112 continuous_toFun := hcont }
114/-- The continuous homomorphism induced on quotients by a continuous homomorphism. -/
115def mapContinuousMonoidHom
116 (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
117 (hNM : N ≤ M.comap f.toMonoidHom) :
118 G ⧸ N →ₜ* H ⧸ M := by
119 let φ : G ⧸ N →* H ⧸ M :=
120 QuotientGroup.map (N := N) (M := M) (f := f.toMonoidHom) hNM
121 have hcomp : Continuous (fun x : G => φ (QuotientGroup.mk' N x)) := by
122 dsimp [φ]
123 exact continuous_quotient_mk'.comp f.continuous_toFun
124 have hcont : Continuous φ :=
125 (QuotientGroup.isQuotientMap_mk (G := G) (N := N)).continuous_iff.2 hcomp
126 exact
127 { toMonoidHom := φ
128 continuous_toFun := hcont }
130/-- Continuous version of the quotient-group map. -/
131def mapₜ
132 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
133 (f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) :
134 G ⧸ N →ₜ* H ⧸ M :=
135 mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNM
137/-- Continuous equivalence between quotients induced by a continuous multiplicative equivalence. -/
138noncomputable def congrₜ
139 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
140 (e : G ≃ₜ* H) (h : N.map e.toMulEquiv.toMonoidHom = M) :
141 G ⧸ N ≃ₜ* H ⧸ M := by
142 let eAlg : G ⧸ N ≃* H ⧸ M :=
143 QuotientGroup.congr (G' := N) (H' := M) e.toMulEquiv h
144 refine
145 { toMulEquiv := eAlg
146 continuous_toFun := ?_
147 continuous_invFun := ?_ }
148 · refine (QuotientGroup.isQuotientMap_mk N).continuous_iff.2 ?_
149 change Continuous fun x : G => QuotientGroup.mk' M (e x)
150 exact continuous_quotient_mk'.comp e.continuous_toFun
151 · refine (QuotientGroup.isQuotientMap_mk M).continuous_iff.2 ?_
152 have hsymm : M.map e.symm.toMulEquiv.toMonoidHom = N :=
153 (Subgroup.map_symm_eq_iff_map_eq (K := N) (H := M) (e := e.toMulEquiv)).mpr h
154 change Continuous fun y : H => QuotientGroup.mk' N (e.symm y)
155 exact continuous_quotient_mk'.comp e.symm.continuous_toFun
157/--
158Continuous version of the quotient-group multiplicative equivalence induced by a surjective map.
159The inverse is continuous by compact-to-Hausdorff automatic continuity, so the result is a
160topological-group isomorphism when the source quotient is compact and the target quotient is
161Hausdorff.
162-/
163noncomputable def mapContinuousMulEquivOfSurjective
164 (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
165 [CompactSpace (G ⧸ N)] [T2Space (H ⧸ M)]
166 (hf : Function.Surjective f) (hmap : N.map f.toMonoidHom = M)
167 (hker : f.toMonoidHom.ker ≤ N) :
168 G ⧸ N ≃ₜ* H ⧸ M := by
169 have hNM : N ≤ M.comap f.toMonoidHom := by
170 intro x hx
171 change f x ∈ M
172 rw [← hmap]
173 exact ⟨x, hx, rfl⟩
174 let φ := mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNM
175 have hsurj : Function.Surjective φ := by
176 intro y
177 obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective M y
178 rcases hf h with ⟨g, rfl⟩
179 exact ⟨QuotientGroup.mk' N g, rfl⟩
180 have hkerφ : φ.toMonoidHom.ker = ⊥ := by
181 dsimp [φ, mapContinuousMonoidHom]
182 exact map_ker_eq_bot_of_map_eq_of_ker_le (f := f.toMonoidHom) hNM hmap hker
183 have hinj : Function.Injective φ :=
184 (MonoidHom.ker_eq_bot_iff (f := φ.toMonoidHom)).1 hkerφ
185 exact ContinuousMulEquiv.ofBijectiveCompactToT2
186 φ.toMonoidHom φ.continuous_toFun ⟨hinj, hsurj⟩
188/--
189The lifted continuous quotient map evaluates on quotient classes by applying the underlying map
190to representatives.
191-/
192@[simp] theorem liftₜ_apply_mk
193 (N : Subgroup G) [N.Normal] (f : G →ₜ* H)
194 (hN : N ≤ f.toMonoidHom.ker) (g : G) :
195 liftₜ (G := G) (H := H) N f hN (QuotientGroup.mk' N g) = f g := by
196 rfl
198/-- The monoid homomorphism underlying `liftₜ` is the usual quotient lift. -/
199@[simp] theorem liftₜ_toMonoidHom
200 (N : Subgroup G) [N.Normal] (f : G →ₜ* H)
201 (hN : N ≤ f.toMonoidHom.ker) :
202 (liftₜ (G := G) (H := H) N f hN).toMonoidHom =
203 QuotientGroup.lift N f.toMonoidHom hN := by
204 rfl
206/-- The induced continuous monoid homomorphism sends a quotient class to the class of its image. -/
207@[simp] theorem mapContinuousMonoidHom_apply_mk
208 (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
209 (hNM : N ≤ M.comap f.toMonoidHom) (g : G) :
210 mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNM
211 (QuotientGroup.mk' N g) =
212 QuotientGroup.mk' M (f g) := by
213 rfl
215/-- The continuous quotient map sends the class of \(g\) to the class of \(f(g)\). -/
216@[simp] theorem mapₜ_apply_mk
217 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
218 (f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) (g : G) :
219 mapₜ (G := G) (H := H) N M f hNM (QuotientGroup.mk' N g) =
220 QuotientGroup.mk' M (f g) := by
221 rfl
223/-- The monoid homomorphism underlying `mapₜ` is the usual map between quotient groups. -/
224@[simp] theorem mapₜ_toMonoidHom
225 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
226 (f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) :
227 (mapₜ (G := G) (H := H) N M f hNM).toMonoidHom =
228 QuotientGroup.map (N := N) (M := M) (f := f.toMonoidHom) hNM := by
229 rfl
231/--
232The continuous quotient congruence map evaluates on quotient classes by applying the underlying
233map to representatives.
234-/
235@[simp] theorem congrₜ_apply_mk
236 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
237 (e : G ≃ₜ* H) (h : N.map e.toMulEquiv.toMonoidHom = M) (g : G) :
238 congrₜ (G := G) (H := H) N M e h (QuotientGroup.mk' N g) =
239 QuotientGroup.mk' M (e g) := by
240 rfl
242/--
243The induced continuous multiplicative equivalence sends a quotient class to the class of its
244image.
245-/
246@[simp 900] theorem mapContinuousMulEquivOfSurjective_apply_mk
247 (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
248 [CompactSpace (G ⧸ N)] [T2Space (H ⧸ M)]
249 (hf : Function.Surjective f) (hmap : N.map f.toMonoidHom = M)
250 (hker : f.toMonoidHom.ker ≤ N) (g : G) :
251 mapContinuousMulEquivOfSurjective (G := G) (H := H) f hf hmap hker
252 (QuotientGroup.mk' N g) =
253 QuotientGroup.mk' M (f g) := by
254 rfl
256end Topology
258end QuotientGroup
260namespace ContinuousMonoidHom
262section RestrictPreimage
264variable {G : Type u} {Q : Type v}
265variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
266variable [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
268/-- A continuous homomorphism restricts to the preimage of a subgroup of the target. -/
269def restrictPreimage (f : G →ₜ* Q) (H : Subgroup Q) :
270 (H.comap f.toMonoidHom) →ₜ* H := by
271 refine
272 { toMonoidHom :=
273 { toFun := fun x => ⟨f x.1, x.2⟩
274 map_one' := by
275 ext
276 simp only [_root_.ContinuousMonoidHom.coe_toMonoidHom, OneMemClass.coe_one, map_one]
277 map_mul' := by
278 intro x y
279 ext
280 exact f.map_mul x.1 y.1}
281 continuous_toFun := by
282 have hcont : Continuous (fun x : H.comap f.toMonoidHom => f x.1) :=
283 f.continuous.comp continuous_subtype_val
284 exact hcont.subtype_mk (by intro x; exact x.2) }
286omit [IsTopologicalGroup G] [IsTopologicalGroup Q] in
287/-- The restriction to a subgroup preimage is surjective if the original map is surjective. -/
288theorem restrictPreimage_surjective (f : G →ₜ* Q) (hf : Function.Surjective f)
289 (H : Subgroup Q) :
290 Function.Surjective (restrictPreimage f H) := by
291 intro y
292 rcases hf y.1 with ⟨x, hx⟩
293 refine ⟨⟨x, ?_⟩, ?_⟩
294 · change f x ∈ H
295 simp only [hx, SetLike.coe_mem]
296 · exact Subtype.ext hx
298omit [IsTopologicalGroup G] [IsTopologicalGroup Q] in
299/-- The kernel of the restriction to a subgroup preimage is detected by the ambient map. -/
300theorem restrictPreimage_eq_one_iff {f : G →ₜ* Q} {H : Subgroup Q}
301 {x : H.comap f.toMonoidHom} :
302 restrictPreimage f H x = 1 ↔ f x.1 = 1 := by
303 constructor
304 · intro hx
305 exact congrArg Subtype.val hx
306 · intro hx
307 exact Subtype.ext hx
309/--
310If the restricted map sends \(N\) onto \(M\) and its kernel is contained in \(N\), then the
311induced quotient map is an isomorphism.
312-/
313noncomputable def preimageSubgroupQuotientMulEquivOfSurjective
314 (f : G →ₜ* Q) (hf : Function.Surjective f) (H : Subgroup Q)
315 {N : Subgroup (H.comap f.toMonoidHom)} {M : Subgroup H} [N.Normal] [M.Normal]
316 (hmap : N.map (restrictPreimage f H).toMonoidHom = M)
317 (hker : (restrictPreimage f H).toMonoidHom.ker ≤ N) :
318 (H.comap f.toMonoidHom) ⧸ N ≃* H ⧸ M :=
319 QuotientGroup.mapMulEquivOfSurjective
320 (restrictPreimage f H).toMonoidHom
321 (restrictPreimage_surjective f hf H) hmap hker
323end RestrictPreimage
325end ContinuousMonoidHom
327end ProCGroups