Source: ProCGroups.ProC.MaximalQuotients.UniversalProperty
1import Mathlib.GroupTheory.QuotientGroup.Basic
2import ProCGroups.ProC.MaximalQuotients.ResidualCore
3import ProCGroups.ProC.Quotients.ClosedNormal
4import ProCGroups.ProC.Subgroups.Closed
5import ProCGroups.Topologies.QuotientMaps
7/-!
8# The pro-\(C\) residual quotient
10For a hereditary finite-group class, continuous maps from compact groups into
11pro-\(C\) targets kill the residual core and therefore factor uniquely through
12the residual quotient. The file also proves functoriality of the core and its
13behaviour under continuous epimorphisms for full formations.
14-/
16open Set
18namespace ProCGroups.ProC
20universe u
22variable {C : FiniteGroupClass}
24/-- Any closed normal subgroup whose quotient has an open-normal quotient-in-\(C\) basis contains
25the residual core. -/
26theorem proCResidualCore_le_of_proCQuotient
27 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28 (K : Subgroup G) [K.Normal]
29 (hKclosed : IsClosed (K : Set G))
30 (hK : HasOpenNormalBasisInClass C (G ⧸ K)) :
31 proCResidualCore C G ≤ K := by
32 let N : ProCQuotientKernel C G :=
33 { toSubgroup := K
34 isClosed' := hKclosed
35 normal := inferInstance
36 quotient_hasOpenNormalBasisInClass := hK }
37 have hle : proCResidualCore C G ≤ N.toSubgroup := by
38 simpa [proCResidualCore] using
39 (sInf_le (Set.mem_range_self N) :
40 sInf (Set.range fun N : ProCQuotientKernel C G => N.toSubgroup) ≤ N.toSubgroup)
41 intro x hx
42 exact hle hx
44/-- A compact group's quotient by the kernel of a continuous map into a group with an open-normal
45quotient-in-\(C\) basis inherits that basis property when `C` is hereditary. -/
46private theorem hasOpenNormalBasisInClass_quotient_ker
47 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
48 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
49 (hHer : FiniteGroupClass.Hereditary C)
50 (f : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H) :
51 HasOpenNormalBasisInClass C (G ⧸ f.toMonoidHom.ker) := by
52 have hRange : HasOpenNormalBasisInClass C f.toMonoidHom.range :=
53 HasOpenNormalBasisInClass.of_isClosed_subgroup
54 C.isomClosed hHer.subgroupClosed hH f.toMonoidHom.range (ContinuousMonoidHom.isClosed_range f)
55 exact HasOpenNormalBasisInClass.ofContinuousMulEquiv hRange
56 (ContinuousMonoidHom.quotientKerContinuousMulEquivRange f).symm
58/-- Under hereditary finite quotients, continuous homomorphisms from compact groups send the
59residual core into the residual core. -/
60theorem map_proCResidualCore_le_of_hom
61 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
62 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
63 (hHer : FiniteGroupClass.Hereditary C)
64 (φ : G →* H) (hφ : Continuous φ) :
65 (proCResidualCore C G).map φ ≤ proCResidualCore C H := by
66 refine le_sInf ?_
67 intro N hN
68 rw [Set.mem_range] at hN
69 rcases hN with ⟨N, rfl⟩
70 letI : IsClosed (N.toSubgroup : Set H) := N.isClosed'
71 refine Subgroup.map_le_iff_le_comap.2 ?_
72 let α : G →ₜ* H ⧸ N.toSubgroup :=
73 { toMonoidHom := (QuotientGroup.mk' N.toSubgroup).comp φ
74 continuous_toFun := QuotientGroup.continuous_mk.comp hφ }
75 have hαker_proC : HasOpenNormalBasisInClass C (G ⧸ α.toMonoidHom.ker) :=
76 hasOpenNormalBasisInClass_quotient_ker hHer α N.quotient_hasOpenNormalBasisInClass
77 have hαker_eq : α.toMonoidHom.ker = Subgroup.comap φ N.toSubgroup := by
78 ext x
79 simp only [MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
80 QuotientGroup.eq_one_iff, Subgroup.mem_comap, α]
81 have hcore_le : proCResidualCore C G ≤ α.toMonoidHom.ker :=
82 proCResidualCore_le_of_proCQuotient (C := C) α.toMonoidHom.ker
83 (ContinuousMonoidHom.isClosed_ker α) hαker_proC
84 rw [hαker_eq] at hcore_le
85 exact hcore_le
87/--
88A continuous monoid homomorphism sends the pro-\(C\) residual core of the source into the
89pro-\(C\) residual core of the target.
90-/
91theorem map_proCResidualCore_le_of_continuousMonoidHom
92 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
93 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
94 (hHer : FiniteGroupClass.Hereditary C)
95 (φ : G →ₜ* H) :
96 (proCResidualCore C G).map φ.toMonoidHom ≤ proCResidualCore C H :=
97 map_proCResidualCore_le_of_hom (C := C) hHer φ.toMonoidHom φ.continuous_toFun
99/-- Any continuous homomorphism from a compact group to a group with an open-normal
100quotient-in-\(C\) basis kills the residual core when `C` is hereditary. -/
101theorem proCResidualCore_le_ker_of_continuousMonoidHom_to_proC
102 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
103 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
104 (hHer : FiniteGroupClass.Hereditary C)
105 (φ : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H) :
106 proCResidualCore C G ≤ φ.toMonoidHom.ker := by
107 let K : Subgroup G := φ.toMonoidHom.ker
108 letI : K.Normal := MonoidHom.normal_ker φ.toMonoidHom
109 have hquot : HasOpenNormalBasisInClass C (G ⧸ K) := by
110 simpa [K] using hasOpenNormalBasisInClass_quotient_ker hHer φ hH
111 simpa [K] using
112 proCResidualCore_le_of_proCQuotient (C := C) (G := G) K (ContinuousMonoidHom.isClosed_ker φ)
113 hquot
115/-- Every continuous homomorphism from \(G\) to a group with an open-normal quotient-in-\(C\)
116basis factors through the quotient by the pro-\(C\) residual core. -/
117noncomputable def lift_proCResidualCoreQuotient
118 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
119 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
120 (hHer : FiniteGroupClass.Hereditary C)
121 (φ : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H) :
122 G ⧸ proCResidualCore C G →ₜ* H := by
123 let R : Subgroup G := proCResidualCore C G
124 letI : R.Normal := proCResidualCore_normal C G
125 have hRker : R ≤ φ.toMonoidHom.ker := by
126 simpa [R] using
127 proCResidualCore_le_ker_of_continuousMonoidHom_to_proC
128 (C := C) hHer φ hH
129 exact QuotientGroup.liftₜ R φ hRker
131/--
132The lifted map from the residual-core quotient agrees with the original map on quotient classes.
133-/
134@[simp] theorem lift_proCResidualCoreQuotient_mk
135 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
136 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
137 (hHer : FiniteGroupClass.Hereditary C)
138 (φ : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H) (x : G) :
139 lift_proCResidualCoreQuotient (C := C) hHer φ hH
140 (QuotientGroup.mk' (proCResidualCore C G) x) = φ x := by
141 dsimp [lift_proCResidualCoreQuotient]
142 rfl
144/--
145The lift from the residual-core quotient is unique among continuous homomorphisms agreeing on
146all quotient classes.
147-/
148theorem lift_proCResidualCoreQuotient_unique
149 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
150 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
151 (hHer : FiniteGroupClass.Hereditary C)
152 (φ : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H)
153 (ψ : G ⧸ proCResidualCore C G →ₜ* H)
154 (hψ : ∀ x : G, ψ (QuotientGroup.mk' (proCResidualCore C G) x) = φ x) :
155 ψ = lift_proCResidualCoreQuotient (C := C) hHer φ hH := by
156 apply ContinuousMonoidHom.toMonoidHom_injective
157 apply MonoidHom.ext
158 intro q
159 refine Quotient.inductionOn' q ?_
160 intro x
161 calc
162 ψ (QuotientGroup.mk' (proCResidualCore C G) x) = φ x := hψ x
163 _ = lift_proCResidualCoreQuotient (C := C) hHer φ hH
164 (QuotientGroup.mk' (proCResidualCore C G) x) := by
165 exact (lift_proCResidualCoreQuotient_mk (C := C) hHer φ hH x).symm
167/-- Continuous epimorphisms carry the residual core onto the residual core for a full formation
168when the source residual quotient is pro-\(C\). -/
169theorem map_proCResidualCore_eq_of_surjective
170 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
171 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
172 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
173 (hC : FiniteGroupClass.FullFormation C)
174 (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ)
175 (hcoreQuot :
176 letI : (proCResidualCore C G).Normal := proCResidualCore_normal C G
177 HasOpenNormalBasisInClass C (G ⧸ proCResidualCore C G)) :
178 (proCResidualCore C G).map φ = proCResidualCore C H := by
179 let R : Subgroup G := proCResidualCore C G
180 letI : R.Normal := proCResidualCore_normal C G
181 let N : Subgroup H := R.map φ
182 have hNnormal : N.Normal := by
183 refine ⟨?_⟩
184 intro y hy h
185 rcases hy with ⟨x, hx, rfl⟩
186 rcases hφsurj h with ⟨g, rfl⟩
187 exact (Subgroup.mem_map).2 ⟨g * x * g⁻¹, (show R.Normal from inferInstance).conj_mem x hx g, by
188 simp only [mul_assoc, map_mul, map_inv]⟩
189 letI : N.Normal := hNnormal
190 have hRclosed : IsClosed (R : Set G) := by
191 simpa [R] using proCResidualCore_isClosed C G
192 letI : IsClosed (R : Set G) := hRclosed
193 letI : TotallyDisconnectedSpace (G ⧸ R) :=
195 have hNclosed : IsClosed (N : Set H) := by
196 simpa [N, Subgroup.coe_map] using (hRclosed.isCompact.image hφ).isClosed
197 letI : IsClosed (N : Set H) := hNclosed
198 have hmap_le :
199 R.map φ ≤ proCResidualCore C H :=
200 map_proCResidualCore_le_of_hom (C := C) hC.hereditary φ hφ
201 have hRle : R ≤ Subgroup.comap φ N := by
202 intro x hx
203 exact (Subgroup.mem_comap).2 <| (Subgroup.mem_map).2 ⟨x, hx, rfl⟩
204 let φₜ : G →ₜ* H :=
205 { toMonoidHom := φ
206 continuous_toFun := hφ }
207 let βₜ : G ⧸ R →ₜ* H ⧸ N := QuotientGroup.mapₜ R N φₜ hRle
208 let β : G ⧸ R →* H ⧸ N := βₜ.toMonoidHom
209 have hβsurj : Function.Surjective β := by
210 have hmkφ_surj : Function.Surjective (QuotientGroup.mk ∘ φ : G → H ⧸ N) := by
211 intro y
212 rcases QuotientGroup.mk'_surjective N y with ⟨h, rfl⟩
213 rcases hφsurj h with ⟨g, rfl⟩
214 exact ⟨g, rfl⟩
215 exact QuotientGroup.map_surjective_of_surjective (N := R) (M := N) φ hmkφ_surj hRle
216 letI : T2Space (H ⧸ N) := by infer_instance
217 have hNquot : HasOpenNormalBasisInClass C (H ⧸ N) :=
218 HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation hcoreQuot βₜ hβsurj
219 have hcoreH_le : proCResidualCore C H ≤ N :=
220 proCResidualCore_le_of_proCQuotient (C := C) N hNclosed hNquot
221 exact le_antisymm hmap_le hcoreH_le
223end ProCGroups.ProC