Yamaguchi Lean 4 Library
ProCGroups/Topologies/QuotientMaps.lean
ProCGroups/Topologies/QuotientMaps/Source

ProCGroups/Topologies/QuotientMaps.lean

1import Mathlib.Topology.Algebra.Group.Quotient
2import ProCGroups.Topologies.ContinuousMulEquiv
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Topologies/QuotientMaps.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Topological group constructions
15Topological subgroup, quotient, continuous homomorphism, continuous equivalence, conjugation, and full-subgroup-topology lemmas.
16-/
18open scoped Topology
20universe u v
22namespace QuotientGroup
24section Algebra
26variable {G : Type u} {H : Type v} [Group G] [Group H]
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
38 (f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
39 (hNM : N ≤ M.comap f) (hmap : N.map f = M) (hker : f.ker ≤ N) :
40 (QuotientGroup.map (N := N) (M := M) (f := f) hNM).ker = ⊥ := by
41 have hcomap : M.comap f = N := comap_eq_of_map_eq_of_ker_le f hmap hker
42 calc
43 (QuotientGroup.map (N := N) (M := M) (f := f) hNM).ker =
44 Subgroup.map (QuotientGroup.mk' N) (Subgroup.comap f M) := by
45 simpa using QuotientGroup.ker_map (N := N) (M := M) (f := f) hNM
46 _ = Subgroup.map (QuotientGroup.mk' N) N := by simp only [hcomap, map_mk'_self]
47 _ = ⊥ := by
48 refine (Subgroup.map_eq_bot_iff (f := QuotientGroup.mk' N) (H := N)).2 ?_
49 intro x hx
50 simpa using hx
52/-- A surjective homomorphism induces an isomorphism on quotients whenever it maps the source
53normal subgroup onto the target normal subgroup and its kernel is contained in the source normal
54subgroup.
56This is the algebraic core behind the usual snake-lemma argument for quotient diagrams. -/
57noncomputable def mapMulEquivOfSurjective
58 (f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
59 (hf : Function.Surjective f) (hmap : N.map f = M) (hker : f.ker ≤ N) :
60 G ⧸ N ≃* H ⧸ M := by
61 have hNM : N ≤ M.comap f := by
62 intro x hx
63 change f x ∈ M
64 simpa [hmap] using (show f x ∈ N.map f from ⟨x, hx, rfl⟩)
65 let φ : G ⧸ N →* H ⧸ M :=
66 QuotientGroup.map (N := N) (M := M) (f := f) hNM
67 have hsurj : Function.Surjective φ := by
68 intro y
69 obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective M y
70 rcases hf h with ⟨g, rfl⟩
71 exact ⟨QuotientGroup.mk' N g, rfl⟩
72 have hkerφ : φ.ker = ⊥ := by
73 dsimp [φ]
74 exact map_ker_eq_bot_of_map_eq_of_ker_le (f := f) hNM hmap hker
75 have hinj : Function.Injective φ :=
76 (MonoidHom.ker_eq_bot_iff (f := φ)).1 hkerφ
77 exact MulEquiv.ofBijective φ ⟨hinj, hsurj⟩
80 (f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
81 (hf : Function.Surjective f) (hmap : N.map f = M) (hker : f.ker ≤ N) (g : G) :
82 mapMulEquivOfSurjective (G := G) (H := H) f hf hmap hker (QuotientGroup.mk' N g) =
83 QuotientGroup.mk' M (f g) := by
84 rfl
86end Algebra
88section Topology
90variable {G : Type u} {H : Type v}
91variable [Group G] [TopologicalSpace G]
92variable [Group H] [TopologicalSpace H]
94/-- Continuous version of `QuotientGroup.lift`. -/
96 (N : Subgroup G) [N.Normal] (f : G →ₜ* H)
97 (hN : N ≤ f.toMonoidHom.ker) :
98 G ⧸ N →ₜ* H := by
99 let φ : G ⧸ N →* H := QuotientGroup.lift N f.toMonoidHom hN
100 have hcomp : Continuous (fun x : G => φ (QuotientGroup.mk' N x)) := by
101 simpa [φ, QuotientGroup.lift_mk'] using f.continuous_toFun
102 have hcont : Continuous φ :=
103 (QuotientGroup.isQuotientMap_mk (G := G) (N := N)).continuous_iff.2 hcomp
104 exact
105 { toMonoidHom := φ
106 continuous_toFun := hcont }
108/-- The continuous homomorphism induced on quotients by a continuous homomorphism. -/
110 (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
111 (hNM : N ≤ M.comap f.toMonoidHom) :
112 G ⧸ N →ₜ* H ⧸ M := by
113 let φ : G ⧸ N →* H ⧸ M :=
114 QuotientGroup.map (N := N) (M := M) (f := f.toMonoidHom) hNM
115 have hcomp : Continuous (fun x : G => φ (QuotientGroup.mk' N x)) := by
116 dsimp [φ]
117 exact continuous_quotient_mk'.comp f.continuous_toFun
118 have hcont : Continuous φ :=
119 (QuotientGroup.isQuotientMap_mk (G := G) (N := N)).continuous_iff.2 hcomp
120 exact
121 { toMonoidHom := φ
122 continuous_toFun := hcont }
124/-- Continuous version of `QuotientGroup.map`. -/
126 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
127 (f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) :
128 G ⧸ N →ₜ* H ⧸ M :=
129 mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNM
131/-- Continuous equivalence between quotients induced by a continuous multiplicative equivalence. -/
132noncomputable def congrₜ
133 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
134 (e : G ≃ₜ* H) (h : N.map e.toMulEquiv.toMonoidHom = M) :
135 G ⧸ N ≃ₜ* H ⧸ M := by
136 let eAlg : G ⧸ N ≃* H ⧸ M :=
137 QuotientGroup.congr (G' := N) (H' := M) e.toMulEquiv h
138 refine
139 { toMulEquiv := eAlg
140 continuous_toFun := ?_
141 continuous_invFun := ?_ }
142 · refine (QuotientGroup.isQuotientMap_mk N).continuous_iff.2 ?_
143 change Continuous fun x : G => eAlg (QuotientGroup.mk' N x)
144 simpa [eAlg, QuotientGroup.congr_mk'] using
145 (continuous_quotient_mk'.comp e.continuous_toFun)
146 · refine (QuotientGroup.isQuotientMap_mk M).continuous_iff.2 ?_
147 change Continuous fun y : H => eAlg.symm (QuotientGroup.mk' M y)
148 have hsymm : M.map e.symm.toMulEquiv.toMonoidHom = N :=
149 (Subgroup.map_symm_eq_iff_map_eq (K := N) (H := M) (e := e.toMulEquiv)).mpr h
150 simpa [eAlg, hsymm, QuotientGroup.congr_symm, QuotientGroup.congr_mk'] using
151 (continuous_quotient_mk'.comp e.symm.continuous_toFun)
153/-- Continuous version of `QuotientGroup.mapMulEquivOfSurjective`. The inverse is continuous by
154compact-to-Hausdorff automatic continuity, so the result is a topological-group isomorphism when the
155source quotient is compact and the target quotient is Hausdorff. -/
157 (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
158 [CompactSpace (G ⧸ N)] [T2Space (H ⧸ M)]
159 (hf : Function.Surjective f) (hmap : N.map f.toMonoidHom = M)
160 (hker : f.toMonoidHom.ker ≤ N) :
161 G ⧸ N ≃ₜ* H ⧸ M := by
162 have hNM : N ≤ M.comap f.toMonoidHom := by
163 intro x hx
164 change f x ∈ M
165 rw [← hmap]
166 exact ⟨x, hx, rfl⟩
167 let φ := mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNM
168 have hsurj : Function.Surjective φ := by
169 intro y
170 obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective M y
171 rcases hf h with ⟨g, rfl⟩
172 exact ⟨QuotientGroup.mk' N g, rfl⟩
173 have hkerφ : φ.toMonoidHom.ker = ⊥ := by
175 exact map_ker_eq_bot_of_map_eq_of_ker_le (f := f.toMonoidHom) hNM hmap hker
176 have hinj : Function.Injective φ :=
177 (MonoidHom.ker_eq_bot_iff (f := φ.toMonoidHom)).1 hkerφ
178 exact ContinuousMulEquiv.ofBijectiveCompactToT2
179 φ.toMonoidHom φ.continuous_toFun ⟨hinj, hsurj⟩
181@[simp] theorem liftₜ_apply_mk
182 (N : Subgroup G) [N.Normal] (f : G →ₜ* H)
183 (hN : N ≤ f.toMonoidHom.ker) (g : G) :
184 liftₜ (G := G) (H := H) N f hN (QuotientGroup.mk' N g) = f g := by
185 rfl
187@[simp] theorem liftₜ_toMonoidHom
188 (N : Subgroup G) [N.Normal] (f : G →ₜ* H)
189 (hN : N ≤ f.toMonoidHom.ker) :
190 (liftₜ (G := G) (H := H) N f hN).toMonoidHom =
191 QuotientGroup.lift N f.toMonoidHom hN := by
192 rfl
195 (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
196 (hNM : N ≤ M.comap f.toMonoidHom) (g : G) :
197 mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNM
198 (QuotientGroup.mk' N g) =
199 QuotientGroup.mk' M (f g) := by
200 rfl
202@[simp] theorem mapₜ_apply_mk
203 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
204 (f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) (g : G) :
205 mapₜ (G := G) (H := H) N M f hNM (QuotientGroup.mk' N g) =
206 QuotientGroup.mk' M (f g) := by
207 rfl
209@[simp] theorem mapₜ_toMonoidHom
210 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
211 (f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) :
212 (mapₜ (G := G) (H := H) N M f hNM).toMonoidHom =
213 QuotientGroup.map (N := N) (M := M) (f := f.toMonoidHom) hNM := by
214 rfl
216@[simp] theorem congrₜ_apply_mk
217 (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
218 (e : G ≃ₜ* H) (h : N.map e.toMulEquiv.toMonoidHom = M) (g : G) :
219 congrₜ (G := G) (H := H) N M e h (QuotientGroup.mk' N g) =
220 QuotientGroup.mk' M (e g) := by
221 rfl
224 (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
225 [CompactSpace (G ⧸ N)] [T2Space (H ⧸ M)]
226 (hf : Function.Surjective f) (hmap : N.map f.toMonoidHom = M)
227 (hker : f.toMonoidHom.ker ≤ N) (g : G) :
228 mapContinuousMulEquivOfSurjective (G := G) (H := H) f hf hmap hker
229 (QuotientGroup.mk' N g) =
230 QuotientGroup.mk' M (f g) := by
231 rfl
233end Topology
235end QuotientGroup
237namespace ContinuousMonoidHom
239section RestrictPreimage
241variable {G : Type u} {Q : Type v}
242variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
243variable [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
245/-- Restrict a continuous homomorphism to the preimage of a subgroup of the target. -/
246def restrictPreimage (f : G →ₜ* Q) (H : Subgroup Q) :
247 (H.comap f.toMonoidHom) →ₜ* H := by
248 refine
249 { toMonoidHom :=
250 { toFun := fun x => ⟨f x.1, x.2⟩
251 map_one' := by
252 ext
253 simp only [coe_toMonoidHom, OneMemClass.coe_one, map_one]
254 map_mul' := by
255 intro x y
256 ext
257 simp only [coe_toMonoidHom, Subgroup.coe_mul, map_mul]}
258 continuous_toFun := by
259 have hcont : Continuous (fun x : H.comap f.toMonoidHom => f x.1) :=
260 f.continuous.comp continuous_subtype_val
261 exact hcont.subtype_mk (by intro x; exact x.2) }
263omit [IsTopologicalGroup G] [IsTopologicalGroup Q] in
264/-- The restriction to a subgroup preimage is surjective if the original map is surjective. -/
265theorem restrictPreimage_surjective (f : G →ₜ* Q) (hf : Function.Surjective f)
266 (H : Subgroup Q) :
267 Function.Surjective (f.restrictPreimage H) := by
268 intro y
269 rcases hf y.1 with ⟨x, hx⟩
270 refine ⟨⟨x, ?_⟩, ?_⟩
271 · change f x ∈ H
272 simp only [hx, SetLike.coe_mem]
273 · exact Subtype.ext hx
275omit [IsTopologicalGroup G] [IsTopologicalGroup Q] in
276/-- The kernel of the restriction to a subgroup preimage is detected by the ambient map. -/
277theorem restrictPreimage_eq_one_iff (f : G →ₜ* Q) (H : Subgroup Q)
278 (x : H.comap f.toMonoidHom) :
279 f.restrictPreimage H x = 1 ↔ f x.1 = 1 := by
280 constructor
281 · intro hx
282 exact congrArg Subtype.val hx
283 · intro hx
284 exact Subtype.ext hx
286/-- Non-m-step quotient comparison for a subgroup preimage. This is the reusable form of the
287standard diagram/snake-lemma argument: if the restricted map sends `N` onto `M` and its kernel is
288absorbed by `N`, then the induced quotient map is an isomorphism. -/
290 (f : G →ₜ* Q) (hf : Function.Surjective f) (H : Subgroup Q)
291 {N : Subgroup (H.comap f.toMonoidHom)} {M : Subgroup H} [N.Normal] [M.Normal]
292 (hmap : N.map (f.restrictPreimage H).toMonoidHom = M)
293 (hker : (f.restrictPreimage H).toMonoidHom.ker ≤ N) :
294 (H.comap f.toMonoidHom) ⧸ N ≃* H ⧸ M :=
296 (f.restrictPreimage H).toMonoidHom
297 (f.restrictPreimage_surjective hf H) hmap hker
299end RestrictPreimage
301end ContinuousMonoidHom