Yamaguchi Lean 4 Library
ProCGroups/FreeProducts/UniversalProperty.lean
ProCGroups/FreeProducts/UniversalProperty/Source

ProCGroups/FreeProducts/UniversalProperty.lean

1import Mathlib.GroupTheory.Coprod.Basic
2import ProCGroups.Categorical.PushoutSquares
3import ProCGroups.Completion.UniversalProperty
4import ProCGroups.ProC.GroupPredicates.Basic
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/FreeProducts/UniversalProperty.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
22namespace ProCGroups.FreeProducts
24universe u v
26section AbstractFreeProducts
28variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
29variable [Group G₁] [Group G₂] [Group F]
31/-- Binary free products, expressed through the usual universal property. -/
32structure IsFreeProduct (ι₁ : G₁ →* F) (ι₂ : G₂ →* F) : Prop where
34 ∀ {K : Type u} [Group K] (φ₁ : G₁ →* K) (φ₂ : G₂ →* K),
35 ∃! φ : F →* K, φ.comp ι₁ = φ₁ ∧ φ.comp ι₂ = φ₂
37namespace IsFreeProduct
39variable {ι₁ : G₁ →* F} {ι₂ : G₂ →* F}
41/-- Chosen descent morphism from a binary free product object. -/
42noncomputable def lift (hF : IsFreeProduct ι₁ ι₂)
43 {K : Type u} [Group K] (φ₁ : G₁ →* K) (φ₂ : G₂ →* K) : F →* K :=
44 Classical.choose (ExistsUnique.exists (hF.existsUnique_lift φ₁ φ₂))
46/-- The chosen free-product descent morphism has the prescribed composites. -/
47theorem lift_spec (hF : IsFreeProduct ι₁ ι₂)
48 {K : Type u} [Group K] (φ₁ : G₁ →* K) (φ₂ : G₂ →* K) :
49 (hF.lift φ₁ φ₂).comp ι₁ = φ₁ ∧ (hF.lift φ₁ φ₂).comp ι₂ = φ₂ :=
50 Classical.choose_spec (ExistsUnique.exists (hF.existsUnique_lift φ₁ φ₂))
52/-- Left composite of the chosen free-product descent morphism. -/
53@[simp] theorem lift_left (hF : IsFreeProduct ι₁ ι₂)
54 {K : Type u} [Group K] (φ₁ : G₁ →* K) (φ₂ : G₂ →* K) :
55 (hF.lift φ₁ φ₂).comp ι₁ = φ₁ :=
56 (hF.lift_spec φ₁ φ₂).1
58/-- Right composite of the chosen free-product descent morphism. -/
59@[simp] theorem lift_right (hF : IsFreeProduct ι₁ ι₂)
60 {K : Type u} [Group K] (φ₁ : G₁ →* K) (φ₂ : G₂ →* K) :
61 (hF.lift φ₁ φ₂).comp ι₂ = φ₂ :=
62 (hF.lift_spec φ₁ φ₂).2
64/-- Uniqueness of the chosen free-product descent morphism. -/
65theorem lift_unique (hF : IsFreeProduct ι₁ ι₂)
66 {K : Type u} [Group K] (φ₁ : G₁ →* K) (φ₂ : G₂ →* K)
67 {ψ : F →* K} (hψ : ψ.comp ι₁ = φ₁ ∧ ψ.comp ι₂ = φ₂) :
68 ψ = hF.lift φ₁ φ₂ := by
69 rcases hF.existsUnique_lift φ₁ φ₂ with ⟨u, hu, huuniq⟩
70 have hchosen : hF.lift φ₁ φ₂ = u := huuniq _ (hF.lift_spec φ₁ φ₂)
71 exact (huuniq _ hψ).trans hchosen.symm
73/-- The distinguished descent map from a free product object to itself is the identity. -/
74@[simp] theorem lift_self (hF : IsFreeProduct ι₁ ι₂) :
75 hF.lift ι₁ ι₂ = MonoidHom.id F := by
76 symm
77 exact hF.lift_unique ι₁ ι₂ ⟨rfl, rfl⟩
79/-- Extensionality of homomorphisms out of a free product object. -/
80theorem hom_ext (hF : IsFreeProduct ι₁ ι₂)
81 {K : Type u} [Group K] {ψ ψ' : F →* K}
82 (h₁ : ψ.comp ι₁ = ψ'.comp ι₁) (h₂ : ψ.comp ι₂ = ψ'.comp ι₂) :
83 ψ = ψ' := by
84 have hψ : ψ = hF.lift (K := K) (ψ.comp ι₁) (ψ.comp ι₂) := by
85 exact hF.lift_unique (K := K) (ψ.comp ι₁) (ψ.comp ι₂) ⟨rfl, rfl⟩
86 have hψ' : ψ' = hF.lift (K := K) (ψ.comp ι₁) (ψ.comp ι₂) := by
87 exact hF.lift_unique (K := K) (ψ.comp ι₁) (ψ.comp ι₂) ⟨h₁.symm, h₂.symm⟩
88 exact hψ.trans hψ'.symm
90variable {F' : Type u} [Group F']
91variable {ι₁' : G₁ →* F'} {ι₂' : G₂ →* F'}
93/-- Canonical comparison morphism between two free product objects on the same pair of factors. -/
94noncomputable def compare (hF : IsFreeProduct ι₁ ι₂) : F →* F' :=
95 hF.lift ι₁' ι₂'
97/-- Left composite of the canonical comparison map between free product objects. -/
98@[simp 900] theorem compare_left (hF : IsFreeProduct ι₁ ι₂) :
99 (hF.compare (ι₁' := ι₁') (ι₂' := ι₂')).comp ι₁ = ι₁' :=
100 hF.lift_left ι₁' ι₂'
102/-- Right composite of the canonical comparison map between free product objects. -/
103@[simp 900] theorem compare_right (hF : IsFreeProduct ι₁ ι₂) :
104 (hF.compare (ι₁' := ι₁') (ι₂' := ι₂')).comp ι₂ = ι₂' :=
105 hF.lift_right ι₁' ι₂'
107/-- The canonical comparison map from a free product object to itself is the identity. -/
108@[simp 900] theorem compare_self (hF : IsFreeProduct ι₁ ι₂) :
109 hF.compare (ι₁' := ι₁) (ι₂' := ι₂) = MonoidHom.id F := by
110 exact hF.lift_self
112variable {F'' : Type u} [Group F'']
113variable {ι₁'' : G₁ →* F''} {ι₂'' : G₂ →* F''}
115/-- Composition of free-product comparison maps is the expected direct comparison map. -/
116theorem compare_comp (hF : IsFreeProduct ι₁ ι₂)
117 (hF' : IsFreeProduct ι₁' ι₂') :
118 (hF'.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F' →* F'').comp
119 (hF.compare (ι₁' := ι₁') (ι₂' := ι₂') : F →* F') =
120 (hF.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F →* F'') := by
121 apply hF.hom_ext
122 · calc
123 ((hF'.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F' →* F'').comp
124 (hF.compare (ι₁' := ι₁') (ι₂' := ι₂') : F →* F')).comp ι₁
125 = (hF'.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F' →* F'').comp
126 ((hF.compare (ι₁' := ι₁') (ι₂' := ι₂') : F →* F').comp ι₁) := by rfl
127 _ = (hF'.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F' →* F'').comp ι₁' := by
128 rw [hF.compare_left (ι₁' := ι₁') (ι₂' := ι₂')]
129 _ = ι₁'' := hF'.compare_left (ι₁' := ι₁'') (ι₂' := ι₂'')
130 _ = (hF.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F →* F'').comp ι₁ :=
131 (hF.compare_left (ι₁' := ι₁'') (ι₂' := ι₂'')).symm
132 · calc
133 ((hF'.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F' →* F'').comp
134 (hF.compare (ι₁' := ι₁') (ι₂' := ι₂') : F →* F')).comp ι₂
135 = (hF'.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F' →* F'').comp
136 ((hF.compare (ι₁' := ι₁') (ι₂' := ι₂') : F →* F').comp ι₂) := by rfl
137 _ = (hF'.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F' →* F'').comp ι₂' := by
138 rw [hF.compare_right (ι₁' := ι₁') (ι₂' := ι₂')]
139 _ = ι₂'' := hF'.compare_right (ι₁' := ι₁'') (ι₂' := ι₂'')
140 _ = (hF.compare (ι₁' := ι₁'') (ι₂' := ι₂'') : F →* F'').comp ι₂ :=
141 (hF.compare_right (ι₁' := ι₁'') (ι₂' := ι₂'')).symm
143/-- Any two binary free product objects on the same factors are canonically isomorphic. -/
144noncomputable def equiv (hF : IsFreeProduct ι₁ ι₂) (hF' : IsFreeProduct ι₁' ι₂') :
145 F ≃* F' :=
146 MonoidHom.toMulEquiv
147 (hF.compare (ι₁' := ι₁') (ι₂' := ι₂') : F →* F')
148 (hF'.compare (ι₁' := ι₁) (ι₂' := ι₂) : F' →* F)
149 (by
150 calc
151 (hF'.compare (ι₁' := ι₁) (ι₂' := ι₂) : F' →* F).comp
152 (hF.compare (ι₁' := ι₁') (ι₂' := ι₂') : F →* F') =
153 (hF.compare (ι₁' := ι₁) (ι₂' := ι₂) : F →* F) := by
154 simpa using hF.compare_comp (ι₁'' := ι₁) (ι₂'' := ι₂) hF'
155 _ = MonoidHom.id F := hF.compare_self)
156 (by
157 calc
158 (hF.compare (ι₁' := ι₁') (ι₂' := ι₂') : F →* F').comp
159 (hF'.compare (ι₁' := ι₁) (ι₂' := ι₂) : F' →* F) =
160 (hF'.compare (ι₁' := ι₁') (ι₂' := ι₂') : F' →* F') := by
161 simpa using hF'.compare_comp (ι₁'' := ι₁') (ι₂'' := ι₂') hF
162 _ = MonoidHom.id F' := hF'.compare_self)
164/-- Left composite of the canonical equivalence between free product objects. -/
165@[simp] theorem equiv_left (hF : IsFreeProduct ι₁ ι₂) (hF' : IsFreeProduct ι₁' ι₂') :
166 (hF.equiv hF').toMonoidHom.comp ι₁ = ι₁' := by
167 exact hF.compare_left (ι₁' := ι₁') (ι₂' := ι₂')
169/-- Right composite of the canonical equivalence between free product objects. -/
170@[simp] theorem equiv_right (hF : IsFreeProduct ι₁ ι₂) (hF' : IsFreeProduct ι₁' ι₂') :
171 (hF.equiv hF').toMonoidHom.comp ι₂ = ι₂' := by
172 exact hF.compare_right (ι₁' := ι₁') (ι₂' := ι₂')
174/-- Left-leg formula for the inverse canonical free-product equivalence. -/
175theorem equiv_symm_left (hF : IsFreeProduct ι₁ ι₂) (hF' : IsFreeProduct ι₁' ι₂') :
176 (hF.equiv hF').symm.toMonoidHom.comp ι₁' = ι₁ := by
177 change (hF'.compare (ι₁' := ι₁) (ι₂' := ι₂) : F' →* F).comp ι₁' = ι₁
178 exact hF'.compare_left (ι₁' := ι₁) (ι₂' := ι₂)
180/-- Right-leg formula for the inverse canonical free-product equivalence. -/
181theorem equiv_symm_right (hF : IsFreeProduct ι₁ ι₂) (hF' : IsFreeProduct ι₁' ι₂') :
182 (hF.equiv hF').symm.toMonoidHom.comp ι₂' = ι₂ := by
183 change (hF'.compare (ι₁' := ι₁) (ι₂' := ι₂) : F' →* F).comp ι₂' = ι₂
184 exact hF'.compare_right (ι₁' := ι₁) (ι₂' := ι₂)
186/-- A binary free product is a pushout over the trivial group. -/
187theorem isPushoutSquare (hF : IsFreeProduct ι₁ ι₂) :
189 (1 : ULift.{u, 0} Unit →* G₁) (1 : ULift.{u, 0} Unit →* G₂) ι₁ ι₂ := by
190 constructor
191 · ext u
192 cases u
193 simp only [MonoidHom.comp_one, MonoidHom.one_apply]
194 · intro K _ φ₁ φ₂ _hφ
195 refine ⟨hF.lift φ₁ φ₂, hF.lift_spec φ₁ φ₂, ?_⟩
196 intro ψ hψ
197 exact hF.lift_unique φ₁ φ₂ hψ
199/-- A pushout over the trivial group satisfies the binary free-product universal property. -/
202 (1 : ULift.{u, 0} Unit →* G₁) (1 : ULift.{u, 0} Unit →* G₂) ι₁ ι₂) :
203 IsFreeProduct ι₁ ι₂ := by
204 refine ⟨?_⟩
205 intro K _ φ₁ φ₂
206 have hφ : φ₁.comp (1 : ULift.{u, 0} Unit →* G₁) =
207 φ₂.comp (1 : ULift.{u, 0} Unit →* G₂) := by
208 ext u
209 cases u
210 simp only [MonoidHom.comp_one, MonoidHom.one_apply]
211 simpa using hpo.2 φ₁ φ₂ hφ
215/-- Free-product universal property for mathlib's concrete coproduct model. -/
216theorem coprod_isFreeProduct (G₁ : Type u) (G₂ : Type u) [Group G₁] [Group G₂] :
218 (Monoid.Coprod.inl : G₁ →* G₁ ∗ G₂)
219 (Monoid.Coprod.inr : G₂ →* G₁ ∗ G₂) := by
220 refine ⟨?_⟩
221 intro K _ φ₁ φ₂
222 refine ⟨Monoid.Coprod.lift φ₁ φ₂, ?_, ?_⟩
223 · exact ⟨Monoid.Coprod.lift_comp_inl φ₁ φ₂, Monoid.Coprod.lift_comp_inr φ₁ φ₂⟩
224 · intro ψ hψ
225 exact Monoid.Coprod.lift_unique hψ.1 hψ.2
227/-- The concrete coproduct model is a pushout over the trivial group. -/
228theorem coprod_isPushoutSquare (G₁ : Type u) (G₂ : Type u) [Group G₁] [Group G₂] :
230 (1 : ULift.{u, 0} Unit →* G₁) (1 : ULift.{u, 0} Unit →* G₂)
231 (Monoid.Coprod.inl : G₁ →* G₁ ∗ G₂)
232 (Monoid.Coprod.inr : G₂ →* G₁ ∗ G₂) :=
235/-- Binary free products are exactly pushouts over the trivial group. -/
236theorem isFreeProduct_iff_isPushoutSquare {ι₁ : G₁ →* F} {ι₂ : G₂ →* F} :
237 IsFreeProduct ι₁ ι₂ ↔
239 (1 : ULift.{u, 0} Unit →* G₁) (1 : ULift.{u, 0} Unit →* G₂) ι₁ ι₂ :=
240 ⟨IsFreeProduct.isPushoutSquare, IsFreeProduct.of_isPushoutSquare⟩
242/-- Indexed free products, expressed through the usual universal property. -/
243structure IsFreeProductFamily {A : Type u} (G : A → Type u) [∀ a, Group (G a)]
244 {F : Type u} [Group F] (ι : ∀ a, G a →* F) : Prop where
246 ∀ {K : Type u} [Group K] (φ : ∀ a, G a →* K),
247 ∃! ψ : F →* K, ∀ a, ψ.comp (ι a) = φ a
251variable {A : Type u} {G : A → Type u} [∀ a, Group (G a)]
252variable {F : Type u} [Group F]
253variable {ι : ∀ a, G a →* F}
255/-- Chosen descent morphism from a family free-product object. -/
256noncomputable def lift (hF : IsFreeProductFamily G ι)
257 {K : Type u} [Group K] (φ : ∀ a, G a →* K) : F →* K :=
258 Classical.choose (ExistsUnique.exists (hF.existsUnique_lift φ))
260/-- Component formula for the chosen family free-product descent morphism. -/
261@[simp] theorem lift_ι (hF : IsFreeProductFamily G ι)
262 {K : Type u} [Group K] (φ : ∀ a, G a →* K) (a : A) :
263 (hF.lift φ).comp (ι a) = φ a :=
264 Classical.choose_spec (ExistsUnique.exists (hF.existsUnique_lift φ)) a
266/-- Uniqueness of the chosen family free-product descent morphism. -/
267theorem lift_unique (hF : IsFreeProductFamily G ι)
268 {K : Type u} [Group K] (φ : ∀ a, G a →* K)
269 {ψ : F →* K} (hψ : ∀ a, ψ.comp (ι a) = φ a) :
270 ψ = hF.lift φ := by
271 rcases hF.existsUnique_lift φ with ⟨u, hu, huuniq⟩
272 have hchosen : hF.lift φ = u := huuniq _ (fun a => hF.lift_ι φ a)
273 exact (huuniq _ hψ).trans hchosen.symm
275/-- The distinguished descent map from a family free-product object to itself is the identity. -/
276@[simp] theorem lift_self (hF : IsFreeProductFamily G ι) :
277 hF.lift ι = MonoidHom.id F := by
278 symm
279 exact hF.lift_unique ι (fun _ => rfl)
281/-- Extensionality of homomorphisms out of a family free-product object. -/
282theorem hom_ext (hF : IsFreeProductFamily G ι)
283 {K : Type u} [Group K] {ψ ψ' : F →* K}
284 (h : ∀ a, ψ.comp (ι a) = ψ'.comp (ι a)) :
285 ψ = ψ' := by
286 have hψ : ψ = hF.lift (fun a => ψ.comp (ι a)) := by
287 exact hF.lift_unique (fun a => ψ.comp (ι a)) (fun _ => rfl)
288 have hψ' : ψ' = hF.lift (fun a => ψ.comp (ι a)) := by
289 exact hF.lift_unique (fun a => ψ.comp (ι a)) (fun a => (h a).symm)
290 exact hψ.trans hψ'.symm
292variable {F' : Type u} [Group F']
293variable {ι' : ∀ a, G a →* F'}
295/-- Canonical comparison morphism between two family free-product objects on the same factors. -/
296noncomputable def compare (hF : IsFreeProductFamily G ι) : F →* F' :=
297 hF.lift ι'
299/-- Component formula for the canonical comparison map between family free-product objects. -/
300@[simp 900] theorem compare_ι (hF : IsFreeProductFamily G ι) (a : A) :
301 (hF.compare (ι' := ι')).comp (ι a) = ι' a :=
302 hF.lift_ι ι' a
304/-- The canonical comparison map from a family free-product object to itself is the identity. -/
305@[simp 900] theorem compare_self (hF : IsFreeProductFamily G ι) :
306 hF.compare (ι' := ι) = MonoidHom.id F := by
307 exact hF.lift_self
309variable {F'' : Type u} [Group F'']
310variable {ι'' : ∀ a, G a →* F''}
312/-- Composition of family free-product comparison maps is the expected direct comparison map. -/
313theorem compare_comp (hF : IsFreeProductFamily G ι)
314 (hF' : IsFreeProductFamily G ι') :
315 (hF'.compare (ι' := ι'') : F' →* F'').comp
316 (hF.compare (ι' := ι') : F →* F') =
317 (hF.compare (ι' := ι'') : F →* F'') := by
318 apply hF.hom_ext
319 intro a
320 calc
321 ((hF'.compare (ι' := ι'') : F' →* F'').comp
322 (hF.compare (ι' := ι') : F →* F')).comp (ι a)
323 = (hF'.compare (ι' := ι'') : F' →* F'').comp
324 ((hF.compare (ι' := ι') : F →* F').comp (ι a)) := by rfl
325 _ = (hF'.compare (ι' := ι'') : F' →* F'').comp (ι' a) := by
326 rw [hF.compare_ι (ι' := ι') a]
327 _ = ι'' a := hF'.compare_ι (ι' := ι'') a
328 _ = (hF.compare (ι' := ι'') : F →* F'').comp (ι a) :=
329 (hF.compare_ι (ι' := ι'') a).symm
331/-- Any two family free-product objects on the same factors are canonically isomorphic. -/
332noncomputable def equiv (hF : IsFreeProductFamily G ι) (hF' : IsFreeProductFamily G ι') :
333 F ≃* F' :=
334 MonoidHom.toMulEquiv
335 (hF.compare (ι' := ι') : F →* F') (hF'.compare (ι' := ι) : F' →* F)
336 (by
337 calc
338 (hF'.compare (ι' := ι) : F' →* F).comp (hF.compare (ι' := ι') : F →* F') =
339 (hF.compare (ι' := ι) : F →* F) := by
340 simpa using hF.compare_comp (ι'' := ι) hF'
341 _ = MonoidHom.id F := hF.compare_self)
342 (by
343 calc
344 (hF.compare (ι' := ι') : F →* F').comp (hF'.compare (ι' := ι) : F' →* F) =
345 (hF'.compare (ι' := ι') : F' →* F') := by
346 simpa using hF'.compare_comp (ι'' := ι') hF
347 _ = MonoidHom.id F' := hF'.compare_self)
349/-- Component formula for the canonical equivalence between family free-product objects. -/
350@[simp] theorem equiv_ι (hF : IsFreeProductFamily G ι) (hF' : IsFreeProductFamily G ι')
351 (a : A) :
352 (hF.equiv hF').toMonoidHom.comp (ι a) = ι' a := by
353 exact hF.compare_ι (ι' := ι') a
355/-- Component formula for the inverse canonical equivalence between family free-product objects. -/
356theorem equiv_symm_ι (hF : IsFreeProductFamily G ι) (hF' : IsFreeProductFamily G ι')
357 (a : A) :
358 (hF.equiv hF').symm.toMonoidHom.comp (ι' a) = ι a := by
359 change (hF'.compare (ι' := ι) : F' →* F).comp (ι' a) = ι a
360 exact hF'.compare_ι (ι' := ι) a
364end AbstractFreeProducts
366section TopologicalFreeProducts
368variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
369variable [Group G₁] [TopologicalSpace G₁]
370variable [Group G₂] [TopologicalSpace G₂]
371variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
373/-- A topology on an abstract binary free product compatible with the usual continuous universal
374property. This is the interface needed to turn a pro-`C` completion of the topological free product
375into a free pro-`C` product. -/
376structure IsTopologicalFreeProduct (ι₁ : G₁ →ₜ* F) (ι₂ : G₂ →ₜ* F) : Prop where
377 isFreeProduct : IsFreeProduct ι₁.toMonoidHom ι₂.toMonoidHom
378 lift_continuous :
379 ∀ {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
380 ∀ (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K),
381 Continuous (isFreeProduct.lift φ₁.toMonoidHom φ₂.toMonoidHom)
385variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
387/-- The continuous lift out of a topological free product. -/
388noncomputable def lift (hF : IsTopologicalFreeProduct ι₁ ι₂)
389 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
390 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) : F →ₜ* K where
391 toMonoidHom := hF.isFreeProduct.lift φ₁.toMonoidHom φ₂.toMonoidHom
392 continuous_toFun := hF.lift_continuous φ₁ φ₂
394omit [IsTopologicalGroup F] in
395/-- The lift from a topological free product restricts to the prescribed map on the left factor. -/
396@[simp] theorem lift_left (hF : IsTopologicalFreeProduct ι₁ ι₂)
397 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
398 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
399 (hF.lift φ₁ φ₂).comp ι₁ = φ₁ := by
400 apply ContinuousMonoidHom.toMonoidHom_injective
401 exact hF.isFreeProduct.lift_left φ₁.toMonoidHom φ₂.toMonoidHom
403omit [IsTopologicalGroup F] in
404/-- The lift from a topological free product restricts to the prescribed map on the right factor. -/
405@[simp 900] theorem lift_right (hF : IsTopologicalFreeProduct ι₁ ι₂)
406 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
407 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
408 (hF.lift φ₁ φ₂).comp ι₂ = φ₂ := by
409 apply ContinuousMonoidHom.toMonoidHom_injective
410 exact hF.isFreeProduct.lift_right φ₁.toMonoidHom φ₂.toMonoidHom
414end TopologicalFreeProducts
416section FreeProCProducts
419variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
420variable [Group G₁] [TopologicalSpace G₁]
421variable [Group G₂] [TopologicalSpace G₂]
422variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
424/-- Binary free pro-`C` products via the strengthened universal property used elsewhere in the
425project: every pair of continuous homomorphisms into a pro-`C` target extends uniquely. -/
426structure IsFreeProCProduct (ι₁ : G₁ →ₜ* F) (ι₂ : G₂ →ₜ* F) : Prop where
427 isProC : ProC (G := F)
429 ∀ {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
430 ProC (G := K) →
431 ∀ (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K),
432 ∃! φ : F →ₜ* K, φ.comp ι₁ = φ₁ ∧ φ.comp ι₂ = φ₂
434/-- The mapping property part of a binary free pro-`C` product. -/
435def HasFreeProCProductMappingProperty (ι₁ : G₁ →ₜ* F) (ι₂ : G₂ →ₜ* F) : Prop :=
436 ∀ {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
437 ProC (G := K) →
438 ∀ (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K),
439 ∃! φ : F →ₜ* K, φ.comp ι₁ = φ₁ ∧ φ.comp ι₂ = φ₂
441/-- A stricter free pro-`C` product statement in which the factors are also pro-`C` objects. -/
443 [IsTopologicalGroup G₁] [IsTopologicalGroup G₂]
444 (ι₁ : G₁ →ₜ* F) (ι₂ : G₂ →ₜ* F) : Prop where
445 left_isProC : ProC (G := G₁)
446 right_isProC : ProC (G := G₂)
447 product_isProC : ProC (G := F)
448 property : HasFreeProCProductMappingProperty (ProC := ProC) ι₁ ι₂
452variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
454/-- Chosen descent morphism from a binary free pro-`C` product object. -/
455noncomputable def lift (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
456 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
457 (hK : ProC (G := K))
458 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) : F →ₜ* K :=
459 Classical.choose (ExistsUnique.exists (hF.existsUnique_lift hK φ₁ φ₂))
461/-- The chosen free pro-`C` descent morphism has the prescribed composites. -/
462theorem lift_spec (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
463 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
464 (hK : ProC (G := K))
465 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
466 (hF.lift hK φ₁ φ₂).comp ι₁ = φ₁ ∧ (hF.lift hK φ₁ φ₂).comp ι₂ = φ₂ :=
467 Classical.choose_spec (ExistsUnique.exists (hF.existsUnique_lift hK φ₁ φ₂))
469/-- Left composite of the chosen free pro-`C` descent morphism. -/
470@[simp] theorem lift_left (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
471 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
472 (hK : ProC (G := K))
473 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
474 (hF.lift hK φ₁ φ₂).comp ι₁ = φ₁ :=
475 (hF.lift_spec hK φ₁ φ₂).1
477/-- Right composite of the chosen free pro-`C` descent morphism. -/
478@[simp] theorem lift_right (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
479 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
480 (hK : ProC (G := K))
481 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K) :
482 (hF.lift hK φ₁ φ₂).comp ι₂ = φ₂ :=
483 (hF.lift_spec hK φ₁ φ₂).2
485/-- Uniqueness of the chosen free pro-`C` descent morphism. -/
486theorem lift_unique (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
487 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
488 (hK : ProC (G := K))
489 (φ₁ : G₁ →ₜ* K) (φ₂ : G₂ →ₜ* K)
490 {ψ : F →ₜ* K} (hψ : ψ.comp ι₁ = φ₁ ∧ ψ.comp ι₂ = φ₂) :
491 ψ = hF.lift hK φ₁ φ₂ := by
492 rcases hF.existsUnique_lift hK φ₁ φ₂ with ⟨u, hu, huuniq⟩
493 have hchosen : hF.lift hK φ₁ φ₂ = u := huuniq _ (hF.lift_spec hK φ₁ φ₂)
494 exact (huuniq _ hψ).trans hchosen.symm
496/-- The distinguished descent map from a free pro-`C` product object to itself is the identity. -/
497@[simp] theorem lift_self (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂) :
498 hF.lift hF.isProC ι₁ ι₂ = ContinuousMonoidHom.id F := by
499 symm
500 exact hF.lift_unique hF.isProC ι₁ ι₂ ⟨rfl, rfl⟩
502/-- Extensionality of continuous homomorphisms out of a free pro-`C` product object. -/
503theorem hom_ext (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
504 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
505 (hK : ProC (G := K))
506 {ψ ψ' : F →ₜ* K}
507 (h₁ : ψ.comp ι₁ = ψ'.comp ι₁) (h₂ : ψ.comp ι₂ = ψ'.comp ι₂) :
508 ψ = ψ' := by
509 have hψ : ψ = hF.lift (K := K) hK (ψ.comp ι₁) (ψ.comp ι₂) := by
510 exact hF.lift_unique (K := K) hK (ψ.comp ι₁) (ψ.comp ι₂) ⟨rfl, rfl⟩
511 have hψ' : ψ' = hF.lift (K := K) hK (ψ.comp ι₁) (ψ.comp ι₂) := by
512 exact hF.lift_unique (K := K) hK (ψ.comp ι₁) (ψ.comp ι₂) ⟨h₁.symm, h₂.symm⟩
513 exact hψ.trans hψ'.symm
515variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
516variable {ι₁' : G₁ →ₜ* F'} {ι₂' : G₂ →ₜ* F'}
518/-- Canonical comparison morphism between two free pro-`C` product objects on the same factors. -/
519noncomputable def compare (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
520 (hF' : IsFreeProCProduct (ProC := ProC) ι₁' ι₂') :
521 F →ₜ* F' :=
522 hF.lift hF'.isProC ι₁' ι₂'
524/-- Left composite of the canonical comparison map between free pro-`C` product objects. -/
525@[simp 900] theorem compare_left (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
526 (hF' : IsFreeProCProduct (ProC := ProC) ι₁' ι₂') :
527 (hF.compare hF').comp ι₁ = ι₁' :=
528 hF.lift_left hF'.isProC ι₁' ι₂'
530/-- Right composite of the canonical comparison map between free pro-`C` product objects. -/
531@[simp 900] theorem compare_right (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
532 (hF' : IsFreeProCProduct (ProC := ProC) ι₁' ι₂') :
533 (hF.compare hF').comp ι₂ = ι₂' :=
534 hF.lift_right hF'.isProC ι₁' ι₂'
536/-- The canonical comparison map from a free pro-`C` product object to itself is the identity. -/
537@[simp 900] theorem compare_self (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂) :
538 hF.compare hF = ContinuousMonoidHom.id F := by
539 exact hF.lift_self
541variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
542variable {ι₁'' : G₁ →ₜ* F''} {ι₂'' : G₂ →ₜ* F''}
544/-- Composition of free pro-`C` comparison maps is the expected direct comparison map. -/
545theorem compare_comp (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
546 (hF' : IsFreeProCProduct (ProC := ProC) ι₁' ι₂')
547 (hF'' : IsFreeProCProduct (ProC := ProC) ι₁'' ι₂'') :
548 (hF'.compare hF'').comp (hF.compare hF') = hF.compare hF'' := by
549 apply hF.hom_ext hF''.isProC
550 · calc
551 ((hF'.compare hF'').comp (hF.compare hF')).comp ι₁
552 = (hF'.compare hF'').comp ((hF.compare hF').comp ι₁) := by rfl
553 _ = (hF'.compare hF'').comp ι₁' := by rw [hF.compare_left hF']
554 _ = ι₁'' := hF'.compare_left hF''
555 _ = (hF.compare hF'').comp ι₁ := (hF.compare_left hF'').symm
556 · calc
557 ((hF'.compare hF'').comp (hF.compare hF')).comp ι₂
558 = (hF'.compare hF'').comp ((hF.compare hF').comp ι₂) := by rfl
559 _ = (hF'.compare hF'').comp ι₂' := by rw [hF.compare_right hF']
560 _ = ι₂'' := hF'.compare_right hF''
561 _ = (hF.compare hF'').comp ι₂ := (hF.compare_right hF'').symm
563/-- Any two binary free pro-`C` product objects on the same factors are canonically equivalent as
564topological groups. -/
565noncomputable def equiv (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
566 (hF' : IsFreeProCProduct (ProC := ProC) ι₁' ι₂') :
567 F ≃ₜ* F' := by
568 let φ : F →ₜ* F' := hF.compare hF'
569 let ψ : F' →ₜ* F := hF'.compare hF
570 have hleft : ψ.comp φ = ContinuousMonoidHom.id F := by
571 calc
572 ψ.comp φ = hF.compare hF := by
573 simpa [φ, ψ] using hF.compare_comp hF' hF
574 _ = ContinuousMonoidHom.id F := hF.compare_self
575 have hright : φ.comp ψ = ContinuousMonoidHom.id F' := by
576 calc
577 φ.comp ψ = hF'.compare hF' := by
578 simpa [φ, ψ] using hF'.compare_comp hF hF'
579 _ = ContinuousMonoidHom.id F' := hF'.compare_self
580 refine ContinuousMulEquiv.mk'
581 (Homeomorph.mk
582 (MonoidHom.toMulEquiv φ.toMonoidHom ψ.toMonoidHom
583 (by simpa using congrArg ContinuousMonoidHom.toMonoidHom hleft)
584 (by simpa using congrArg ContinuousMonoidHom.toMonoidHom hright))
585 φ.continuous_toFun ψ.continuous_toFun)
586 ?_
587 intro x y
588 exact φ.map_mul x y
590/-- Left composite of the canonical free pro-`C` product equivalence. -/
591@[simp] theorem equiv_left (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
592 (hF' : IsFreeProCProduct (ProC := ProC) ι₁' ι₂') :
593 ((hF.equiv hF' : F →ₜ* F').comp ι₁) = ι₁' := by
594 exact hF.compare_left hF'
596/-- Right composite of the canonical free pro-`C` product equivalence. -/
597@[simp] theorem equiv_right (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
598 (hF' : IsFreeProCProduct (ProC := ProC) ι₁' ι₂') :
599 ((hF.equiv hF' : F →ₜ* F').comp ι₂) = ι₂' := by
600 exact hF.compare_right hF'
602/-- Left-leg formula for the inverse canonical free pro-`C` product equivalence. -/
603theorem equiv_symm_left (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
604 (hF' : IsFreeProCProduct (ProC := ProC) ι₁' ι₂') :
605 (((hF.equiv hF').symm : F' →ₜ* F).comp ι₁') = ι₁ := by
606 change (hF'.compare hF).comp ι₁' = ι₁
607 exact hF'.compare_left hF
609/-- Right-leg formula for the inverse canonical free pro-`C` product equivalence. -/
610theorem equiv_symm_right (hF : IsFreeProCProduct (ProC := ProC) ι₁ ι₂)
611 (hF' : IsFreeProCProduct (ProC := ProC) ι₁' ι₂') :
612 (((hF.equiv hF').symm : F' →ₜ* F).comp ι₂') = ι₂ := by
613 change (hF'.compare hF).comp ι₂' = ι₂
614 exact hF'.compare_right hF
621variable {G₁ : Type u} {G₂ : Type u} {F₀ : Type u} {Fhat : Type u}
622variable [Group G₁] [TopologicalSpace G₁]
623variable [Group G₂] [TopologicalSpace G₂]
624variable [Group F₀] [TopologicalSpace F₀] [IsTopologicalGroup F₀]
625variable [Group Fhat] [TopologicalSpace Fhat] [IsTopologicalGroup Fhat]
626variable {j₁ : G₁ →ₜ* F₀} {j₂ : G₂ →ₜ* F₀} {η : F₀ →ₜ* Fhat}
628/-- The left factor map into a pro-`C` completion of a topological free product model. -/
630 (_hη : ProCGroups.Completion.IsProCCompletion ProC F₀ Fhat η)
631 (j₁ : G₁ →ₜ* F₀) : G₁ →ₜ* Fhat :=
632 η.comp j₁
634/-- The right factor map into a pro-`C` completion of a topological free product model. -/
636 (_hη : ProCGroups.Completion.IsProCCompletion ProC F₀ Fhat η)
637 (j₂ : G₂ →ₜ* F₀) : G₂ →ₜ* Fhat :=
638 η.comp j₂
640/-- The completed left inclusion evaluates to the corresponding generator in the completed free product. -/
641@[simp 900] theorem completionInl_apply
643 (j₁ : G₁ →ₜ* F₀) (x : G₁) :
644 completionInl (ProC := ProC) hη j₁ x = η (j₁ x) :=
645 rfl
647/-- The completed right inclusion evaluates to the corresponding generator in the completed free product. -/
648@[simp 900] theorem completionInr_apply
650 (j₂ : G₂ →ₜ* F₀) (x : G₂) :
651 completionInr (ProC := ProC) hη j₂ x = η (j₂ x) :=
652 rfl
654/-- A pro-`C` completion of a topological free product model is a free pro-`C` product. This is
655the construction theorem separating the topological-free-product model from the pro-`C`
656reflection/completion step. -/
658 (hF₀ : IsTopologicalFreeProduct j₁ j₂)
659 (hη : ProCGroups.Completion.IsProCCompletion ProC F₀ Fhat η) :
660 IsFreeProCProduct (ProC := ProC)
661 (completionInl (ProC := ProC) hη j₁)
662 (completionInr (ProC := ProC) hη j₂) := by
663 refine ⟨hη.isProC, ?_⟩
664 intro K _ _ _ hK φ₁ φ₂
665 let ψ₀ : F₀ →ₜ* K :=
666 { toMonoidHom := hF₀.isFreeProduct.lift φ₁.toMonoidHom φ₂.toMonoidHom
667 continuous_toFun := hF₀.lift_continuous φ₁ φ₂ }
668 rcases hη.existsUnique_lift hK ψ₀ with ⟨Ψ, hΨ, huniq⟩
669 refine ⟨Ψ, ?_, ?_⟩
670 · constructor
671 · ext x
672 have hfacx := congrArg (fun f : F₀ →ₜ* K => f (j₁ x)) hΨ
673 have hleftx :=
674 congrArg (fun f : G₁ →* K => f x)
675 (hF₀.isFreeProduct.lift_left φ₁.toMonoidHom φ₂.toMonoidHom)
676 calc
677 Ψ (completionInl (ProC := ProC) hη j₁ x) = Ψ (η (j₁ x)) := rfl
678 _ = ψ₀ (j₁ x) := hfacx
679 _ = φ₁ x := hleftx
680 · ext x
681 have hfacx := congrArg (fun f : F₀ →ₜ* K => f (j₂ x)) hΨ
682 have hrightx :=
683 congrArg (fun f : G₂ →* K => f x)
684 (hF₀.isFreeProduct.lift_right φ₁.toMonoidHom φ₂.toMonoidHom)
685 calc
686 Ψ (completionInr (ProC := ProC) hη j₂ x) = Ψ (η (j₂ x)) := rfl
687 _ = ψ₀ (j₂ x) := hfacx
688 _ = φ₂ x := hrightx
689 · intro Χ hΧ
690 apply huniq
691 apply ContinuousMonoidHom.toMonoidHom_injective
692 apply hF₀.isFreeProduct.hom_ext
693 · ext x
694 have hΧx := congrArg (fun f : G₁ →ₜ* K => f x) hΧ.1
695 have hleftx :=
696 congrArg (fun f : G₁ →* K => f x)
697 (hF₀.isFreeProduct.lift_left φ₁.toMonoidHom φ₂.toMonoidHom)
698 calc
699 ((Χ.comp η).toMonoidHom.comp j₁.toMonoidHom) x =
700 (Χ.comp (completionInl (ProC := ProC) hη j₁)) x := rfl
701 _ = φ₁ x := hΧx
702 _ = ψ₀ (j₁ x) := hleftx.symm
703 · ext x
704 have hΧx := congrArg (fun f : G₂ →ₜ* K => f x) hΧ.2
705 have hrightx :=
706 congrArg (fun f : G₂ →* K => f x)
707 (hF₀.isFreeProduct.lift_right φ₁.toMonoidHom φ₂.toMonoidHom)
708 calc
709 ((Χ.comp η).toMonoidHom.comp j₂.toMonoidHom) x =
710 (Χ.comp (completionInr (ProC := ProC) hη j₂)) x := rfl
711 _ = φ₂ x := hΧx
712 _ = ψ₀ (j₂ x) := hrightx.symm
714/-- Existence form of `isFreeProCProduct_of_completion`, exposing the completed factor maps as
715the constructed coproduct legs. -/
717 (hF₀ : IsTopologicalFreeProduct j₁ j₂)
718 (hη : ProCGroups.Completion.IsProCCompletion ProC F₀ Fhat η) :
719 ∃ (ι₁hat : G₁ →ₜ* Fhat) (ι₂hat : G₂ →ₜ* Fhat),
720 IsFreeProCProduct (ProC := ProC) ι₁hat ι₂hat :=
721 ⟨completionInl (ProC := ProC) hη j₁,
722 completionInr (ProC := ProC) hη j₂,
723 isFreeProCProduct_of_completion (ProC := ProC) hF₀ hη⟩
727namespace IsFreeProfiniteProduct
729variable {G₁ : Type u} {G₂ : Type u} {F : Type u}
730variable [Group G₁] [TopologicalSpace G₁]
731variable [Group G₂] [TopologicalSpace G₂]
732variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
733variable {ι₁ : G₁ →ₜ* F} {ι₂ : G₂ →ₜ* F}
735/-- The underlying profiniteness of a free profinite product object. -/
736theorem isProfiniteGroup
737 (hF : IsFreeProCProduct (ProC := ProCGroups.ProC.allFiniteProC) ι₁ ι₂) :
739 hF.isProC
741/-- A binary free profinite product is a pushout over the trivial profinite group. -/
743 (hF : IsFreeProCProduct (ProC := ProCGroups.ProC.allFiniteProC) ι₁ ι₂) :
744 ProCGroups.Categorical.HasProfiniteTestPushoutProperty
745 (1 : ULift.{u, 0} Unit →ₜ* G₁) (1 : ULift.{u, 0} Unit →ₜ* G₂) ι₁ ι₂ := by
746 constructor
747 · ext u
748 cases u
749 simp only [ContinuousMonoidHom.comp_toFun, ContinuousMonoidHom.one_toFun, map_one]
750 · intro K _ _ _ hK φ₁ φ₂ _hφ
751 refine ⟨hF.lift hK φ₁ φ₂, hF.lift_spec hK φ₁ φ₂, ?_⟩
752 intro ψ hψ
753 exact hF.lift_unique hK φ₁ φ₂ hψ
755/-- A profinite pushout over the trivial group satisfies the binary free profinite-product
756universal property. -/
758 (hpo : ProCGroups.Categorical.HasProfiniteTestPushoutProperty
759 (1 : ULift.{u, 0} Unit →ₜ* G₁) (1 : ULift.{u, 0} Unit →ₜ* G₂) ι₁ ι₂) :
761 refine ⟨hF, ?_⟩
762 intro K _ _ _ hK φ₁ φ₂
763 have hφ : φ₁.comp (1 : ULift.{u, 0} Unit →ₜ* G₁) =
764 φ₂.comp (1 : ULift.{u, 0} Unit →ₜ* G₂) := by
765 ext u
766 cases u
767 simp only [ContinuousMonoidHom.comp_toFun, ContinuousMonoidHom.one_toFun, map_one]
768 simpa using hpo.2 hK φ₁ φ₂ hφ
770/-- Binary free profinite products are exactly profinite pushouts over the trivial group. -/
773 ProCGroups.Categorical.HasProfiniteTestPushoutProperty
774 (1 : ULift.{u, 0} Unit →ₜ* G₁) (1 : ULift.{u, 0} Unit →ₜ* G₂) ι₁ ι₂ :=
777end IsFreeProfiniteProduct
779/-- Indexed free pro-`C` products via the strengthened universal property used elsewhere in the
780project. This is the family-indexed analogue needed by Kurosh-type decompositions. -/
781structure IsFreeProCProductFamily {A : Type u} (G : A → Type u)
782 [∀ a, Group (G a)] [∀ a, TopologicalSpace (G a)] [∀ a, IsTopologicalGroup (G a)]
783 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
784 (ι : ∀ a, G a →ₜ* F) : Prop where
785 isProC : ProC (G := F)
787 ∀ {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
788 ProC (G := K) →
789 ∀ (φ : ∀ a, G a →ₜ* K),
790 ∃! ψ : F →ₜ* K, ∀ a, ψ.comp (ι a) = φ a
794variable {A : Type u} {G : A → Type u}
795variable [∀ a, Group (G a)] [∀ a, TopologicalSpace (G a)] [∀ a, IsTopologicalGroup (G a)]
796variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
797variable {ι : ∀ a, G a →ₜ* F}
799/-- Chosen descent morphism from a family free pro-`C` product object. -/
800noncomputable def lift (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
801 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
802 (hK : ProC (G := K))
803 (φ : ∀ a, G a →ₜ* K) : F →ₜ* K :=
804 Classical.choose (ExistsUnique.exists (hF.existsUnique_lift hK φ))
806/-- Component formula for the chosen family free pro-`C` descent morphism. -/
807@[simp] theorem lift_ι (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
808 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
809 (hK : ProC (G := K))
810 (φ : ∀ a, G a →ₜ* K) (a : A) :
811 (hF.lift hK φ).comp (ι a) = φ a :=
812 Classical.choose_spec (ExistsUnique.exists (hF.existsUnique_lift hK φ)) a
814/-- Uniqueness of the chosen family free pro-`C` descent morphism. -/
815theorem lift_unique (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
816 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
817 (hK : ProC (G := K))
818 (φ : ∀ a, G a →ₜ* K)
819 {ψ : F →ₜ* K} (hψ : ∀ a, ψ.comp (ι a) = φ a) :
820 ψ = hF.lift hK φ := by
821 rcases hF.existsUnique_lift hK φ with ⟨u, hu, huuniq⟩
822 have hchosen : hF.lift hK φ = u := huuniq _ (fun a => hF.lift_ι hK φ a)
823 exact (huuniq _ hψ).trans hchosen.symm
825/-- The distinguished descent map from a family free pro-`C` product object to itself is the
826identity. -/
827@[simp] theorem lift_self (hF : IsFreeProCProductFamily (ProC := ProC) G ι) :
828 hF.lift hF.isProC ι = ContinuousMonoidHom.id F := by
829 symm
830 exact hF.lift_unique hF.isProC ι (fun _ => rfl)
832/-- Extensionality of continuous homomorphisms out of a family free pro-`C` product object. -/
833theorem hom_ext (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
834 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
835 (hK : ProC (G := K))
836 {ψ ψ' : F →ₜ* K}
837 (h : ∀ a, ψ.comp (ι a) = ψ'.comp (ι a)) :
838 ψ = ψ' := by
839 have hψ : ψ = hF.lift hK (fun a => ψ.comp (ι a)) := by
840 exact hF.lift_unique hK (fun a => ψ.comp (ι a)) (fun _ => rfl)
841 have hψ' : ψ' = hF.lift hK (fun a => ψ.comp (ι a)) := by
842 exact hF.lift_unique hK (fun a => ψ.comp (ι a)) (fun a => (h a).symm)
843 exact hψ.trans hψ'.symm
845variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
846variable {ι' : ∀ a, G a →ₜ* F'}
848/-- Canonical comparison morphism between two family free pro-`C` product objects on the same
849factors. -/
850noncomputable def compare
851 (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
852 (hF' : IsFreeProCProductFamily (ProC := ProC) G ι') :
853 F →ₜ* F' :=
854 hF.lift hF'.isProC ι'
856/-- Component formula for the canonical comparison map between family free pro-`C` product
857objects. -/
858@[simp 900] theorem compare_ι
859 (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
860 (hF' : IsFreeProCProductFamily (ProC := ProC) G ι') (a : A) :
861 (hF.compare hF').comp (ι a) = ι' a :=
862 hF.lift_ι hF'.isProC ι' a
864/-- The canonical comparison map from a family free pro-`C` product object to itself is the
865identity. -/
866@[simp 900] theorem compare_self (hF : IsFreeProCProductFamily (ProC := ProC) G ι) :
867 hF.compare hF = ContinuousMonoidHom.id F := by
868 exact hF.lift_self
870variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
871variable {ι'' : ∀ a, G a →ₜ* F''}
873/-- Composition of family free pro-`C` comparison maps is the expected direct comparison map. -/
874theorem compare_comp
875 (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
876 (hF' : IsFreeProCProductFamily (ProC := ProC) G ι')
877 (hF'' : IsFreeProCProductFamily (ProC := ProC) G ι'') :
878 (hF'.compare hF'').comp (hF.compare hF') = hF.compare hF'' := by
879 apply hF.hom_ext hF''.isProC
880 intro a
881 calc
882 ((hF'.compare hF'').comp (hF.compare hF')).comp (ι a)
883 = (hF'.compare hF'').comp ((hF.compare hF').comp (ι a)) := by rfl
884 _ = (hF'.compare hF'').comp (ι' a) := by rw [hF.compare_ι hF' a]
885 _ = ι'' a := hF'.compare_ι hF'' a
886 _ = (hF.compare hF'').comp (ι a) := (hF.compare_ι hF'' a).symm
888/-- Any two family free pro-`C` product objects on the same factors are canonically equivalent as
889topological groups. -/
890noncomputable def equiv
891 (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
892 (hF' : IsFreeProCProductFamily (ProC := ProC) G ι') :
893 F ≃ₜ* F' := by
894 let φ : F →ₜ* F' := hF.compare hF'
895 let ψ : F' →ₜ* F := hF'.compare hF
896 have hleft : ψ.comp φ = ContinuousMonoidHom.id F := by
897 calc
898 ψ.comp φ = hF.compare hF := by
899 simpa [φ, ψ] using hF.compare_comp hF' hF
900 _ = ContinuousMonoidHom.id F := hF.compare_self
901 have hright : φ.comp ψ = ContinuousMonoidHom.id F' := by
902 calc
903 φ.comp ψ = hF'.compare hF' := by
904 simpa [φ, ψ] using hF'.compare_comp hF hF'
905 _ = ContinuousMonoidHom.id F' := hF'.compare_self
906 refine ContinuousMulEquiv.mk'
907 (Homeomorph.mk
908 (MonoidHom.toMulEquiv φ.toMonoidHom ψ.toMonoidHom
909 (by simpa using congrArg ContinuousMonoidHom.toMonoidHom hleft)
910 (by simpa using congrArg ContinuousMonoidHom.toMonoidHom hright))
911 φ.continuous_toFun ψ.continuous_toFun)
912 ?_
913 intro x y
914 exact φ.map_mul x y
916/-- Component formula for the canonical equivalence between family free pro-`C` product objects. -/
917@[simp] theorem equiv_ι
918 (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
919 (hF' : IsFreeProCProductFamily (ProC := ProC) G ι') (a : A) :
920 ((hF.equiv hF' : F →ₜ* F').comp (ι a)) = ι' a := by
921 exact hF.compare_ι hF' a
923/-- Component formula for the inverse canonical equivalence between family free pro-`C` product
924objects. -/
925theorem equiv_symm_ι
926 (hF : IsFreeProCProductFamily (ProC := ProC) G ι)
927 (hF' : IsFreeProCProductFamily (ProC := ProC) G ι') (a : A) :
928 (((hF.equiv hF').symm : F' →ₜ* F).comp (ι' a)) = ι a := by
929 change (hF'.compare hF).comp (ι' a) = ι a
930 exact hF'.compare_ι hF a
934/-- A family of continuous homomorphisms converges to `1` if every open subgroup of the target
935contains the image of all but finitely many components. This is the convergence hypothesis used in
936the indexed-family free pro-`C` product universal property. -/
937def ContinuousHomFamilyConvergesToOne {A : Type u} (G : A → Type u)
938 [∀ a, Group (G a)] [∀ a, TopologicalSpace (G a)]
939 {K : Type u} [Group K] [TopologicalSpace K]
940 (φ : ∀ a, G a →ₜ* K) : Prop :=
941 ∀ U : OpenSubgroup K, {a | ¬ (φ a).toMonoidHom.range ≤ (U : Subgroup K)}.Finite
945variable {A : Type u} {G : A → Type u}
946variable [∀ a, Group (G a)] [∀ a, TopologicalSpace (G a)]
947variable {K : Type u} [Group K] [TopologicalSpace K]
948variable {L : Type u} [Group L] [TopologicalSpace L]
949variable {φ : ∀ a, G a →ₜ* K}
951/-- Postcomposing a convergent family of homomorphisms with a continuous homomorphism preserves
952convergence to `1`. -/
953theorem comp (hφ : ContinuousHomFamilyConvergesToOne G φ) (ψ : K →ₜ* L) :
954 ContinuousHomFamilyConvergesToOne G (fun a => ψ.comp (φ a)) := by
955 intro U
956 let V : OpenSubgroup K := OpenSubgroup.comap (f := ψ.toMonoidHom) ψ.continuous_toFun U
957 refine (hφ V).subset ?_
958 intro a ha hle
959 apply ha
960 intro y hy
961 rcases hy with ⟨x, rfl⟩
962 have hxV : φ a x ∈ (V : Subgroup K) := hle ⟨x, rfl⟩
963 simpa [V] using hxV
967/-- Indexed free pro-`C` products in the infinite indexed-family form: the universal property
968is tested only against families of maps converging to `1`, and the distinguished inclusions
969themselves converge to `1`. -/
970structure IsIndexedFreeProCProductFamily {A : Type u} (G : A → Type u)
971 [∀ a, Group (G a)] [∀ a, TopologicalSpace (G a)] [∀ a, IsTopologicalGroup (G a)]
972 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
973 (ι : ∀ a, G a →ₜ* F) : Prop where
974 isProC : ProC (G := F)
975 inclusionsConverge : ContinuousHomFamilyConvergesToOne G ι
977 ∀ {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
978 ProC (G := K) →
979 ∀ (φ : ∀ a, G a →ₜ* K),
981 ∃! ψ : F →ₜ* K, ∀ a, ψ.comp (ι a) = φ a
985variable {A : Type u} {G : A → Type u}
986variable [∀ a, Group (G a)] [∀ a, TopologicalSpace (G a)] [∀ a, IsTopologicalGroup (G a)]
987variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
988variable {ι : ∀ a, G a →ₜ* F}
990/-- Chosen descent morphism from an indexed-family free pro-`C` product object. -/
991noncomputable def lift (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
992 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
993 (hK : ProC (G := K))
994 (φ : ∀ a, G a →ₜ* K)
995 (hφ : ContinuousHomFamilyConvergesToOne G φ) : F →ₜ* K :=
996 Classical.choose (ExistsUnique.exists (hF.existsUnique_lift hK φ hφ))
998/-- Component formula for the chosen indexed-family descent morphism. -/
999@[simp] theorem lift_ι (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
1000 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
1001 (hK : ProC (G := K))
1002 (φ : ∀ a, G a →ₜ* K)
1004 (hF.lift hK φ hφ).comp (ι a) = φ a :=
1005 Classical.choose_spec (ExistsUnique.exists (hF.existsUnique_lift hK φ hφ)) a
1007/-- Uniqueness of the chosen indexed-family descent morphism. -/
1008theorem lift_unique (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
1009 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
1010 (hK : ProC (G := K))
1011 (φ : ∀ a, G a →ₜ* K)
1013 {ψ : F →ₜ* K} (hψ : ∀ a, ψ.comp (ι a) = φ a) :
1014 ψ = hF.lift hK φ hφ := by
1015 rcases hF.existsUnique_lift hK φ hφ with ⟨u, hu, huuniq⟩
1016 have hchosen : hF.lift hK φ hφ = u := huuniq _ (fun a => hF.lift_ι hK φ hφ a)
1017 exact (huuniq _ hψ).trans hchosen.symm
1019/-- The distinguished descent map from an indexed-family free pro-`C` product object to
1020itself is the identity. -/
1021@[simp] theorem lift_self (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι) :
1022 hF.lift hF.isProC ι hF.inclusionsConverge = ContinuousMonoidHom.id F := by
1023 symm
1024 exact hF.lift_unique hF.isProC ι hF.inclusionsConverge (fun _ => rfl)
1026/-- Extensionality of continuous homomorphisms out of an indexed-family free pro-`C`
1027product object. -/
1028theorem hom_ext (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
1029 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
1030 (hK : ProC (G := K))
1031 {ψ ψ' : F →ₜ* K}
1032 (h : ∀ a, ψ.comp (ι a) = ψ'.comp (ι a)) :
1033 ψ = ψ' := by
1034 have hconv :
1035 ContinuousHomFamilyConvergesToOne G (fun a => ψ.comp (ι a)) :=
1036 hF.inclusionsConverge.comp ψ
1037 have hψ : ψ = hF.lift hK (fun a => ψ.comp (ι a)) hconv := by
1038 exact hF.lift_unique hK (fun a => ψ.comp (ι a)) hconv (fun _ => rfl)
1039 have hψ' : ψ' = hF.lift hK (fun a => ψ.comp (ι a)) hconv := by
1040 exact hF.lift_unique hK (fun a => ψ.comp (ι a)) hconv (fun a => (h a).symm)
1041 exact hψ.trans hψ'.symm
1043variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
1044variable {ι' : ∀ a, G a →ₜ* F'}
1046/-- Canonical comparison morphism between two indexed-family free pro-`C` product objects
1047on the same factors. -/
1048noncomputable def compare
1049 (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
1050 (hF' : IsIndexedFreeProCProductFamily (ProC := ProC) G ι') :
1051 F →ₜ* F' :=
1052 hF.lift hF'.isProC ι' hF'.inclusionsConverge
1054/-- Component formula for the canonical comparison map between indexed-family free pro-`C`
1055product objects. -/
1056@[simp 900] theorem compare_ι
1057 (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
1058 (hF' : IsIndexedFreeProCProductFamily (ProC := ProC) G ι') (a : A) :
1059 (hF.compare hF').comp (ι a) = ι' a :=
1060 hF.lift_ι hF'.isProC ι' hF'.inclusionsConverge a
1062/-- The canonical comparison map from an indexed-family free pro-`C` product object to
1063itself is the identity. -/
1064@[simp 900] theorem compare_self (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι) :
1065 hF.compare hF = ContinuousMonoidHom.id F := by
1066 exact hF.lift_self
1068variable {F'' : Type u} [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
1069variable {ι'' : ∀ a, G a →ₜ* F''}
1071/-- Composition of indexed-family free pro-`C` comparison maps is the expected direct
1073theorem compare_comp
1074 (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
1075 (hF' : IsIndexedFreeProCProductFamily (ProC := ProC) G ι')
1076 (hF'' : IsIndexedFreeProCProductFamily (ProC := ProC) G ι'') :
1077 (hF'.compare hF'').comp (hF.compare hF') = hF.compare hF'' := by
1078 apply hF.hom_ext hF''.isProC
1079 intro a
1080 calc
1081 ((hF'.compare hF'').comp (hF.compare hF')).comp (ι a)
1082 = (hF'.compare hF'').comp ((hF.compare hF').comp (ι a)) := by rfl
1083 _ = (hF'.compare hF'').comp (ι' a) := by rw [hF.compare_ι hF' a]
1084 _ = ι'' a := hF'.compare_ι hF'' a
1085 _ = (hF.compare hF'').comp (ι a) := (hF.compare_ι hF'' a).symm
1087/-- Any two indexed-family free pro-`C` product objects on the same factors are canonically
1088equivalent as topological groups. -/
1089noncomputable def equiv
1090 (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
1091 (hF' : IsIndexedFreeProCProductFamily (ProC := ProC) G ι') :
1092 F ≃ₜ* F' := by
1093 let φ : F →ₜ* F' := hF.compare hF'
1094 let ψ : F' →ₜ* F := hF'.compare hF
1095 have hleft : ψ.comp φ = ContinuousMonoidHom.id F := by
1096 calc
1097 ψ.comp φ = hF.compare hF := by
1098 simpa [φ, ψ] using hF.compare_comp hF' hF
1099 _ = ContinuousMonoidHom.id F := hF.compare_self
1100 have hright : φ.comp ψ = ContinuousMonoidHom.id F' := by
1101 calc
1102 φ.comp ψ = hF'.compare hF' := by
1103 simpa [φ, ψ] using hF'.compare_comp hF hF'
1104 _ = ContinuousMonoidHom.id F' := hF'.compare_self
1105 refine ContinuousMulEquiv.mk'
1106 (Homeomorph.mk
1107 (MonoidHom.toMulEquiv φ.toMonoidHom ψ.toMonoidHom
1108 (by simpa using congrArg ContinuousMonoidHom.toMonoidHom hleft)
1109 (by simpa using congrArg ContinuousMonoidHom.toMonoidHom hright))
1110 φ.continuous_toFun ψ.continuous_toFun)
1111 ?_
1112 intro x y
1113 exact φ.map_mul x y
1115/-- Component formula for the canonical equivalence between indexed-family free pro-`C`
1116product objects. -/
1117@[simp] theorem equiv_ι
1118 (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
1119 (hF' : IsIndexedFreeProCProductFamily (ProC := ProC) G ι') (a : A) :
1120 ((hF.equiv hF' : F →ₜ* F').comp (ι a)) = ι' a := by
1121 exact hF.compare_ι hF' a
1123/-- Component formula for the inverse canonical equivalence between indexed-family free
1124pro-`C` product objects. -/
1125theorem equiv_symm_ι
1126 (hF : IsIndexedFreeProCProductFamily (ProC := ProC) G ι)
1127 (hF' : IsIndexedFreeProCProductFamily (ProC := ProC) G ι') (a : A) :
1128 (((hF.equiv hF').symm : F' →ₜ* F).comp (ι' a)) = ι a := by
1129 change (hF'.compare hF).comp (ι' a) = ι a
1130 exact hF'.compare_ι hF a
1134end FreeProCProducts
1136end ProCGroups.FreeProducts