ProCGroups/ProC/InverseLimits/Limits.lean
1import ProCGroups.InverseSystems.FiniteStageFactorization
2import ProCGroups.ProC.InverseLimits.FiniteQuotients
3import ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies
4import ProCGroups.Topologies.ContinuousMulEquiv
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/ProC/InverseLimits/Limits.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Pro-C groups and open normal quotients
17Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
18-/
20open Set
21open scoped Topology Pointwise
23namespace ProCGroups.ProC
25universe u v
27open InverseSystems
29section
31variable {C : FiniteGroupClass.{u}}
32variable {I : Type u} [Preorder I] [Nonempty I]
33variable (S : InverseSystems.InverseSystem (I := I))
34instance instTopologicalSpaceX (i : I) : TopologicalSpace (S.X i) := S.topologicalSpace i
35variable [∀ i, Group (S.X i)]
36variable [∀ i, IsTopologicalGroup (S.X i)]
37variable [InverseSystems.IsGroupSystem S]
39/-- A directed inverse limit of pro-`C` groups is pro-`C`. -/
40theorem inverseLimit
41 (hIso : FiniteGroupClass.IsomClosed C)
42 (hQuot : FiniteGroupClass.QuotientClosed C)
43 (hdir : Directed (· ≤ ·) (id : I → I))
44 (hX : ∀ i, IsProCGroup C (S.X i)) :
45 IsProCGroup C S.inverseLimit := by
46 letI : ∀ i, CompactSpace (S.X i) := fun i => IsProCGroup.compactSpace (hX i)
47 letI : ∀ i, T2Space (S.X i) := fun i => IsProCGroup.t2Space (hX i)
48 letI : ∀ i, TotallyDisconnectedSpace (S.X i) := fun i =>
49 IsProCGroup.totallyDisconnectedSpace (hX i)
50 refine IsProCGroup.of_allOpenNormalQuotients (C := C)
51 ⟨inferInstance,
52 inferInstance,
53 InverseSystems.InverseSystem.t2Space_inverseLimit (S := S),
54 InverseSystems.InverseSystem.totallyDisconnectedSpace_inverseLimit (S := S)⟩ ?_
55 intro U
56 letI : CompactSpace S.inverseLimit := inferInstance
57 letI : T2Space S.inverseLimit := InverseSystems.InverseSystem.t2Space_inverseLimit (S := S)
58 letI : Finite (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
59 openNormalSubgroup_finiteQuotient (G := S.inverseLimit) U
60 letI : DiscreteTopology (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
61 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := S.inverseLimit) U)
62 let β : S.inverseLimit →* S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) :=
63 QuotientGroup.mk' (U : Subgroup S.inverseLimit)
64 rcases InverseSystems.InverseSystem.factors_through_projection_finite_group_hom
65 (S := S) hdir β continuous_quotient_mk' with ⟨k, βk, hβk_continuous, hβfac⟩
66 have hβk_surj : Function.Surjective βk := by
67 intro q
68 rcases QuotientGroup.mk'_surjective (U : Subgroup S.inverseLimit) q with ⟨x, rfl⟩
69 exact ⟨S.projection k x, by
70 simpa [Function.comp] using
71 (congrArg (fun f : S.inverseLimit → S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) =>
72 f x) hβfac).symm⟩
73 have hker_closed : IsClosed ((βk.ker : Subgroup (S.X k)) : Set (S.X k)) := by
74 simpa [MonoidHom.mem_ker] using
75 isClosed_eq hβk_continuous continuous_const
76 have hker_finite : Finite (S.X k ⧸ βk.ker) := by
77 exact Finite.of_injective (QuotientGroup.quotientKerEquivOfSurjective βk hβk_surj)
78 (QuotientGroup.quotientKerEquivOfSurjective βk hβk_surj).injective
79 have hker_open : IsOpen ((βk.ker : Subgroup (S.X k)) : Set (S.X k)) :=
80 (subgroup_isOpen_iff_isClosed_finite_quotient (G := S.X k) (U := βk.ker)).2
81 ⟨hker_closed, hker_finite⟩
82 let V : OpenNormalSubgroup (S.X k) :=
83 { toOpenSubgroup := ⟨βk.ker, hker_open⟩
84 isNormal' := inferInstance }
85 have hQV : C (S.X k ⧸ (V : Subgroup (S.X k))) :=
86 IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
87 hIso hQuot (hX k) V
88 exact hIso ⟨QuotientGroup.quotientKerEquivOfSurjective βk hβk_surj⟩ hQV
90variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
92/-- If `G` is pro-`C` and `C` is
93closed under quotients, then every quotient of `G` by a closed normal subgroup is again pro-`C`.
96normal subgroups `U` containing `K`, then applies the inverse-limit permanence result above.
97-/
98theorem quotient_closedNormalSubgroup
99 (hIso : FiniteGroupClass.IsomClosed C)
100 (hQuot : FiniteGroupClass.QuotientClosed C)
101 (hG : IsProCGroup C G)
102 (K : Subgroup G) [K.Normal] (hK : IsClosed (K : Set G)) :
103 IsProCGroup C (G ⧸ K) := by
104 classical
105 let topU : OpenNormalSubgroup G :=
106 { toOpenSubgroup := ⟨⊤, isOpen_univ⟩
107 isNormal' := inferInstance }
108 letI : Nonempty (OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}) :=
109 ⟨OrderDual.toDual ⟨topU, le_top⟩⟩
110 let S : InverseSystems.InverseSystem
111 (I := OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}) := {
112 X := fun U => G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
113 topologicalSpace := fun _ => inferInstance
114 map := fun {U V} hUV =>
115 QuotientGroup.map
116 (((OrderDual.ofDual V).1 : OpenNormalSubgroup G) : Subgroup G)
117 (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
118 (MonoidHom.id G)
119 hUV
120 continuous_map := by
121 intro U V hUV
122 letI : DiscreteTopology
123 (G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)) :=
124 QuotientGroup.discreteTopology
125 (openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
126 exact continuous_of_discreteTopology
127 map_id := by
128 intro U
129 simp only [QuotientGroup.map_id, MonoidHom.coe_id]
130 map_comp := by
131 intro U V W hUV hVW
132 funext x
133 simpa [Function.comp] using congrArg (fun f => f x)
134 (QuotientGroup.map_comp_map
135 (N := (((OrderDual.ofDual W).1 : OpenNormalSubgroup G) : Subgroup G))
136 (M := (((OrderDual.ofDual V).1 : OpenNormalSubgroup G) : Subgroup G))
137 (O := (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))
138 (f := MonoidHom.id G) (g := MonoidHom.id G) hVW hUV) }
139 letI : InverseSystems.IsGroupSystem S := {
141 intro i j hij
142 rfl
144 intro i j hij x y
145 change
146 QuotientGroup.map
147 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
148 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
149 (MonoidHom.id G) hij (x * y) =
150 QuotientGroup.map
151 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
152 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
153 (MonoidHom.id G) hij x *
154 QuotientGroup.map
155 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
156 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
157 (MonoidHom.id G) hij y
158 exact
159 (QuotientGroup.map
160 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
161 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
163 map_inv := by
164 intro i j hij x
165 change
166 QuotientGroup.map
167 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
168 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
169 (MonoidHom.id G) hij x⁻¹ =
170 (QuotientGroup.map
171 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
172 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
173 (MonoidHom.id G) hij x)⁻¹
174 exact
175 (QuotientGroup.map
176 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
177 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
178 (MonoidHom.id G) hij).map_inv x }
179 have hdir :
180 Directed (· ≤ ·) (id : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)} →
181 OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}) := by
182 intro i j
183 refine ⟨OrderDual.toDual ⟨(OrderDual.ofDual i).1 ⊓ (OrderDual.ofDual j).1, ?_⟩, ?_, ?_⟩
184 · intro x hx
185 exact ⟨(OrderDual.ofDual i).2 hx, (OrderDual.ofDual j).2 hx⟩
186 · exact show
187 (((OrderDual.ofDual i).1 ⊓ (OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G) ≤
188 ((OrderDual.ofDual i).1 : Subgroup G) from inf_le_left
189 · exact show
190 (((OrderDual.ofDual i).1 ⊓ (OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G) ≤
191 ((OrderDual.ofDual j).1 : Subgroup G) from inf_le_right
192 have hX :
193 ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}, IsProCGroup C (S.X i) :=
194 by
195 intro i
196 let U : OpenNormalSubgroup G := (OrderDual.ofDual i).1
197 letI : Finite (G ⧸ (U : Subgroup G)) := hG.finite_quotient U
198 letI : DiscreteTopology (G ⧸ (U : Subgroup G)) :=
199 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U)
200 exact IsProCGroup.of_finite_discrete (C := C) (G := G ⧸ (U : Subgroup G))
201 hQuot
202 (IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
203 hIso hQuot hG U)
204 letI : ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}, T2Space (S.X i) :=
205 fun i => IsProCGroup.t2Space (hX i)
206 have hSinv : IsProCGroup C S.inverseLimit :=
207 inverseLimit (C := C) (S := S) hIso hQuot hdir hX
208 let ψ :
209 ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)},
210 G ⧸ K → S.X i := fun i =>
211 QuotientGroup.map
212 K
213 (((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G)
214 (MonoidHom.id G)
215 (OrderDual.ofDual i).2
216 have hψcont :
217 ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}, Continuous (ψ i) := by
218 intro i
219 let U : Subgroup G := (((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G)
220 have hmk : Continuous (QuotientGroup.mk' U : G → G ⧸ U) := continuous_quotient_mk'
221 have hconst :
222 ∀ a b : G, QuotientGroup.leftRel K a b →
223 (QuotientGroup.mk' U) a = (QuotientGroup.mk' U) b := by
224 intro a b hab
225 apply QuotientGroup.eq.2
226 exact (OrderDual.ofDual i).2 (by simpa using (QuotientGroup.leftRel_apply.mp hab))
227 simpa [ψ, U, QuotientGroup.map, MonoidHom.comp_apply] using hmk.quotient_lift hconst
228 have hψcompat : S.CompatibleMaps ψ := by
229 intro i j hij
230 funext x
231 rcases QuotientGroup.mk'_surjective K x with ⟨g, rfl⟩
232 rfl
233 let φ : G ⧸ K →* S.inverseLimit := {
234 toFun := S.inverseLimitLift ψ hψcompat
235 map_one' := by
236 apply S.ext
237 intro i
238 rfl
239 map_mul' := by
240 intro x y
241 apply S.ext
242 intro i
243 rcases QuotientGroup.mk'_surjective K x with ⟨gx, rfl⟩
244 rcases QuotientGroup.mk'_surjective K y with ⟨gy, rfl⟩
245 rfl }
246 have hφcont : Continuous φ := S.continuous_inverseLimitLift ψ hψcont hψcompat
247 have hφsurj : Function.Surjective φ := by
248 letI : CompactSpace (G ⧸ K) := by
249 letI : CompactSpace G := IsProCGroup.compactSpace hG
250 infer_instance
251 letI : T2Space (G ⧸ K) := by
252 letI : T2Space G := IsProCGroup.t2Space hG
253 letI : IsClosed (K : Set G) := hK
254 infer_instance
255 exact InverseSystems.InverseSystem.surjective_inverseLimitLift
256 (S := S) ψ hψcont hψcompat
257 (fun i => by
258 intro x
259 rcases QuotientGroup.mk'_surjective
260 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G)) x with ⟨g, rfl⟩
261 exact ⟨QuotientGroup.mk' K g, rfl⟩)
262 hdir
263 have hφinj : Function.Injective φ := by
264 intro x y hxy
265 rcases QuotientGroup.mk'_surjective K x with ⟨gx, rfl⟩
266 rcases QuotientGroup.mk'_surjective K y with ⟨gy, rfl⟩
267 apply QuotientGroup.eq.2
268 have hmem :
269 ∀ U : OpenNormalSubgroup G, K ≤ (U : Subgroup G) → gx⁻¹ * gy ∈ (U : Subgroup G) := by
270 intro U hKU
271 let i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)} :=
272 OrderDual.toDual ⟨U, hKU⟩
273 have hi : ψ i (QuotientGroup.mk' K gx) = ψ i (QuotientGroup.mk' K gy) := by
274 simpa [φ] using congrArg (fun z : S.inverseLimit => S.projection i z) hxy
275 exact QuotientGroup.eq.mp hi
276 let HC : ClosedSubgroup G := { toSubgroup := K, isClosed' := hK }
277 letI : CompactSpace G := IsProCGroup.compactSpace hG
278 letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
279 have hx :
280 gx⁻¹ * gy ∈
281 sInf {N : Subgroup G | IsOpen (N : Set G) ∧ K ≤ N ∧ N.Normal} := by
282 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
283 intro N hN
284 let U : OpenNormalSubgroup G :=
285 { toOpenSubgroup := ⟨N, hN.1⟩
286 isNormal' := hN.2.2 }
287 exact hmem U hN.2.1
288 have hxK : gx⁻¹ * gy ∈ K := by
289 have hEq :
290 (K : Subgroup G) =
291 sInf {N : Subgroup G | IsOpen (N : Set G) ∧ K ≤ N ∧ N.Normal} :=
292 closedSubgroup_eq_sInf_openNormal (G := G) HC
293 exact hEq.symm ▸ hx
294 exact hxK
295 letI : CompactSpace (G ⧸ K) := by
296 letI : CompactSpace G := IsProCGroup.compactSpace hG
297 infer_instance
298 letI : T2Space S.inverseLimit := IsProCGroup.t2Space hSinv
299 let e : G ⧸ K ≃ₜ* S.inverseLimit :=
300 ContinuousMulEquiv.ofBijectiveCompactToT2 φ hφcont ⟨hφinj, hφsurj⟩
301 simpa using IsProCGroup.ofContinuousMulEquiv (C := C) hIso hQuot hSinv e.symm
303end
305end ProCGroups.ProC