ProCGroups/Categorical/ProfinitePullbacks.lean
1import ProCGroups.Categorical.AlgebraicPullbacks
2import ProCGroups.Profinite.Basic
3import ProCGroups.Topologies.ContinuousMulEquiv
4import ProCGroups.TopologicalGroups
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/Categorical/ProfinitePullbacks.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Pullbacks, pushouts, and quotient comparison
17Concrete algebraic and topological pullbacks and pushouts of groups and profinite groups, with comparison maps, universal properties, kernel criteria, and quotient pullback equivalences.
18-/
20namespace ProCGroups.Categorical
22open CategoryTheory Limits
24universe u v
26section
28open ContinuousMonoidHom
30variable {A G H H₁ H₂ K : Type u}
32/-- Continuous pullback carrier attached to two continuous homomorphisms. -/
33abbrev TopologicalFiberProduct.carrier
34 [Group H] [Group H₁] [Group H₂]
35 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
36 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :=
37 FiberProduct.carrier (β₁ : H₁ →* H) (β₂ : H₂ →* H)
39/-- The first projection from the continuous pullback. -/
40def TopologicalFiberProduct.fst
41 [Group H] [Group H₁] [Group H₂]
42 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
43 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
44 TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₁ :=
45 { FiberProduct.fst (β₁ : H₁ →* H) (β₂ : H₂ →* H) with
46 continuous_toFun := continuous_fst.comp continuous_subtype_val }
48/-- The second projection from the continuous pullback. -/
49def TopologicalFiberProduct.snd
50 [Group H] [Group H₁] [Group H₂]
51 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
52 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
53 TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₂ :=
54 { FiberProduct.snd (β₁ : H₁ →* H) (β₂ : H₂ →* H) with
55 continuous_toFun := continuous_snd.comp continuous_subtype_val }
57/-- Extensionality for continuous homomorphisms into the concrete profinite pullback. -/
58theorem TopologicalFiberProduct.hom_ext
59 [Group H] [Group H₁] [Group H₂] [Group K]
60 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
61 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
62 {ψ ψ' : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂}
63 (h₁ : ∀ k, TopologicalFiberProduct.fst β₁ β₂ (ψ k) = TopologicalFiberProduct.fst β₁ β₂ (ψ' k))
64 (h₂ : ∀ k, TopologicalFiberProduct.snd β₁ β₂ (ψ k) = TopologicalFiberProduct.snd β₁ β₂ (ψ' k)) :
65 ψ = ψ' := by
66 apply ContinuousMonoidHom.ext
67 intro k
68 exact Subtype.ext <| Prod.ext (h₁ k) (h₂ k)
70/-- If `β₂` is surjective, then the first continuous pullback projection is surjective. -/
72 [Group H] [Group H₁] [Group H₂]
73 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
74 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
75 (hβ₂ : Function.Surjective β₂) :
76 Function.Surjective (TopologicalFiberProduct.fst β₁ β₂) := by
77 simpa [TopologicalFiberProduct.fst, TopologicalFiberProduct.carrier] using
79 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H)) hβ₂)
81/-- If `β₁` is surjective, then the second continuous pullback projection is surjective. -/
83 [Group H] [Group H₁] [Group H₂]
84 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
85 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
86 (hβ₁ : Function.Surjective β₁) :
87 Function.Surjective (TopologicalFiberProduct.snd β₁ β₂) := by
88 simpa [TopologicalFiberProduct.snd, TopologicalFiberProduct.carrier] using
90 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H)) hβ₁)
92/-- If `β₂` is injective, then the first continuous pullback projection is injective. -/
94 [Group H] [Group H₁] [Group H₂]
95 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
96 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
97 (hβ₂ : Function.Injective β₂) :
98 Function.Injective (TopologicalFiberProduct.fst β₁ β₂) := by
99 simpa [TopologicalFiberProduct.fst, TopologicalFiberProduct.carrier] using
101 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H)) hβ₂)
103/-- If `β₁` is injective, then the second continuous pullback projection is injective. -/
105 [Group H] [Group H₁] [Group H₂]
106 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
107 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
108 (hβ₁ : Function.Injective β₁) :
109 Function.Injective (TopologicalFiberProduct.snd β₁ β₂) := by
110 simpa [TopologicalFiberProduct.snd, TopologicalFiberProduct.carrier] using
112 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H)) hβ₁)
114/-- The canonical continuous map into the pullback. -/
115def TopologicalFiberProduct.lift
116 [Group H] [Group H₁] [Group H₂] [Group K]
117 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
118 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
119 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
120 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
121 K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
122 { FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
123 (φ₁ : K →* H₁) (φ₂ : K →* H₂) h with
124 continuous_toFun := by
125 exact Continuous.subtype_mk
126 (φ₁.continuous_toFun.prodMk φ₂.continuous_toFun)
127 (by
128 intro k
129 exact h k) }
131/-- The first projection composed with the continuous pullback lift is `φ₁`. -/
132@[simp] theorem pullbackFstCont_pullbackLiftCont
133 [Group H] [Group H₁] [Group H₂] [Group K]
134 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
135 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
136 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
137 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
138 (TopologicalFiberProduct.fst β₁ β₂).comp (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₁ := by
139 ext k
140 rfl
142/-- The second projection composed with the continuous pullback lift is `φ₂`. -/
143@[simp] theorem pullbackSndCont_pullbackLiftCont
144 [Group H] [Group H₁] [Group H₂] [Group K]
145 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
146 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
147 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
148 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
149 (TopologicalFiberProduct.snd β₁ β₂).comp (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₂ := by
150 ext k
151 rfl
153/-- The continuous pullback is reconstructed from its two projections by the canonical lift. -/
154@[simp] theorem pullbackLiftCont_eta
155 [Group H] [Group H₁] [Group H₂] [Group K]
156 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
157 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
158 (ψ : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂) :
159 TopologicalFiberProduct.lift β₁ β₂
160 ((TopologicalFiberProduct.fst β₁ β₂).comp ψ)
161 ((TopologicalFiberProduct.snd β₁ β₂).comp ψ)
162 (fun k => by exact (ψ k).2) = ψ := by
163 apply TopologicalFiberProduct.hom_ext
164 · intro k
165 rfl
166 · intro k
167 rfl
169/-- The concrete topological fiber product as a categorical pullback cone in `TopGrp`. -/
170def TopologicalFiberProduct.cone
171 [Group H] [Group H₁] [Group H₂]
172 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
173 [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
174 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
175 PullbackCone (TopGrp.ofHom β₁) (TopGrp.ofHom β₂) :=
176 PullbackCone.mk
177 (TopGrp.ofHom (TopologicalFiberProduct.fst β₁ β₂))
178 (TopGrp.ofHom (TopologicalFiberProduct.snd β₁ β₂))
179 (by
180 apply TopGrp.hom_ext
181 ext x
182 exact x.2)
184/-- The concrete topological fiber product cone is a limit cone in `TopGrp`. -/
185def TopologicalFiberProduct.isLimit
186 [Group H] [Group H₁] [Group H₂]
187 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
188 [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
189 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
190 IsLimit (TopologicalFiberProduct.cone β₁ β₂) := by
191 refine PullbackCone.IsLimit.mk (by
192 apply TopGrp.hom_ext
193 ext x
195 · intro s
196 exact TopGrp.ofHom <|
197 TopologicalFiberProduct.lift β₁ β₂ s.fst.hom s.snd.hom (fun x => by
198 have hcondition :
199 (s.fst ≫ TopGrp.ofHom β₁).hom =
200 (s.snd ≫ TopGrp.ofHom β₂).hom :=
202 exact DFunLike.congr_fun hcondition x)
203 · intro s
204 apply TopGrp.hom_ext
205 rfl
206 · intro s
207 apply TopGrp.hom_ext
208 rfl
209 · intro s m hfst hsnd
210 apply TopGrp.hom_ext
211 ext x
212 · have hfst' :
213 (m ≫ TopGrp.ofHom (TopologicalFiberProduct.fst β₁ β₂)).hom = s.fst.hom :=
215 exact DFunLike.congr_fun hfst' x
216 · have hsnd' :
217 (m ≫ TopGrp.ofHom (TopologicalFiberProduct.snd β₁ β₂)).hom = s.snd.hom :=
219 exact DFunLike.congr_fun hsnd' x
221/--
222If `φ₁` is injective, then the continuous canonical map into the profinite pullback is injective.
223-/
225 [Group H] [Group H₁] [Group H₂] [Group K]
226 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
227 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
228 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
229 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
230 (hφ₁ : Function.Injective φ₁) :
231 Function.Injective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) := by
232 simpa [TopologicalFiberProduct.lift, TopologicalFiberProduct.carrier] using
234 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
235 (φ₁ := (φ₁ : K →* H₁)) (φ₂ := (φ₂ : K →* H₂))
236 h hφ₁)
238/--
239If `φ₂` is injective, then the continuous canonical map into the profinite pullback is injective.
240-/
242 [Group H] [Group H₁] [Group H₂] [Group K]
243 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
244 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
245 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
246 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
247 (hφ₂ : Function.Injective φ₂) :
248 Function.Injective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) := by
249 simpa [TopologicalFiberProduct.lift, TopologicalFiberProduct.carrier] using
251 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
252 (φ₁ := (φ₁ : K →* H₁)) (φ₂ := (φ₂ : K →* H₂))
253 h hφ₂)
255/-- Continuous pullback property tested by all topological-group source objects. -/
257 [Group G] [Group H] [Group H₁] [Group H₂]
258 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
259 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
260 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) : Prop :=
261 β₁.comp α₁ = β₂.comp α₂ ∧
262 ∀ ⦃K : Type u⦄ [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
263 ∀ (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂),
264 β₁.comp φ₁ = β₂.comp φ₂ →
265 ∃! φ : K →ₜ* G, α₁.comp φ = φ₁ ∧ α₂.comp φ = φ₂
267/-- The concrete continuous pullback satisfies the topological pullback universal property. -/
268theorem TopologicalFiberProduct.isTopologicalPullback
269 {H H₁ H₂ : Type u}
270 [Group H] [Group H₁] [Group H₂]
271 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
272 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
273 HasTopologicalPullbackProperty (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
274 β₁ β₂ := by
275 refine ⟨?_, ?_⟩
276 · ext x
277 exact x.2
278 · intro K _ _ _ φ₁ φ₂ hφ
279 let φ : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
280 TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)
281 refine ⟨φ, ?_, ?_⟩
282 · exact ⟨pullbackFstCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
283 (fun k => DFunLike.congr_fun hφ k),
284 pullbackSndCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
285 (fun k => DFunLike.congr_fun hφ k)⟩
286 · intro ψ hψ
287 apply TopologicalFiberProduct.hom_ext
288 · intro k
289 calc
290 TopologicalFiberProduct.fst β₁ β₂ (ψ k) = φ₁ k :=
291 congrArg (fun f : K →ₜ* H₁ => f k) hψ.1
292 _ = TopologicalFiberProduct.fst β₁ β₂ (φ k) := by
293 symm
294 exact congrArg (fun f : K →ₜ* H₁ => f k)
295 (pullbackFstCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
296 (fun k => DFunLike.congr_fun hφ k))
297 · intro k
298 calc
299 TopologicalFiberProduct.snd β₁ β₂ (ψ k) = φ₂ k :=
300 congrArg (fun f : K →ₜ* H₂ => f k) hψ.2
301 _ = TopologicalFiberProduct.snd β₁ β₂ (φ k) := by
302 symm
303 exact congrArg (fun f : K →ₜ* H₂ => f k)
304 (pullbackSndCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
305 (fun k => DFunLike.congr_fun hφ k))
307/-- Continuous pullback property tested by profinite source objects.
309This definition does not assert that the four objects in the square are themselves profinite. -/
311 [Group G] [Group H] [Group H₁] [Group H₂]
312 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
313 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
314 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) : Prop :=
315 β₁.comp α₁ = β₂.comp α₂ ∧
316 ∀ ⦃K : Type u⦄ [Group K] [TopologicalSpace K] [IsTopologicalGroup K],
317 IsProfiniteGroup K →
318 ∀ (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂),
319 β₁.comp φ₁ = β₂.comp φ₂ →
320 ∃! φ : K →ₜ* G, α₁.comp φ = φ₁ ∧ α₂.comp φ = φ₂
322namespace HasTopologicalPullbackProperty
324/-- A topological pullback square has the restricted profinite-source test property. -/
325theorem hasProfiniteTestPullbackProperty
326 [Group G] [Group H] [Group H₁] [Group H₂]
327 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
328 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
329 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
330 (hpb : HasTopologicalPullbackProperty α₁ α₂ β₁ β₂) :
331 HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂ := by
332 refine ⟨hpb.1, ?_⟩
333 intro K _ _ _ _ φ₁ φ₂ hφ
334 exact hpb.2 φ₁ φ₂ hφ
338/-- A topological pullback square between profinite groups is a profinite pullback square. -/
340 [Group G] [Group H] [Group H₁] [Group H₂]
341 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
342 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
343 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
344 (hpb : HasTopologicalPullbackProperty α₁ α₂ β₁ β₂)
345 (_hG : IsProfiniteGroup G) (_hH₁ : IsProfiniteGroup H₁)
346 (_hH₂ : IsProfiniteGroup H₂) (_hH : IsProfiniteGroup H) :
347 HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂ :=
348 hpb.hasProfiniteTestPullbackProperty
350/-- Chosen continuous morphism induced by the pullback universal property. -/
351noncomputable def pullbackDescCont
352 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
353 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
354 [TopologicalSpace K]
355 [IsTopologicalGroup K]
356 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
357 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
358 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
359 (hK : IsProfiniteGroup K)
360 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
361 (hφ : β₁.comp φ₁ = β₂.comp φ₂) : K →ₜ* G :=
362 Classical.choose (ExistsUnique.exists (hpb.2 (K := K) hK φ₁ φ₂ hφ))
364/-- Specification of the chosen continuous pullback descent map. -/
365theorem pullbackDescCont_spec
366 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
367 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
368 [TopologicalSpace K]
369 [IsTopologicalGroup K]
370 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
371 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
372 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
373 (hK : IsProfiniteGroup K)
374 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
375 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
376 α₁.comp (pullbackDescCont hpb hK φ₁ φ₂ hφ) = φ₁ ∧
377 α₂.comp (pullbackDescCont hpb hK φ₁ φ₂ hφ) = φ₂ :=
378 Classical.choose_spec (ExistsUnique.exists (hpb.2 (K := K) hK φ₁ φ₂ hφ))
380/-- Left composite of the chosen continuous pullback descent map. -/
381@[simp] theorem pullbackDescCont_left
382 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
383 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
384 [TopologicalSpace K]
385 [IsTopologicalGroup K]
386 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
387 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
388 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
389 (hK : IsProfiniteGroup K)
390 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
391 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
392 α₁.comp (pullbackDescCont hpb hK φ₁ φ₂ hφ) = φ₁ :=
393 (pullbackDescCont_spec hpb hK φ₁ φ₂ hφ).1
395/-- Right composite of the chosen continuous pullback descent map. -/
396@[simp] theorem pullbackDescCont_right
397 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
398 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
399 [TopologicalSpace K]
400 [IsTopologicalGroup K]
401 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
402 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
403 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
404 (hK : IsProfiniteGroup K)
405 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
406 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
407 α₂.comp (pullbackDescCont hpb hK φ₁ φ₂ hφ) = φ₂ :=
408 (pullbackDescCont_spec hpb hK φ₁ φ₂ hφ).2
410/-- Uniqueness of the chosen continuous pullback descent map. -/
411theorem pullbackDescCont_uniq
412 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
413 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
414 [TopologicalSpace K]
415 [IsTopologicalGroup K]
416 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
417 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
418 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
419 (hK : IsProfiniteGroup K)
420 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
421 (hφ : β₁.comp φ₁ = β₂.comp φ₂)
422 {ψ : K →ₜ* G}
423 (hψ : α₁.comp ψ = φ₁ ∧ α₂.comp ψ = φ₂) :
424 ψ = pullbackDescCont hpb hK φ₁ φ₂ hφ := by
425 rcases hpb.2 (K := K) hK φ₁ φ₂ hφ with ⟨u, hu, huuniq⟩
426 have hψ' : ψ = u := huuniq _ hψ
427 have hdesc : pullbackDescCont hpb hK φ₁ φ₂ hφ = u :=
428 huuniq _ (pullbackDescCont_spec hpb hK φ₁ φ₂ hφ)
429 exact hψ'.trans hdesc.symm
431/-- The concrete pullback subgroup is closed in `H₁ × H₂`. -/
432theorem pullback_isClosed
433 {H H₁ H₂ : Type u}
434 [Group H] [Group H₁] [Group H₂]
435 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [T2Space H]
436 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
437 IsClosed ((FiberProduct.subgroup (β₁ : H₁ →* H) (β₂ : H₂ →* H) : Subgroup (H₁ × H₂)) :
438 Set (H₁ × H₂)) := by
439 change IsClosed { x : H₁ × H₂ | β₁ x.1 = β₂ x.2 }
440 exact isClosed_eq (β₁.continuous_toFun.comp continuous_fst)
441 (β₂.continuous_toFun.comp continuous_snd)
443/-- The concrete pullback of continuous maps between profinite groups is again profinite. -/
444theorem TopologicalFiberProduct.isProfiniteGroup
445 {H H₁ H₂ : Type u}
446 [Group H] [Group H₁] [Group H₂]
447 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
448 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
449 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
450 (hH₁ : IsProfiniteGroup H₁) (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H) :
451 IsProfiniteGroup (TopologicalFiberProduct.carrier β₁ β₂) := by
452 letI : CompactSpace H := IsProfiniteGroup.compactSpace hH
453 letI : CompactSpace H₁ := IsProfiniteGroup.compactSpace hH₁
454 letI : CompactSpace H₂ := IsProfiniteGroup.compactSpace hH₂
455 letI : T2Space H := IsProfiniteGroup.t2Space hH
456 letI : T2Space H₁ := IsProfiniteGroup.t2Space hH₁
457 letI : T2Space H₂ := IsProfiniteGroup.t2Space hH₂
458 letI : TotallyDisconnectedSpace H := IsProfiniteGroup.totallyDisconnectedSpace hH
459 letI : TotallyDisconnectedSpace H₁ := IsProfiniteGroup.totallyDisconnectedSpace hH₁
460 letI : TotallyDisconnectedSpace H₂ := IsProfiniteGroup.totallyDisconnectedSpace hH₂
461 have hprod : IsProfiniteGroup (H₁ × H₂) :=
462 ProCGroups.IsProfiniteGroup.prod (G := H₁) (H := H₂) hH₁ hH₂
463 simpa [TopologicalFiberProduct.carrier, FiberProduct.carrier] using
464 (ProCGroups.IsProfiniteGroup.of_isClosed_subgroup
465 (G := H₁ × H₂)
466 (hG := hprod)
467 (H := FiberProduct.subgroup (β₁ : H₁ →* H) (β₂ : H₂ →* H))
468 (pullback_isClosed β₁ β₂))
470namespace FiberProduct
472/-- The concrete fiber-product subgroup of continuous maps is closed in the product. -/
473theorem isClosed
474 {H H₁ H₂ : Type u}
475 [Group H] [Group H₁] [Group H₂]
476 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [T2Space H]
477 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
478 IsClosed ((subgroup (β₁ : H₁ →* H) (β₂ : H₂ →* H) : Subgroup (H₁ × H₂)) :
479 Set (H₁ × H₂)) :=
480 pullback_isClosed β₁ β₂
482/-- The concrete fiber product of continuous maps between profinite groups is profinite. -/
483theorem isProfiniteGroup
484 {H H₁ H₂ : Type u}
485 [Group H] [Group H₁] [Group H₂]
486 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
487 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
488 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
489 (hH₁ : IsProfiniteGroup H₁) (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H) :
490 IsProfiniteGroup (carrier (β₁ : H₁ →* H) (β₂ : H₂ →* H)) :=
491 TopologicalFiberProduct.isProfiniteGroup β₁ β₂ hH₁ hH₂ hH
493end FiberProduct
495/-- The concrete profinite pullback satisfies the continuous pullback universal property. -/
496theorem TopologicalFiberProduct.hasProfiniteTestPullbackProperty
497 {H H₁ H₂ : Type u}
498 [Group H] [Group H₁] [Group H₂]
499 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
500 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
501 HasProfiniteTestPullbackProperty (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂) β₁ β₂ := by
502 refine ⟨?_, ?_⟩
503 · ext x
504 exact x.2
505 · intro K _ _ _ hK φ₁ φ₂ hφ
506 refine ⟨TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k), ?_, ?_⟩
507 · exact ⟨pullbackFstCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
508 (fun k => DFunLike.congr_fun hφ k),
509 pullbackSndCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
510 (fun k => DFunLike.congr_fun hφ k)⟩
511 · intro ψ hψ
512 have hfst :
513 (TopologicalFiberProduct.fst β₁ β₂).comp ψ =
514 (TopologicalFiberProduct.fst β₁ β₂).comp
515 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
516 calc
517 (TopologicalFiberProduct.fst β₁ β₂).comp ψ = φ₁ := hψ.1
518 _ =
519 (TopologicalFiberProduct.fst β₁ β₂).comp
520 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
521 symm
522 exact pullbackFstCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
523 (fun k => DFunLike.congr_fun hφ k)
524 have hsnd :
525 (TopologicalFiberProduct.snd β₁ β₂).comp ψ =
526 (TopologicalFiberProduct.snd β₁ β₂).comp
527 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
528 calc
529 (TopologicalFiberProduct.snd β₁ β₂).comp ψ = φ₂ := hψ.2
530 _ =
531 (TopologicalFiberProduct.snd β₁ β₂).comp
532 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
533 symm
534 exact pullbackSndCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
535 (fun k => DFunLike.congr_fun hφ k)
536 exact TopologicalFiberProduct.hom_ext
537 (fun k => by
538 exact congrArg (fun f : K →ₜ* H₁ => f k) hfst)
539 (fun k => by
540 exact congrArg (fun f : K →ₜ* H₂ => f k) hsnd)
544/-- A profinite square with a bijective continuous comparison map to the concrete pullback is a
545continuous pullback square.
546-/
548 {G H H₁ H₂ : Type u}
549 [Group G] [Group H] [Group H₁] [Group H₂]
550 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
551 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
552 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
553 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
554 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
555 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
556 (τ : G →ₜ* TopologicalFiberProduct.carrier β₁ β₂)
557 (hτ : Function.Bijective τ)
558 (h₁ : (TopologicalFiberProduct.fst β₁ β₂).comp τ = α₁)
559 (h₂ : (TopologicalFiberProduct.snd β₁ β₂).comp τ = α₂) :
560 HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂ := by
561 refine ⟨?_, ?_⟩
562 · ext g
563 have hτ₁ : TopologicalFiberProduct.fst β₁ β₂ (τ g) = α₁ g := by
564 simpa using congrArg (fun f : G →ₜ* H₁ => f g) h₁
565 have hτ₂ : TopologicalFiberProduct.snd β₁ β₂ (τ g) = α₂ g := by
566 simpa using congrArg (fun f : G →ₜ* H₂ => f g) h₂
567 calc
568 β₁ (α₁ g) = β₁ (TopologicalFiberProduct.fst β₁ β₂ (τ g)) := by rw [← hτ₁]
569 _ = β₂ (TopologicalFiberProduct.snd β₁ β₂ (τ g)) := (τ g).2
570 _ = β₂ (α₂ g) := by rw [hτ₂]
571 · intro K _ _ _ hK φ₁ φ₂ hφ
572 let hP : IsProfiniteGroup (TopologicalFiberProduct.carrier β₁ β₂) :=
573 TopologicalFiberProduct.isProfiniteGroup β₁ β₂ hH₁ hH₂ hH
574 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
575 letI : T2Space (TopologicalFiberProduct.carrier β₁ β₂) := IsProfiniteGroup.t2Space hP
576 let e : G ≃ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
577 ContinuousMulEquiv.ofBijectiveCompactToT2 τ τ.continuous_toFun hτ
578 let θ : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
579 TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)
580 have hθ₁ : (TopologicalFiberProduct.fst β₁ β₂).comp θ = φ₁ := by
581 ext k
582 rfl
583 have hθ₂ : (TopologicalFiberProduct.snd β₁ β₂).comp θ = φ₂ := by
584 ext k
585 rfl
586 refine ⟨e.symm.toContinuousMonoidHom.comp θ, ?_, ?_⟩
587 · constructor
588 · ext k
589 have hτ₁ : TopologicalFiberProduct.fst β₁ β₂ (τ (e.symm (θ k))) = α₁ (e.symm (θ k)) := by
590 simpa using congrArg (fun f : G →ₜ* H₁ => f (e.symm (θ k))) h₁
591 have hθ₁' : TopologicalFiberProduct.fst β₁ β₂ (θ k) = φ₁ k := by
592 simpa using congrArg (fun f : K →ₜ* H₁ => f k) hθ₁
593 calc
594 α₁ (e.symm (θ k)) = TopologicalFiberProduct.fst β₁ β₂ (τ (e.symm (θ k))) := by
595 simpa using hτ₁.symm
596 _ = TopologicalFiberProduct.fst β₁ β₂ (θ k) := by
597 rw [show τ (e.symm (θ k)) = θ k from e.apply_symm_apply (θ k)]
598 _ = φ₁ k := hθ₁'
599 · ext k
600 have hτ₂ : TopologicalFiberProduct.snd β₁ β₂ (τ (e.symm (θ k))) = α₂ (e.symm (θ k)) := by
601 simpa using congrArg (fun f : G →ₜ* H₂ => f (e.symm (θ k))) h₂
602 have hθ₂' : TopologicalFiberProduct.snd β₁ β₂ (θ k) = φ₂ k := by
603 simpa using congrArg (fun f : K →ₜ* H₂ => f k) hθ₂
604 calc
605 α₂ (e.symm (θ k)) = TopologicalFiberProduct.snd β₁ β₂ (τ (e.symm (θ k))) := by
606 simpa using hτ₂.symm
607 _ = TopologicalFiberProduct.snd β₁ β₂ (θ k) := by
608 rw [show τ (e.symm (θ k)) = θ k from e.apply_symm_apply (θ k)]
609 _ = φ₂ k := hθ₂'
610 · intro ψ hψ
611 have hcoord : τ.comp ψ = θ := by
612 apply TopologicalFiberProduct.hom_ext
613 · intro k
614 have hτ₁ : TopologicalFiberProduct.fst β₁ β₂ (τ (ψ k)) = α₁ (ψ k) := by
615 simpa using congrArg (fun f : G →ₜ* H₁ => f (ψ k)) h₁
616 have hψ₁ : α₁ (ψ k) = φ₁ k := by
617 simpa using congrArg (fun f : K →ₜ* H₁ => f k) hψ.1
618 have hθ₁' : TopologicalFiberProduct.fst β₁ β₂ (θ k) = φ₁ k := by
619 simpa using congrArg (fun f : K →ₜ* H₁ => f k) hθ₁
620 calc
621 TopologicalFiberProduct.fst β₁ β₂ ((τ.comp ψ) k) = α₁ (ψ k) := by
622 simpa using hτ₁
623 _ = φ₁ k := hψ₁
624 _ = TopologicalFiberProduct.fst β₁ β₂ (θ k) := hθ₁'.symm
625 · intro k
626 have hτ₂ : TopologicalFiberProduct.snd β₁ β₂ (τ (ψ k)) = α₂ (ψ k) := by
627 simpa using congrArg (fun f : G →ₜ* H₂ => f (ψ k)) h₂
628 have hψ₂ : α₂ (ψ k) = φ₂ k := by
629 simpa using congrArg (fun f : K →ₜ* H₂ => f k) hψ.2
630 have hθ₂' : TopologicalFiberProduct.snd β₁ β₂ (θ k) = φ₂ k := by
631 simpa using congrArg (fun f : K →ₜ* H₂ => f k) hθ₂
632 calc
633 TopologicalFiberProduct.snd β₁ β₂ ((τ.comp ψ) k) = α₂ (ψ k) := by
634 simpa using hτ₂
635 _ = φ₂ k := hψ₂
636 _ = TopologicalFiberProduct.snd β₁ β₂ (θ k) := hθ₂'.symm
637 ext k
638 apply hτ.1
639 calc
640 τ (ψ k) = (τ.comp ψ) k := by rfl
641 _ = θ k := by
642 exact congrArg (fun f : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ => f k) hcoord
643 _ = τ ((e.symm.toContinuousMonoidHom.comp θ) k) := by
644 change θ k = τ (e.symm (θ k))
645 symm
646 exact e.apply_symm_apply (θ k)
649/-- Transport of the continuous pullback universal property across a continuous multiplicative
650 equivalence with the concrete pullback.
651-/
653 [Group G] [Group H] [Group H₁] [Group H₂]
654 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
655 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
656 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
657 (e : G ≃ₜ* TopologicalFiberProduct.carrier β₁ β₂)
658 (h₁ : (TopologicalFiberProduct.fst β₁ β₂).comp e.toContinuousMonoidHom = α₁)
659 (h₂ : (TopologicalFiberProduct.snd β₁ β₂).comp e.toContinuousMonoidHom = α₂) :
660 HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂ := by
661 refine ⟨?_, ?_⟩
662 · ext g
663 have h₁g : TopologicalFiberProduct.fst β₁ β₂ (e g) = α₁ g := by
664 simpa using congrArg (fun f : G →ₜ* H₁ => f g) h₁
665 have h₂g : TopologicalFiberProduct.snd β₁ β₂ (e g) = α₂ g := by
666 simpa using congrArg (fun f : G →ₜ* H₂ => f g) h₂
667 calc
668 β₁ (α₁ g) = β₁ (TopologicalFiberProduct.fst β₁ β₂ (e g)) := by rw [← h₁g]
669 _ = β₂ (TopologicalFiberProduct.snd β₁ β₂ (e g)) := (e g).2
670 _ = β₂ (α₂ g) := by rw [h₂g]
671 · intro K _ _ _ hK φ₁ φ₂ hφ
672 let θ : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
673 TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)
674 refine ⟨e.symm.toContinuousMonoidHom.comp θ, ?_, ?_⟩
675 · constructor
676 · ext k
677 have h₁k : TopologicalFiberProduct.fst β₁ β₂ (e (e.symm (θ k))) = α₁ (e.symm (θ k)) := by
678 simpa using congrArg (fun f : G →ₜ* H₁ => f (e.symm (θ k))) h₁
679 calc
680 α₁ ((e.symm.toContinuousMonoidHom.comp θ) k) = α₁ (e.symm (θ k)) := rfl
681 _ = TopologicalFiberProduct.fst β₁ β₂ (e (e.symm (θ k))) := by
682 simpa using h₁k.symm
683 _ = TopologicalFiberProduct.fst β₁ β₂ (θ k) := by rw [e.apply_symm_apply]
684 _ = φ₁ k := by
685 change
686 TopologicalFiberProduct.fst β₁ β₂
687 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k) =
688 φ₁ k
689 rfl
690 · ext k
691 have h₂k : TopologicalFiberProduct.snd β₁ β₂ (e (e.symm (θ k))) = α₂ (e.symm (θ k)) := by
692 simpa using congrArg (fun f : G →ₜ* H₂ => f (e.symm (θ k))) h₂
693 calc
694 α₂ ((e.symm.toContinuousMonoidHom.comp θ) k) = α₂ (e.symm (θ k)) := rfl
695 _ = TopologicalFiberProduct.snd β₁ β₂ (e (e.symm (θ k))) := by
696 simpa using h₂k.symm
697 _ = TopologicalFiberProduct.snd β₁ β₂ (θ k) := by rw [e.apply_symm_apply]
698 _ = φ₂ k := by
699 change
700 TopologicalFiberProduct.snd β₁ β₂
701 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k) =
702 φ₂ k
703 rfl
704 · intro ψ hψ
705 have hcoord : e.toContinuousMonoidHom.comp ψ = θ := by
706 apply TopologicalFiberProduct.hom_ext
707 · intro k
708 have h₁ψ : TopologicalFiberProduct.fst β₁ β₂ (e (ψ k)) = α₁ (ψ k) := by
709 simpa using congrArg (fun f : G →ₜ* H₁ => f (ψ k)) h₁
710 have hψ₁ : α₁ (ψ k) = φ₁ k := by
711 simpa using congrArg (fun f : K →ₜ* H₁ => f k) hψ.1
712 calc
713 TopologicalFiberProduct.fst β₁ β₂ ((e.toContinuousMonoidHom.comp ψ) k) = α₁ (ψ k) := by
714 simpa using h₁ψ
715 _ = φ₁ k := hψ₁
716 _ = TopologicalFiberProduct.fst β₁ β₂ (θ k) := by
717 change
718 φ₁ k =
719 TopologicalFiberProduct.fst β₁ β₂
720 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k)
721 rfl
722 · intro k
723 have h₂ψ : TopologicalFiberProduct.snd β₁ β₂ (e (ψ k)) = α₂ (ψ k) := by
724 simpa using congrArg (fun f : G →ₜ* H₂ => f (ψ k)) h₂
725 have hψ₂ : α₂ (ψ k) = φ₂ k := by
726 simpa using congrArg (fun f : K →ₜ* H₂ => f k) hψ.2
727 calc
728 TopologicalFiberProduct.snd β₁ β₂ ((e.toContinuousMonoidHom.comp ψ) k) = α₂ (ψ k) := by
729 simpa using h₂ψ
730 _ = φ₂ k := hψ₂
731 _ = TopologicalFiberProduct.snd β₁ β₂ (θ k) := by
732 change
733 φ₂ k =
734 TopologicalFiberProduct.snd β₁ β₂
735 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k)
736 rfl
737 ext k
738 apply e.injective
739 calc
740 e (ψ k) = (e.toContinuousMonoidHom.comp ψ) k := by rfl
741 _ = θ k := by
742 exact congrArg (fun f : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ => f k) hcoord
743 _ = e (e.symm (θ k)) := by rw [e.apply_symm_apply]
745/-- Continuous surjectivity criterion for the canonical map into the pullback, in kernel-inclusion
746form. -/
748 [Group A] [Group H] [Group H₁] [Group H₂]
749 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
750 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
751 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
752 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
753 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
754 Function.Surjective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂
755 (fun a => DFunLike.congr_fun hcomp a)) ↔
759 have hcomp' :
760 ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)) =
761 ((β₂ : H₂ →* H).comp (φ₂ : A →* H₂)) := by
762 ext a
763 exact DFunLike.congr_fun hcomp a
764 simpa [TopologicalFiberProduct.lift, TopologicalFiberProduct.carrier] using
766 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
767 (φ₁ := (φ₁ : A →* H₁)) (φ₂ := (φ₂ : A →* H₂))
768 hφ₁ hφ₂ hcomp')
770/-- Continuous surjectivity criterion for the canonical map into the pullback. -/
772 [Group A] [Group H] [Group H₁] [Group H₂]
773 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
774 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
775 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
776 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
777 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
778 Function.Surjective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂
779 (fun a => DFunLike.congr_fun hcomp a)) ↔
783 have hcomp' :
784 ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)) =
785 ((β₂ : H₂ →* H).comp (φ₂ : A →* H₂)) := by
786 ext a
787 exact DFunLike.congr_fun hcomp a
788 simpa [TopologicalFiberProduct.lift, TopologicalFiberProduct.carrier] using
790 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
791 (φ₁ := (φ₁ : A →* H₁)) (φ₂ := (φ₂ : A →* H₂))
792 hφ₁ hφ₂ hcomp')
794/-- Continuous surjectivity criterion for the canonical map into the pullback. -/
796 [Group A] [Group H] [Group H₁] [Group H₂]
797 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
798 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
799 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
800 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
801 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
804 Function.Surjective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
805 exact DFunLike.congr_fun hcomp a)) := by
806 exact (pullbackLiftCont_surjective_iff_ker_eq β₁ β₂ φ₁ φ₂ hφ₁ hφ₂ hcomp).2 hker
808/-- Reusable bijectivity package for the continuous pullback map, using injectivity of `φ₁`. -/
810 [Group A] [Group H] [Group H₁] [Group H₂]
811 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
812 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
813 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
814 (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
815 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
818 (hφ₁inj : Function.Injective φ₁) :
819 Function.Bijective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
820 exact DFunLike.congr_fun hcomp a)) := by
821 refine ⟨?_, ?_⟩
822 · exact pullbackLiftCont_injective_of_left_injective β₁ β₂ φ₁ φ₂
823 (fun a => DFunLike.congr_fun hcomp a) hφ₁inj
824 · exact surjective_pullbackLiftCont_of_ker_eq β₁ β₂ φ₁ φ₂
825 hφ₁surj hφ₂surj hcomp hker
827/-- Reusable bijectivity package for the continuous pullback map, using injectivity of `φ₂`. -/
829 [Group A] [Group H] [Group H₁] [Group H₂]
830 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
831 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
832 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
833 (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
834 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
837 (hφ₂inj : Function.Injective φ₂) :
838 Function.Bijective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
839 exact DFunLike.congr_fun hcomp a)) := by
840 refine ⟨?_, ?_⟩
841 · exact pullbackLiftCont_injective_of_right_injective β₁ β₂ φ₁ φ₂
842 (fun a => DFunLike.congr_fun hcomp a) hφ₂inj
843 · exact surjective_pullbackLiftCont_of_ker_eq β₁ β₂ φ₁ φ₂
844 hφ₁surj hφ₂surj hcomp hker
846namespace TopologicalFiberProduct
848/-- The first projection composed with a topological fiber-product lift is the left map. -/
849@[simp] theorem fst_lift
850 [Group H] [Group H₁] [Group H₂] [Group K]
851 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
852 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
853 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
854 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
855 (fst β₁ β₂).comp (lift β₁ β₂ φ₁ φ₂ h) = φ₁ :=
856 pullbackFstCont_pullbackLiftCont β₁ β₂ φ₁ φ₂ h
858/-- The second projection composed with a topological fiber-product lift is the right map. -/
859@[simp] theorem snd_lift
860 [Group H] [Group H₁] [Group H₂] [Group K]
861 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
862 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
863 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
864 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
865 (snd β₁ β₂).comp (lift β₁ β₂ φ₁ φ₂ h) = φ₂ :=
866 pullbackSndCont_pullbackLiftCont β₁ β₂ φ₁ φ₂ h
868@[simp] theorem fst_lift_apply
869 [Group H] [Group H₁] [Group H₂] [Group K]
870 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
871 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
872 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
873 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
874 fst β₁ β₂ (lift β₁ β₂ φ₁ φ₂ h k) = φ₁ k :=
875 rfl
877@[simp] theorem snd_lift_apply
878 [Group H] [Group H₁] [Group H₂] [Group K]
879 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
880 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
881 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
882 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
883 snd β₁ β₂ (lift β₁ β₂ φ₁ φ₂ h k) = φ₂ k :=
884 rfl
886end TopologicalFiberProduct
888end
892end ProCGroups.Categorical