Yamaguchi Lean 4 Library
ProCGroups/Categorical/PushoutSquares.lean
ProCGroups/Categorical/PushoutSquares/Source

ProCGroups/Categorical/PushoutSquares.lean

1import Mathlib.GroupTheory.Coprod.Basic
2import ProCGroups.Profinite.Basic
3import ProCGroups.Topologies.ContinuousMulEquiv
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/Categorical/PushoutSquares.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pullbacks, pushouts, and quotient comparison
16Concrete algebraic and topological pullbacks and pushouts of groups and profinite groups, with comparison maps, universal properties, kernel criteria, and quotient pullback equivalences.
17-/
19namespace ProCGroups.Categorical
21open scoped Monoid.Coprod
23universe u v
25section
27variable {G G' H H₁ H₂ : Type u}
28variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
30/-- The abstract free product used as the carrier before imposing pushout relations. -/
31abbrev PushoutFreeProduct (H₁ H₂ : Type u) [Group H₁] [Group H₂] :=
32 Monoid.Coprod H₁ H₂
34/-- The relators identifying the two legs of a group cospan inside the free product. -/
35def pushoutRelators (β₁ : H →* H₁) (β₂ : H →* H₂) :
36 Set (PushoutFreeProduct H₁ H₂) :=
37 {z | ∃ h : H,
38 z = (Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂)⁻¹ *
39 (Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂)}
41/-- The normal subgroup generated by the cospan-identifying relators. -/
42def pushoutNormalClosure (β₁ : H →* H₁) (β₂ : H →* H₂) :
43 Subgroup (PushoutFreeProduct H₁ H₂) :=
44 Subgroup.normalClosure (pushoutRelators β₁ β₂)
46/-- The relator closure used in the concrete pushout is normal. -/
47instance pushoutNormalClosure_normal (β₁ : H →* H₁) (β₂ : H →* H₂) :
48 (pushoutNormalClosure β₁ β₂).Normal :=
49 Subgroup.normalClosure_normal
51namespace AlgebraicPushout
53/-- Algebraic group pushout carrier: the free product modulo the normal closure of
54`inl (β₁ h)⁻¹ * inr (β₂ h)`. -/
55abbrev Carrier (β₁ : H →* H₁) (β₂ : H →* H₂) :=
56 PushoutFreeProduct H₁ H₂ ⧸ pushoutNormalClosure β₁ β₂
58/-- The left structural map into the algebraic pushout. -/
59def inl (β₁ : H →* H₁) (β₂ : H →* H₂) :
60 H₁ →* Carrier β₁ β₂ :=
61 (QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)).comp Monoid.Coprod.inl
63/-- The right structural map into the algebraic pushout. -/
64def inr (β₁ : H →* H₁) (β₂ : H →* H₂) :
65 H₂ →* Carrier β₁ β₂ :=
66 (QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)).comp Monoid.Coprod.inr
68/-- The algebraic pushout maps coequalize the original cospan. -/
70 (β₁ : H →* H₁) (β₂ : H →* H₂) :
71 (inl β₁ β₂).comp β₁ = (inr β₁ β₂).comp β₂ := by
72 ext h
73 change QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
74 (Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂) =
75 QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
76 (Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂)
77 apply QuotientGroup.eq.2
78 exact Subgroup.subset_normalClosure ⟨h, rfl⟩
80/-- The algebraic pushout descent map. -/
81noncomputable def concretePushoutDesc
82 (β₁ : H →* H₁) (β₂ : H →* H₂)
83 {K : Type u} [Group K]
84 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
85 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
86 Carrier β₁ β₂ →* K :=
87 let F : PushoutFreeProduct H₁ H₂ →* K := Monoid.Coprod.lift φ₁ φ₂
88 QuotientGroup.lift (pushoutNormalClosure β₁ β₂) F <| by
89 refine Subgroup.normalClosure_le_normal ?_
90 rintro z ⟨h, rfl⟩
91 change F ((Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂)⁻¹ *
92 (Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂)) = 1
93 rw [map_mul, map_inv]
94 have hleft :
95 F (Monoid.Coprod.inl (β₁ h) : PushoutFreeProduct H₁ H₂) = φ₁ (β₁ h) :=
96 DFunLike.congr_fun (Monoid.Coprod.lift_comp_inl φ₁ φ₂) (β₁ h)
97 have hright :
98 F (Monoid.Coprod.inr (β₂ h) : PushoutFreeProduct H₁ H₂) = φ₂ (β₂ h) :=
99 DFunLike.congr_fun (Monoid.Coprod.lift_comp_inr φ₁ φ₂) (β₂ h)
100 have hcomp : φ₁ (β₁ h) = φ₂ (β₂ h) := DFunLike.congr_fun hφ h
101 rw [hleft, hright, hcomp]
102 simp only [inv_mul_cancel]
104@[simp 900] theorem concretePushoutDesc_inl
105 (β₁ : H →* H₁) (β₂ : H →* H₂)
106 {K : Type u} [Group K]
107 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
108 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
109 (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inl β₁ β₂) = φ₁ := by
110 ext x
111 change concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ
112 (QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
113 (Monoid.Coprod.inl x : PushoutFreeProduct H₁ H₂)) = φ₁ x
114 simp only [concretePushoutDesc, QuotientGroup.mk'_apply, QuotientGroup.lift_mk, Monoid.Coprod.lift_apply_inl]
116@[simp 900] theorem concretePushoutDesc_inr
117 (β₁ : H →* H₁) (β₂ : H →* H₂)
118 {K : Type u} [Group K]
119 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
120 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
121 (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inr β₁ β₂) = φ₂ := by
122 ext x
123 change concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ
124 (QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
125 (Monoid.Coprod.inr x : PushoutFreeProduct H₁ H₂)) = φ₂ x
126 simp only [concretePushoutDesc, QuotientGroup.mk'_apply, QuotientGroup.lift_mk, Monoid.Coprod.lift_apply_inr]
128end AlgebraicPushout
130/-- Pushout squares in the category of groups.
131-/
132def IsPushoutSquare (β₁ : H →* H₁) (β₂ : H →* H₂)
133 (α₁ : H₁ →* G) (α₂ : H₂ →* G) : Prop :=
134 α₁.comp β₁ = α₂.comp β₂ ∧
135 ∀ ⦃K : Type u⦄ [Group K] (φ₁ : H₁ →* K) (φ₂ : H₂ →* K),
136 φ₁.comp β₁ = φ₂.comp β₂ →
137 ∃! φ : G →* K, φ.comp α₁ = φ₁ ∧ φ.comp α₂ = φ₂
139namespace AlgebraicPushout
141/-- The algebraic pushout carrier satisfies the ordinary group pushout universal property. -/
142theorem concretePushout_isPushoutSquare (β₁ : H →* H₁) (β₂ : H →* H₂) :
143 IsPushoutSquare β₁ β₂ (inl β₁ β₂) (inr β₁ β₂) := by
144 refine ⟨inl_comp_eq_inr_comp β₁ β₂, ?_⟩
145 intro K _ φ₁ φ₂ hφ
146 refine ⟨concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ, ⟨concretePushoutDesc_inl β₁ β₂ φ₁ φ₂ hφ,
147 concretePushoutDesc_inr β₁ β₂ φ₁ φ₂ hφ⟩, ?_⟩
148 intro ψ hψ
149 let q : PushoutFreeProduct H₁ H₂ →* Carrier β₁ β₂ :=
150 QuotientGroup.mk' (pushoutNormalClosure β₁ β₂)
151 let F : PushoutFreeProduct H₁ H₂ →* K := Monoid.Coprod.lift φ₁ φ₂
152 have hψq : ψ.comp q = F := by
153 apply Monoid.Coprod.hom_ext
154 · calc
155 (ψ.comp q).comp Monoid.Coprod.inl = ψ.comp (inl β₁ β₂) := rfl
156 _ = φ₁ := hψ.1
157 _ = F.comp Monoid.Coprod.inl := (Monoid.Coprod.lift_comp_inl φ₁ φ₂).symm
158 · calc
159 (ψ.comp q).comp Monoid.Coprod.inr = ψ.comp (inr β₁ β₂) := rfl
160 _ = φ₂ := hψ.2
161 _ = F.comp Monoid.Coprod.inr := (Monoid.Coprod.lift_comp_inr φ₁ φ₂).symm
162 have hdescq : (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp q = F := by
163 apply Monoid.Coprod.hom_ext
164 · calc
165 ((concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp q).comp Monoid.Coprod.inl =
166 (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inl β₁ β₂) := rfl
167 _ = φ₁ := concretePushoutDesc_inl β₁ β₂ φ₁ φ₂ hφ
168 _ = F.comp Monoid.Coprod.inl := (Monoid.Coprod.lift_comp_inl φ₁ φ₂).symm
169 · calc
170 ((concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp q).comp Monoid.Coprod.inr =
171 (concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ).comp (inr β₁ β₂) := rfl
172 _ = φ₂ := concretePushoutDesc_inr β₁ β₂ φ₁ φ₂ hφ
173 _ = F.comp Monoid.Coprod.inr := (Monoid.Coprod.lift_comp_inr φ₁ φ₂).symm
174 apply MonoidHom.ext
175 intro y
176 rcases QuotientGroup.mk'_surjective (pushoutNormalClosure β₁ β₂) y with ⟨z, rfl⟩
177 change ψ (q z) = concretePushoutDesc β₁ β₂ φ₁ φ₂ hφ (q z)
178 exact congrArg (fun f : PushoutFreeProduct H₁ H₂ →* K => f z)
179 (hψq.trans hdescq.symm)
181end AlgebraicPushout
183/-- Chosen morphism induced by the pushout universal property.
184-/
185noncomputable def pushoutDesc
186 {β₁ : H →* H₁} {β₂ : H →* H₂}
187 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
188 {K : Type u} [Group K]
189 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
190 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
191 (hφ : φ₁.comp β₁ = φ₂.comp β₂) : G →* K :=
192 Classical.choose (ExistsUnique.exists (hpo.2 φ₁ φ₂ hφ))
194/-- The chosen pushout descent map has the prescribed left and right composites.
195-/
196theorem pushoutDesc_spec
197 {β₁ : H →* H₁} {β₂ : H →* H₂}
198 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
199 {K : Type u} [Group K]
200 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
201 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
202 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
203 (pushoutDesc hpo φ₁ φ₂ hφ).comp α₁ = φ₁ ∧
204 (pushoutDesc hpo φ₁ φ₂ hφ).comp α₂ = φ₂ :=
205 Classical.choose_spec (ExistsUnique.exists (hpo.2 φ₁ φ₂ hφ))
207/-- Left composite of the chosen pushout descent map.
208-/
209@[simp] theorem pushoutDesc_left
210 {β₁ : H →* H₁} {β₂ : H →* H₂}
211 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
212 {K : Type u} [Group K]
213 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
214 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
215 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
216 (pushoutDesc hpo φ₁ φ₂ hφ).comp α₁ = φ₁ :=
217 (pushoutDesc_spec hpo φ₁ φ₂ hφ).1
219/-- Right composite of the chosen pushout descent map.
220-/
221@[simp] theorem pushoutDesc_right
222 {β₁ : H →* H₁} {β₂ : H →* H₂}
223 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
224 {K : Type u} [Group K]
225 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
226 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
227 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
228 (pushoutDesc hpo φ₁ φ₂ hφ).comp α₂ = φ₂ :=
229 (pushoutDesc_spec hpo φ₁ φ₂ hφ).2
231/-- Uniqueness of the chosen pushout descent map.
232-/
234 {β₁ : H →* H₁} {β₂ : H →* H₂}
235 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
236 {K : Type u} [Group K]
237 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
238 (φ₁ : H₁ →* K) (φ₂ : H₂ →* K)
239 (hφ : φ₁.comp β₁ = φ₂.comp β₂)
240 {ψ : G →* K}
241 (hψ : ψ.comp α₁ = φ₁ ∧ ψ.comp α₂ = φ₂) :
242 ψ = pushoutDesc hpo φ₁ φ₂ hφ := by
243 rcases hpo.2 φ₁ φ₂ hφ with ⟨u, hu, huuniq⟩
244 have hψ' : ψ = u := huuniq _ hψ
245 have hdesc : pushoutDesc hpo φ₁ φ₂ hφ = u :=
246 huuniq _ (pushoutDesc_spec hpo φ₁ φ₂ hφ)
247 exact hψ'.trans hdesc.symm
249/-- The distinguished map from a pushout object to itself is the identity.
250-/
251@[simp] theorem pushoutDesc_self
252 {β₁ : H →* H₁} {β₂ : H →* H₂}
253 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
254 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂) :
255 pushoutDesc hpo α₁ α₂ hpo.1 = MonoidHom.id G := by
256 symm
257 exact pushoutDesc_uniq hpo α₁ α₂ hpo.1 (ψ := MonoidHom.id G) (by simp only [MonoidHom.CompTriple.comp_eq, and_self])
259/-- Extensionality of morphisms out of a pushout object.
260-/
261theorem pushout_hom_ext
262 {β₁ : H →* H₁} {β₂ : H →* H₂}
263 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
264 {K : Type u} [Group K]
265 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
266 {ψ ψ' : G →* K}
267 (h₁ : ψ.comp α₁ = ψ'.comp α₁)
268 (h₂ : ψ.comp α₂ = ψ'.comp α₂) :
269 ψ = ψ' := by
270 have hφ : (ψ.comp α₁).comp β₁ = (ψ.comp α₂).comp β₂ := by
271 simpa using congrArg (fun f : H →* G => ψ.comp f) hpo.1
272 have hψ :
273 ψ = pushoutDesc hpo (ψ.comp α₁) (ψ.comp α₂) hφ := by
274 exact pushoutDesc_uniq hpo (ψ.comp α₁) (ψ.comp α₂) hφ (ψ := ψ) ⟨rfl, rfl⟩
275 have hψ' :
276 ψ' = pushoutDesc hpo (ψ.comp α₁) (ψ.comp α₂) hφ := by
277 exact pushoutDesc_uniq hpo (ψ.comp α₁) (ψ.comp α₂) hφ (ψ := ψ') ⟨h₁.symm, h₂.symm⟩
278 exact hψ.trans hψ'.symm
280/-- Canonical comparison map between two pushout objects of the same cospan.
281-/
282noncomputable def pushoutMapOfIsPushout
283 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
284 {α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
285 (β₁ : H →* H₁) (β₂ : H →* H₂)
286 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
287 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
288 G →* G' :=
289 pushoutDesc hpo α₁' α₂' hpo'.1
291/-- The canonical comparison map from a pushout object to itself is the identity.
292-/
293@[simp 900] theorem pushoutMapOfIsPushout_self
294 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
295 (β₁ : H →* H₁) (β₂ : H →* H₂)
296 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂) :
297 pushoutMapOfIsPushout β₁ β₂ hpo hpo = MonoidHom.id G := by
298 change pushoutDesc hpo α₁ α₂ hpo.1 = MonoidHom.id G
299 exact pushoutDesc_self (hpo := hpo)
301/-- Left composite of the canonical comparison map between pushout objects.
302-/
303@[simp 900] theorem pushoutMapOfIsPushout_left
304 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
305 {α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
306 (β₁ : H →* H₁) (β₂ : H →* H₂)
307 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
308 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
309 (pushoutMapOfIsPushout β₁ β₂ hpo hpo').comp α₁ = α₁' :=
310 by
311 change (pushoutDesc hpo α₁' α₂' hpo'.1).comp α₁ = α₁'
312 exact pushoutDesc_left hpo α₁' α₂' hpo'.1
314/-- Right composite of the canonical comparison map between pushout objects.
315-/
316@[simp 900] theorem pushoutMapOfIsPushout_right
317 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
318 {α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
319 (β₁ : H →* H₁) (β₂ : H →* H₂)
320 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
321 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
322 (pushoutMapOfIsPushout β₁ β₂ hpo hpo').comp α₂ = α₂' :=
323 by
324 change (pushoutDesc hpo α₁' α₂' hpo'.1).comp α₂ = α₂'
325 exact pushoutDesc_right hpo α₁' α₂' hpo'.1
328/-- Any two pushout objects of the same cospan are canonically isomorphic.
329-/
331 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
332 {α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
333 (β₁ : H →* H₁) (β₂ : H →* H₂)
334 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
335 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
336 Function.Bijective (pushoutMapOfIsPushout β₁ β₂ hpo hpo') := by
337 let φ : G →* G' := pushoutMapOfIsPushout β₁ β₂ hpo hpo'
338 let ψ : G' →* G := pushoutMapOfIsPushout β₁ β₂ hpo' hpo
339 have hleft : ψ.comp φ = MonoidHom.id G := by
340 apply pushout_hom_ext hpo
341 · calc
342 (ψ.comp φ).comp α₁ = ψ.comp (φ.comp α₁) := by rfl
343 _ = ψ.comp α₁' := by rw [pushoutMapOfIsPushout_left β₁ β₂ hpo hpo']
344 _ = α₁ := pushoutMapOfIsPushout_left β₁ β₂ hpo' hpo
345 · calc
346 (ψ.comp φ).comp α₂ = ψ.comp (φ.comp α₂) := by rfl
347 _ = ψ.comp α₂' := by rw [pushoutMapOfIsPushout_right β₁ β₂ hpo hpo']
348 _ = α₂ := pushoutMapOfIsPushout_right β₁ β₂ hpo' hpo
349 have hright : φ.comp ψ = MonoidHom.id G' := by
350 apply pushout_hom_ext hpo'
351 · calc
352 (φ.comp ψ).comp α₁' = φ.comp (ψ.comp α₁') := by rfl
353 _ = φ.comp α₁ := by rw [pushoutMapOfIsPushout_left β₁ β₂ hpo' hpo]
354 _ = α₁' := pushoutMapOfIsPushout_left β₁ β₂ hpo hpo'
355 · calc
356 (φ.comp ψ).comp α₂' = φ.comp (ψ.comp α₂') := by rfl
357 _ = φ.comp α₂ := by rw [pushoutMapOfIsPushout_right β₁ β₂ hpo' hpo]
358 _ = α₂' := pushoutMapOfIsPushout_right β₁ β₂ hpo hpo'
359 refine ⟨?_, ?_⟩
360 · intro x y hxy
361 have hx : ψ (φ x) = x := by
362 simpa [φ, ψ] using congrArg (fun f : G →* G => f x) hleft
363 have hy : ψ (φ y) = y := by
364 simpa [φ, ψ] using congrArg (fun f : G →* G => f y) hleft
365 calc
366 x = ψ (φ x) := hx.symm
367 _ = ψ (φ y) := by simpa [φ] using congrArg ψ hxy
368 _ = y := hy
369 · intro y
370 refine ⟨ψ y, ?_⟩
371 simpa [φ, ψ] using congrArg (fun f : G' →* G' => f y) hright
373/-- Canonical multiplicative equivalence between two pushout objects of the same cospan.
374-/
375noncomputable def pushoutEquivOfIsPushout
376 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
377 {α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
378 (β₁ : H →* H₁) (β₂ : H →* H₂)
379 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
380 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
381 G ≃* G' :=
382 MulEquiv.ofBijective
383 (pushoutMapOfIsPushout β₁ β₂ hpo hpo')
384 (bijective_pushoutMapOfIsPushout β₁ β₂ hpo hpo')
386/-- Left composite of the canonical pushout equivalence.
387-/
389 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
390 {α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
391 (β₁ : H →* H₁) (β₂ : H →* H₂)
392 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
393 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
394 (pushoutEquivOfIsPushout β₁ β₂ hpo hpo').toMonoidHom.comp α₁ = α₁' := by
395 change (pushoutMapOfIsPushout β₁ β₂ hpo hpo').comp α₁ = α₁'
396 exact pushoutMapOfIsPushout_left β₁ β₂ hpo hpo'
398/-- Right composite of the canonical pushout equivalence.
399-/
401 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
402 {α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
403 (β₁ : H →* H₁) (β₂ : H →* H₂)
404 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
405 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
406 (pushoutEquivOfIsPushout β₁ β₂ hpo hpo').toMonoidHom.comp α₂ = α₂' := by
407 change (pushoutMapOfIsPushout β₁ β₂ hpo hpo').comp α₂ = α₂'
408 exact pushoutMapOfIsPushout_right β₁ β₂ hpo hpo'
410end
412section
414variable {G G' H H₁ H₂ : Type u}
415variable [Group G] [Group G'] [Group H] [Group H₁] [Group H₂]
416variable [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
417variable [TopologicalSpace H₁] [TopologicalSpace H₂]
418variable [IsTopologicalGroup G] [IsTopologicalGroup G'] [IsTopologicalGroup H]
419variable [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
421namespace TopologicalPushout
423/-- Continuous pushout property tested by all topological-group target objects. -/
424def HasTopologicalPushoutProperty (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
425 (α₁ : H₁ →ₜ* G) (α₂ : H₂ →ₜ* G) : Prop :=
426 α₁.comp β₁ = α₂.comp β₂ ∧
427 ∀ ⦃K : Type u⦄ [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
428 ∀ (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K),
429 φ₁.comp β₁ = φ₂.comp β₂ →
430 ∃! φ : G →ₜ* K, φ.comp α₁ = φ₁ ∧ φ.comp α₂ = φ₂
432end TopologicalPushout
434/-- Continuous pushout property tested by profinite target objects.
436This definition does not assert that the four objects in the square are themselves profinite. -/
437def HasProfiniteTestPushoutProperty (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
438 (α₁ : H₁ →ₜ* G) (α₂ : H₂ →ₜ* G) : Prop :=
439 α₁.comp β₁ = α₂.comp β₂ ∧
440 ∀ ⦃K : Type u⦄ [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
442 ∀ (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K),
443 φ₁.comp β₁ = φ₂.comp β₂ →
444 ∃! φ : G →ₜ* K, φ.comp α₁ = φ₁ ∧ φ.comp α₂ = φ₂
446/-- A genuine profinite pushout square: all four objects are profinite, and the square has the
447continuous universal property tested by profinite target objects. -/
448structure IsProfinitePushoutSquare (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
449 (α₁ : H₁ →ₜ* G) (α₂ : H₂ →ₜ* G) : Prop where
450 source_profinite : IsProfiniteGroup H
451 left_profinite : IsProfiniteGroup H₁
452 right_profinite : IsProfiniteGroup H₂
453 pushout_profinite : IsProfiniteGroup G
454 property : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂
456/-- Chosen continuous morphism induced by the profinite pushout universal property.
457-/
458noncomputable def pushoutDescCont
459 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
460 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
461 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
462 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
464 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
465 (hφ : φ₁.comp β₁ = φ₂.comp β₂) : G →ₜ* K :=
466 Classical.choose (ExistsUnique.exists (hpo.2 (K := K) hK φ₁ φ₂ hφ))
468omit [IsTopologicalGroup G] [IsTopologicalGroup H]
469 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
470/-- Specification of the chosen continuous pushout descent map.
471-/
473 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
474 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
475 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
476 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
478 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
479 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
480 (pushoutDescCont hpo hK φ₁ φ₂ hφ).comp α₁ = φ₁ ∧
481 (pushoutDescCont hpo hK φ₁ φ₂ hφ).comp α₂ = φ₂ :=
482 Classical.choose_spec (ExistsUnique.exists (hpo.2 (K := K) hK φ₁ φ₂ hφ))
484omit [IsTopologicalGroup G] [IsTopologicalGroup H]
485 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
486/-- Left composite of the chosen continuous pushout descent map.
487-/
488@[simp] theorem pushoutDescCont_left
489 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
490 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
491 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
492 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
494 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
495 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
496 (pushoutDescCont hpo hK φ₁ φ₂ hφ).comp α₁ = φ₁ :=
497 (pushoutDescCont_spec hpo hK φ₁ φ₂ hφ).1
499omit [IsTopologicalGroup G] [IsTopologicalGroup H]
500 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
501/-- Right composite of the chosen continuous pushout descent map.
502-/
503@[simp] theorem pushoutDescCont_right
504 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
505 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
506 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
507 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
509 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
510 (hφ : φ₁.comp β₁ = φ₂.comp β₂) :
511 (pushoutDescCont hpo hK φ₁ φ₂ hφ).comp α₂ = φ₂ :=
512 (pushoutDescCont_spec hpo hK φ₁ φ₂ hφ).2
514omit [IsTopologicalGroup G] [IsTopologicalGroup H]
515 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
516/-- Uniqueness of the chosen continuous pushout descent map.
517-/
519 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
520 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
521 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
522 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
524 (φ₁ : H₁ →ₜ* K) (φ₂ : H₂ →ₜ* K)
525 (hφ : φ₁.comp β₁ = φ₂.comp β₂)
526 {ψ : G →ₜ* K}
527 (hψ : ψ.comp α₁ = φ₁ ∧ ψ.comp α₂ = φ₂) :
528 ψ = pushoutDescCont hpo hK φ₁ φ₂ hφ := by
529 rcases hpo.2 (K := K) hK φ₁ φ₂ hφ with ⟨u, hu, huuniq⟩
530 have hψ' : ψ = u := huuniq _ hψ
531 have hdesc : pushoutDescCont hpo hK φ₁ φ₂ hφ = u :=
532 huuniq _ (pushoutDescCont_spec hpo hK φ₁ φ₂ hφ)
533 exact hψ'.trans hdesc.symm
535omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
536/-- The distinguished map from a profinite pushout object to itself is the identity.
537-/
538@[simp 900] theorem pushoutDescCont_self
539 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
540 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
541 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
543 pushoutDescCont hpo hG α₁ α₂ hpo.1 = ContinuousMonoidHom.id G := by
544 symm
545 exact
546 pushoutDescCont_uniq (K := G) hpo hG α₁ α₂ hpo.1
547 (ψ := ContinuousMonoidHom.id G) ⟨rfl, rfl⟩
549omit [IsTopologicalGroup G] [IsTopologicalGroup H]
550 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
551/-- Extensionality of continuous morphisms out of a profinite pushout object.
552-/
554 {β₁ : H →ₜ* H₁} {β₂ : H →ₜ* H₂}
555 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
556 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
557 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
558 {ψ ψ' : G →ₜ* K}
560 (h₁ : ψ.comp α₁ = ψ'.comp α₁)
561 (h₂ : ψ.comp α₂ = ψ'.comp α₂) :
562 ψ = ψ' := by
563 have hφ : (ψ.comp α₁).comp β₁ = (ψ.comp α₂).comp β₂ := by
564 simpa using congrArg (fun f : H →ₜ* G => ψ.comp f) hpo.1
565 have hψ :
566 ψ = pushoutDescCont hpo hK (ψ.comp α₁) (ψ.comp α₂) hφ := by
567 exact pushoutDescCont_uniq hpo hK (ψ.comp α₁) (ψ.comp α₂) hφ (ψ := ψ) ⟨rfl, rfl⟩
568 have hψ' :
569 ψ' = pushoutDescCont hpo hK (ψ.comp α₁) (ψ.comp α₂) hφ := by
570 exact pushoutDescCont_uniq hpo hK (ψ.comp α₁) (ψ.comp α₂) hφ
571 (ψ := ψ') ⟨h₁.symm, h₂.symm⟩
572 exact hψ.trans hψ'.symm
574/-- Canonical comparison map between two profinite pushout objects of the same cospan.
575-/
577 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
578 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
579 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
580 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
581 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
582 (hG' : IsProfiniteGroup G') :
583 G →ₜ* G' :=
584 pushoutDescCont hpo hG' α₁' α₂' hpo'.1
586omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
587/-- The canonical comparison map from a profinite pushout object to itself is the identity.
588-/
590 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
591 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
592 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
594 pushoutContMapOfIsPushout β₁ β₂ hpo hpo hG = ContinuousMonoidHom.id G := by
595 change pushoutDescCont hpo hG α₁ α₂ hpo.1 = ContinuousMonoidHom.id G
596 exact pushoutDescCont_self (hpo := hpo) (hG := hG)
598omit [IsTopologicalGroup G] [IsTopologicalGroup H]
599 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
600/-- Left composite of the canonical comparison map between profinite pushout objects.
601-/
603 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
604 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
605 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
606 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
607 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
608 (hG' : IsProfiniteGroup G') :
609 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₁ = α₁' :=
610 by
611 change (pushoutDescCont hpo hG' α₁' α₂' hpo'.1).comp α₁ = α₁'
612 exact pushoutDescCont_left hpo hG' α₁' α₂' hpo'.1
614omit [IsTopologicalGroup G] [IsTopologicalGroup H]
615 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
616/-- Right composite of the canonical comparison map between profinite pushout objects.
617-/
619 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
620 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
621 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
622 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
623 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
624 (hG' : IsProfiniteGroup G') :
625 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₂ = α₂' :=
626 by
627 change (pushoutDescCont hpo hG' α₁' α₂' hpo'.1).comp α₂ = α₂'
628 exact pushoutDescCont_right hpo hG' α₁' α₂' hpo'.1
631omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
632/-- Any two profinite pushout objects of the same cospan are canonically bijective.
633-/
635 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
636 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
637 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
638 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
639 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
640 (hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
641 Function.Bijective (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG') := by
642 let φ : G →ₜ* G' := pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG'
643 let ψ : G' →ₜ* G := pushoutContMapOfIsPushout β₁ β₂ hpo' hpo hG
644 have hleft : ψ.comp φ = ContinuousMonoidHom.id G := by
646 · calc
647 (ψ.comp φ).comp α₁ = ψ.comp (φ.comp α₁) := by rfl
648 _ = ψ.comp α₁' := by rw [pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo' hG']
649 _ = α₁ := pushoutContMapOfIsPushout_left β₁ β₂ hpo' hpo hG
650 · calc
651 (ψ.comp φ).comp α₂ = ψ.comp (φ.comp α₂) := by rfl
652 _ = ψ.comp α₂' := by rw [pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo' hG']
653 _ = α₂ := pushoutContMapOfIsPushout_right β₁ β₂ hpo' hpo hG
654 have hright : φ.comp ψ = ContinuousMonoidHom.id G' := by
655 apply pushoutCont_hom_ext hpo' hG'
656 · calc
657 (φ.comp ψ).comp α₁' = φ.comp (ψ.comp α₁') := by rfl
658 _ = φ.comp α₁ := by rw [pushoutContMapOfIsPushout_left β₁ β₂ hpo' hpo hG]
659 _ = α₁' := pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo' hG'
660 · calc
661 (φ.comp ψ).comp α₂' = φ.comp (ψ.comp α₂') := by rfl
662 _ = φ.comp α₂ := by rw [pushoutContMapOfIsPushout_right β₁ β₂ hpo' hpo hG]
663 _ = α₂' := pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo' hG'
664 refine ⟨?_, ?_⟩
665 · intro x y hxy
666 have hx : ψ (φ x) = x := by
667 simpa [φ, ψ] using congrArg (fun f : G →ₜ* G => f x) hleft
668 have hy : ψ (φ y) = y := by
669 simpa [φ, ψ] using congrArg (fun f : G →ₜ* G => f y) hleft
670 calc
671 x = ψ (φ x) := hx.symm
672 _ = ψ (φ y) := by simpa [φ] using congrArg ψ hxy
673 _ = y := hy
674 · intro y
675 refine ⟨ψ y, ?_⟩
676 simpa [φ, ψ] using congrArg (fun f : G' →ₜ* G' => f y) hright
678/-- Canonical continuous multiplicative equivalence between two profinite pushout objects.
679-/
681 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
682 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
683 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
684 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
685 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
686 (hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
687 G ≃ₜ* G' := by
688 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
689 letI : T2Space G' := IsProfiniteGroup.t2Space hG'
690 exact ContinuousMulEquiv.ofBijectiveCompactToT2
691 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG')
692 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').continuous_toFun
693 (bijective_pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG hG')
695omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
696/-- Left composite of the canonical continuous pushout equivalence.
697-/
699 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
700 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
701 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
702 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
703 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
704 (hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
705 ((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG' : G →ₜ* G').comp α₁) = α₁' := by
706 change (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₁ = α₁'
707 exact pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo' hG'
709omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
710/-- Right composite of the canonical continuous pushout equivalence.
711-/
713 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
714 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
715 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
716 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
717 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
718 (hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
719 ((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG' : G →ₜ* G').comp α₂) = α₂' := by
720 change (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₂ = α₂'
721 exact pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo' hG'
723omit [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
724 [TopologicalSpace H₁] [TopologicalSpace H₂] [IsTopologicalGroup G]
725 [IsTopologicalGroup G'] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
726 [IsTopologicalGroup H₂] in
727/-- Left-leg formula for the inverse pushout comparison equivalence. -/
729 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
730 {α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
731 (β₁ : H →* H₁) (β₂ : H →* H₂)
732 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
733 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
734 (pushoutEquivOfIsPushout β₁ β₂ hpo hpo').symm.toMonoidHom.comp α₁' = α₁ := by
735 ext x
736 let e := pushoutEquivOfIsPushout β₁ β₂ hpo hpo'
737 exact e.injective <| by
738 calc
739 e ((e.symm.toMonoidHom.comp α₁') x) = α₁' x := by
740 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.comp_apply, MonoidHom.coe_coe, MulEquiv.apply_symm_apply]
741 _ = e (α₁ x) := by
742 simpa using
743 (congrArg (fun f : H₁ →* G' => f x)
744 (pushoutEquivOfIsPushout_left β₁ β₂ hpo hpo')).symm
746omit [TopologicalSpace G] [TopologicalSpace G'] [TopologicalSpace H]
747 [TopologicalSpace H₁] [TopologicalSpace H₂] [IsTopologicalGroup G]
748 [IsTopologicalGroup G'] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
749 [IsTopologicalGroup H₂] in
750/-- Right-leg formula for the inverse pushout comparison equivalence. -/
752 {α₁ : H₁ →* G} {α₂ : H₂ →* G}
753 {α₁' : H₁ →* G'} {α₂' : H₂ →* G'}
754 (β₁ : H →* H₁) (β₂ : H →* H₂)
755 (hpo : IsPushoutSquare β₁ β₂ α₁ α₂)
756 (hpo' : IsPushoutSquare β₁ β₂ α₁' α₂') :
757 (pushoutEquivOfIsPushout β₁ β₂ hpo hpo').symm.toMonoidHom.comp α₂' = α₂ := by
758 ext x
759 let e := pushoutEquivOfIsPushout β₁ β₂ hpo hpo'
760 exact e.injective <| by
761 calc
762 e ((e.symm.toMonoidHom.comp α₂') x) = α₂' x := by
763 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.comp_apply, MonoidHom.coe_coe, MulEquiv.apply_symm_apply]
764 _ = e (α₂ x) := by
765 simpa using
766 (congrArg (fun f : H₂ →* G' => f x)
767 (pushoutEquivOfIsPushout_right β₁ β₂ hpo hpo')).symm
769omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
770/-- Left-leg formula for the inverse profinite pushout comparison equivalence. -/
772 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
773 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
774 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
775 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
776 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
777 (hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
778 (((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG').symm : G' →ₜ* G).comp α₁') = α₁ := by
779 ext x
780 let e := pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG'
781 exact e.injective <| by
782 calc
783 e ((((e.symm : G' →ₜ* G).comp α₁') x)) = α₁' x := by
784 change e (e.symm (α₁' x)) = α₁' x
785 simp only [ContinuousMulEquiv.apply_symm_apply]
786 _ = e (α₁ x) := by
787 have hleft :
788 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₁ = α₁' :=
789 pushoutContMapOfIsPushout_left β₁ β₂ hpo hpo' hG'
790 have hleft_apply :
791 pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG' (α₁ x) = α₁' x := by
792 exact congrFun (congrArg (fun f : H₁ →ₜ* G' => (f : H₁ → G')) hleft) x
793 change α₁' x = pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG' (α₁ x)
794 simpa using hleft_apply.symm
796omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
797/-- Right-leg formula for the inverse profinite pushout comparison equivalence. -/
799 {α₁ : H₁ →ₜ* G} {α₂ : H₂ →ₜ* G}
800 {α₁' : H₁ →ₜ* G'} {α₂' : H₂ →ₜ* G'}
801 (β₁ : H →ₜ* H₁) (β₂ : H →ₜ* H₂)
802 (hpo : HasProfiniteTestPushoutProperty β₁ β₂ α₁ α₂)
803 (hpo' : HasProfiniteTestPushoutProperty β₁ β₂ α₁' α₂')
804 (hG : IsProfiniteGroup G) (hG' : IsProfiniteGroup G') :
805 (((pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG').symm : G' →ₜ* G).comp α₂') = α₂ := by
806 ext x
807 let e := pushoutContEquivOfIsPushout β₁ β₂ hpo hpo' hG hG'
808 exact e.injective <| by
809 calc
810 e ((((e.symm : G' →ₜ* G).comp α₂') x)) = α₂' x := by
811 change e (e.symm (α₂' x)) = α₂' x
812 simp only [ContinuousMulEquiv.apply_symm_apply]
813 _ = e (α₂ x) := by
814 have hright :
815 (pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG').comp α₂ = α₂' :=
816 pushoutContMapOfIsPushout_right β₁ β₂ hpo hpo' hG'
817 have hright_apply :
818 pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG' (α₂ x) = α₂' x := by
819 exact congrFun (congrArg (fun f : H₂ →ₜ* G' => (f : H₂ → G')) hright) x
820 change α₂' x = pushoutContMapOfIsPushout β₁ β₂ hpo hpo' hG' (α₂ x)
821 simpa using hright_apply.symm
823end
826end ProCGroups.Categorical