Source: ProCGroups.ProC.Subgroups.Products
1import ProCGroups.ProC.Subgroups.Closed
3/-!
4# Closed subgroups of products of pro-\(C\) groups
6This file transfers an open-normal quotient basis in \(C\) from a product to a closed subgroup
7when \(C\) is subgroup closed, and specializes the result to subdirect products.
8-/
10open Set
11open scoped Topology Pointwise
13namespace ProCGroups.ProC
15universe u
17section
19variable {ι : Type u}
20variable {Gs : ι → Type u}
21variable {C : FiniteGroupClass.{u}}
23variable [∀ i, Group (Gs i)]
24variable [∀ i, TopologicalSpace (Gs i)]
25variable [∀ i, IsTopologicalGroup (Gs i)]
26variable [∀ i, T2Space (Gs i)]
28/-- A closed subgroup of a product of groups with open-normal \(C\)-bases again has such a basis. -/
29theorem HasOpenNormalBasisInClass.of_closedSubgroup_pi
30 [∀ i, CompactSpace (Gs i)] [∀ i, TotallyDisconnectedSpace (Gs i)]
31 {H : Subgroup ((i : ι) → Gs i)}
32 (hH : IsClosed (((H : Subgroup ((i : ι) → Gs i)) : Set ((i : ι) → Gs i))))
33 (hForm : FiniteGroupClass.Formation C)
34 (hSub : FiniteGroupClass.SubgroupClosed C)
35 (hGs : ∀ i, HasOpenNormalBasisInClass C (Gs i)) :
36 HasOpenNormalBasisInClass C ↥H := by
37 have hpi : HasOpenNormalBasisInClass C ((i : ι) → Gs i) :=
38 HasOpenNormalBasisInClass.pi (C := C) (α := ι) (β := Gs) hForm hGs
39 simpa using
40 (HasOpenNormalBasisInClass.of_isClosed_subgroup
41 (C := C)
42 (G := ((i : ι) → Gs i))
43 (H := H)
44 hForm.isomClosed
45 hSub
46 (hG := hpi)
47 hH)
49omit [∀ i, IsTopologicalGroup (Gs i)] in
50/-- A profinite group embedded as a subdirect product of groups with open-normal \(C\)-bases again
51has such a basis; the coordinatewise finite-subdirect-product criterion is exposed for reuse. -/
52theorem HasOpenNormalBasisInClass.of_subdirectProduct
53 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
54 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
55 (φ : H →* ((i : ι) → Gs i)) (hφcont : Continuous φ)
56 (hφinj : Function.Injective φ)
57 (hφsurj : ∀ i, Function.Surjective (fun x : H => φ x i))
58 (hForm : FiniteGroupClass.Formation C)
59 (hGs : ∀ i, HasOpenNormalBasisInClass C (Gs i)) :
60 HasOpenNormalBasisInClass C H := by
61 classical
62 let φrange : H →* ↥(φ.range : Subgroup ((i : ι) → Gs i)) := φ.rangeRestrict
63 have hφrange_continuous : Continuous φrange := by
64 change Continuous (fun x : H => (⟨φ x, ⟨x, rfl⟩⟩ : ↥(φ.range : Subgroup ((i : ι) → Gs i))))
65 exact Continuous.subtype_mk hφcont (fun x => ⟨x, rfl⟩)
66 have hφrange_bij : Function.Bijective φrange := by
67 constructor
68 · intro x y hxy
69 apply hφinj
70 exact congrArg Subtype.val hxy
71 · exact φ.rangeRestrict_surjective
72 let e : H ≃ₜ* ↥(φ.range : Subgroup ((i : ι) → Gs i)) :=
73 ContinuousMulEquiv.ofBijectiveCompactToT2 φrange hφrange_continuous hφrange_bij
74 refine HasOpenNormalBasisInClass.of_allOpenNormalQuotients (C := C) ?_
75 intro U
76 let imgU : Set ↥(φ.range : Subgroup ((i : ι) → Gs i)) :=
77 e.toHomeomorph '' (((U : Subgroup H) : Set H))
78 have himgU_open : IsOpen imgU := e.toHomeomorph.isOpenMap _ U.isOpen'
79 have h1imgU : (1 : ↥(φ.range : Subgroup ((i : ι) → Gs i))) ∈ imgU := by
80 refine ⟨1, U.one_mem', ?_⟩
81 change e 1 = 1
82 simp only [map_one]
83 have himgU_nhds : imgU ∈ 𝓝 (1 : ↥(φ.range : Subgroup ((i : ι) → Gs i))) := by
84 exact himgU_open.mem_nhds h1imgU
85 rcases (mem_nhds_subtype
86 ((φ.range : Subgroup ((i : ι) → Gs i)) : Set ((i : ι) → Gs i))
87 (1 : ↥(φ.range : Subgroup ((i : ι) → Gs i))) imgU).1 himgU_nhds with
88 ⟨W, hW_nhds, hWU⟩
89 rcases mem_nhds_iff.mp hW_nhds with ⟨W', hW'W, hW'open, h1W'⟩
90 rcases (isOpen_pi_iff.mp hW'open) (1 : (i : ι) → Gs i) h1W' with ⟨J, WJ, hJ1, hJ2⟩
91 let V : ∀ j : J, OpenNormalSubgroup (Gs j) := fun j =>
92 Classical.choose <|
93 hGs j (WJ j) (hJ1 j j.property).1 (hJ1 j j.property).2
94 have hVsub : ∀ j : J, ((V j : Subgroup (Gs j)) : Set (Gs j)) ⊆ WJ j := fun j =>
95 (Classical.choose_spec <|
96 hGs j (WJ j) (hJ1 j j.property).1 (hJ1 j j.property).2).1
97 have hVquot : ∀ j : J, C (Gs j ⧸ (V j : Subgroup (Gs j))) := fun j =>
98 (Classical.choose_spec <|
99 hGs j (WJ j) (hJ1 j j.property).1 (hJ1 j j.property).2).2
100 let ψ : ∀ j : J, H →* Gs j := fun j =>
101 { toFun := fun h => φ h j
102 map_one' := by simp only [map_one, Pi.one_apply]
103 map_mul' := by intro x y; simp only [map_mul, Pi.mul_apply]}
104 let M : Subgroup H :=
105 iInf fun j : J =>
106 ((OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) :
107 OpenNormalSubgroup H) : Subgroup H)
108 letI : M.Normal := by
109 exact Subgroup.normal_iInf_normal fun j : J =>
110 (OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j)).isNormal'
111 have hMU : M ≤ (U : Subgroup H) := by
112 intro x hx
113 have hxM :
114 ∀ j : J,
115 x ∈ ((OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) :
116 OpenNormalSubgroup H) : Subgroup H) := by
117 change x ∈ iInf (fun j : J =>
118 ((OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) :
119 OpenNormalSubgroup H) : Subgroup H)) at hx
120 exact (Subgroup.mem_iInf).1 hx
121 have hxW' : φ x ∈ W' := by
122 apply hJ2
123 intro j hj
124 have hxj : ψ ⟨j, hj⟩ x ∈ (V ⟨j, hj⟩ : Subgroup (Gs j)) := by
125 have h := hxM ⟨j, hj⟩
126 change ψ ⟨j, hj⟩ x ∈ (V ⟨j, hj⟩ : Subgroup (Gs j)) at h
127 exact h
128 exact hVsub ⟨j, hj⟩ hxj
129 have hxW :
130 ((e x : ↥(φ.range : Subgroup ((i : ι) → Gs i))) : ((i : ι) → Gs i)) ∈ W := by
131 apply hW'W
132 simpa [e, φrange] using hxW'
133 rcases hWU hxW with ⟨u, huU, hux⟩
134 have hxu : x = u := by
135 apply hφinj
136 exact congrArg Subtype.val hux.symm
137 simpa [hxu] using huU
138 let φM : H →* ∀ j : J, Gs j ⧸ (V j : Subgroup (Gs j)) :=
139 { toFun := fun h j => QuotientGroup.mk' (V j : Subgroup (Gs j)) (φ h j)
140 map_one' := by
141 funext j
142 simp only [map_one, Pi.one_apply]
143 map_mul' := by
144 intro x y
145 funext j
146 simp only [map_mul, Pi.mul_apply]}
147 have hRange : C φM.range := by
148 let χ : φM.range →* ∀ j : J, Gs j ⧸ (V j : Subgroup (Gs j)) := φM.range.subtype
149 have hχinj : Function.Injective χ := Subtype.coe_injective
150 have hχsurj : ∀ j : J, Function.Surjective fun x : φM.range => χ x j := by
151 intro j y
152 rcases QuotientGroup.mk'_surjective (V j : Subgroup (Gs j)) y with ⟨g, rfl⟩
153 rcases hφsurj j g with ⟨x, hx⟩
154 refine ⟨⟨φM x, ⟨x, rfl⟩⟩, ?_⟩
155 change
156 QuotientGroup.mk' (V j : Subgroup (Gs j)) (φ x j) =
157 QuotientGroup.mk' (V j : Subgroup (Gs j)) g
158 have hx' : φ x j = g := hx
159 exact congrArg (QuotientGroup.mk' (V j : Subgroup (Gs j))) hx'
160 exact hForm.finiteSubdirectProductClosed χ hχinj hχsurj hVquot
161 have hKerEq : M = φM.ker := by
162 ext x
163 constructor
164 · intro hx
165 have hxM :
166 ∀ j : J,
167 x ∈ ((OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) :
168 OpenNormalSubgroup H) : Subgroup H) := by
169 change x ∈ iInf (fun j : J =>
170 ((OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) :
171 OpenNormalSubgroup H) : Subgroup H)) at hx
172 exact (Subgroup.mem_iInf).1 hx
173 change (fun j : J => QuotientGroup.mk' (V j : Subgroup (Gs j)) (φ x j)) = 1
174 funext j
175 apply (QuotientGroup.eq_one_iff (N := (V j : Subgroup (Gs j))) (φ x j)).2
176 have h := hxM j
177 change φ x j ∈ (V j : Subgroup (Gs j)) at h
178 exact h
179 · intro hx
180 have hxker :
181 (fun j : J => QuotientGroup.mk' (V j : Subgroup (Gs j)) (φ x j)) = 1 := by
182 simpa [MonoidHom.mem_ker, φM] using hx
183 have hxM :
184 ∀ j : J,
185 x ∈ ((OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) :
186 OpenNormalSubgroup H) : Subgroup H) := by
187 intro j
188 change φ x j ∈ (V j : Subgroup (Gs j))
189 exact (QuotientGroup.eq_one_iff (N := (V j : Subgroup (Gs j))) (φ x j)).1
190 (congrArg
191 (fun f : (j : J) → Gs j ⧸ (V j : Subgroup (Gs j)) => f j)
192 hxker)
193 change x ∈ iInf (fun j : J =>
194 ((OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) :
195 OpenNormalSubgroup H) : Subgroup H))
196 exact (Subgroup.mem_iInf).2 hxM
197 have hQuotM : C (H ⧸ M) := by
198 let e1 : H ⧸ M ≃* H ⧸ φM.ker :=
199 QuotientGroup.quotientMulEquivOfEq hKerEq
200 exact hForm.isomClosed
201 ⟨(e1.trans (QuotientGroup.quotientKerEquivRange φM)).symm⟩
202 hRange
203 have hQuotU :
204 C ((H ⧸ M) ⧸ Subgroup.map (QuotientGroup.mk' M) (U : Subgroup H)) := by
205 exact hForm.quotientClosed
206 (N := Subgroup.map (QuotientGroup.mk' M) (U : Subgroup H)) hQuotM
207 exact hForm.isomClosed
208 ⟨QuotientGroup.quotientQuotientEquivQuotient M (U : Subgroup H) hMU⟩
209 hQuotU
211end
213end ProCGroups.ProC