ProCGroups/FreeProducts/Concrete.lean
1import ProCGroups.FreeProducts.UniversalProperty
2import ProCGroups.ProC.InverseLimits.Limits
3import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
4import ProCGroups.ProC.OpenNormalSubgroups.Separation
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/FreeProducts/Concrete.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Free pro-C products
17Constructs free pro-C products from finite admissible quotients and proves the universal property and comparison isomorphisms.
18-/
20open scoped Monoid.Coprod Topology
22namespace ProCGroups.FreeProducts
24universe u
26namespace Concrete
28variable {A B : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
29variable [Group B] [TopologicalSpace B] [IsTopologicalGroup B]
31/-- The abstract group underlying the binary free product of the two factors. -/
32abbrev AbstractFreeProduct (A B : Type u) [Group A] [Group B] :=
33 A ∗ B
35variable {C : ProCGroups.FiniteGroupClass.{u}}
37/-- An admissible finite quotient of the abstract free product: the quotient lies in `C`, and the
38two factor maps into that quotient are continuous. -/
39structure AdmissibleQuotient (C : ProCGroups.FiniteGroupClass.{u})
40 (A B : Type u) [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
41 [Group B] [TopologicalSpace B] [IsTopologicalGroup B] where
42 toSubgroup : Subgroup (AbstractFreeProduct A B)
43 normal' : toSubgroup.Normal
44 quotient_mem' : C (AbstractFreeProduct A B ⧸ toSubgroup)
45 inl_continuous' :
46 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ toSubgroup) := ⊥
47 Continuous ((QuotientGroup.mk' toSubgroup).comp
48 (Monoid.Coprod.inl : A →* AbstractFreeProduct A B))
49 inr_continuous' :
50 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ toSubgroup) := ⊥
51 Continuous ((QuotientGroup.mk' toSubgroup).comp
52 (Monoid.Coprod.inr : B →* AbstractFreeProduct A B))
54namespace AdmissibleQuotient
56/-- Coerce an admissible quotient to its underlying normal subgroup of the abstract free
57product. -/
58instance instCoeOutAdmissibleQuotient :
59 CoeOut (AdmissibleQuotient C A B) (Subgroup (AbstractFreeProduct A B)) where
60 coe U := U.toSubgroup
62/-- The subgroup underlying an admissible quotient is normal. -/
63instance instNormalCoeAdmissibleQuotient (U : AdmissibleQuotient C A B) :
64 (U : Subgroup (AbstractFreeProduct A B)).Normal :=
65 U.normal'
67/-- Order admissible quotients by reverse inclusion of their kernels. -/
68instance instLEAdmissibleQuotient : LE (AdmissibleQuotient C A B) where
69 le U V := (V : Subgroup (AbstractFreeProduct A B)) ≤
70 (U : Subgroup (AbstractFreeProduct A B))
72/-- Admissible quotients form a preorder under reverse inclusion of kernels. -/
73instance instPreorderAdmissibleQuotient : Preorder (AdmissibleQuotient C A B) where
74 le := fun U V => (V : Subgroup (AbstractFreeProduct A B)) ≤
75 (U : Subgroup (AbstractFreeProduct A B))
76 le_refl U := le_rfl
77 le_trans U V W hUV hVW := hVW.trans hUV
79/-- The finite admissible quotient attached to an admissible quotient lies in the class `C`. -/
80theorem quotient_mem (U : AdmissibleQuotient C A B) :
81 C (AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B))) :=
82 U.quotient_mem'
84/-- The left inclusion into an admissible quotient is continuous. -/
85theorem inl_continuous (U : AdmissibleQuotient C A B) :
86 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B))) :=
87 ⊥
88 Continuous ((QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))).comp
89 (Monoid.Coprod.inl : A →* AbstractFreeProduct A B)) :=
90 U.inl_continuous'
92/-- The right inclusion into an admissible quotient is continuous. -/
93theorem inr_continuous (U : AdmissibleQuotient C A B) :
94 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B))) :=
95 ⊥
96 Continuous ((QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))).comp
97 (Monoid.Coprod.inr : B →* AbstractFreeProduct A B)) :=
98 U.inr_continuous'
100/-- The canonical transition map between admissible free-product quotients. -/
101def map {U V : AdmissibleQuotient C A B}
102 (hUV : (V : Subgroup (AbstractFreeProduct A B)) ≤
103 (U : Subgroup (AbstractFreeProduct A B))) :
104 AbstractFreeProduct A B ⧸ (V : Subgroup (AbstractFreeProduct A B)) →*
105 AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B)) :=
106 QuotientGroup.map _ _ (MonoidHom.id (AbstractFreeProduct A B)) hUV
108/-- Transition maps between admissible quotients are surjective. -/
109theorem map_surjective {U V : AdmissibleQuotient C A B}
110 (hUV : (V : Subgroup (AbstractFreeProduct A B)) ≤
111 (U : Subgroup (AbstractFreeProduct A B))) :
112 Function.Surjective (map (C := C) (A := A) (B := B) hUV) := by
113 intro x
114 rcases QuotientGroup.mk'_surjective
115 (U : Subgroup (AbstractFreeProduct A B)) x with ⟨g, rfl⟩
116 exact ⟨QuotientGroup.mk' (V : Subgroup (AbstractFreeProduct A B)) g, rfl⟩
118/-- The transition map from an admissible quotient to itself is the identity. -/
119theorem map_id (U : AdmissibleQuotient C A B) :
120 map (C := C) (A := A) (B := B)
121 (le_rfl : (U : Subgroup (AbstractFreeProduct A B)) ≤
122 (U : Subgroup (AbstractFreeProduct A B))) = MonoidHom.id _ := by
123 simp only [map, QuotientGroup.map_id]
125/-- Transition maps between admissible quotients compose along refinements. -/
126theorem map_comp {U V W : AdmissibleQuotient C A B}
127 (hUV : (V : Subgroup (AbstractFreeProduct A B)) ≤
128 (U : Subgroup (AbstractFreeProduct A B)))
129 (hVW : (W : Subgroup (AbstractFreeProduct A B)) ≤
130 (V : Subgroup (AbstractFreeProduct A B))) :
131 (map (C := C) (A := A) (B := B) hUV).comp
132 (map (C := C) (A := A) (B := B) hVW) =
133 map (C := C) (A := A) (B := B) (hVW.trans hUV) := by
134 simpa [map] using QuotientGroup.map_comp_map
135 (N := (W : Subgroup (AbstractFreeProduct A B)))
136 (M := (V : Subgroup (AbstractFreeProduct A B)))
137 (O := (U : Subgroup (AbstractFreeProduct A B)))
138 (f := MonoidHom.id (AbstractFreeProduct A B))
139 (g := MonoidHom.id (AbstractFreeProduct A B)) hVW hUV
141/-- The top quotient, used as a nonempty index. -/
142noncomputable def quotientTopMulEquivPUnit (G : Type u) [Group G] :
143 G ⧸ (⊤ : Subgroup G) ≃* PUnit where
144 toFun := fun _ => PUnit.unit
145 invFun := fun _ => 1
146 left_inv := by
147 intro x
148 refine Quotient.inductionOn' x ?_
149 intro g
150 apply QuotientGroup.eq.2
151 simp only [inv_one, one_mul, Subgroup.mem_top]
152 right_inv := by
153 intro x
154 cases x
155 rfl
156 map_mul' := by
157 intro x y
158 rfl
160/-- The trivial admissible quotient. -/
161noncomputable def top (hForm : ProCGroups.FiniteGroupClass.Formation C) :
162 AdmissibleQuotient C A B where
163 toSubgroup := ⊤
164 normal' := inferInstance
165 quotient_mem' :=
166 hForm.isomClosed ⟨(quotientTopMulEquivPUnit (AbstractFreeProduct A B)).symm⟩
167 hForm.one_mem
168 inl_continuous' := by
169 letI : TopologicalSpace (AbstractFreeProduct A B ⧸
170 (⊤ : Subgroup (AbstractFreeProduct A B))) := ⊥
171 refine (continuous_const : Continuous fun _ : A =>
172 (1 : AbstractFreeProduct A B ⧸
173 (⊤ : Subgroup (AbstractFreeProduct A B)))).congr ?_
174 intro a
175 apply QuotientGroup.eq.2
176 simp only [inv_one, one_mul, Subgroup.mem_top]
177 inr_continuous' := by
178 letI : TopologicalSpace (AbstractFreeProduct A B ⧸
179 (⊤ : Subgroup (AbstractFreeProduct A B))) := ⊥
180 refine (continuous_const : Continuous fun _ : B =>
181 (1 : AbstractFreeProduct A B ⧸
182 (⊤ : Subgroup (AbstractFreeProduct A B)))).congr ?_
183 intro b
184 apply QuotientGroup.eq.2
185 simp only [inv_one, one_mul, Subgroup.mem_top]
187private theorem isOpen_ker_of_continuous_quotient_inl (U : AdmissibleQuotient C A B) :
188 IsOpen ((((QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))).comp
189 (Monoid.Coprod.inl : A →* AbstractFreeProduct A B)).ker : Subgroup A) : Set A) := by
190 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B))) :=
191 ⊥
192 letI : DiscreteTopology (AbstractFreeProduct A B ⧸
193 (U : Subgroup (AbstractFreeProduct A B))) := ⟨rfl⟩
194 have hcont := U.inl_continuous
195 simpa [MonoidHom.mem_ker] using (isOpen_discrete ({1} :
196 Set (AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B))))).preimage hcont
198private theorem isOpen_ker_of_continuous_quotient_inr (U : AdmissibleQuotient C A B) :
199 IsOpen ((((QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))).comp
200 (Monoid.Coprod.inr : B →* AbstractFreeProduct A B)).ker : Subgroup B) : Set B) := by
201 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B))) :=
202 ⊥
203 letI : DiscreteTopology (AbstractFreeProduct A B ⧸
204 (U : Subgroup (AbstractFreeProduct A B))) := ⟨rfl⟩
205 have hcont := U.inr_continuous
206 simpa [MonoidHom.mem_ker] using (isOpen_discrete ({1} :
207 Set (AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B))))).preimage hcont
209/-- Intersections of admissible quotients are admissible for a formation. -/
210noncomputable def inf (hForm : ProCGroups.FiniteGroupClass.Formation C)
211 (U V : AdmissibleQuotient C A B) : AdmissibleQuotient C A B where
212 toSubgroup := (U : Subgroup (AbstractFreeProduct A B)) ⊓
213 (V : Subgroup (AbstractFreeProduct A B))
214 normal' := inferInstance
215 quotient_mem' :=
217 (C := C) (G := AbstractFreeProduct A B) hForm
218 (U : Subgroup (AbstractFreeProduct A B))
219 (V : Subgroup (AbstractFreeProduct A B)) U.quotient_mem V.quotient_mem
220 inl_continuous' := by
221 let N : Subgroup (AbstractFreeProduct A B) :=
222 (U : Subgroup (AbstractFreeProduct A B)) ⊓
223 (V : Subgroup (AbstractFreeProduct A B))
224 let fN : A →* AbstractFreeProduct A B ⧸ N :=
225 (QuotientGroup.mk' N).comp (Monoid.Coprod.inl : A →* AbstractFreeProduct A B)
226 let fU : A →* AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B)) :=
227 (QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))).comp
228 (Monoid.Coprod.inl : A →* AbstractFreeProduct A B)
229 let fV : A →* AbstractFreeProduct A B ⧸ (V : Subgroup (AbstractFreeProduct A B)) :=
230 (QuotientGroup.mk' (V : Subgroup (AbstractFreeProduct A B))).comp
231 (Monoid.Coprod.inl : A →* AbstractFreeProduct A B)
232 have hker :
233 IsOpen (((fN.ker : Subgroup A) : Set A)) := by
234 have hEq : ((fN.ker : Subgroup A) : Set A) =
235 ((fU.ker : Subgroup A) : Set A) ∩ ((fV.ker : Subgroup A) : Set A) := by
236 ext x
237 simp only [SetLike.mem_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
238 QuotientGroup.eq_one_iff, Subgroup.mem_inf, Set.mem_inter_iff, N, fN, fU, fV]
239 rw [hEq]
240 exact (isOpen_ker_of_continuous_quotient_inl (C := C) (A := A) (B := B) U).inter
241 (isOpen_ker_of_continuous_quotient_inl (C := C) (A := A) (B := B) V)
242 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ N) := ⊥
243 letI : DiscreteTopology (AbstractFreeProduct A B ⧸ N) := ⟨rfl⟩
244 exact fN.continuous_of_isOpen_ker_to_discrete hker
245 inr_continuous' := by
246 let N : Subgroup (AbstractFreeProduct A B) :=
247 (U : Subgroup (AbstractFreeProduct A B)) ⊓
248 (V : Subgroup (AbstractFreeProduct A B))
249 let fN : B →* AbstractFreeProduct A B ⧸ N :=
250 (QuotientGroup.mk' N).comp (Monoid.Coprod.inr : B →* AbstractFreeProduct A B)
251 let fU : B →* AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B)) :=
252 (QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))).comp
253 (Monoid.Coprod.inr : B →* AbstractFreeProduct A B)
254 let fV : B →* AbstractFreeProduct A B ⧸ (V : Subgroup (AbstractFreeProduct A B)) :=
255 (QuotientGroup.mk' (V : Subgroup (AbstractFreeProduct A B))).comp
256 (Monoid.Coprod.inr : B →* AbstractFreeProduct A B)
257 have hker :
258 IsOpen (((fN.ker : Subgroup B) : Set B)) := by
259 have hEq : ((fN.ker : Subgroup B) : Set B) =
260 ((fU.ker : Subgroup B) : Set B) ∩ ((fV.ker : Subgroup B) : Set B) := by
261 ext x
262 simp only [SetLike.mem_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
263 QuotientGroup.eq_one_iff, Subgroup.mem_inf, Set.mem_inter_iff, N, fN, fU, fV]
264 rw [hEq]
265 exact (isOpen_ker_of_continuous_quotient_inr (C := C) (A := A) (B := B) U).inter
266 (isOpen_ker_of_continuous_quotient_inr (C := C) (A := A) (B := B) V)
267 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ N) := ⊥
268 letI : DiscreteTopology (AbstractFreeProduct A B ⧸ N) := ⟨rfl⟩
269 exact fN.continuous_of_isOpen_ker_to_discrete hker
271/-- Admissible quotients form a directed preorder under refinement. -/
272theorem directed (hForm : ProCGroups.FiniteGroupClass.Formation C) :
273 Directed (α := AdmissibleQuotient C A B) (· ≤ ·) fun U => U := by
274 intro U V
275 refine ⟨inf (C := C) (A := A) (B := B) hForm U V, ?_, ?_⟩
276 · show (((inf (C := C) (A := A) (B := B) hForm U V :
277 AdmissibleQuotient C A B) : Subgroup (AbstractFreeProduct A B)) ≤
278 (U : Subgroup (AbstractFreeProduct A B)))
279 exact inf_le_left
280 · show (((inf (C := C) (A := A) (B := B) hForm U V :
281 AdmissibleQuotient C A B) : Subgroup (AbstractFreeProduct A B)) ≤
282 (V : Subgroup (AbstractFreeProduct A B)))
283 exact inf_le_right
285section OfHom
287variable {Q : Type u} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
289/-- The admissible quotient cut out by a homomorphism from the abstract free product to a finite
290`C`-group, provided the two restrictions to the factors are continuous. -/
291noncomputable def ofHom (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
292 (hQ : C Q) (φ : AbstractFreeProduct A B →* Q)
293 (hφl : Continuous (φ.comp (Monoid.Coprod.inl : A →* AbstractFreeProduct A B)))
294 (hφr : Continuous (φ.comp (Monoid.Coprod.inr : B →* AbstractFreeProduct A B))) :
295 AdmissibleQuotient C A B where
296 toSubgroup := φ.ker
297 normal' := inferInstance
298 quotient_mem' := by
299 let e : AbstractFreeProduct A B ⧸ φ.ker ≃* φ.range :=
300 QuotientGroup.quotientKerEquivRange φ
301 let f : AbstractFreeProduct A B ⧸ φ.ker →* Q :=
302 φ.range.subtype.comp e.toMonoidHom
303 have hf : Function.Injective f := by
304 intro x y hxy
305 apply e.injective
306 apply Subtype.val_injective
307 exact hxy
308 exact hHer.of_injective hQ f hf
309 inl_continuous' := by
310 let fN : A →* AbstractFreeProduct A B ⧸ φ.ker :=
311 (QuotientGroup.mk' φ.ker).comp
312 (Monoid.Coprod.inl : A →* AbstractFreeProduct A B)
313 have hker : IsOpen ((fN.ker : Subgroup A) : Set A) := by
314 have hEq : ((fN.ker : Subgroup A) : Set A) =
315 (((φ.comp (Monoid.Coprod.inl :
316 A →* AbstractFreeProduct A B)).ker : Subgroup A) : Set A) := by
317 ext x
318 simp only [SetLike.mem_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
319 QuotientGroup.eq_one_iff, fN]
320 rw [hEq]
321 simpa [MonoidHom.mem_ker] using (isOpen_discrete ({1} : Set Q)).preimage hφl
322 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ φ.ker) := ⊥
323 letI : DiscreteTopology (AbstractFreeProduct A B ⧸ φ.ker) := ⟨rfl⟩
324 exact fN.continuous_of_isOpen_ker_to_discrete hker
325 inr_continuous' := by
326 let fN : B →* AbstractFreeProduct A B ⧸ φ.ker :=
327 (QuotientGroup.mk' φ.ker).comp
328 (Monoid.Coprod.inr : B →* AbstractFreeProduct A B)
329 have hker : IsOpen ((fN.ker : Subgroup B) : Set B) := by
330 have hEq : ((fN.ker : Subgroup B) : Set B) =
331 (((φ.comp (Monoid.Coprod.inr :
332 B →* AbstractFreeProduct A B)).ker : Subgroup B) : Set B) := by
333 ext x
334 simp only [SetLike.mem_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
335 QuotientGroup.eq_one_iff, fN]
336 rw [hEq]
337 simpa [MonoidHom.mem_ker] using (isOpen_discrete ({1} : Set Q)).preimage hφr
338 letI : TopologicalSpace (AbstractFreeProduct A B ⧸ φ.ker) := ⊥
339 letI : DiscreteTopology (AbstractFreeProduct A B ⧸ φ.ker) := ⟨rfl⟩
340 exact fN.continuous_of_isOpen_ker_to_discrete hker
342/-- The admissible quotient induced by a target homomorphism has the expected kernel subgroup. -/
343@[simp] theorem ofHom_toSubgroup (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
344 (hQ : C Q) (φ : AbstractFreeProduct A B →* Q)
345 (hφl : Continuous (φ.comp (Monoid.Coprod.inl : A →* AbstractFreeProduct A B)))
346 (hφr : Continuous (φ.comp (Monoid.Coprod.inr : B →* AbstractFreeProduct A B))) :
347 ((ofHom (C := C) (A := A) (B := B) hHer hQ φ hφl hφr :
348 AdmissibleQuotient C A B) : Subgroup (AbstractFreeProduct A B)) = φ.ker :=
349 rfl
351end OfHom
355/-- The inverse system of admissible finite quotients of the abstract free product. -/
356def admissibleQuotientSystem (C : ProCGroups.FiniteGroupClass.{u})
357 (A B : Type u) [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
358 [Group B] [TopologicalSpace B] [IsTopologicalGroup B] :
359 ProCGroups.InverseSystems.InverseSystem (I := AdmissibleQuotient C A B) where
360 X := fun U => AbstractFreeProduct A B ⧸ (U : Subgroup (AbstractFreeProduct A B))
361 topologicalSpace := fun _ => ⊥
362 map := fun {U V} hUV =>
363 AdmissibleQuotient.map (C := C) (A := A) (B := B)
364 (U := U) (V := V)
365 (show (V : Subgroup (AbstractFreeProduct A B)) ≤
366 (U : Subgroup (AbstractFreeProduct A B)) from hUV)
367 continuous_map := by
368 intro U V hUV
369 letI : TopologicalSpace (AbstractFreeProduct A B ⧸
370 (V : Subgroup (AbstractFreeProduct A B))) := ⊥
371 letI : DiscreteTopology (AbstractFreeProduct A B ⧸
372 (V : Subgroup (AbstractFreeProduct A B))) := ⟨rfl⟩
373 letI : TopologicalSpace (AbstractFreeProduct A B ⧸
374 (U : Subgroup (AbstractFreeProduct A B))) := ⊥
375 change Continuous (AdmissibleQuotient.map (C := C) (A := A) (B := B)
376 (U := U) (V := V)
377 (show (V : Subgroup (AbstractFreeProduct A B)) ≤
378 (U : Subgroup (AbstractFreeProduct A B)) from hUV))
379 exact continuous_of_discreteTopology
380 map_id := by
381 intro U
382 ext x
383 rcases QuotientGroup.mk'_surjective (U : Subgroup (AbstractFreeProduct A B)) x with
384 ⟨g, rfl⟩
385 rfl
386 map_comp := by
387 intro U V W hUV hVW
388 ext x
389 rcases QuotientGroup.mk'_surjective (W : Subgroup (AbstractFreeProduct A B)) x with
390 ⟨g, rfl⟩
391 rfl
393/-- Each admissible quotient stage carries its quotient group structure. -/
395 (U : AdmissibleQuotient C A B) :
396 Group ((admissibleQuotientSystem C A B).X U) := by
397 dsimp [admissibleQuotientSystem]
398 infer_instance
400/-- Each admissible quotient stage carries the discrete topology. -/
402 (U : AdmissibleQuotient C A B) :
403 DiscreteTopology ((admissibleQuotientSystem C A B).X U) := by
404 exact ⟨rfl⟩
406/-- Each admissible quotient stage is a topological group with the discrete topology. -/
408 (U : AdmissibleQuotient C A B) :
409 IsTopologicalGroup ((admissibleQuotientSystem C A B).X U) := by
410 infer_instance
412/-- The admissible quotient system is a group-valued inverse system. -/
413instance instIsGroupSystemAdmissibleQuotientSystem :
416 intro U V hUV
417 rfl
419 intro U V hUV x y
420 exact (AdmissibleQuotient.map (C := C) (A := A) (B := B)
422 map_inv := by
423 intro U V hUV x
424 exact (AdmissibleQuotient.map (C := C) (A := A) (B := B)
425 (U := U) (V := V) hUV).map_inv x
427/-- The concrete binary free pro-`C` product model. -/
428abbrev freeProCProduct (C : ProCGroups.FiniteGroupClass.{u})
429 (A B : Type u) [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
430 [Group B] [TopologicalSpace B] [IsTopologicalGroup B] :=
431 (admissibleQuotientSystem C A B).inverseLimit
433/-- The concrete free pro-`C` product inherits the inverse-limit group structure. -/
434instance instGroupFreeProCProduct : Group (freeProCProduct C A B) := by
435 dsimp [freeProCProduct]
436 infer_instance
438/-- The concrete free pro-`C` product inherits the inverse-limit topological group structure. -/
439instance instIsTopologicalGroupFreeProCProduct :
440 IsTopologicalGroup (freeProCProduct C A B) := by
441 dsimp [freeProCProduct]
442 infer_instance
444/-- The canonical projection from the concrete free pro-`C` product to an admissible quotient,
445bundled as a homomorphism. -/
446def freeProCProductπHom (U : AdmissibleQuotient C A B) :
447 freeProCProduct C A B →* AbstractFreeProduct A B ⧸
448 (U : Subgroup (AbstractFreeProduct A B)) where
449 toFun := (admissibleQuotientSystem C A B).projection U
450 map_one' := rfl
451 map_mul' := by
452 intro x y
453 rfl
455/-- The canonical projection homomorphism from the concrete free pro-`C` product evaluates as the inverse-limit projection. -/
456@[simp] theorem freeProCProductπHom_apply
457 (U : AdmissibleQuotient C A B) (x : freeProCProduct C A B) :
458 freeProCProductπHom (C := C) (A := A) (B := B) U x =
459 (admissibleQuotientSystem C A B).projection U x :=
460 rfl
462private def completionMapFamily (C : ProCGroups.FiniteGroupClass.{u})
463 (A B : Type u) [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
464 [Group B] [TopologicalSpace B] [IsTopologicalGroup B] :
465 ∀ U : AdmissibleQuotient C A B,
466 AbstractFreeProduct A B → (admissibleQuotientSystem C A B).X U :=
467 fun U g => QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B)) g
469private theorem completionMapFamily_compatible :
471 (completionMapFamily C A B) := by
472 intro U V hUV
473 funext g
474 rfl
476/-- The canonical abstract map from the free product to its admissible pro-`C` completion. -/
477noncomputable def completionMap :
478 AbstractFreeProduct A B →* freeProCProduct C A B where
479 toFun g :=
480 ⟨fun U => QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B)) g, by
481 intro U V hUV
482 rfl⟩
483 map_one' := by
484 apply (admissibleQuotientSystem C A B).ext
485 intro U
486 change QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
487 (1 : AbstractFreeProduct A B) = 1
488 simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one]
489 map_mul' := by
490 intro x y
491 apply (admissibleQuotientSystem C A B).ext
492 intro U
493 change QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B)) (x * y) =
494 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B)) x *
495 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B)) y
496 simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_mul]
498/-- The completion map followed by a finite admissible quotient projection is the quotient map. -/
499@[simp] theorem π_completionMap (U : AdmissibleQuotient C A B)
500 (g : AbstractFreeProduct A B) :
501 (admissibleQuotientSystem C A B).projection U (completionMap (C := C) (A := A) (B := B) g) =
502 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B)) g :=
503 rfl
505private theorem denseRange_completionMap_of_formation
506 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
507 DenseRange (completionMap (C := C) (A := A) (B := B)) := by
508 let S := admissibleQuotientSystem C A B
509 letI : Nonempty (AdmissibleQuotient C A B) :=
510 ⟨AdmissibleQuotient.top (C := C) (A := A) (B := B) hForm⟩
511 letI : TopologicalSpace (AbstractFreeProduct A B) := ⊥
512 simpa [completionMap, S] using
513 S.denseRange_lift
514 (completionMapFamily C A B)
515 (completionMapFamily_compatible (C := C) (A := A) (B := B))
516 (fun U => QuotientGroup.mk'_surjective (U : Subgroup (AbstractFreeProduct A B)))
517 (AdmissibleQuotient.directed (C := C) (A := A) (B := B) hForm)
520 (A B : Type u) [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
521 [Group B] [TopologicalSpace B] [IsTopologicalGroup B] :
522 ∀ U : AdmissibleQuotient C A B,
523 A → (admissibleQuotientSystem C A B).X U :=
524 fun U a => QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
525 ((Monoid.Coprod.inl : A →* AbstractFreeProduct A B) a)
527private theorem inlFamily_compatible :
530 intro U V hUV
531 funext a
532 rfl
535 (A B : Type u) [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
536 [Group B] [TopologicalSpace B] [IsTopologicalGroup B] :
537 ∀ U : AdmissibleQuotient C A B,
538 B → (admissibleQuotientSystem C A B).X U :=
539 fun U b => QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
540 ((Monoid.Coprod.inr : B →* AbstractFreeProduct A B) b)
542private theorem inrFamily_compatible :
545 intro U V hUV
546 funext b
547 rfl
549section TargetQuotients
551variable {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
553/-- The abstract free-product homomorphism induced by a pair of maps to an open normal quotient of a
554target group. -/
555noncomputable def targetQuotientHom
556 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
557 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) :
558 AbstractFreeProduct A B →* K ⧸ (U.1 : Subgroup K) :=
559 Monoid.Coprod.lift
560 ((ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U).comp φ₁).toMonoidHom
561 ((ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U).comp φ₂).toMonoidHom
563omit [IsTopologicalGroup A] [IsTopologicalGroup B] [IsTopologicalGroup K] in
564/-- The target quotient homomorphism agrees with the left input homomorphism on the left factor. -/
565@[simp] theorem targetQuotientHom_comp_inl
566 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
567 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) :
568 (targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U).comp
569 (Monoid.Coprod.inl : A →* AbstractFreeProduct A B) =
570 ((ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U).comp
571 φ₁).toMonoidHom :=
572 Monoid.Coprod.lift_comp_inl _ _
574omit [IsTopologicalGroup A] [IsTopologicalGroup B] [IsTopologicalGroup K] in
575/-- The target quotient homomorphism agrees with the right input homomorphism on the right factor. -/
576@[simp] theorem targetQuotientHom_comp_inr
577 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
578 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) :
579 (targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U).comp
580 (Monoid.Coprod.inr : B →* AbstractFreeProduct A B) =
581 ((ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U).comp
582 φ₂).toMonoidHom :=
583 Monoid.Coprod.lift_comp_inr _ _
585omit [IsTopologicalGroup A] [IsTopologicalGroup B] [IsTopologicalGroup K] in
586/-- Target quotient homomorphisms are compatible with admissible-quotient transition maps. -/
587theorem targetQuotientHom_transition
588 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
589 {U V : ProCGroups.ProC.OpenNormalSubgroupInClass C K}
590 (hUV : (V.1 : Subgroup K) ≤ (U.1 : Subgroup K)) :
591 (ProCGroups.ProC.OpenNormalSubgroupInClass.map (C := C) (G := K) hUV).comp
592 (targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ V) =
593 targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U := by
594 apply Monoid.Coprod.hom_ext
595 · ext a
596 rfl
597 · ext b
598 rfl
600/-- The admissible quotient of the abstract free product induced by an open normal quotient of a
601pro-`C` target. Heredity is used because the image in the target quotient may be a proper subgroup. -/
602noncomputable def targetAdmissible
603 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
604 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
605 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) :
606 AdmissibleQuotient C A B := by
607 letI : DiscreteTopology (K ⧸ (U.1 : Subgroup K)) :=
608 QuotientGroup.discreteTopology
609 (openNormalSubgroup_isOpen (G := K) (U.1 : OpenNormalSubgroup K))
610 refine AdmissibleQuotient.ofHom (C := C) (A := A) (B := B)
611 hHer U.2 (targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U) ?_ ?_
612 · rw [targetQuotientHom_comp_inl]
613 exact ((ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U).comp
614 φ₁).continuous_toFun
615 · rw [targetQuotientHom_comp_inr]
616 exact ((ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U).comp
617 φ₂).continuous_toFun
619/-- The target admissible quotient has the expected defining subgroup. -/
620theorem targetAdmissible_toSubgroup
621 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
622 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
623 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) :
624 ((targetAdmissible (C := C) (A := A) (B := B) hHer φ₁ φ₂ U :
625 AdmissibleQuotient C A B) : Subgroup (AbstractFreeProduct A B)) =
626 (targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U).ker := by
627 dsimp [targetAdmissible]
629/-- Map from the admissible quotient induced by a target quotient to that target quotient. -/
630noncomputable def targetAdmissibleQuotientMap
631 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
632 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
633 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) :
634 AbstractFreeProduct A B ⧸
635 (targetAdmissible (C := C) (A := A) (B := B) hHer φ₁ φ₂ U :
636 Subgroup (AbstractFreeProduct A B)) →*
637 K ⧸ (U.1 : Subgroup K) :=
638 QuotientGroup.lift
639 (targetAdmissible (C := C) (A := A) (B := B) hHer φ₁ φ₂ U :
640 Subgroup (AbstractFreeProduct A B))
641 (targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U)
642 (by
643 intro g hg
644 have hg' :
645 g ∈ (targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U).ker := by
646 simpa [targetAdmissible_toSubgroup (C := C) (A := A) (B := B)
647 hHer φ₁ φ₂ U] using hg
648 exact hg')
650/-- The target admissible quotient map evaluates on representatives as expected. -/
651@[simp] theorem targetAdmissibleQuotientMap_mk
652 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
653 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
654 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K)
655 (g : AbstractFreeProduct A B) :
656 targetAdmissibleQuotientMap (C := C) (A := A) (B := B) hHer φ₁ φ₂ U
657 (QuotientGroup.mk'
658 (targetAdmissible (C := C) (A := A) (B := B) hHer φ₁ φ₂ U :
659 Subgroup (AbstractFreeProduct A B)) g) =
660 targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U g :=
661 rfl
663/-- Coordinate map from the concrete free pro-`C` product to one finite quotient of a pro-`C`
664target. -/
665noncomputable def targetCoordinate
666 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
667 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
668 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) :
669 freeProCProduct C A B →ₜ* K ⧸ (U.1 : Subgroup K) where
670 toMonoidHom :=
671 (targetAdmissibleQuotientMap (C := C) (A := A) (B := B) hHer φ₁ φ₂ U).comp
672 (freeProCProductπHom (C := C) (A := A) (B := B)
673 (targetAdmissible (C := C) (A := A) (B := B) hHer φ₁ φ₂ U))
674 continuous_toFun := by
675 let S := admissibleQuotientSystem C A B
676 let N := targetAdmissible (C := C) (A := A) (B := B) hHer φ₁ φ₂ U
677 letI : TopologicalSpace (AbstractFreeProduct A B ⧸
678 (N : Subgroup (AbstractFreeProduct A B))) := ⊥
679 letI : DiscreteTopology (AbstractFreeProduct A B ⧸
680 (N : Subgroup (AbstractFreeProduct A B))) := ⟨rfl⟩
681 letI : DiscreteTopology (S.X N) :=
682 instDiscreteTopologyAdmissibleQuotientSystemX (C := C) (A := A) (B := B) N
683 have hq : Continuous
684 (targetAdmissibleQuotientMap (C := C) (A := A) (B := B) hHer φ₁ φ₂ U) :=
685 continuous_of_discreteTopology
686 exact hq.comp (S.continuous_projection N)
688/-- The target coordinate map agrees with the completion map after projection to a finite quotient. -/
690 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
691 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
692 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K)
693 (g : AbstractFreeProduct A B) :
694 targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂ U
695 (completionMap (C := C) (A := A) (B := B) g) =
696 targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U g := by
697 change targetAdmissibleQuotientMap (C := C) (A := A) (B := B) hHer φ₁ φ₂ U
698 (QuotientGroup.mk'
699 (targetAdmissible (C := C) (A := A) (B := B) hHer φ₁ φ₂ U :
700 Subgroup (AbstractFreeProduct A B)) g) =
701 targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U g
704/-- The family of target-coordinate maps into the finite quotients of a pro-`C` target. -/
705noncomputable def targetCoordinateFamily
706 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
707 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K) :
708 ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C K),
709 freeProCProduct C A B →
710 (ProCGroups.ProC.openNormalSubgroupInClassSystem C K).X U :=
711 fun U x => targetCoordinate (C := C) (A := A) (B := B)
712 hHer φ₁ φ₂ (OrderDual.ofDual U) x
714/-- The target coordinate maps form a compatible family over admissible quotients. -/
716 (hForm : ProCGroups.FiniteGroupClass.Formation C)
717 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
718 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K) :
720 (targetCoordinateFamily (C := C) (A := A) (B := B) hHer φ₁ φ₂) := by
721 let T := ProCGroups.ProC.openNormalSubgroupInClassSystem C K
722 intro U V hUV
723 funext x
724 letI : DiscreteTopology (T.X U) := by
726 exact QuotientGroup.discreteTopology
727 (openNormalSubgroup_isOpen (G := K)
728 ((OrderDual.ofDual U).1 : OpenNormalSubgroup K))
729 letI : T2Space (T.X U) := by infer_instance
730 have hEqFun :
731 (T.map hUV ∘ targetCoordinateFamily (C := C) (A := A) (B := B) hHer φ₁ φ₂ V) =
732 targetCoordinateFamily (C := C) (A := A) (B := B) hHer φ₁ φ₂ U := by
733 apply Continuous.ext_on
734 (s := Set.range (completionMap (C := C) (A := A) (B := B)))
735 (denseRange_completionMap_of_formation (C := C) (A := A) (B := B) hForm)
736 · exact (T.continuous_map hUV).comp
737 (targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂
738 (OrderDual.ofDual V)).continuous_toFun
739 · exact (targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂
740 (OrderDual.ofDual U)).continuous_toFun
741 · rintro _ ⟨g, rfl⟩
742 change T.map hUV
743 (targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂
744 (OrderDual.ofDual V) g) =
745 targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂
746 (OrderDual.ofDual U) g
747 exact congrArg (fun f : AbstractFreeProduct A B →* T.X U => f g)
748 (targetQuotientHom_transition (C := C) (A := A) (B := B)
749 φ₁ φ₂ (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
750 exact congrFun hEqFun x
752/-- The map from the concrete free pro-`C` product to the canonical inverse-limit presentation of a
753pro-`C` target induced by maps on the two factors. -/
754noncomputable def targetInverseLimitMap
755 (hForm : ProCGroups.FiniteGroupClass.Formation C)
756 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
757 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K) :
758 freeProCProduct C A B →ₜ*
759 (ProCGroups.ProC.openNormalSubgroupInClassSystem C K).inverseLimit where
760 toFun :=
762 (targetCoordinateFamily (C := C) (A := A) (B := B) hHer φ₁ φ₂)
763 (targetCoordinateFamily_compatible (C := C) (A := A) (B := B)
764 hForm hHer φ₁ φ₂)
765 map_one' := by
766 apply (ProCGroups.ProC.openNormalSubgroupInClassSystem C K).ext
767 intro U
768 change targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂
769 (OrderDual.ofDual U) 1 = 1
771 map_mul' := by
772 intro x y
773 apply (ProCGroups.ProC.openNormalSubgroupInClassSystem C K).ext
774 intro U
775 change targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂
776 (OrderDual.ofDual U) (x * y) =
777 targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂
778 (OrderDual.ofDual U) x *
779 targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂
780 (OrderDual.ofDual U) y
782 continuous_toFun := by
783 let T := ProCGroups.ProC.openNormalSubgroupInClassSystem C K
784 exact T.continuous_inverseLimitLift
785 (targetCoordinateFamily (C := C) (A := A) (B := B) hHer φ₁ φ₂)
786 (fun U => (targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂
787 (OrderDual.ofDual U)).continuous_toFun)
788 (targetCoordinateFamily_compatible (C := C) (A := A) (B := B)
789 hForm hHer φ₁ φ₂)
792 (hForm : ProCGroups.FiniteGroupClass.Formation C)
793 (hK : ProCGroups.ProC.IsProCGroup C K)
794 (U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C K)) (x : K) :
795 (ProCGroups.ProC.openNormalSubgroupInClassSystem C K).projection U
797 (C := C) (G := K) hForm hK) x) =
798 ProCGroups.ProC.openNormalSubgroupInClassProj (C := C) (G := K) U x := by
799 rfl
801/-- The continuous homomorphism to a pro-`C` target induced by maps from the two factors. -/
802noncomputable def liftToTarget
803 (hForm : ProCGroups.FiniteGroupClass.Formation C)
804 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
805 (hK : ProCGroups.ProC.IsProCGroup C K)
806 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K) :
807 freeProCProduct C A B →ₜ* K :=
810 (C := C) (G := K) hForm hK).symm).comp
811 (targetInverseLimitMap (C := C) (A := A) (B := B) hForm hHer φ₁ φ₂)
813/-- The lift to a target has the prescribed finite quotient coordinates. -/
814theorem quotientProj_liftToTarget
815 (hForm : ProCGroups.FiniteGroupClass.Formation C)
816 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
817 (hK : ProCGroups.ProC.IsProCGroup C K)
818 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
819 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) :
820 (ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U).comp
821 (liftToTarget (C := C) (A := A) (B := B) hForm hHer hK φ₁ φ₂) =
822 targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂ U := by
823 ext x
824 let T := ProCGroups.ProC.openNormalSubgroupInClassSystem C K
825 let e :=
827 (C := C) (G := K) hForm hK
828 let θ := targetInverseLimitMap (C := C) (A := A) (B := B) hForm hHer φ₁ φ₂
829 have hCoord :
830 T.projection (OrderDual.toDual U) (e (e.symm (θ x))) =
831 T.projection (OrderDual.toDual U) (θ x) := by
832 exact congrArg (fun z : T.inverseLimit => T.projection (OrderDual.toDual U) z)
833 (e.apply_symm_apply (θ x))
835 (C := C) (K := K) hForm hK (OrderDual.toDual U)] at hCoord
836 simpa [liftToTarget, θ, targetInverseLimitMap, targetCoordinateFamily,
838 ProCGroups.ProC.openNormalSubgroupInClassProj, e] using hCoord
840end TargetQuotients
842/-- The left factor map into the concrete free pro-`C` product. -/
843noncomputable def inl : A →ₜ* freeProCProduct C A B where
844 toFun :=
847 (inlFamily_compatible (C := C) (A := A) (B := B))
848 map_one' := by
849 apply (admissibleQuotientSystem C A B).ext
850 intro U
851 change QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
852 ((Monoid.Coprod.inl : A →* AbstractFreeProduct A B) 1) = 1
854 map_mul' := by
855 intro x y
856 apply (admissibleQuotientSystem C A B).ext
857 intro U
858 change QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
859 ((Monoid.Coprod.inl : A →* AbstractFreeProduct A B) (x * y)) =
860 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
861 ((Monoid.Coprod.inl : A →* AbstractFreeProduct A B) x) *
862 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
863 ((Monoid.Coprod.inl : A →* AbstractFreeProduct A B) y)
865 continuous_toFun := by
866 let S := admissibleQuotientSystem C A B
867 exact S.continuous_inverseLimitLift
869 (fun U => U.inl_continuous)
870 (inlFamily_compatible (C := C) (A := A) (B := B))
872/-- The right factor map into the concrete free pro-`C` product. -/
873noncomputable def inr : B →ₜ* freeProCProduct C A B where
874 toFun :=
877 (inrFamily_compatible (C := C) (A := A) (B := B))
878 map_one' := by
879 apply (admissibleQuotientSystem C A B).ext
880 intro U
881 change QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
882 ((Monoid.Coprod.inr : B →* AbstractFreeProduct A B) 1) = 1
884 map_mul' := by
885 intro x y
886 apply (admissibleQuotientSystem C A B).ext
887 intro U
888 change QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
889 ((Monoid.Coprod.inr : B →* AbstractFreeProduct A B) (x * y)) =
890 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
891 ((Monoid.Coprod.inr : B →* AbstractFreeProduct A B) x) *
892 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
893 ((Monoid.Coprod.inr : B →* AbstractFreeProduct A B) y)
895 continuous_toFun := by
896 let S := admissibleQuotientSystem C A B
897 exact S.continuous_inverseLimitLift
899 (fun U => U.inr_continuous)
900 (inrFamily_compatible (C := C) (A := A) (B := B))
902/-- The finite projection of the left inclusion is the left inclusion into the admissible quotient. -/
903@[simp] theorem π_inl (U : AdmissibleQuotient C A B) (a : A) :
904 (admissibleQuotientSystem C A B).projection U (inl (C := C) (A := A) (B := B) a) =
905 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
906 ((Monoid.Coprod.inl : A →* AbstractFreeProduct A B) a) :=
907 by
908 change (admissibleQuotientSystem C A B).projection U
909 ((admissibleQuotientSystem C A B).inverseLimitLift
911 (inlFamily_compatible (C := C) (A := A) (B := B)) a) =
912 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
913 ((Monoid.Coprod.inl : A →* AbstractFreeProduct A B) a)
914 rw [(admissibleQuotientSystem C A B).projection_inverseLimitLift_apply]
915 rfl
917/-- The finite projection of the right inclusion is the right inclusion into the admissible quotient. -/
918@[simp] theorem π_inr (U : AdmissibleQuotient C A B) (b : B) :
919 (admissibleQuotientSystem C A B).projection U (inr (C := C) (A := A) (B := B) b) =
920 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
921 ((Monoid.Coprod.inr : B →* AbstractFreeProduct A B) b) :=
922 by
923 change (admissibleQuotientSystem C A B).projection U
924 ((admissibleQuotientSystem C A B).inverseLimitLift
926 (inrFamily_compatible (C := C) (A := A) (B := B)) b) =
927 QuotientGroup.mk' (U : Subgroup (AbstractFreeProduct A B))
928 ((Monoid.Coprod.inr : B →* AbstractFreeProduct A B) b)
929 rw [(admissibleQuotientSystem C A B).projection_inverseLimitLift_apply]
930 rfl
932/-- The completion map composed with the left inclusion is the left inclusion into the free pro-`C` product. -/
933@[simp] theorem completionMap_comp_inl :
934 (completionMap (C := C) (A := A) (B := B)).comp
935 (Monoid.Coprod.inl : A →* AbstractFreeProduct A B) =
936 (inl (C := C) (A := A) (B := B)).toMonoidHom := by
937 ext a U
938 change (admissibleQuotientSystem C A B).projection U
939 (completionMap (C := C) (A := A) (B := B)
940 ((Monoid.Coprod.inl : A →* AbstractFreeProduct A B) a)) =
941 (admissibleQuotientSystem C A B).projection U
942 (inl (C := C) (A := A) (B := B) a)
943 rw [π_completionMap, π_inl]
945/-- The completion map composed with the right inclusion is the right inclusion into the free pro-`C` product. -/
946@[simp] theorem completionMap_comp_inr :
947 (completionMap (C := C) (A := A) (B := B)).comp
948 (Monoid.Coprod.inr : B →* AbstractFreeProduct A B) =
949 (inr (C := C) (A := A) (B := B)).toMonoidHom := by
950 ext b U
951 change (admissibleQuotientSystem C A B).projection U
952 (completionMap (C := C) (A := A) (B := B)
953 ((Monoid.Coprod.inr : B →* AbstractFreeProduct A B) b)) =
954 (admissibleQuotientSystem C A B).projection U
955 (inr (C := C) (A := A) (B := B) b)
956 rw [π_completionMap, π_inr]
958section TargetCoordinateFactorMaps
960variable {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
962/-- The target coordinate map sends the left inclusion to the prescribed left homomorphism. -/
963@[simp] theorem targetCoordinate_inl
964 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
965 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
966 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) (a : A) :
967 targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂ U
968 (inl (C := C) (A := A) (B := B) a) =
969 ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U (φ₁ a) := by
972 targetCoordinate_completionMap (C := C) (A := A) (B := B)
973 hHer φ₁ φ₂ U ((Monoid.Coprod.inl : A →* AbstractFreeProduct A B) a)
975/-- The target coordinate map sends the right inclusion to the prescribed right homomorphism. -/
976@[simp] theorem targetCoordinate_inr
977 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
978 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
979 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) (b : B) :
980 targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂ U
981 (inr (C := C) (A := A) (B := B) b) =
982 ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U (φ₂ b) := by
985 targetCoordinate_completionMap (C := C) (A := A) (B := B)
986 hHer φ₁ φ₂ U ((Monoid.Coprod.inr : B →* AbstractFreeProduct A B) b)
988/-- The constructed lift has the prescribed left composite. -/
989theorem liftToTarget_comp_inl
990 (hForm : ProCGroups.FiniteGroupClass.Formation C)
991 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
992 (hK : ProCGroups.ProC.IsProCGroup C K)
993 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K) :
994 (liftToTarget (C := C) (A := A) (B := B) hForm hHer hK φ₁ φ₂).comp
995 (inl (C := C) (A := A) (B := B)) = φ₁ := by
997 intro U
998 let Uc : ProCGroups.ProC.OpenNormalSubgroupInClass C K :=
999 ⟨U, ProCGroups.ProC.IsProCGroup.quotient_mem hForm hK U⟩
1000 ext a
1001 have hq := congrArg (fun f : freeProCProduct C A B →ₜ* K ⧸ (U : Subgroup K) =>
1002 f (inl (C := C) (A := A) (B := B) a))
1003 (quotientProj_liftToTarget (C := C) (A := A) (B := B)
1004 hForm hHer hK φ₁ φ₂ Uc)
1005 simpa [Uc, ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj] using hq
1007/-- The constructed lift has the prescribed right composite. -/
1008theorem liftToTarget_comp_inr
1009 (hForm : ProCGroups.FiniteGroupClass.Formation C)
1010 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
1011 (hK : ProCGroups.ProC.IsProCGroup C K)
1012 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K) :
1013 (liftToTarget (C := C) (A := A) (B := B) hForm hHer hK φ₁ φ₂).comp
1014 (inr (C := C) (A := A) (B := B)) = φ₂ := by
1016 intro U
1017 let Uc : ProCGroups.ProC.OpenNormalSubgroupInClass C K :=
1018 ⟨U, ProCGroups.ProC.IsProCGroup.quotient_mem hForm hK U⟩
1019 ext b
1020 have hq := congrArg (fun f : freeProCProduct C A B →ₜ* K ⧸ (U : Subgroup K) =>
1021 f (inr (C := C) (A := A) (B := B) b))
1022 (quotientProj_liftToTarget (C := C) (A := A) (B := B)
1023 hForm hHer hK φ₁ φ₂ Uc)
1024 simpa [Uc, ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj] using hq
1026/-- Equality after all quotient projections follows from equality of the corresponding target coordinates. -/
1028 (hForm : ProCGroups.FiniteGroupClass.Formation C)
1029 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
1030 (φ₁ : A →ₜ* K) (φ₂ : B →ₜ* K)
1031 (Ψ : freeProCProduct C A B →ₜ* K)
1032 (hΨ₁ : Ψ.comp (inl (C := C) (A := A) (B := B)) = φ₁)
1033 (hΨ₂ : Ψ.comp (inr (C := C) (A := A) (B := B)) = φ₂)
1034 (U : ProCGroups.ProC.OpenNormalSubgroupInClass C K) :
1035 (ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U).comp Ψ =
1036 targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂ U := by
1037 let qU := ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj (C := C) U
1038 letI : DiscreteTopology (K ⧸ (U.1 : Subgroup K)) :=
1039 QuotientGroup.discreteTopology
1040 (openNormalSubgroup_isOpen (G := K) (U.1 : OpenNormalSubgroup K))
1041 letI : T2Space (K ⧸ (U.1 : Subgroup K)) := by infer_instance
1042 ext x
1043 have hfun :
1044 ((qU.comp Ψ : freeProCProduct C A B →ₜ* K ⧸ (U.1 : Subgroup K)) :
1045 freeProCProduct C A B → K ⧸ (U.1 : Subgroup K)) =
1046 targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂ U := by
1047 apply Continuous.ext_on
1048 (s := Set.range (completionMap (C := C) (A := A) (B := B)))
1049 (denseRange_completionMap_of_formation (C := C) (A := A) (B := B) hForm)
1050 · exact (qU.comp Ψ).continuous_toFun
1051 · exact (targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂ U).continuous_toFun
1052 · rintro _ ⟨g, rfl⟩
1053 have hhom :
1054 ((qU.comp Ψ).toMonoidHom.comp
1055 (completionMap (C := C) (A := A) (B := B))) =
1056 targetQuotientHom (C := C) (A := A) (B := B) φ₁ φ₂ U := by
1057 apply Monoid.Coprod.hom_ext
1058 · ext a
1059 have ha := congrArg (fun f : A →ₜ* K => qU (f a)) hΨ₁
1060 simpa [qU] using ha
1061 · ext b
1062 have hb := congrArg (fun f : B →ₜ* K => qU (f b)) hΨ₂
1063 simpa [qU] using hb
1064 simpa using congrArg (fun f : AbstractFreeProduct A B →*
1065 K ⧸ (U.1 : Subgroup K) => f g) hhom
1066 exact congrFun hfun x
1068end TargetCoordinateFactorMaps
1070/-- The completion map into the concrete free pro-`C` product has dense range. -/
1071theorem denseRange_completionMap
1072 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
1073 DenseRange (completionMap (C := C) (A := A) (B := B)) := by
1074 let S := admissibleQuotientSystem C A B
1075 letI : Nonempty (AdmissibleQuotient C A B) :=
1076 ⟨AdmissibleQuotient.top (C := C) (A := A) (B := B) hForm⟩
1077 letI : TopologicalSpace (AbstractFreeProduct A B) := ⊥
1078 simpa [completionMap, S] using
1079 S.denseRange_lift
1080 (completionMapFamily C A B)
1081 (completionMapFamily_compatible (C := C) (A := A) (B := B))
1082 (fun U => QuotientGroup.mk'_surjective (U : Subgroup (AbstractFreeProduct A B)))
1083 (AdmissibleQuotient.directed (C := C) (A := A) (B := B) hForm)
1085/-- The concrete free product model is pro-`C`. -/
1086theorem isProCGroup
1087 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
1088 ProCGroups.ProC.IsProCGroup C (freeProCProduct C A B) := by
1089 let S := admissibleQuotientSystem C A B
1090 letI : Nonempty (AdmissibleQuotient C A B) :=
1091 ⟨AdmissibleQuotient.top (C := C) (A := A) (B := B) hForm⟩
1092 have hX : ∀ U : AdmissibleQuotient C A B, ProCGroups.ProC.IsProCGroup C (S.X U) := by
1093 intro U
1094 letI : Finite (S.X U) := hForm.finiteOnly U.quotient_mem
1095 letI : DiscreteTopology (S.X U) :=
1096 instDiscreteTopologyAdmissibleQuotientSystemX (C := C) (A := A) (B := B) U
1098 (C := C) (G := S.X U) hForm.quotientClosed U.quotient_mem
1099 simpa [freeProCProduct, S] using
1101 (C := C) (S := S) hForm.isomClosed
1102 hForm.quotientClosed
1103 (AdmissibleQuotient.directed (C := C) (A := A) (B := B) hForm)
1104 hX
1106/-- The concrete inverse-limit model satisfies the binary free pro-`C` product universal property
1107for hereditary formations. -/
1108theorem isFreeProCProduct
1109 (hForm : ProCGroups.FiniteGroupClass.Formation C)
1110 (hHer : ProCGroups.FiniteGroupClass.Hereditary C) :
1112 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
1113 (inl (C := C) (A := A) (B := B))
1114 (inr (C := C) (A := A) (B := B)) := by
1115 refine ⟨?_, ?_⟩
1116 · exact isProCGroup (C := C) (A := A) (B := B) hForm
1117 · intro K _ _ _ hK φ₁ φ₂
1118 have hK' : ProCGroups.ProC.IsProCGroup C K := by
1119 simpa [ProCGroups.ProC.finiteGroupClassProCPredicate_holds_iff] using hK
1120 let Φ := liftToTarget (C := C) (A := A) (B := B) hForm hHer hK' φ₁ φ₂
1121 refine ⟨Φ, ?_, ?_⟩
1122 · exact ⟨liftToTarget_comp_inl (C := C) (A := A) (B := B)
1123 hForm hHer hK' φ₁ φ₂,
1124 liftToTarget_comp_inr (C := C) (A := A) (B := B)
1125 hForm hHer hK' φ₁ φ₂⟩
1126 · intro Ψ hΨ
1128 intro U
1129 let Uc : ProCGroups.ProC.OpenNormalSubgroupInClass C K :=
1130 ⟨U, ProCGroups.ProC.IsProCGroup.quotient_mem hForm hK' U⟩
1131 calc
1132 (ProCGroups.ProC.OpenNormalSubgroup.quotientProj U).comp Ψ =
1133 targetCoordinate (C := C) (A := A) (B := B) hHer φ₁ φ₂ Uc := by
1134 simpa [Uc, ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj] using
1136 (C := C) (A := A) (B := B) hForm hHer φ₁ φ₂ Ψ hΨ.1 hΨ.2 Uc
1137 _ = (ProCGroups.ProC.OpenNormalSubgroup.quotientProj U).comp Φ := by
1138 symm
1139 simpa [Uc, ProCGroups.ProC.OpenNormalSubgroupInClass.quotientProj, Φ] using
1141 (C := C) (A := A) (B := B) hForm hHer hK' φ₁ φ₂ Uc
1143end Concrete
1145end ProCGroups.FreeProducts