ProCGroups/ProC/OpenNormalSubgroups/Basic.lean
1import Mathlib.Topology.Algebra.ContinuousMonoidHom
2import ProCGroups.Profinite.OpenSubgroups
3import ProCGroups.Topologies.QuotientMaps
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/ProC/OpenNormalSubgroups/Basic.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pro-C groups and open normal quotients
16Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
17-/
19open scoped Topology
21namespace ProCGroups.ProC
23universe u v
25variable {G : Type u} [Group G] [TopologicalSpace G]
27namespace OpenNormalSubgroup
29/-- Open normal subgroups have a top element. -/
30instance instTopOpenNormalSubgroup : Top (OpenNormalSubgroup G) :=
31 ⟨{ toOpenSubgroup := ⊤
32 isNormal' := by
33 change (⊤ : Subgroup G).Normal
34 infer_instance }⟩
36/-- The kernel of a continuous homomorphism into a discrete group, as an open normal subgroup. -/
38 (f : G →ₜ* Q) : OpenNormalSubgroup G where
39 toOpenSubgroup :=
40 { toSubgroup := f.toMonoidHom.ker
41 isOpen' := by
42 change IsOpen (f ⁻¹' ({1} : Set Q))
43 exact (isOpen_discrete _).preimage f.continuous_toFun }
44 isNormal' := by
45 change f.toMonoidHom.ker.Normal
46 infer_instance
48/-- The underlying subgroup of `OpenNormalSubgroup.ker` is the algebraic kernel. -/
49@[simp, norm_cast]
50theorem toSubgroup_ker {Q : Type v} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
51 (f : G →ₜ* Q) :
53 rfl
55/-- Membership in the open normal kernel is exactly mapping to `1`. -/
56@[simp]
58 {f : G →ₜ* Q} {x : G} :
60 rfl
62/-- Push an open normal subgroup forward along an open surjective continuous homomorphism. -/
63def map {H : Type v} [Group H] [TopologicalSpace H]
64 (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
65 (U : OpenNormalSubgroup G) : OpenNormalSubgroup H where
66 toOpenSubgroup :=
67 { toSubgroup := (U : Subgroup G).map f.toMonoidHom
68 isOpen' := by
69 change IsOpen (f '' ((U : Subgroup G) : Set G))
70 exact hfopen _ (openNormalSubgroup_isOpen (G := G) U) }
71 isNormal' := by
72 change ((U : Subgroup G).map f.toMonoidHom).Normal
73 exact Subgroup.Normal.map U.isNormal' f.toMonoidHom hfsurj
75/-- The underlying subgroup of the image open normal subgroup is the subgroup image. -/
76@[simp, norm_cast]
77theorem toSubgroup_map {H : Type v} [Group H] [TopologicalSpace H]
78 (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
79 (U : OpenNormalSubgroup G) :
80 ((map f hfopen hfsurj U : OpenNormalSubgroup H) : Subgroup H) =
81 (U : Subgroup G).map f.toMonoidHom :=
82 rfl
84/-- The canonical quotient projection attached to an open normal subgroup. -/
85def quotientProj (U : OpenNormalSubgroup G) : G →ₜ* G ⧸ (U : Subgroup G) where
86 toMonoidHom := QuotientGroup.mk' (U : Subgroup G)
87 continuous_toFun := continuous_quotient_mk'
89/-- Quotients by open normal subgroups of compact groups are finite. -/
90instance quotientFinite [ContinuousMul G] [CompactSpace G] (U : OpenNormalSubgroup G) :
91 Finite (G ⧸ (U : Subgroup G)) :=
92 openNormalSubgroup_finiteQuotient (G := G) U
94/-- Quotients by open normal subgroups carry the discrete topology. -/
95instance quotientDiscrete [ContinuousMul G] (U : OpenNormalSubgroup G) :
96 DiscreteTopology (G ⧸ (U : Subgroup G)) :=
97 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U)
99theorem quotientProj_toMonoidHom (U : OpenNormalSubgroup G) :
100 (quotientProj U).toMonoidHom = QuotientGroup.mk' (U : Subgroup G) :=
101 rfl
103/-- The quotient projection sends an element to its quotient class. -/
104@[simp]
105theorem quotientProj_apply (U : OpenNormalSubgroup G) (x : G) :
106 quotientProj U x = QuotientGroup.mk' (U : Subgroup G) x :=
107 rfl
109/-- The quotient projection by an open normal subgroup is surjective. -/
110@[simp]
111theorem quotientProj_surjective (U : OpenNormalSubgroup G) :
112 Function.Surjective (quotientProj U) :=
113 QuotientGroup.mk'_surjective (U : Subgroup G)
115/-- The quotient projection maps an element to `1` exactly on the subgroup. -/
116@[simp]
117theorem quotientProj_eq_one_iff {U : OpenNormalSubgroup G} {x : G} :
118 quotientProj U x = 1 ↔ x ∈ (U : Subgroup G) := by
119 change (QuotientGroup.mk' (U : Subgroup G) x) = 1 ↔ x ∈ (U : Subgroup G)
120 exact QuotientGroup.eq_one_iff (N := (U : Subgroup G)) x
122/-- Equality under a quotient projection is membership of the quotient difference in the subgroup. -/
123theorem quotientProj_eq_quotientProj_iff {U : OpenNormalSubgroup G} {x y : G} :
124 quotientProj U x = quotientProj U y ↔ x / y ∈ (U : Subgroup G) := by
125 change QuotientGroup.mk' (U : Subgroup G) x = QuotientGroup.mk' (U : Subgroup G) y ↔
126 x / y ∈ (U : Subgroup G)
127 exact QuotientGroup.eq_iff_div_mem (N := (U : Subgroup G)) (x := x) (y := y)
129/-- Kernel membership for the quotient projection is subgroup membership. -/
130@[simp]
131theorem mem_ker_quotientProj [ContinuousMul G] {U : OpenNormalSubgroup G} {x : G} :
133 exact quotientProj_eq_one_iff (U := U)
135/-- The open normal kernel of the quotient projection is the original subgroup. -/
136@[simp]
137theorem ker_quotientProj [ContinuousMul G] (U : OpenNormalSubgroup G) :
139 exact QuotientGroup.ker_mk' (U : Subgroup G)
141/-- Kernels commute with composition of continuous homomorphisms into discrete groups. -/
142@[simp]
144 {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
145 (g : H →ₜ* Q) (f : G →ₜ* H) :
148 ext x
149 rfl
151/-- The comap of a kernel is the kernel of the composite. -/
152@[simp]
154 {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
155 (f : G →ₜ* H) (g : H →ₜ* Q) :
160/-- Comapping an open normal subgroup is the kernel of the composite quotient projection. -/
161@[simp]
162theorem comap_quotientProj {H : Type v} [Group H] [TopologicalSpace H] [ContinuousMul H]
163 (f : G →ₜ* H) (U : OpenNormalSubgroup H) :
164 OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun U =
166 ext x
167 exact (quotientProj_eq_one_iff (U := U)).symm
169/-- The natural transition map between quotients by open normal subgroups `U ≤ V`. -/
170def transition [ContinuousMul G] {U V : OpenNormalSubgroup G}
171 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
172 G ⧸ (U : Subgroup G) →ₜ* G ⧸ (V : Subgroup G) :=
173 QuotientGroup.mapₜ (U : Subgroup G) (V : Subgroup G) (ContinuousMonoidHom.id G) (by
174 intro x hx
175 exact hUV hx)
177/-- Transition maps send quotient classes to quotient classes. -/
178@[simp]
179theorem transition_mk {U V : OpenNormalSubgroup G}
180 [ContinuousMul G]
181 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) (x : G) :
182 transition hUV (QuotientGroup.mk' (U : Subgroup G) x) =
183 QuotientGroup.mk' (V : Subgroup G) x := by
184 rfl
186/-- A transition map composed with the smaller quotient projection is the larger quotient
187projection. -/
188@[simp]
189theorem transition_comp_quotientProj {U V : OpenNormalSubgroup G}
190 [ContinuousMul G]
191 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
192 (transition hUV).comp (quotientProj U) = quotientProj V := by
193 rfl
195/-- Transition maps between quotients by nested open normal subgroups are surjective. -/
196theorem transition_surjective {U V : OpenNormalSubgroup G}
197 [ContinuousMul G]
198 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
199 Function.Surjective (transition hUV) := by
200 intro y
201 rcases QuotientGroup.mk'_surjective (V : Subgroup G) y with ⟨x, rfl⟩
202 exact ⟨QuotientGroup.mk' (U : Subgroup G) x, rfl⟩
204/-- The kernel of the transition map is the image of the larger subgroup in the smaller
205quotient. -/
206@[simp]
207theorem ker_transition {U V : OpenNormalSubgroup G}
208 [ContinuousMul G]
209 (hUV : (U : Subgroup G) ≤ (V : Subgroup G)) :
211 Subgroup (G ⧸ (U : Subgroup G))) =
212 (V : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G)) := by
213 simpa [transition] using
214 (QuotientGroup.ker_map (N := (U : Subgroup G)) (M := (V : Subgroup G))
215 (f := MonoidHom.id G) hUV)
217/-- The normal core of an open subgroup in a compact topological group, as an open normal
218subgroup. -/
219def normalCore [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :
220 OpenNormalSubgroup G where
221 toOpenSubgroup :=
222 { toSubgroup := Subgroup.normalCore (U : Subgroup G)
223 isOpen' := by
224 have hclosed : IsClosed ((U : Subgroup G) : Set G) :=
225 openSubgroup_isClosed (G := G) U
226 letI : (U : Subgroup G).FiniteIndex := by
227 letI : Finite (G ⧸ (U : Subgroup G)) := openSubgroup_finiteQuotient (G := G) U
228 exact Subgroup.finiteIndex_of_finite_quotient
229 exact Subgroup.isOpen_of_isClosed_of_finiteIndex _
230 ((U : Subgroup G).normalCore_isClosed hclosed) }
231 isNormal' := by
232 change (Subgroup.normalCore (U : Subgroup G)).Normal
233 infer_instance
235/-- The underlying subgroup of `normalCore` is the algebraic normal core. -/
236@[simp, norm_cast]
237theorem toSubgroup_normalCore [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :
238 ((normalCore U : OpenNormalSubgroup G) : Subgroup G) =
239 Subgroup.normalCore (U : Subgroup G) :=
240 rfl
242/-- The normal core of an open subgroup is contained in that open subgroup. -/
243theorem normalCore_le [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :
244 (normalCore U : Subgroup G) ≤ (U : Subgroup G) :=
245 Subgroup.normalCore_le (U : Subgroup G)
247/-- The infimum of a finite family of open normal subgroups. -/
249 OpenNormalSubgroup G :=
250 s.fold (fun A B => A ⊓ B) ⊤ U
252end OpenNormalSubgroup
254end ProCGroups.ProC