Source: ProCGroups.Categorical.PushoutSquares
1import Mathlib.Algebra.Category.Grp.Basic
2import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
3import Mathlib.GroupTheory.Coprod.Basic
4import ProCGroups.Profinite.Basic
5import ProCGroups.Topologies.ContinuousMulEquiv
7/-!
8# Pro C Groups / Categorical / Pushout Squares
10This module constructs algebraic group pushouts from free products and normal
11closures, and develops algebraic and profinite-tested pushout universal properties.
12-/
14namespace ProCGroups.Categorical
16open CategoryTheory Limits
17open scoped Monoid.Coprod
19universe u v
21section
23variable {G G' H H₁ H₂ : Type u}
24variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
26/-- The abstract free product used as the carrier before imposing pushout relations. -/
27abbrev PushoutFreeProduct (H₁ H₂ : Type u) [Group H₁] [Group H₂] :=
28 Monoid.Coprod H₁ H₂
30/-- The relators identifying the two legs of a group cospan inside the free product. -/
31def pushoutRelators (β₁ : H →* H₁) (β₂ : H →* H₂) :
32 Set (PushoutFreeProduct H₁ H₂) :=
33 {z | ∃ h : H,
34 z = (Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂)⁻¹ *
35 (Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂)}
37/-- The normal subgroup generated by the cospan-identifying relators. -/
38def pushoutNormalClosure (β₁ : H →* H₁) (β₂ : H →* H₂) :
39 Subgroup (PushoutFreeProduct H₁ H₂) :=
40 Subgroup.normalClosure (pushoutRelators β₁ β₂)
42/-- The relator closure used in the concrete pushout is normal. -/
43instance pushoutNormalClosure_normal (β₁ : H →* H₁) (β₂ : H →* H₂) :
44 (pushoutNormalClosure β₁ β₂).Normal :=
45 Subgroup.normalClosure_normal
47namespace AlgebraicPushout
49/--
50Algebraic group pushout carrier: the free product modulo the normal closure of
51\(\operatorname{inl}(\beta_1 h)^{-1} * \operatorname{inr}(\beta_2 h)\).
52-/
53abbrev Carrier (β₁ : H →* H₁) (β₂ : H →* H₂) :=
54 PushoutFreeProduct H₁ H₂ ⧸ pushoutNormalClosure β₁ β₂
56/-- The left structural map into the algebraic pushout. -/
57def inl (β₁ : H →* H₁) (β₂ : H →* H₂) :
58 H₁ →* Carrier β₁ β₂ :=
59 (QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)).comp Monoid.Coprod.inl
61/-- The right structural map into the algebraic pushout. -/
62def inr (β₁ : H →* H₁) (β₂ : H →* H₂) :
63 H₂ →* Carrier β₁ β₂ :=
64 (QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)).comp Monoid.Coprod.inr
66/-- The algebraic pushout maps coequalize the original cospan. -/
67theorem inl_comp_eq_inr_comp
68 (β₁ : H →* H₁) (β₂ : H →* H₂) :
69 (inl β₁ β₂).comp β₁ = (inr β₁ β₂).comp β₂ := by
70 ext h
71 change QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
72 (Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂) =
73 QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
74 (Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂)
75 apply QuotientGroup.eq.2
76 exact Subgroup.subset_normalClosure ⟨h, rfl⟩
78/--
79The concrete pushout descent map is characterized by its compatibility with the two canonical
80inclusions.
81-/
82noncomputable def concretePushoutDesc
83 (β₁ : H →* H₁) (β₂ : H →* H₂)
84 {K : Type u} [Group K]
85 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
86 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
87 Carrier β₁ β₂ →* K :=
88 let F : PushoutFreeProduct H₁ H₂ →* K := Monoid.Coprod.lift φ₁ φ₂
89 QuotientGroup.lift (pushoutNormalClosure β₁ β₂) F <| by
90 refine Subgroup.normalClosure_le_normal ?_
91 rintro z ⟨h, rfl⟩
92 change F ((Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂)⁻¹ *
93 (Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂)) = 1
94 rw [map_mul, map_inv]
95 have hleft :
96 F (Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂) = φ₁ (β₁ h) :=
97 DFunLike.congr_fun (Monoid.Coprod.lift_comp_inl φ₁ φ₂) (β₁ h)
98 have hright :
99 F (Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂) = φ₂ (β₂ h) :=
100 DFunLike.congr_fun (Monoid.Coprod.lift_comp_inr φ₁ φ₂) (β₂ h)
101 have hcomp : φ₁ (β₁ h) = φ₂ (β₂ h) := DFunLike.congr_fun hφ h
102 rw [hleft, hright, hcomp]
103 simp only [inv_mul_cancel]
105/-- The concrete pushout descent map is compatible with the left inclusion. -/
106@[simp 900] theorem concretePushoutDesc_inl
107 (β₁ : H →* H₁) (β₂ : H →* H₂)
108 {K : Type u} [Group K]
109 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
110 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
111 (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inl β₁ β₂) = φ₁ := by
112 ext x
113 change concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ
114 (QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
115 (Monoid.Coprod.inl x : PushoutFreeProduct H₁ H₂)) = φ₁ x
116 simp only [concretePushoutDesc, QuotientGroup.mk'_apply, QuotientGroup.lift_mk,
117 Monoid.Coprod.lift_apply_inl]
119/-- The concrete pushout descent map is compatible with the right inclusion. -/
120@[simp 900] theorem concretePushoutDesc_inr
121 (β₁ : H →* H₁) (β₂ : H →* H₂)
122 {K : Type u} [Group K]
123 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
124 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
125 (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inr β₁ β₂) = φ₂ := by
126 ext x
127 change concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ
128 (QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
129 (Monoid.Coprod.inr x : PushoutFreeProduct H₁ H₂)) = φ₂ x
130 simp only [concretePushoutDesc, QuotientGroup.mk'_apply, QuotientGroup.lift_mk,
131 Monoid.Coprod.lift_apply_inr]
133end AlgebraicPushout
135/-- The concrete free-product quotient is a pushout in mathlib's category of groups. -/
136theorem AlgebraicPushout.isPushout (β₁ : H →* H₁) (β₂ : H →* H₂) :
137 CategoryTheory.IsPushout
138 (GrpCat.ofHom β₁) (GrpCat.ofHom β₂)
139 (GrpCat.ofHom (AlgebraicPushout.inl β₁ β₂))
140 (GrpCat.ofHom (AlgebraicPushout.inr β₁ β₂)) := by
141 let condition :
142 GrpCat.ofHom β₁ ≫ GrpCat.ofHom (AlgebraicPushout.inl β₁ β₂) =
143 GrpCat.ofHom β₂ ≫ GrpCat.ofHom (AlgebraicPushout.inr β₁ β₂) :=
144 GrpCat.hom_ext (AlgebraicPushout.inl_comp_eq_inr_comp β₁ β₂)
145 refine { w := condition, isColimit' := ⟨?_⟩ }
146 refine PushoutCocone.IsColimit.mk condition ?_ ?_ ?_ ?_
147 · intro s
148 exact GrpCat.ofHom <|
149 AlgebraicPushout.concretePushoutDesc β₁ β₂ s.inl.hom s.inr.hom
150 (congrArg GrpCat.Hom.hom s.condition)
151 · intro s
152 apply GrpCat.hom_ext
153 exact AlgebraicPushout.concretePushoutDesc_inl β₁ β₂ s.inl.hom s.inr.hom
154 (congrArg GrpCat.Hom.hom s.condition)
155 · intro s
156 apply GrpCat.hom_ext
157 exact AlgebraicPushout.concretePushoutDesc_inr β₁ β₂ s.inl.hom s.inr.hom
158 (congrArg GrpCat.Hom.hom s.condition)
159 · intro s m hm1 hm2
160 apply GrpCat.hom_ext
161 let q : PushoutFreeProduct H₁ H₂ →* AlgebraicPushout.Carrier β₁ β₂ :=
162 QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
163 let F : PushoutFreeProduct H₁ H₂ →* s.pt :=
164 Monoid.Coprod.lift s.inl.hom s.inr.hom
165 have hmq : m.hom.comp q = F := by
166 apply Monoid.Coprod.hom_ext
167 · calc
168 (m.hom.comp q).comp Monoid.Coprod.inl =
169 m.hom.comp (AlgebraicPushout.inl β₁ β₂) := rfl
170 _ = s.inl.hom := congrArg GrpCat.Hom.hom hm1
171 _ = F.comp Monoid.Coprod.inl :=
172 (Monoid.Coprod.lift_comp_inl s.inl.hom s.inr.hom).symm
173 · calc
174 (m.hom.comp q).comp Monoid.Coprod.inr =
175 m.hom.comp (AlgebraicPushout.inr β₁ β₂) := rfl
176 _ = s.inr.hom := congrArg GrpCat.Hom.hom hm2
177 _ = F.comp Monoid.Coprod.inr :=
178 (Monoid.Coprod.lift_comp_inr s.inl.hom s.inr.hom).symm
179 have hdescq :
180 (AlgebraicPushout.concretePushoutDesc β₁ β₂ s.inl.hom s.inr.hom
181 (congrArg GrpCat.Hom.hom s.condition)).comp q = F := by
182 apply Monoid.Coprod.hom_ext
183 · calc
184 ((AlgebraicPushout.concretePushoutDesc β₁ β₂ s.inl.hom s.inr.hom
185 (congrArg GrpCat.Hom.hom s.condition)).comp q).comp
186 Monoid.Coprod.inl =
187 (AlgebraicPushout.concretePushoutDesc β₁ β₂ s.inl.hom s.inr.hom
188 (congrArg GrpCat.Hom.hom s.condition)).comp
189 (AlgebraicPushout.inl β₁ β₂) := rfl
190 _ = s.inl.hom :=
191 AlgebraicPushout.concretePushoutDesc_inl β₁ β₂ s.inl.hom s.inr.hom
192 (congrArg GrpCat.Hom.hom s.condition)
193 _ = F.comp Monoid.Coprod.inl :=
194 (Monoid.Coprod.lift_comp_inl s.inl.hom s.inr.hom).symm
195 · calc
196 ((AlgebraicPushout.concretePushoutDesc β₁ β₂ s.inl.hom s.inr.hom
197 (congrArg GrpCat.Hom.hom s.condition)).comp q).comp
198 Monoid.Coprod.inr =
199 (AlgebraicPushout.concretePushoutDesc β₁ β₂ s.inl.hom s.inr.hom
200 (congrArg GrpCat.Hom.hom s.condition)).comp
201 (AlgebraicPushout.inr β₁ β₂) := rfl
202 _ = s.inr.hom :=
203 AlgebraicPushout.concretePushoutDesc_inr β₁ β₂ s.inl.hom s.inr.hom
204 (congrArg GrpCat.Hom.hom s.condition)
205 _ = F.comp Monoid.Coprod.inr :=
206 (Monoid.Coprod.lift_comp_inr s.inl.hom s.inr.hom).symm
207 apply MonoidHom.ext
208 intro y
209 rcases QuotientGroup.mk'_surjective
210 (pushoutNormalClosure β₁ β₂) y with ⟨z, rfl⟩
211 exact congrArg (fun f : PushoutFreeProduct H₁ H₂ →* s.pt => f z)
212 (hmq.trans hdescq.symm)
213end
215section
217variable {G G' H H₁ H₂ : Type u}
218variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
219variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
220variable [TopologicalSpace H₁] [TopologicalSpace H₂]
221variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
222variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
223variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
224variable [CompactSpace G'] [T2Space G'] [TotallyDisconnectedSpace G']
227/-- Continuous pushout property tested by profinite target objects.
229This definition does not assert that the four objects in the square are themselves profinite. -/
230def HasProfiniteTestPushoutProperty (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
231 (α₁ : H₁ →ₜ* G) (α₂ : H₂ →ₜ* G) : Prop :=
232 α₁.comp β₁ = α₂.comp β₂ ∧
233 ∀ ⦃K : Type u⦄ [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
234 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K],
235 ∀ (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K),
236 φ₁.comp β₁ = φ₂.comp β₂ →
237 ∃! φ : G →ₜ* K, φ.comp α₁ = φ₁ ∧ φ.comp α₂ = φ₂
239/-- Chosen continuous morphism induced by the profinite pushout universal property. -/
240noncomputable def pushoutDescCont
241 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
242 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
243 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
244 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
245 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
246 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
247 (hφ : φ₁.comp β₁ = φ₂.comp β₂) : G →ₜ* K :=
248 Classical.choose (ExistsUnique.exists (hpo.2 (K := K) φ₁ φ₂ hφ))
250omit [IsTopologicalGroup G] [IsTopologicalGroup H]
251 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
252 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
253/-- Specification of the chosen continuous pushout descent map. -/
254theorem pushoutDescCont_spec
255 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
256 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
257 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
258 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
259 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
260 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
261 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
262 (pushoutDescCont hpo φ₁ φ₂ hφ).comp α₁ = φ₁ ∧
263 (pushoutDescCont hpo φ₁ φ₂ hφ).comp α₂ = φ₂ :=
264 Classical.choose_spec (ExistsUnique.exists (hpo.2 (K := K) φ₁ φ₂ hφ))
266omit [IsTopologicalGroup G] [IsTopologicalGroup H]
267 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
268 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
269/-- Left composite of the chosen continuous pushout descent map.
270-/
271@[simp] theorem pushoutDescCont_left
272 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
273 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
274 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
275 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
276 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
277 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
278 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
279 (pushoutDescCont hpo φ₁ φ₂ hφ).comp α₁ = φ₁ :=
280 (pushoutDescCont_spec hpo φ₁ φ₂ hφ).1
282omit [IsTopologicalGroup G] [IsTopologicalGroup H]
283 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
284 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
285/-- Right composite of the chosen continuous pushout descent map.
286-/
287@[simp] theorem pushoutDescCont_right
288 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
289 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
290 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
291 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
292 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
293 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
294 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
295 (pushoutDescCont hpo φ₁ φ₂ hφ).comp α₂ = φ₂ :=
296 (pushoutDescCont_spec hpo φ₁ φ₂ hφ).2
298omit [IsTopologicalGroup G] [IsTopologicalGroup H]
299 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
300 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
301/-- Uniqueness of the chosen continuous pushout descent map. -/
302theorem pushoutDescCont_uniq
303 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
304 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
305 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
306 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
307 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
308 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
309 (hφ : φ₁.comp β₁ = φ₂.comp β₂)
310 {ψ : G →ₜ* K}
311 (hψ : ψ.comp α₁ = φ₁ ∧ ψ.comp α₂ = φ₂) :
312 ψ = pushoutDescCont hpo φ₁ φ₂ hφ :=
313 (hpo.2 (K := K) φ₁ φ₂ hφ).unique hψ
314 (pushoutDescCont_spec hpo φ₁ φ₂ hφ)
316omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
317/-- The distinguished map from a profinite pushout object to itself is the identity. -/
318@[simp 900] theorem pushoutDescCont_self
319 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
320 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
321 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
322 : pushoutDescCont hpo α₁ α₂ hpo.1 = ContinuousMonoidHom.id G := by
323 symm
324 exact
325 pushoutDescCont_uniq (K := G) hpo α₁ α₂ hpo.1
326 (ψ := ContinuousMonoidHom.id G) ⟨rfl, rfl⟩
328omit [IsTopologicalGroup G] [IsTopologicalGroup H]
329 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
330 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
331/-- Extensionality of continuous morphisms out of a profinite pushout object. -/
332theorem pushoutCont_hom_ext
333 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
334 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
335 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
336 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
337 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
338 {ψ ψ' : G →ₜ* K}
339 (h₁ : ψ.comp α₁ = ψ'.comp α₁)
340 (h₂ : ψ.comp α₂ = ψ'.comp α₂) :
341 ψ = ψ' := by
342 have hφ : (ψ.comp α₁).comp β₁ = (ψ.comp α₂).comp β₂ := by
343 ext x
344 exact congrArg ψ (DFunLike.congr_fun hpo.1 x)
345 have hψ :
346 ψ = pushoutDescCont hpo (ψ.comp α₁) (ψ.comp α₂) hφ := by
347 exact pushoutDescCont_uniq hpo (ψ.comp α₁) (ψ.comp α₂) hφ (ψ := ψ) ⟨rfl, rfl⟩
348 have hψ' :
349 ψ' = pushoutDescCont hpo (ψ.comp α₁) (ψ.comp α₂) hφ := by
350 exact pushoutDescCont_uniq hpo (ψ.comp α₁) (ψ.comp α₂) hφ
351 (ψ := ψ') ⟨h₁.symm, h₂.symm⟩
352 exact hψ.trans hψ'.symm
354/-- Canonical comparison map between two profinite pushout objects of the same cospan.
355-/
356noncomputable def pushoutContMapOfIsPushout
357 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
358 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
359 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
360 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
361 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
362 : G →ₜ* G' :=
363 pushoutDescCont hpo α₁' α₂' hpo'.1
365omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
366/-- The canonical comparison map from a profinite pushout object to itself is the identity. -/
367@[simp 900] theorem pushoutContMapOfIsPushout_self
368 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
369 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
370 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
371 : pushoutContMapOfIsPushout β₁ β₂ hpo hpo = ContinuousMonoidHom.id G := by
372 change pushoutDescCont hpo α₁ α₂ hpo.1 = ContinuousMonoidHom.id G
373 exact pushoutDescCont_self (hpo := hpo)
375omit [IsTopologicalGroup G] [IsTopologicalGroup H]
376 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
377 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
378/-- Left composite of the canonical comparison map between profinite pushout objects.
379-/
380@[simp 900] theorem pushoutContMapOfIsPushout_left
381 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
382 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
383 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
384 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
385 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
386 : (pushoutContMapOfIsPushout β₁ β₂ hpo hpo').comp α₁ = α₁' :=
387 by
388 change (pushoutDescCont hpo α₁' α₂' hpo'.1).comp α₁ = α₁'
389 exact pushoutDescCont_left hpo α₁' α₂' hpo'.1
391omit [IsTopologicalGroup G] [IsTopologicalGroup H]
392 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
393 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
394/-- Right composite of the canonical comparison map between profinite pushout objects.
395-/
396@[simp 900] theorem pushoutContMapOfIsPushout_right
397 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
398 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
399 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
400 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
401 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
402 : (pushoutContMapOfIsPushout β₁ β₂ hpo hpo').comp α₂ = α₂' :=
403 by
404 change (pushoutDescCont hpo α₁' α₂' hpo'.1).comp α₂ = α₂'
405 exact pushoutDescCont_right hpo α₁' α₂' hpo'.1
408omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
409/-- Any two profinite pushout objects of the same cospan are canonically bijective. -/
410theorem bijective_pushoutContMapOfIsPushout
411 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
412 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
413 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
414 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
415 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
416 : Function.Bijective (pushoutContMapOfIsPushout β₁ β₂ hpo hpo') := by
417 let φ : G →ₜ* G' := pushoutContMapOfIsPushout β₁ β₂ hpo hpo'
418 let ψ : G' →ₜ* G := pushoutContMapOfIsPushout β₁ β₂ hpo' hpo
419 have hleft : ψ.comp φ = ContinuousMonoidHom.id G := by
420 apply pushoutCont_hom_ext hpo
421 · calc
422 (ψ.comp φ).comp α₁ = ψ.comp (φ.comp α₁) := by rfl
423 _ = ψ.comp α₁' := by rw [pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo']
424 _ = α₁ := pushoutContMapOfIsPushout_left β₁ β₂ hpo' hpo
425 · calc
426 (ψ.comp φ).comp α₂ = ψ.comp (φ.comp α₂) := by rfl
427 _ = ψ.comp α₂' := by rw [pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo']
428 _ = α₂ := pushoutContMapOfIsPushout_right β₁ β₂ hpo' hpo
429 have hright : φ.comp ψ = ContinuousMonoidHom.id G' := by
430 apply pushoutCont_hom_ext hpo'
431 · calc
432 (φ.comp ψ).comp α₁' = φ.comp (ψ.comp α₁') := by rfl
433 _ = φ.comp α₁ := by rw [pushoutContMapOfIsPushout_left β₁ β₂ hpo' hpo]
434 _ = α₁' := pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo'
435 · calc
436 (φ.comp ψ).comp α₂' = φ.comp (ψ.comp α₂') := by rfl
437 _ = φ.comp α₂ := by rw [pushoutContMapOfIsPushout_right β₁ β₂ hpo' hpo]
438 _ = α₂' := pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo'
439 refine ⟨?_, ?_⟩
440 · intro x y hxy
441 have hx : ψ (φ x) = x := by
442 simpa [φ, ψ] using congrArg (fun f : G →ₜ* G => f x) hleft
443 have hy : ψ (φ y) = y := by
444 simpa [φ, ψ] using congrArg (fun f : G →ₜ* G => f y) hleft
445 calc
446 x = ψ (φ x) := hx.symm
447 _ = ψ (φ y) := by simpa [φ] using congrArg ψ hxy
448 _ = y := hy
449 · intro y
450 refine ⟨ψ y, ?_⟩
451 simpa [φ, ψ] using congrArg (fun f : G' →ₜ* G' => f y) hright
453/-- Canonical continuous multiplicative equivalence between two profinite pushout objects.
454-/
455noncomputable def pushoutContEquivOfIsPushout
456 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
457 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
458 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
459 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
460 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
461 : G ≃ₜ* G' := by
462 exact ContinuousMulEquiv.ofBijectiveCompactToT2
463 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo')
464 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo').continuous_toFun
465 (bijective_pushoutContMapOfIsPushout β₁ β₂ hpo hpo')
467omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
468/-- Left composite of the canonical continuous pushout equivalence.
469-/
470@[simp] theorem pushoutContEquivOfIsPushout_left
471 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
472 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
473 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
474 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
475 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
476 : ((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' : G →ₜ* G').comp α₁) = α₁' := by
477 change (pushoutContMapOfIsPushout β₁ β₂ hpo hpo').comp α₁ = α₁'
478 exact pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo'
480omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
481/-- Right composite of the canonical continuous pushout equivalence.
482-/
483@[simp] theorem pushoutContEquivOfIsPushout_right
484 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
485 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
486 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
487 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
488 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
489 : ((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' : G →ₜ* G').comp α₂) = α₂' := by
490 change (pushoutContMapOfIsPushout β₁ β₂ hpo hpo').comp α₂ = α₂'
491 exact pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo'
493omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
494/-- Left-leg formula for the inverse profinite pushout comparison equivalence. -/
495@[simp 900] theorem pushoutContEquivOfIsPushout_symm_left
496 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
497 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
498 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
499 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
500 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
501 : (((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo').symm : G' →ₜ* G).comp α₁') = α₁ := by
502 ext x
503 let e := pushoutContEquivOfIsPushout β₁ β₂ hpo hpo'
504 exact e.injective <| by
505 calc
506 e ((((e.symm : G' →ₜ* G).comp α₁') x)) = α₁' x := by
507 change e (e.symm (α₁' x)) = α₁' x
508 simp only [ContinuousMulEquiv.apply_symm_apply]
509 _ = e (α₁ x) := by
510 have hleft :
511 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo').comp α₁ = α₁' :=
512 pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo'
513 have hleft_apply :
514 pushoutContMapOfIsPushout β₁ β₂ hpo hpo' (α₁ x) = α₁' x := by
515 exact congrFun (congrArg (fun f : H₁ →ₜ* G' => (f : H₁ → G')) hleft) x
516 change α₁' x = pushoutContMapOfIsPushout β₁ β₂ hpo hpo' (α₁ x)
517 simpa using hleft_apply.symm
519omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
520/-- Right-leg formula for the inverse profinite pushout comparison equivalence. -/
521@[simp 900] theorem pushoutContEquivOfIsPushout_symm_right
522 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
523 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
524 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
525 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
526 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
527 : (((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo').symm : G' →ₜ* G).comp α₂') = α₂ := by
528 ext x
529 let e := pushoutContEquivOfIsPushout β₁ β₂ hpo hpo'
530 exact e.injective <| by
531 calc
532 e ((((e.symm : G' →ₜ* G).comp α₂') x)) = α₂' x := by
533 change e (e.symm (α₂' x)) = α₂' x
534 simp only [ContinuousMulEquiv.apply_symm_apply]
535 _ = e (α₂ x) := by
536 have hright :
537 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo').comp α₂ = α₂' :=
538 pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo'
539 have hright_apply :
540 pushoutContMapOfIsPushout β₁ β₂ hpo hpo' (α₂ x) = α₂' x := by
541 exact congrFun (congrArg (fun f : H₂ →ₜ* G' => (f : H₂ → G')) hright) x
542 change α₂' x = pushoutContMapOfIsPushout β₁ β₂ hpo hpo' (α₂ x)
543 simpa using hright_apply.symm
545end
548end ProCGroups.Categorical