Source: ProCGroups.ProC.InverseLimits.FiniteQuotients
1import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
3/-!
4# Finite quotient objects for pro-\(C\) inverse limits
6This file bundles finite discrete groups and quotients by open normal subgroups as profinite
7objects. It records the induced pro-\(C\) structures and the corresponding product construction.
8-/
10open Set
11open scoped Topology Pointwise
13namespace ProCGroups.ProC
15universe u v
17open InverseSystems
19section
21variable {C : FiniteGroupClass.{u}}
22variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24namespace HasOpenNormalBasisInClass
26/-- Any finite discrete group already lying in the class \(C\) is pro-\(C\). -/
27theorem of_finite_discrete (hquot : FiniteGroupClass.QuotientClosed C)
28 [Finite G] [DiscreteTopology G] (hCG : C G) : HasOpenNormalBasisInClass C G := by
29 letI : Fintype G := Fintype.ofFinite G
30 letI : CompactSpace G := by infer_instance
31 letI : T2Space G := by infer_instance
32 letI : TotallyDisconnectedSpace G := by infer_instance
33 refine HasOpenNormalBasisInClass.of_allOpenNormalQuotients (C := C) (G := G) ?_
34 intro U
35 exact hquot (N := (U : Subgroup G)) hCG
37/--
38If \(G\) is pro-\(C\) and \(C\) is closed under quotients, then every quotient of \(G\) by an
39open normal subgroup is again pro-\(C\).
40-/
41theorem quotient_openNormalSubgroup
42 (hForm : FiniteGroupClass.Formation C)
43 [CompactSpace G] [T2Space G]
44 (hG : HasOpenNormalBasisInClass C G) (U : OpenNormalSubgroup G) :
45 HasOpenNormalBasisInClass C (G ⧸ (U : Subgroup G)) := by
46 letI : Finite (G ⧸ (U : Subgroup G)) :=
47 openNormalSubgroup_finiteQuotient (G := G) U
48 letI : DiscreteTopology (G ⧸ (U : Subgroup G)) :=
49 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U)
50 exact HasOpenNormalBasisInClass.of_finite_discrete (C := C) (G := G ⧸ (U : Subgroup G))
51 hForm.quotientClosed (hG.quotient_mem hForm U)
53/-- Quotients by open normal subgroups in the class-indexing family are pro-\(C\). -/
54theorem quotient_openNormalSubgroupInClass
55 (hquot : FiniteGroupClass.QuotientClosed C)
56 (U : OpenNormalSubgroupInClass C G) :
57 HasOpenNormalBasisInClass C (G ⧸ (U.1 : Subgroup G)) :=
58 by
59 letI : Finite (G ⧸ (U.1 : Subgroup G)) := C.finite U.2
60 letI : DiscreteTopology (G ⧸ (U.1 : Subgroup G)) :=
61 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U.1)
62 exact HasOpenNormalBasisInClass.of_finite_discrete (C := C)
63 (G := G ⧸ (U.1 : Subgroup G)) hquot U.2
65-- Product permanence for pro-`C` groups reduces an open normal subgroup of a product to a finite
66-- product of open normal subgroups, then uses formation closure for the resulting finite quotient.
67/-- Arbitrary products of pro-\(C\) groups remain pro-\(C\) when \(C\) is a formation. -/
68theorem pi {α : Type u} {β : α → Type u}
69 [∀ a, Group (β a)] [∀ a, TopologicalSpace (β a)] [∀ a, IsTopologicalGroup (β a)]
70 [∀ a, CompactSpace (β a)] [∀ a, T2Space (β a)]
71 [∀ a, TotallyDisconnectedSpace (β a)]
72 (hForm : FiniteGroupClass.Formation C)
73 (hβ : ∀ a, HasOpenNormalBasisInClass C (β a)) :
74 HasOpenNormalBasisInClass C ((a : α) → β a) := by
75 classical
76 let G : Type u := (a : α) → β a
77 letI : Group G := by
78 dsimp [G]
79 infer_instance
80 letI : TopologicalSpace G := by
81 dsimp [G]
82 infer_instance
83 letI : IsTopologicalGroup G := by
84 change IsTopologicalGroup ((a : α) → β a)
85 exact Pi.topologicalGroup
86 letI : CompactSpace G := by
87 change CompactSpace ((a : α) → β a)
88 exact Pi.compactSpace
89 letI : T2Space G := by
90 change T2Space ((a : α) → β a)
91 exact Pi.t2Space
92 letI : TotallyDisconnectedSpace G := by
93 change TotallyDisconnectedSpace ((a : α) → β a)
94 exact Pi.totallyDisconnectedSpace
95 refine HasOpenNormalBasisInClass.of_allOpenNormalQuotients (C := C) (G := G) ?_
96 intro U
97 let hUnhds : ((U : Subgroup G) : Set G) ∈ 𝓝 (1 : G) := by
98 exact U.toOpenSubgroup.isOpen'.mem_nhds U.one_mem'
99 rcases mem_nhds_iff.mp hUnhds with ⟨W, hWU, hWopen, h1W⟩
100 rcases (isOpen_pi_iff.mp hWopen) (1 : G) h1W with ⟨J, WJ, hJ1, hJ2⟩
101 let V : ∀ j : J, OpenNormalSubgroup (β j) := fun j =>
102 Classical.choose <|
103 hβ j (WJ j) (hJ1 j j.property).1 (hJ1 j j.property).2
104 have hVsub : ∀ j : J, ((V j : Subgroup (β j)) : Set (β j)) ⊆ WJ j := fun j =>
105 (Classical.choose_spec <|
106 hβ j (WJ j) (hJ1 j j.property).1 (hJ1 j j.property).2).1
107 have hVquot : ∀ j : J, C (β j ⧸ (V j : Subgroup (β j))) := fun j =>
108 (Classical.choose_spec <|
109 hβ j (WJ j) (hJ1 j j.property).1 (hJ1 j j.property).2).2
110 let M : Subgroup G :=
111 iInf fun j : J =>
112 ((OpenNormalSubgroup.comap
113 ({ toFun := fun g : G => g j.1
114 map_one' := rfl
115 map_mul' := by intro x y; rfl } : G →* β j.1)
116 (continuous_apply j.1) (V j) : OpenNormalSubgroup G) : Subgroup G)
117 letI : M.Normal := by
118 exact Subgroup.normal_iInf_normal fun j : J =>
119 (OpenNormalSubgroup.comap
120 ({ toFun := fun g : G => g j.1
121 map_one' := rfl
122 map_mul' := by intro x y; rfl } : G →* β j.1)
123 (continuous_apply j.1) (V j)).isNormal'
124 have hMU : M ≤ (U : Subgroup G) := by
125 intro x hx
126 apply hWU
127 apply hJ2
128 intro j hj
129 have hxall := hx
130 simp only [M, Subgroup.mem_iInf] at hxall
131 have hxj := hxall ⟨j, hj⟩
132 change x j ∈ (V ⟨j, hj⟩ : Subgroup (β j)) at hxj
133 have hxj' : x j ∈ (V ⟨j, hj⟩ : Subgroup (β j)) := hxj
134 exact hVsub ⟨j, hj⟩ hxj'
135 let φ : G →* ∀ j : J, β j ⧸ (V j : Subgroup (β j)) :=
136 { toFun := fun g j => QuotientGroup.mk' (V j : Subgroup (β j)) (g j)
137 map_one' := by funext j; rfl
138 map_mul' := by intro x y; funext j; rfl }
139 have hProd : C (∀ j : J, β j ⧸ (V j : Subgroup (β j))) := by
140 exact FiniteGroupClass.Formation.finiteProductClosed (C := C) hForm hVquot
141 have hRange : C φ.range := by
142 let ψ : φ.range →* ∀ j : J, β j ⧸ (V j : Subgroup (β j)) :=
143 φ.range.subtype
144 have hψinj : Function.Injective ψ := Subtype.coe_injective
145 have hψsurj : ∀ j : J, Function.Surjective fun x : φ.range => ψ x j := by
146 intro j y
147 rcases QuotientGroup.mk'_surjective (V j : Subgroup (β j)) y with ⟨xj, rfl⟩
148 let g : G := Function.update 1 j.1 xj
149 refine ⟨⟨φ g, ⟨g, rfl⟩⟩, ?_⟩
150 change
151 QuotientGroup.mk' (V j : Subgroup (β j)) (g j.1) =
152 QuotientGroup.mk' (V j : Subgroup (β j)) xj
153 simp only [g, Function.update_self]
154 exact hForm.finiteSubdirectProductClosed ψ hψinj hψsurj hVquot
155 have hKerEq : M = φ.ker := by
156 ext x
157 constructor
158 · intro hx
159 have hxM : ∀ j : J, x j.1 ∈ (V j : Subgroup (β j)) := by
160 have hxall := hx
161 simp only [M, Subgroup.mem_iInf] at hxall
162 intro j
163 have hxj := hxall j
164 change x j.1 ∈ (V j : Subgroup (β j)) at hxj
165 exact hxj
166 change (fun j : J => QuotientGroup.mk' (V j : Subgroup (β j)) (x j.1)) = 1
167 funext j
168 exact (QuotientGroup.eq_one_iff (N := (V j : Subgroup (β j))) (x j.1)).2 (hxM j)
169 · intro hx
170 have hx' := (MonoidHom.mem_ker.mp hx)
171 have hxker :
172 (fun j : J => QuotientGroup.mk' (V j : Subgroup (β j)) (x j.1)) = 1 := by
173 change
174 (fun j : J => QuotientGroup.mk' (V j : Subgroup (β j)) (x j.1)) = 1 at hx'
175 exact hx'
176 have hxM : ∀ j : J, x j.1 ∈ (V j : Subgroup (β j)) := by
177 intro j
178 exact (QuotientGroup.eq_one_iff (N := (V j : Subgroup (β j))) (x j.1)).1
179 (congrArg (fun f : (j : J) → β j ⧸ (V j : Subgroup (β j)) => f j) hxker)
180 simp only [M, Subgroup.mem_iInf]
181 intro j
182 change x j.1 ∈ (V j : Subgroup (β j))
183 exact hxM j
184 have hQuotM : C (G ⧸ M) := by
185 let e1 : G ⧸ M ≃* G ⧸ φ.ker :=
186 QuotientGroup.quotientMulEquivOfEq hKerEq
187 exact hForm.isomClosed
188 ⟨(e1.trans (QuotientGroup.quotientKerEquivRange φ)).symm⟩
189 hRange
190 have hQuotU' :
191 C ((G ⧸ M) ⧸ Subgroup.map (QuotientGroup.mk' M) (U : Subgroup G)) := by
192 exact hForm.quotientClosed
193 (N := Subgroup.map (QuotientGroup.mk' M) (U : Subgroup G)) hQuotM
194 exact hForm.isomClosed
195 ⟨QuotientGroup.quotientQuotientEquivQuotient M (U : Subgroup G) hMU⟩
196 hQuotU'
198end HasOpenNormalBasisInClass
200/-- Every profinite group has an open-normal basis with finite quotients. -/
201theorem hasOpenNormalBasisInClass_allFinite
202 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
203 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
204 HasOpenNormalBasisInClass FiniteGroupClass.allFinite G := by
205 refine HasOpenNormalBasisInClass.of_allOpenNormalQuotients (C := FiniteGroupClass.allFinite) ?_
206 intro U
207 exact openNormalSubgroup_finiteQuotient (G := G) U
209end
211end ProCGroups.ProC