Source: ProCGroups.ProC.OpenNormalSubgroups.Basic
1import Mathlib.Topology.Algebra.ContinuousMonoidHom
2import ProCGroups.Profinite.OpenSubgroups
3import ProCGroups.Topologies.QuotientMaps
4import ProCGroups.Topologies.ContinuousMulEquiv
6/-!
7# Basic operations on open normal subgroups
9This file develops bundled open normal subgroups, their finite discrete quotients and projections,
10maps and comaps, transition morphisms, normal cores, and finite intersections.
11-/
13open scoped Topology
15namespace ProCGroups.ProC
17universe u v
19variable {G : Type u} [Group G] [TopologicalSpace G]
21namespace OpenNormalSubgroup
23/-- Open normal subgroups have a top element: the whole group. -/
24instance instTopOpenNormalSubgroup : Top (OpenNormalSubgroup G) :=
25 ⟨{ toOpenSubgroup := ⊤
26 isNormal' := by
27 change (⊤ : Subgroup G).Normal
28 infer_instance }⟩
30/-- The kernel of a continuous homomorphism into a discrete group is an open normal subgroup. -/
31def ker {Q : Type v} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
32 (f : G →ₜ* Q) : OpenNormalSubgroup G where
33 toOpenSubgroup :=
34 { toSubgroup := f.toMonoidHom.ker
35 isOpen' := by
36 change IsOpen (f ⁻¹' ({1} : Set Q))
37 exact (isOpen_discrete _).preimage f.continuous_toFun }
38 isNormal' := by
39 change f.toMonoidHom.ker.Normal
40 infer_instance
42/-- The underlying subgroup of OpenNormalSubgroup.kernel is the algebraic kernel. -/
43@[simp, norm_cast]
44theorem toSubgroup_ker {Q : Type v} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
45 (f : G →ₜ* Q) :
46 ((ker f : OpenNormalSubgroup G) : Subgroup G) = f.toMonoidHom.ker :=
47 rfl
49/-- Membership in the open normal kernel is exactly mapping to \(1\). -/
50@[simp]
51theorem mem_ker {Q : Type v} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
52 {f : G →ₜ* Q} {x : G} :
53 x ∈ ker f ↔ f x = 1 := by
54 rfl
56/--
57An open surjective continuous homomorphism sends open normal subgroups to open normal subgroups.
58-/
59def map {H : Type v} [Group H] [TopologicalSpace H]
60 (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
61 (U : OpenNormalSubgroup G) : OpenNormalSubgroup H where
62 toOpenSubgroup :=
63 { toSubgroup := (U : Subgroup G).map f.toMonoidHom
64 isOpen' := by
65 change IsOpen (f '' ((U : Subgroup G) : Set G))
66 exact hfopen _ (openNormalSubgroup_isOpen (G := G) U) }
67 isNormal' := by
68 change ((U : Subgroup G).map f.toMonoidHom).Normal
69 exact Subgroup.Normal.map U.isNormal' f.toMonoidHom hfsurj
71/-- The underlying subgroup of the image open normal subgroup is the subgroup image. -/
72@[simp, norm_cast]
73theorem toSubgroup_map {H : Type v} [Group H] [TopologicalSpace H]
74 (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
75 (U : OpenNormalSubgroup G) :
76 ((map f hfopen hfsurj U : OpenNormalSubgroup H) : Subgroup H) =
77 (U : Subgroup G).map f.toMonoidHom :=
78 rfl
80/-- A multiplicative homeomorphism identifies a quotient with the quotient by the image of an
81open normal subgroup. This is the source-producing transport used to prove that the canonical
82pro-`C` object property is invariant under isomorphism. -/
83noncomputable def quotientMapContinuousMulEquiv
84 {H : Type u} [Group H] [TopologicalSpace H]
85 (e : G ≃ₜ* H) (U : OpenNormalSubgroup G) :
86 G ⧸ (U : Subgroup G) ≃*
87 H ⧸ ((map (ContinuousMonoidHom.toContinuousMonoidHom e)
88 (Homeomorph.isOpenMap e.toHomeomorph) e.surjective U : OpenNormalSubgroup H) :
89 Subgroup H) := by
90 let V : OpenNormalSubgroup H :=
91 map (ContinuousMonoidHom.toContinuousMonoidHom e)
92 (Homeomorph.isOpenMap e.toHomeomorph) e.surjective U
93 have hforward :
94 (U : Subgroup G) ≤ (V : Subgroup H).comap e.toMulEquiv.toMonoidHom := by
95 intro x hx
96 change e x ∈ (U : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom
97 exact ⟨x, hx, rfl⟩
98 have hbackward :
99 (V : Subgroup H) ≤ (U : Subgroup G).comap e.symm.toMulEquiv.toMonoidHom := by
100 intro y hy
101 change e.symm y ∈ (U : Subgroup G)
102 change y ∈ (U : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom at hy
103 rcases hy with ⟨x, hx, hxy⟩
104 have : e.symm y = x := by
105 apply e.injective
106 simpa using hxy.symm
107 rw [this]
108 exact hx
109 let forward : G ⧸ (U : Subgroup G) →* H ⧸ (V : Subgroup H) :=
110 QuotientGroup.map (U : Subgroup G) (V : Subgroup H)
111 e.toMulEquiv.toMonoidHom hforward
112 let backward : H ⧸ (V : Subgroup H) →* G ⧸ (U : Subgroup G) :=
113 QuotientGroup.map (V : Subgroup H) (U : Subgroup G)
114 e.symm.toMulEquiv.toMonoidHom hbackward
115 refine
116 { toFun := forward
117 invFun := backward
118 left_inv := ?_
119 right_inv := ?_
120 map_mul' := forward.map_mul }
121 · intro x
122 refine QuotientGroup.induction_on x ?_
123 intro g
124 change QuotientGroup.mk' (U : Subgroup G) (e.symm (e g)) =
125 QuotientGroup.mk' (U : Subgroup G) g
126 rw [e.symm_apply_apply]
127 · intro y
128 refine QuotientGroup.induction_on y ?_
129 intro h
130 change QuotientGroup.mk' (V : Subgroup H) (e (e.symm h)) =
131 QuotientGroup.mk' (V : Subgroup H) h
132 rw [e.apply_symm_apply]
134/-- The canonical quotient projection attached to an open normal subgroup. -/
135def quotientProj (U : OpenNormalSubgroup G) : G →ₜ* G ⧸ (U : Subgroup G) where
136 toMonoidHom := QuotientGroup.mk' (U : Subgroup G)
137 continuous_toFun := continuous_quotient_mk'
139/-- Quotients by open normal subgroups of compact groups are finite. -/
140instance quotientFinite [ContinuousMul G] [CompactSpace G] (U : OpenNormalSubgroup G) :
141 Finite (G ⧸ (U : Subgroup G)) :=
142 openNormalSubgroup_finiteQuotient (G := G) U
144/-- Quotients by open normal subgroups carry the discrete topology. -/
145instance quotientDiscrete [ContinuousMul G] (U : OpenNormalSubgroup G) :
146 DiscreteTopology (G ⧸ (U : Subgroup G)) :=
147 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U)
149/-- The induced pro-\(C\) map agrees with the corresponding finite-quotient construction. -/
150theorem quotientProj_toMonoidHom (U : OpenNormalSubgroup G) :
151 (quotientProj U).toMonoidHom = QuotientGroup.mk' (U : Subgroup G) :=
152 rfl
154/-- The quotient projection sends an element to its quotient class. -/
155@[simp]
156theorem quotientProj_apply (U : OpenNormalSubgroup G) (x : G) :
157 quotientProj U x = QuotientGroup.mk' (U : Subgroup G) x :=
158 rfl
160/-- The quotient projection by an open normal subgroup is surjective. -/
161@[simp]
162theorem quotientProj_surjective (U : OpenNormalSubgroup G) :
163 Function.Surjective (quotientProj U) :=
164 QuotientGroup.mk'_surjective (U : Subgroup G)
166/-- The quotient projection maps an element to \(1\) exactly on the subgroup. -/
167@[simp]
168theorem quotientProj_eq_one_iff {U : OpenNormalSubgroup G} {x : G} :
169 quotientProj U x = 1 ↔ x ∈ (U : Subgroup G) := by
170 change (QuotientGroup.mk' (U : Subgroup G) x) = 1 ↔ x ∈ (U : Subgroup G)
171 exact QuotientGroup.eq_one_iff (N := (U : Subgroup G)) x
173/--
174Equality under a quotient projection is membership of the quotient difference in the subgroup.
175-/
176theorem quotientProj_eq_quotientProj_iff {U : OpenNormalSubgroup G} {x y : G} :
177 quotientProj U x = quotientProj U y ↔ x / y ∈ (U : Subgroup G) := by
178 change QuotientGroup.mk' (U : Subgroup G) x = QuotientGroup.mk' (U : Subgroup G) y ↔
179 x / y ∈ (U : Subgroup G)
180 exact QuotientGroup.eq_iff_div_mem (N := (U : Subgroup G)) (x := x) (y := y)
182/-- Kernel membership for the quotient projection is subgroup membership. -/
183@[simp]
184theorem mem_ker_quotientProj [ContinuousMul G] {U : OpenNormalSubgroup G} {x : G} :
185 x ∈ ker (quotientProj U) ↔ x ∈ (U : Subgroup G) := by
186 exact quotientProj_eq_one_iff (U := U)
188/-- The open normal kernel of the quotient projection is the original subgroup. -/
189@[simp]
190theorem ker_quotientProj [ContinuousMul G] (U : OpenNormalSubgroup G) :
191 ((ker (quotientProj U) : OpenNormalSubgroup G) : Subgroup G) = (U : Subgroup G) := by
192 exact QuotientGroup.ker_mk' (U : Subgroup G)
194/-- Kernels commute with composition of continuous homomorphisms into discrete groups. -/
195@[simp]
196theorem ker_comp {H : Type v} [Group H] [TopologicalSpace H]
197 {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
198 (g : H →ₜ* Q) (f : G →ₜ* H) :
199 ker (g.comp f) =
200 OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun (ker g) := by
201 ext x
202 rfl
204/-- The comap of a kernel is the kernel of the composite. -/
205@[simp]
206theorem comap_ker {H : Type v} [Group H] [TopologicalSpace H]
207 {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
208 (f : G →ₜ* H) (g : H →ₜ* Q) :
209 OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun (ker g) =
210 ker (g.comp f) := by
211 simp only [ContinuousMonoidHom.coe_toMonoidHom, ker_comp]
213/-- Comapping an open normal subgroup is the kernel of the composite quotient projection. -/
214@[simp]
215theorem comap_quotientProj {H : Type v} [Group H] [TopologicalSpace H] [ContinuousMul H]
216 (f : G →ₜ* H) (U : OpenNormalSubgroup H) :
217 OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun U =
218 ker ((quotientProj U).comp f) := by
219 ext x
220 exact (quotientProj_eq_one_iff (U := U)).symm
222/-- The natural transition map between quotients by open normal subgroups \(U\le V\). -/
223def transition {U V : OpenNormalSubgroup G}
224 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
225 G ⧸ (U : Subgroup G) →ₜ* G ⧸ (V : Subgroup G) :=
226 QuotientGroup.mapₜ (U : Subgroup G) (V : Subgroup G) (ContinuousMonoidHom.id G) (by
227 intro x hx
228 exact hUV hx)
230/-- Transition maps send quotient classes to quotient classes. -/
231@[simp]
232theorem transition_mk {U V : OpenNormalSubgroup G}
233 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) (x : G) :
234 transition hUV (QuotientGroup.mk' (U : Subgroup G) x) =
235 QuotientGroup.mk' (V : Subgroup G) x := by
236 rfl
238/--
239Composing a transition map with the smaller quotient projection gives the larger quotient
240projection.
241-/
242@[simp]
243theorem transition_comp_quotientProj {U V : OpenNormalSubgroup G}
244 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
245 (transition hUV).comp (quotientProj U) = quotientProj V := by
246 rfl
248/-- Transition maps between quotients by nested open normal subgroups are surjective. -/
249theorem transition_surjective {U V : OpenNormalSubgroup G}
250 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
251 Function.Surjective (transition hUV) := by
252 intro y
253 rcases QuotientGroup.mk'_surjective (V : Subgroup G) y with ⟨x, rfl⟩
254 exact ⟨QuotientGroup.mk' (U : Subgroup G) x, rfl⟩
256/-- The kernel of the transition map is the image of the larger subgroup in the smaller quotient. -/
257@[simp]
258theorem ker_transition {U V : OpenNormalSubgroup G}
259 [ContinuousMul G]
260 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
261 ((ker (transition hUV) : OpenNormalSubgroup (G ⧸ (U : Subgroup G))) :
262 Subgroup (G ⧸ (U : Subgroup G))) =
263 (V : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G)) := by
264 change
265 (QuotientGroup.map (N := (U : Subgroup G)) (M := (V : Subgroup G))
266 (f := MonoidHom.id G) hUV).ker =
267 (V : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))
268 exact
269 QuotientGroup.ker_map (N := (U : Subgroup G)) (M := (V : Subgroup G))
270 (f := MonoidHom.id G) hUV
272/--
273The normal core of an open subgroup in a compact topological group is an open normal subgroup.
274-/
275def normalCore [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :
276 OpenNormalSubgroup G where
277 toOpenSubgroup :=
278 { toSubgroup := Subgroup.normalCore (U : Subgroup G)
279 isOpen' := by
280 have hclosed : IsClosed ((U : Subgroup G) : Set G) :=
281 openSubgroup_isClosed (G := G) U
282 letI : (U : Subgroup G).FiniteIndex := by
283 letI : Finite (G ⧸ (U : Subgroup G)) := openSubgroup_finiteQuotient (G := G) U
284 exact Subgroup.finiteIndex_of_finite_quotient
285 exact Subgroup.isOpen_of_isClosed_of_finiteIndex _
286 ((U : Subgroup G).normalCore_isClosed hclosed) }
287 isNormal' := by
288 change (Subgroup.normalCore (U : Subgroup G)).Normal
289 infer_instance
291/-- The underlying subgroup of \(\mathrm{normalCore}\) is the algebraic normal core. -/
292@[simp, norm_cast]
293theorem toSubgroup_normalCore [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :
294 ((normalCore U : OpenNormalSubgroup G) : Subgroup G) =
295 Subgroup.normalCore (U : Subgroup G) :=
296 rfl
298/-- The normal core of an open subgroup is contained in that open subgroup. -/
299theorem normalCore_le [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :
300 (normalCore U : Subgroup G) ≤ (U : Subgroup G) :=
301 Subgroup.normalCore_le (U : Subgroup G)
303/-- The infimum of a finite family of open normal subgroups. -/
304def finsetInf {ι : Type v} (s : Finset ι) (U : ι → OpenNormalSubgroup G) :
305 OpenNormalSubgroup G :=
306 s.fold (fun A B => A ⊓ B) ⊤ U
308end OpenNormalSubgroup
310end ProCGroups.ProC