Yamaguchi Lean 4 Library
ProCGroups/ProC/Subgroups/Products.lean
ProCGroups/ProC/Subgroups/Products/Source

ProCGroups/ProC/Subgroups/Products.lean

1import ProCGroups.ProC.Subgroups.Closed
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/ProC/Subgroups/Products.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Pro-C groups and open normal quotients
14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
15-/
17open Set
18open scoped Topology Pointwise
20namespace ProCGroups.ProC
22universe u v w
24open InverseSystems
26section
28variable {ι : Type (max u v)}
29variable {G₁ : Type u} {G₂ : Type v}
30variable {Gs : ι → Type (max u v)}
31variable {C : FiniteGroupClass.{max u v}}
33variable [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁]
34variable [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂]
35variable [∀ i, Group (Gs i)]
36variable [∀ i, TopologicalSpace (Gs i)]
37variable [∀ i, IsTopologicalGroup (Gs i)]
39/--
40A closed subgroup of a product of profinite groups is profinite.
41This is a direct theorem around the already-completed `pi` and closed-subgroup permanence lemmas.
42-/
43theorem IsProfiniteGroup.of_closedSubgroup_pi
44 {H : Subgroup ((i : ι) → Gs i)}
45 (hH : IsClosed (((H : Subgroup ((i : ι) → Gs i)) : Set ((i : ι) → Gs i))))
46 (hGs : ∀ i, IsProfiniteGroup (Gs i)) :
48 have hpi : IsProfiniteGroup ((i : ι) → Gs i) :=
49 IsProfiniteGroup.pi (β := Gs) hGs
50 simpa using
52 (G := ((i : ι) → Gs i))
53 (H := H)
54 (hG := hpi)
55 hH)
57/--
58A closed subgroup of a binary product of profinite groups is profinite.
59This is the finite-product specialization of `IsProfiniteGroup.of_closedSubgroup_pi`.
60-/
61theorem IsProfiniteGroup.of_closedSubgroup_prod
62 {H : Subgroup (G₁ × G₂)}
63 (hH : IsClosed (((H : Subgroup (G₁ × G₂)) : Set (G₁ × G₂))))
64 (hG₁ : IsProfiniteGroup G₁) (hG₂ : IsProfiniteGroup G₂) :
66 have hprod : IsProfiniteGroup (G₁ × G₂) :=
67 IsProfiniteGroup.prod (G := G₁) (H := G₂) hG₁ hG₂
68 simpa using
70 (G := G₁ × G₂)
71 (H := H)
72 (hG := hprod)
73 hH)
75/--
76A closed subgroup of a product of pro-`C` groups is pro-`C`.
77This is the pro-class analogue of `IsProfiniteGroup.of_closedSubgroup_pi`.
78-/
79theorem IsProCGroup.of_closedSubgroup_pi
80 {H : Subgroup ((i : ι) → Gs i)}
81 (hH : IsClosed (((H : Subgroup ((i : ι) → Gs i)) : Set ((i : ι) → Gs i))))
82 (hForm : FiniteGroupClass.Formation C)
83 (hSub : FiniteGroupClass.SubgroupClosed C)
84 (hGs : ∀ i, IsProCGroup C (Gs i)) :
85 IsProCGroup C ↥H := by
86 have hpi : IsProCGroup C ((i : ι) → Gs i) :=
87 IsProCGroup.pi (C := C) (α := ι) (β := Gs) hForm hGs
88 simpa using
89 (IsProCGroup.of_isClosed_subgroup
90 (C := C)
91 (G := ((i : ι) → Gs i))
92 (H := H)
93 hForm.isomClosed
94 hSub
95 hForm.quotientClosed
96 (hG := hpi)
97 hH)
99omit [∀ i, IsTopologicalGroup (Gs i)] in
100/-- A profinite group embedded as a subdirect product of pro-`C` groups is itself pro-`C`.
102The proof checks the finite-quotient criterion directly: an open normal subgroup of `H` pulls back
103from finitely many coordinate open normal subgroups, and the resulting finite quotient is a finite
104subdirect product of finite quotients lying in `C`.
106The proof is organized coordinatewise so that downstream arguments can reuse the finite-subdirect
107product step without reopening the entire compactness argument. -/
108theorem IsProCGroup.of_subdirectProduct
109 {H : Type (max u v)} [Group H] [TopologicalSpace H]
111 (φ : H →* ((i : ι) → Gs i)) (hφcont : Continuous φ)
112 (hφinj : Function.Injective φ)
113 (hφsurj : ∀ i, Function.Surjective (fun x : H => φ x i))
114 (hForm : FiniteGroupClass.Formation C)
115 (hGs : ∀ i, IsProCGroup C (Gs i)) :
116 IsProCGroup C H := by
117 classical
118 letI : IsTopologicalGroup H := hH.isTopologicalGroup
119 letI : CompactSpace H := IsProfiniteGroup.compactSpace hH
120 letI : T2Space H := IsProfiniteGroup.t2Space hH
121 letI : TotallyDisconnectedSpace H := IsProfiniteGroup.totallyDisconnectedSpace hH
122 letI : ∀ i, CompactSpace (Gs i) := fun i => IsProCGroup.compactSpace (hGs i)
123 letI : ∀ i, T2Space (Gs i) := fun i => IsProCGroup.t2Space (hGs i)
124 letI : ∀ i, TotallyDisconnectedSpace (Gs i) := fun i =>
125 IsProCGroup.totallyDisconnectedSpace (hGs i)
126 let φrange : H →* ↥(φ.range : Subgroup ((i : ι) → Gs i)) := φ.rangeRestrict
127 have hφrange_continuous : Continuous φrange := by
128 change Continuous (fun x : H => (⟨φ x, ⟨x, rfl⟩⟩ : ↥(φ.range : Subgroup ((i : ι) → Gs i))))
129 exact Continuous.subtype_mk hφcont (fun x => ⟨x, rfl⟩)
130 have hφrange_bij : Function.Bijective φrange := by
131 constructor
132 · intro x y hxy
133 apply hφinj
134 exact congrArg Subtype.val hxy
135 · exact φ.rangeRestrict_surjective
136 let e : H ≃ₜ* ↥(φ.range : Subgroup ((i : ι) → Gs i)) :=
137 ContinuousMulEquiv.ofBijectiveCompactToT2 φrange hφrange_continuous hφrange_bij
138 refine IsProCGroup.of_allOpenNormalQuotients (C := C) hH ?_
139 intro U
140 let imgU : Set ↥(φ.range : Subgroup ((i : ι) → Gs i)) :=
141 e.toHomeomorph '' (((U : Subgroup H) : Set H))
142 have himgU_open : IsOpen imgU := e.toHomeomorph.isOpenMap _ U.isOpen'
143 have h1imgU : (1 : ↥(φ.range : Subgroup ((i : ι) → Gs i))) ∈ imgU := by
144 refine ⟨1, U.one_mem', ?_⟩
145 change e 1 = 1
146 simp only [map_one]
147 have himgU_nhds : imgU ∈ 𝓝 (1 : ↥(φ.range : Subgroup ((i : ι) → Gs i))) := by
148 exact himgU_open.mem_nhds h1imgU
149 rcases (mem_nhds_subtype
150 ((φ.range : Subgroup ((i : ι) → Gs i)) : Set ((i : ι) → Gs i))
151 (1 : ↥(φ.range : Subgroup ((i : ι) → Gs i))) imgU).1 himgU_nhds with
152 ⟨W, hW_nhds, hWU⟩
153 rcases mem_nhds_iff.mp hW_nhds with ⟨W', hW'W, hW'open, h1W'⟩
154 rcases (isOpen_pi_iff.mp hW'open) (1 : (i : ι) → Gs i) h1W' with ⟨J, WJ, hJ1, hJ2⟩
155 let V : ∀ j : J, OpenNormalSubgroup (Gs j) := fun j =>
156 Classical.choose <|
157 IsProCGroup.hasOpenNormalBasisInClass (C := C) (G := Gs j) (hGs j) (WJ j)
158 (hJ1 j j.property).1 (hJ1 j j.property).2
159 have hVsub : ∀ j : J, ((V j : Subgroup (Gs j)) : Set (Gs j)) ⊆ WJ j := fun j =>
160 (Classical.choose_spec <|
161 IsProCGroup.hasOpenNormalBasisInClass (C := C) (G := Gs j) (hGs j) (WJ j)
162 (hJ1 j j.property).1 (hJ1 j j.property).2).1
163 have hVquot : ∀ j : J, C (Gs j ⧸ (V j : Subgroup (Gs j))) := fun j =>
164 (Classical.choose_spec <|
165 IsProCGroup.hasOpenNormalBasisInClass (C := C) (G := Gs j) (hGs j) (WJ j)
166 (hJ1 j j.property).1 (hJ1 j j.property).2).2
167 let ψ : ∀ j : J, H →* Gs j := fun j =>
168 { toFun := fun h => φ h j
169 map_one' := by simp only [map_one, Pi.one_apply]
170 map_mul' := by intro x y; simp only [map_mul, Pi.mul_apply]}
171 let M : Subgroup H :=
172 iInf fun j : J =>
173 ((OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) :
174 OpenNormalSubgroup H) : Subgroup H)
175 letI : M.Normal := by
176 exact Subgroup.normal_iInf_normal fun j : J =>
177 (OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j)).isNormal'
178 have hMU : M ≤ (U : Subgroup H) := by
179 intro x hx
180 have hxM :
181 ∀ j : J,
182 x ∈ OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) := by
183 simpa [M, Subgroup.mem_iInf] using hx
184 have hxW' : φ x ∈ W' := by
185 apply hJ2
186 intro j hj
187 have hxj : ψ ⟨j, hj⟩ x ∈ (V ⟨j, hj⟩ : Subgroup (Gs j)) := by
188 simpa [ψ] using hxM ⟨j, hj⟩
189 exact hVsub ⟨j, hj⟩ hxj
190 have hxW :
191 ((e x : ↥(φ.range : Subgroup ((i : ι) → Gs i))) : ((i : ι) → Gs i)) ∈ W := by
192 apply hW'W
193 simpa [e, φrange] using hxW'
194 rcases hWU hxW with ⟨u, huU, hux⟩
195 have hxu : x = u := by
196 apply hφinj
197 exact congrArg Subtype.val hux.symm
198 simpa [hxu] using huU
199 let φM : H →* ∀ j : J, Gs j ⧸ (V j : Subgroup (Gs j)) :=
200 { toFun := fun h j => QuotientGroup.mk' (V j : Subgroup (Gs j)) (φ h j)
201 map_one' := by
202 funext j
203 simp only [map_one, Pi.one_apply]
204 map_mul' := by
205 intro x y
206 funext j
207 simp only [map_mul, Pi.mul_apply]}
208 have hRange : C φM.range := by
209 let χ : φM.range →* ∀ j : J, Gs j ⧸ (V j : Subgroup (Gs j)) := φM.range.subtype
210 have hχinj : Function.Injective χ := Subtype.coe_injective
211 have hχsurj : ∀ j : J, Function.Surjective fun x : φM.range => χ x j := by
212 intro j y
213 rcases QuotientGroup.mk'_surjective (V j : Subgroup (Gs j)) y with ⟨g, rfl⟩
214 rcases hφsurj j g with ⟨x, hx⟩
215 refine ⟨⟨φM x, ⟨x, rfl⟩⟩, ?_⟩
216 simp only [QuotientGroup.mk'_apply, MonoidHom.coe_mk, OneHom.coe_mk, Subgroup.subtype_apply, hx, φM, χ]
217 exact hForm.finiteSubdirectProductClosed χ hχinj hχsurj hVquot
218 have hKerEq : M = φM.ker := by
219 ext x
220 constructor
221 · intro hx
222 have hxM :
223 ∀ j : J,
224 x ∈ OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) := by
225 simpa [M, Subgroup.mem_iInf] using hx
226 change (fun j : J => QuotientGroup.mk' (V j : Subgroup (Gs j)) (φ x j)) = 1
227 funext j
228 exact (QuotientGroup.eq_one_iff (N := (V j : Subgroup (Gs j))) (φ x j)).2 (by
229 simpa [ψ] using hxM j)
230 · intro hx
231 have hxker :
232 (fun j : J => QuotientGroup.mk' (V j : Subgroup (Gs j)) (φ x j)) = 1 := by
233 simpa [MonoidHom.mem_ker, φM] using hx
234 have hxM :
235 ∀ j : J,
236 x ∈ OpenNormalSubgroup.comap (ψ j) ((continuous_apply j.1).comp hφcont) (V j) := by
237 intro j
238 change φ x j ∈ (V j : Subgroup (Gs j))
239 exact (QuotientGroup.eq_one_iff (N := (V j : Subgroup (Gs j))) (φ x j)).1
240 (congrArg
241 (fun f : (j : J) → Gs j ⧸ (V j : Subgroup (Gs j)) => f j)
242 hxker)
243 simpa [M, Subgroup.mem_iInf] using hxM
244 have hQuotM : C (H ⧸ M) := by
245 let e1 : H ⧸ M ≃* H ⧸ φM.ker :=
246 QuotientGroup.quotientMulEquivOfEq hKerEq
247 exact hForm.isomClosed
248 ⟨(e1.trans (QuotientGroup.quotientKerEquivRange φM)).symm⟩
249 hRange
250 have hQuotU :
251 C ((H ⧸ M) ⧸ Subgroup.map (QuotientGroup.mk' M) (U : Subgroup H)) := by
252 exact hForm.quotientClosed
253 (N := Subgroup.map (QuotientGroup.mk' M) (U : Subgroup H)) hQuotM
254 exact hForm.isomClosed
255 ⟨QuotientGroup.quotientQuotientEquivQuotient M (U : Subgroup H) hMU⟩
256 hQuotU
258end
260section BundledSameUniverse
262variable {ι₀ : Type w}
263variable {Gs₀ : ι₀ → Type w}
264variable [∀ i, Group (Gs₀ i)]
265variable [∀ i, TopologicalSpace (Gs₀ i)]
266variable [∀ i, IsTopologicalGroup (Gs₀ i)]
268/-- A closed subgroup of a product of bundled pro-`C` groups is bundled pro-`C`. -/
269theorem ProCGroup.of_closedSubgroup_pi
270 (ProC : ProCGroupPredicate.{w})
271 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientHereditary]
272 [ProC.DeterminedByFiniteQuotients]
273 {H : Subgroup ((i : ι₀) → Gs₀ i)}
274 (hH : IsClosed (((H : Subgroup ((i : ι₀) → Gs₀ i)) : Set ((i : ι₀) → Gs₀ i))))
275 [hGs : ∀ i, ProCGroup ProC (Gs₀ i)] :
276 ProCGroup ProC H :=
277 ProCGroup.of_isProCGroup ProC H
278 (IsProCGroup.of_closedSubgroup_pi.{w, w}
279 (C := ProC.finiteQuotientClass)
280 (Gs := Gs₀)
281 hH
282 ProC.finiteQuotientFormation
283 ProC.finiteQuotientHereditary.subgroupClosed
284 (fun i => (hGs i).isProCGroup))
286/-- Bundled form of `IsProCGroup.of_subdirectProduct`. -/
287theorem ProCGroup.of_subdirectProduct
288 (ProC : ProCGroupPredicate.{w})
289 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
290 {H : Type w} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
292 (φ : H →* ((i : ι₀) → Gs₀ i)) (hφcont : Continuous φ)
293 (hφinj : Function.Injective φ)
294 (hφsurj : ∀ i, Function.Surjective (fun x : H => φ x i))
295 [hGs : ∀ i, ProCGroup ProC (Gs₀ i)] :
296 ProCGroup ProC H :=
297 ProCGroup.of_isProCGroup ProC H
298 (IsProCGroup.of_subdirectProduct.{w, w}
299 (C := ProC.finiteQuotientClass)
300 (Gs := Gs₀)
301 hH φ hφcont hφinj hφsurj
302 ProC.finiteQuotientFormation
303 (fun i => (hGs i).isProCGroup))
305end BundledSameUniverse
307end ProCGroups.ProC