Yamaguchi Lean 4 Library
ProCGroups/ProC/MaximalQuotients/UniversalProperty.lean
ProCGroups/ProC/MaximalQuotients/UniversalProperty/Source

ProCGroups/ProC/MaximalQuotients/UniversalProperty.lean

1import Mathlib.GroupTheory.QuotientGroup.Basic
2import ProCGroups.ProC.MaximalQuotients.ResidualCore
3import ProCGroups.Topologies.QuotientMaps
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/ProC/MaximalQuotients/UniversalProperty.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pro-C groups and open normal quotients
16Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
17-/
19open Set
21namespace ProCGroups.ProC
23universe u
25variable {ProC : ProCGroupPredicate}
27/-- Any normal subgroup with pro-`C` quotient contains the residual core. -/
29 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30 (K : Subgroup G) [K.Normal]
31 (hK : ProC (G := G ⧸ K)) :
32 proCResidualCore ProC G ≤ K := by
33 let N : ProCQuotientKernel ProC G :=
34 { toSubgroup := K
35 normal := inferInstance
36 quotient_isProC := hK }
37 have hle : proCResidualCore ProC G ≤ N.toSubgroup := by
38 simpa [proCResidualCore] using
39 (sInf_le (Set.mem_range_self N) :
40 sInf (Set.range fun N : ProCQuotientKernel ProC G => N.toSubgroup) ≤ N.toSubgroup)
41 intro x hx
42 exact hle hx
45 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
46 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
47 (hsub : IsSubgroupClosedProC ProC)
48 (φ : G →* H) (hφ : Continuous φ) :
49 (proCResidualCore ProC G).map φ ≤ proCResidualCore ProC H := by
50 refine le_sInf ?_
51 intro N hN
52 rw [Set.mem_range] at hN
53 rcases hN with ⟨N, rfl⟩
54 refine Subgroup.map_le_iff_le_comap.2 ?_
55 let α : G →* H ⧸ N.toSubgroup :=
56 (QuotientGroup.mk' N.toSubgroup).comp φ
57 have hα : Continuous α := QuotientGroup.continuous_mk.comp hφ
58 have hkerLift :
59 Continuous (QuotientGroup.kerLift α : G ⧸ α.ker →* H ⧸ N.toSubgroup) := by
60 simpa [QuotientGroup.kerLift, QuotientGroup.lift] using
61 hα.quotient_lift (fun a b hab => by
62 simpa [QuotientGroup.con_ker_eq_conKer α, Con.ker_rel] using hab)
63 have hαker_proC : ProC (G := G ⧸ α.ker) :=
64 hsub.of_injective
65 (QuotientGroup.kerLift α)
66 hkerLift
67 (QuotientGroup.kerLift_injective α)
68 N.quotient_isProC
69 have hαker_eq : α.ker = Subgroup.comap φ N.toSubgroup := by
70 ext x
71 simp only [MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
72 QuotientGroup.eq_one_iff, Subgroup.mem_comap, α]
73 have hcore_le : proCResidualCore ProC G ≤ α.ker :=
74 proCResidualCore_le_of_proCQuotient (ProC := ProC) α.ker hαker_proC
75 rw [hαker_eq] at hcore_le
76 exact hcore_le
78/-- Under subgroup closure, arbitrary continuous homomorphisms send the residual core into the
79residual core. -/
81 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
82 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
83 (hsub : IsSubgroupClosedProC ProC)
84 (φ : G →* H) (hφ : Continuous φ) :
85 (proCResidualCore ProC G).map φ ≤ proCResidualCore ProC H :=
86 map_proCResidualCore_le (ProC := ProC) hsub φ hφ
88/-- Continuous-homomorphism form of residual-core functoriality. -/
90 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
91 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
92 (hsub : IsSubgroupClosedProC ProC)
93 (φ : G →ₜ* H) :
94 (proCResidualCore ProC G).map φ.toMonoidHom ≤ proCResidualCore ProC H :=
95 map_proCResidualCore_le (ProC := ProC) hsub φ.toMonoidHom φ.continuous_toFun
97/-- Any continuous homomorphism to a pro-`C` group kills the residual core, provided the
98pro-`C` predicate is closed under injective continuous homomorphisms. -/
100 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
101 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
103 (φ : G →ₜ* H) (hH : ProC (G := H)) :
104 proCResidualCore ProC G ≤ φ.toMonoidHom.ker := by
105 let K : Subgroup G := φ.toMonoidHom.ker
106 letI : K.Normal := MonoidHom.normal_ker φ.toMonoidHom
107 have hkerLift :
108 Continuous (QuotientGroup.kerLift φ.toMonoidHom : G ⧸ K →* H) := by
109 simpa [K, QuotientGroup.kerLift, QuotientGroup.lift] using
110 φ.continuous_toFun.quotient_lift (fun a b hab => by
111 have hrel : a⁻¹ * b ∈ φ.toMonoidHom.ker := by
112 simpa [K] using (QuotientGroup.leftRel_apply.mp hab)
113 have hEq : (φ a)⁻¹ * φ b = 1 := by
114 simpa [MonoidHom.mem_ker, map_mul, map_inv] using hrel
115 exact inv_mul_eq_one.mp hEq)
116 have hquot : ProC (G := G ⧸ K) :=
117 hsub.of_injective
118 (QuotientGroup.kerLift φ.toMonoidHom)
119 hkerLift
120 (QuotientGroup.kerLift_injective φ.toMonoidHom)
121 hH
122 simpa [K] using proCResidualCore_le_of_proCQuotient (ProC := ProC) (G := G) K hquot
124/-- Universal map out of the maximal pro-`C` quotient: every continuous homomorphism from `G`
125to a pro-`C` group factors through `G / proCResidualCore`. -/
127 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
128 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
130 (φ : G →ₜ* H) (hH : ProC (G := H)) :
131 G ⧸ proCResidualCore ProC G →ₜ* H := by
132 let R : Subgroup G := proCResidualCore ProC G
133 letI : R.Normal := proCResidualCore_normal ProC G
134 have hRker : R ≤ φ.toMonoidHom.ker := by
135 simpa [R] using
137 (ProC := ProC) hsub φ hH
138 exact QuotientGroup.liftₜ R φ hRker
140/-- The lifted map from the residual-core quotient agrees with the original map on quotient
141classes. -/
143 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
144 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
146 (φ : G →ₜ* H) (hH : ProC (G := H)) (x : G) :
147 lift_proCResidualCoreQuotient (ProC := ProC) hsub φ hH
148 (QuotientGroup.mk' (proCResidualCore ProC G) x) = φ x := by
150 rfl
152/-- The lift from the residual-core quotient is unique among continuous homomorphisms agreeing on
153all quotient classes. -/
155 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
156 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
158 (φ : G →ₜ* H) (hH : ProC (G := H))
159 (ψ : G ⧸ proCResidualCore ProC G →ₜ* H)
160 (hψ : ∀ x : G, ψ (QuotientGroup.mk' (proCResidualCore ProC G) x) = φ x) :
161 ψ = lift_proCResidualCoreQuotient (ProC := ProC) hsub φ hH := by
162 apply ContinuousMonoidHom.toMonoidHom_injective
163 apply MonoidHom.ext
164 intro q
165 refine Quotient.inductionOn' q ?_
166 intro x
167 calc
168 ψ (QuotientGroup.mk' (proCResidualCore ProC G) x) = φ x := hψ x
169 _ = lift_proCResidualCoreQuotient (ProC := ProC) hsub φ hH
170 (QuotientGroup.mk' (proCResidualCore ProC G) x) := by
171 exact (lift_proCResidualCoreQuotient_mk (ProC := ProC) hsub φ hH x).symm
173/-- Continuous epimorphisms carry the residual core onto the residual core when the predicate is
174closed under subgroups and surjective continuous images, and the source residual quotient is
175pro-`C`. -/
177 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
178 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
180 (hquotClosed :
181 ∀ {A B : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
182 [Group B] [TopologicalSpace B] [IsTopologicalGroup B],
183 (f : A →* B) → Continuous f → Function.Surjective f →
184 ProC (G := A) → ProC (G := B))
185 (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ)
186 (hcoreQuot :
187 letI : (proCResidualCore ProC G).Normal := proCResidualCore_normal ProC G
188 ProC (G := G ⧸ proCResidualCore ProC G)) :
189 (proCResidualCore ProC G).map φ = proCResidualCore ProC H := by
190 let R : Subgroup G := proCResidualCore ProC G
191 letI : R.Normal := proCResidualCore_normal ProC G
192 let N : Subgroup H := R.map φ
193 have hNnormal : N.Normal := by
194 refine ⟨?_⟩
195 intro y hy h
196 rcases hy with ⟨x, hx, rfl⟩
197 rcases hφsurj h with ⟨g, rfl⟩
198 exact (Subgroup.mem_map).2 ⟨g * x * g⁻¹, (show R.Normal from inferInstance).conj_mem x hx g, by
199 simp only [mul_assoc, map_mul, map_inv]⟩
200 letI : N.Normal := hNnormal
201 have hmap_le :
202 R.map φ ≤ proCResidualCore ProC H :=
203 map_proCResidualCore_le (ProC := ProC) hsub φ hφ
204 have hRle : R ≤ Subgroup.comap φ N := by
205 intro x hx
206 exact (Subgroup.mem_comap).2 <| (Subgroup.mem_map).2 ⟨x, hx, rfl⟩
207 let φₜ : G →ₜ* H :=
208 { toMonoidHom := φ
209 continuous_toFun := hφ }
210 let βₜ : G ⧸ R →ₜ* H ⧸ N := QuotientGroup.mapₜ R N φₜ hRle
211 let β : G ⧸ R →* H ⧸ N := βₜ.toMonoidHom
212 have hβcont : Continuous β := βₜ.continuous_toFun
213 have hβsurj : Function.Surjective β := by
214 have hmkφ_surj : Function.Surjective (QuotientGroup.mk ∘ φ : G → H ⧸ N) := by
215 intro y
216 rcases QuotientGroup.mk'_surjective N y with ⟨h, rfl⟩
217 rcases hφsurj h with ⟨g, rfl⟩
218 exact ⟨g, rfl⟩
219 exact QuotientGroup.map_surjective_of_surjective (N := R) (M := N) φ hmkφ_surj hRle
220 have hNquot : ProC (G := H ⧸ N) := by
221 exact hquotClosed β hβcont hβsurj hcoreQuot
222 have hcoreH_le : proCResidualCore ProC H ≤ N :=
224 exact le_antisymm hmap_le hcoreH_le
226/-- Inside the residual core, any pro-`C` quotient is trivial once the relevant residual-core
227stability equality is available. -/
229 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
230 {R : Subgroup G} [R.Normal]
231 (hR : R = proCResidualCore ProC G)
232 {L : Subgroup ↥R} [L.Normal]
233 (hquot : ProC (G := ↥R ⧸ L))
234 (hmap_eq :
235 (proCResidualCore ProC ↥R).map (R.subtype : ↥R →* G) = proCResidualCore ProC G) :
236 L = ⊤ := by
237 subst hR
238 have hcore_le :
239 proCResidualCore ProC ↥(proCResidualCore ProC G) ≤ L :=
241 have hcore_map_le :
243 L.map ((proCResidualCore ProC G).subtype : ↥(proCResidualCore ProC G) →* G) := by
244 simpa [hmap_eq] using
245 (Subgroup.map_mono
246 (f := ((proCResidualCore ProC G).subtype : ↥(proCResidualCore ProC G) →* G))
247 hcore_le)
248 have htop_map :
249 (⊤ : Subgroup ↥(proCResidualCore ProC G)).map
250 ((proCResidualCore ProC G).subtype : ↥(proCResidualCore ProC G) →* G) =
251 proCResidualCore ProC G := by
252 simpa [MonoidHom.range_eq_map] using
253 (Subgroup.range_subtype (proCResidualCore ProC G))
254 have htop_le :
255 (⊤ : Subgroup ↥(proCResidualCore ProC G)).map
256 ((proCResidualCore ProC G).subtype : ↥(proCResidualCore ProC G) →* G) ≤
257 L.map ((proCResidualCore ProC G).subtype : ↥(proCResidualCore ProC G) →* G) := by
258 rw [htop_map]
259 exact hcore_map_le
260 exact top_le_iff.mp <|
261 (Subgroup.map_subtype_le_map_subtype.1 htop_le)
263/-- The residual core admits no nontrivial pro-`C` quotient once the residual-core stability
264equality for the core subgroup is supplied. -/
266 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
267 {L : Subgroup ↥(proCResidualCore ProC G)} [L.Normal]
268 (hquot : ProC (G := ↥(proCResidualCore ProC G) ⧸ L))
269 (hmap_eq :
270 (proCResidualCore ProC ↥(proCResidualCore ProC G)).map
272 ↥(proCResidualCore ProC G) →* G) =
274 L = ⊤ := by
275 letI : (proCResidualCore ProC G).Normal := by
276 classical
277 change
278 (sInf (Set.range fun N : ProCQuotientKernel ProC G => N.toSubgroup)).Normal
279 simpa [proCResidualCore, sInf_range] using
280 (Subgroup.normal_iInf_normal
281 (a := fun N : ProCQuotientKernel ProC G => N.toSubgroup)
282 (norm := fun N => N.normal))
283 simpa using
285 (ProC := ProC) (G := G) (R := proCResidualCore ProC G) rfl hquot hmap_eq)
287end ProCGroups.ProC