Source: ProCGroups.Categorical.ProfinitePullbacks
1import ProCGroups.Categorical.AlgebraicPullbacks
2import ProCGroups.Profinite.Basic
3import ProCGroups.Topologies.ContinuousMulEquiv
4import ProCGroups.TopologicalGroups
6/-!
7# Continuous pullbacks of topological groups
9This module develops continuous fiber products and the universal property
10obtained by testing a continuous square against profinite source groups. The
11four objects in a tested square are not required to be profinite.
12-/
14namespace ProCGroups.Categorical
16open CategoryTheory Limits
18universe u v
20section
22open ContinuousMonoidHom
24variable {A G H H₁ H₂ K : Type u}
26/-- Continuous pullback carrier attached to two continuous homomorphisms. -/
27abbrev TopologicalFiberProduct.carrier
28 [Group H] [Group H₁] [Group H₂]
29 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
30 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :=
31 FiberProduct.carrier (β₁ : H₁ →* H) (β₂ : H₂ →* H)
33/-- The first projection from the continuous pullback. -/
34def TopologicalFiberProduct.fst
35 [Group H] [Group H₁] [Group H₂]
36 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
37 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
38 TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₁ :=
39 { FiberProduct.fst (β₁ : H₁ →* H) (β₂ : H₂ →* H) with
40 continuous_toFun := continuous_fst.comp continuous_subtype_val }
42/-- The second projection from the continuous pullback. -/
43def TopologicalFiberProduct.snd
44 [Group H] [Group H₁] [Group H₂]
45 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
46 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
47 TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₂ :=
48 { FiberProduct.snd (β₁ : H₁ →* H) (β₂ : H₂ →* H) with
49 continuous_toFun := continuous_snd.comp continuous_subtype_val }
51/-- Extensionality for continuous homomorphisms into the concrete continuous fiber product. -/
52theorem TopologicalFiberProduct.hom_ext
53 [Group H] [Group H₁] [Group H₂] [Group K]
54 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
55 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
56 {ψ ψ' : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂}
57 (h₁ : ∀ k, TopologicalFiberProduct.fst β₁ β₂ (ψ k) = TopologicalFiberProduct.fst β₁ β₂ (ψ' k))
58 (h₂ : ∀ k, TopologicalFiberProduct.snd β₁ β₂ (ψ k) = TopologicalFiberProduct.snd β₁ β₂ (ψ' k)) :
59 ψ = ψ' := by
60 apply ContinuousMonoidHom.ext
61 intro k
62 exact Subtype.ext <| Prod.ext (h₁ k) (h₂ k)
64/--
65If the right map in the pullback square is surjective, then the first projection from the
66continuous pullback is surjective.
67-/
68theorem pullbackFstCont_surjective_of_right_surjective
69 [Group H] [Group H₁] [Group H₂]
70 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
71 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
72 (hβ₂ : Function.Surjective β₂) :
73 Function.Surjective (TopologicalFiberProduct.fst β₁ β₂) := by
74 change Function.Surjective
75 (FiberProduct.fst (β₁ : H₁ →* H) (β₂ : H₂ →* H))
76 exact pullbackFst_surjective_of_right_surjective
77 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H)) hβ₂
79/--
80If the left map in the pullback square is surjective, then the second projection from the
81continuous pullback is surjective.
82-/
83theorem pullbackSndCont_surjective_of_left_surjective
84 [Group H] [Group H₁] [Group H₂]
85 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
86 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
87 (hβ₁ : Function.Surjective β₁) :
88 Function.Surjective (TopologicalFiberProduct.snd β₁ β₂) := by
89 change Function.Surjective
90 (FiberProduct.snd (β₁ : H₁ →* H) (β₂ : H₂ →* H))
91 exact pullbackSnd_surjective_of_left_surjective
92 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H)) hβ₁
94/-- If \(\beta_2\) is injective, then the first continuous pullback projection is injective. -/
95theorem pullbackFstCont_injective_of_right_injective
96 [Group H] [Group H₁] [Group H₂]
97 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
98 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
99 (hβ₂ : Function.Injective β₂) :
100 Function.Injective (TopologicalFiberProduct.fst β₁ β₂) := by
101 change Function.Injective
102 (FiberProduct.fst (β₁ : H₁ →* H) (β₂ : H₂ →* H))
103 exact pullbackFst_injective_of_right_injective
104 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H)) hβ₂
106/-- If \(\beta_1\) is injective, then the second continuous pullback projection is injective. -/
107theorem pullbackSndCont_injective_of_left_injective
108 [Group H] [Group H₁] [Group H₂]
109 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
110 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
111 (hβ₁ : Function.Injective β₁) :
112 Function.Injective (TopologicalFiberProduct.snd β₁ β₂) := by
113 change Function.Injective
114 (FiberProduct.snd (β₁ : H₁ →* H) (β₂ : H₂ →* H))
115 exact pullbackSnd_injective_of_left_injective
116 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H)) hβ₁
118/-- The canonical continuous map into the pullback. -/
119def TopologicalFiberProduct.lift
120 [Group H] [Group H₁] [Group H₂] [Group K]
121 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
122 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
123 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
124 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
125 K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
126 { FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
127 (φ₁ : K →* H₁) (φ₂ : K →* H₂) h with
128 continuous_toFun := by
129 exact Continuous.subtype_mk
130 (φ₁.continuous_toFun.prodMk φ₂.continuous_toFun)
131 (by
132 intro k
133 exact h k) }
135/-- Composing the first projection with the continuous pullback lift gives \(\varphi_1\). -/
136@[simp] theorem pullbackFstCont_pullbackLiftCont
137 [Group H] [Group H₁] [Group H₂] [Group K]
138 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
139 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
140 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
141 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
142 (TopologicalFiberProduct.fst β₁ β₂).comp (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₁ := by
143 ext k
144 rfl
146/-- Composing the second projection with the continuous pullback lift gives \(\varphi_2\). -/
147@[simp] theorem pullbackSndCont_pullbackLiftCont
148 [Group H] [Group H₁] [Group H₂] [Group K]
149 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
150 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
151 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
152 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
153 (TopologicalFiberProduct.snd β₁ β₂).comp (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₂ := by
154 ext k
155 rfl
157/-- The continuous pullback is reconstructed from its two projections by the canonical lift. -/
158@[simp] theorem pullbackLiftCont_eta
159 [Group H] [Group H₁] [Group H₂] [Group K]
160 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
161 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
162 (ψ : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂) :
163 TopologicalFiberProduct.lift β₁ β₂
164 ((TopologicalFiberProduct.fst β₁ β₂).comp ψ)
165 ((TopologicalFiberProduct.snd β₁ β₂).comp ψ)
166 (fun k => by exact (ψ k).2) = ψ := by
167 apply TopologicalFiberProduct.hom_ext
168 · intro k
169 rfl
170 · intro k
171 rfl
173/-- The concrete topological fiber product as a categorical pullback cone in TopGrp. -/
174def TopologicalFiberProduct.cone
175 [Group H] [Group H₁] [Group H₂]
176 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
177 [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
178 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
179 PullbackCone (TopGrp.ofHom β₁) (TopGrp.ofHom β₂) :=
180 PullbackCone.mk
181 (TopGrp.ofHom (TopologicalFiberProduct.fst β₁ β₂))
182 (TopGrp.ofHom (TopologicalFiberProduct.snd β₁ β₂))
183 (by
184 apply TopGrp.hom_ext
185 ext x
186 exact x.2)
188/-- The concrete topological fiber product cone is a limit cone in TopGrp. -/
189def TopologicalFiberProduct.isLimit
190 [Group H] [Group H₁] [Group H₂]
191 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
192 [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
193 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
194 IsLimit (TopologicalFiberProduct.cone β₁ β₂) := by
195 refine PullbackCone.IsLimit.mk (by
196 apply TopGrp.hom_ext
197 ext x
198 exact x.2) ?lift ?fac_left ?fac_right ?uniq
199 · intro s
200 exact TopGrp.ofHom <|
201 TopologicalFiberProduct.lift β₁ β₂ s.fst.hom s.snd.hom (fun x => by
202 have hcondition :
203 (s.fst ≫ TopGrp.ofHom β₁).hom =
204 (s.snd ≫ TopGrp.ofHom β₂).hom :=
205 congrArg (fun f : s.pt ⟶ TopGrp.of H => f.hom) s.condition
206 exact DFunLike.congr_fun hcondition x)
207 · intro s
208 apply TopGrp.hom_ext
209 rfl
210 · intro s
211 apply TopGrp.hom_ext
212 rfl
213 · intro s m hfst hsnd
214 apply TopGrp.hom_ext
215 ext x
216 · have hfst' :
217 (m ≫ TopGrp.ofHom (TopologicalFiberProduct.fst β₁ β₂)).hom = s.fst.hom :=
218 congrArg (fun f : s.pt ⟶ TopGrp.of H₁ => f.hom) hfst
219 exact DFunLike.congr_fun hfst' x
220 · have hsnd' :
221 (m ≫ TopGrp.ofHom (TopologicalFiberProduct.snd β₁ β₂)).hom = s.snd.hom :=
222 congrArg (fun f : s.pt ⟶ TopGrp.of H₂ => f.hom) hsnd
223 exact DFunLike.congr_fun hsnd' x
225/--
226If \(\varphi_1\) is injective, then the continuous canonical map into the continuous fiber
227product is injective.
228-/
229theorem pullbackLiftCont_injective_of_left_injective
230 [Group H] [Group H₁] [Group H₂] [Group K]
231 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
232 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
233 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
234 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
235 (hφ₁ : Function.Injective φ₁) :
236 Function.Injective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) := by
237 change Function.Injective
238 (FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
239 (φ₁ : K →* H₁) (φ₂ : K →* H₂) h)
240 exact pullbackLift_injective_of_left_injective
241 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
242 (φ₁ := (φ₁ : K →* H₁)) (φ₂ := (φ₂ : K →* H₂))
243 h hφ₁
245/--
246If \(\varphi_2\) is injective, then the continuous canonical map into the continuous fiber
247product is injective.
248-/
249theorem pullbackLiftCont_injective_of_right_injective
250 [Group H] [Group H₁] [Group H₂] [Group K]
251 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
252 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
253 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
254 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
255 (hφ₂ : Function.Injective φ₂) :
256 Function.Injective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ h) := by
257 change Function.Injective
258 (FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
259 (φ₁ : K →* H₁) (φ₂ : K →* H₂) h)
260 exact pullbackLift_injective_of_right_injective
261 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
262 (φ₁ := (φ₁ : K →* H₁)) (φ₂ := (φ₂ : K →* H₂))
263 h hφ₂
265/--
266Continuous pullback property tested by profinite source objects. The property tests the square
267against profinite objects without requiring the four objects of the square themselves to be
268profinite.
269-/
270def HasProfiniteTestPullbackProperty
271 [Group G] [Group H] [Group H₁] [Group H₂]
272 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
273 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
274 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) : Prop :=
275 β₁.comp α₁ = β₂.comp α₂ ∧
276 ∀ ⦃K : Type u⦄ [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
277 [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K],
278 ∀ (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂),
279 β₁.comp φ₁ = β₂.comp φ₂ →
280 ∃! φ : K →ₜ* G, α₁.comp φ = φ₁ ∧ α₂.comp φ = φ₂
285/-- Chosen continuous morphism induced by the pullback universal property. -/
286noncomputable def pullbackDescCont
287 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
288 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
289 [TopologicalSpace K]
290 [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
291 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
292 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
293 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
294 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
295 (hφ : β₁.comp φ₁ = β₂.comp φ₂) : K →ₜ* G :=
296 Classical.choose (ExistsUnique.exists (hpb.2 (K := K) φ₁ φ₂ hφ))
298/-- Specification of the chosen continuous pullback descent map. -/
299theorem pullbackDescCont_spec
300 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
301 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
302 [TopologicalSpace K]
303 [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
304 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
305 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
306 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
307 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
308 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
309 α₁.comp (pullbackDescCont hpb φ₁ φ₂ hφ) = φ₁ ∧
310 α₂.comp (pullbackDescCont hpb φ₁ φ₂ hφ) = φ₂ :=
311 Classical.choose_spec (ExistsUnique.exists (hpb.2 (K := K) φ₁ φ₂ hφ))
313/-- The left composite of the chosen continuous pullback descent map is the prescribed left leg. -/
314@[simp] theorem pullbackDescCont_left
315 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
316 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
317 [TopologicalSpace K]
318 [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
319 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
320 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
321 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
322 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
323 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
324 α₁.comp (pullbackDescCont hpb φ₁ φ₂ hφ) = φ₁ :=
325 (pullbackDescCont_spec hpb φ₁ φ₂ hφ).1
327/--
328The right composite of the chosen continuous pullback descent map is the prescribed right leg.
329-/
330@[simp] theorem pullbackDescCont_right
331 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
332 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
333 [TopologicalSpace K]
334 [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
335 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
336 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
337 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
338 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
339 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
340 α₂.comp (pullbackDescCont hpb φ₁ φ₂ hφ) = φ₂ :=
341 (pullbackDescCont_spec hpb φ₁ φ₂ hφ).2
343/-- Uniqueness of the chosen continuous pullback descent map. -/
344theorem pullbackDescCont_uniq
345 [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
346 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
347 [TopologicalSpace K]
348 [IsTopologicalGroup K] [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]
349 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
350 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
351 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
352 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
353 (hφ : β₁.comp φ₁ = β₂.comp φ₂)
354 {ψ : K →ₜ* G}
355 (hψ : α₁.comp ψ = φ₁ ∧ α₂.comp ψ = φ₂) :
356 ψ = pullbackDescCont hpb φ₁ φ₂ hφ :=
357 (hpb.2 (K := K) φ₁ φ₂ hφ).unique hψ
358 (pullbackDescCont_spec hpb φ₁ φ₂ hφ)
360/-- The concrete pullback subgroup is closed in \(H_1 \times H_2\). -/
361theorem pullback_isClosed
362 {H H₁ H₂ : Type u}
363 [Group H] [Group H₁] [Group H₂]
364 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [T2Space H]
365 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
366 IsClosed ((FiberProduct.subgroup (β₁ : H₁ →* H) (β₂ : H₂ →* H) : Subgroup (H₁ × H₂)) :
367 Set (H₁ × H₂)) := by
368 change IsClosed { x : H₁ × H₂ | β₁ x.1 = β₂ x.2 }
369 exact isClosed_eq (β₁.continuous_toFun.comp continuous_fst)
370 (β₂.continuous_toFun.comp continuous_snd)
372/-- The concrete pullback of continuous maps between compact Hausdorff groups is compact. -/
373noncomputable instance TopologicalFiberProduct.compactSpace
374 {H H₁ H₂ : Type u}
375 [Group H] [Group H₁] [Group H₂]
376 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
377 [CompactSpace H₁] [CompactSpace H₂] [T2Space H]
378 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
379 : CompactSpace (TopologicalFiberProduct.carrier β₁ β₂) := by
380 apply isCompact_iff_compactSpace.1
381 simpa [TopologicalFiberProduct.carrier, FiberProduct.carrier] using
382 (pullback_isClosed β₁ β₂).isCompact
384/-- The concrete continuous fiber product has the restricted profinite-source test property. -/
385theorem TopologicalFiberProduct.hasProfiniteTestPullbackProperty
386 {H H₁ H₂ : Type u}
387 [Group H] [Group H₁] [Group H₂]
388 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
389 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
390 HasProfiniteTestPullbackProperty (TopologicalFiberProduct.fst β₁ β₂)
391 (TopologicalFiberProduct.snd β₁ β₂) β₁ β₂ := by
392 refine ⟨?_, ?_⟩
393 · ext x
394 exact x.2
395 · intro K _ _ _ _ _ _ φ₁ φ₂ hφ
396 refine ⟨TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k), ?_, ?_⟩
397 · exact ⟨pullbackFstCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
398 (fun k => DFunLike.congr_fun hφ k),
399 pullbackSndCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
400 (fun k => DFunLike.congr_fun hφ k)⟩
401 · intro ψ hψ
402 have hfst :
403 (TopologicalFiberProduct.fst β₁ β₂).comp ψ =
404 (TopologicalFiberProduct.fst β₁ β₂).comp
405 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
406 calc
407 (TopologicalFiberProduct.fst β₁ β₂).comp ψ = φ₁ := hψ.1
408 _ =
409 (TopologicalFiberProduct.fst β₁ β₂).comp
410 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
411 symm
412 exact pullbackFstCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
413 (fun k => DFunLike.congr_fun hφ k)
414 have hsnd :
415 (TopologicalFiberProduct.snd β₁ β₂).comp ψ =
416 (TopologicalFiberProduct.snd β₁ β₂).comp
417 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
418 calc
419 (TopologicalFiberProduct.snd β₁ β₂).comp ψ = φ₂ := hψ.2
420 _ =
421 (TopologicalFiberProduct.snd β₁ β₂).comp
422 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
423 symm
424 exact pullbackSndCont_pullbackLiftCont β₁ β₂ φ₁ φ₂
425 (fun k => DFunLike.congr_fun hφ k)
426 exact TopologicalFiberProduct.hom_ext
427 (fun k => by
428 exact congrArg (fun f : K →ₜ* H₁ => f k) hfst)
429 (fun k => by
430 exact congrArg (fun f : K →ₜ* H₂ => f k) hsnd)
434/--
435A profinite square with a bijective continuous comparison map to the concrete fiber product has
436the profinite-source test property.
437-/
438theorem hasProfiniteTestPullbackProperty_of_bijective_toConcretePullback
439 {G H H₁ H₂ : Type u}
440 [Group G] [Group H] [Group H₁] [Group H₂]
441 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
442 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
443 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
444 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
445 [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
446 [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
447 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
448 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
449 (τ : G →ₜ* TopologicalFiberProduct.carrier β₁ β₂)
450 (hτ : Function.Bijective τ)
451 (h₁ : (TopologicalFiberProduct.fst β₁ β₂).comp τ = α₁)
452 (h₂ : (TopologicalFiberProduct.snd β₁ β₂).comp τ = α₂) :
453 HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂ := by
454 refine ⟨?_, ?_⟩
455 · ext g
456 have hτ₁ : TopologicalFiberProduct.fst β₁ β₂ (τ g) = α₁ g := by
457 simpa using congrArg (fun f : G →ₜ* H₁ => f g) h₁
458 have hτ₂ : TopologicalFiberProduct.snd β₁ β₂ (τ g) = α₂ g := by
459 simpa using congrArg (fun f : G →ₜ* H₂ => f g) h₂
460 calc
461 β₁ (α₁ g) = β₁ (TopologicalFiberProduct.fst β₁ β₂ (τ g)) := by rw [← hτ₁]
462 _ = β₂ (TopologicalFiberProduct.snd β₁ β₂ (τ g)) := (τ g).2
463 _ = β₂ (α₂ g) := by rw [hτ₂]
464 · intro K _ _ _ _ _ _ φ₁ φ₂ hφ
465 let e : G ≃ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
466 ContinuousMulEquiv.ofBijectiveCompactToT2 τ τ.continuous_toFun hτ
467 let θ : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
468 TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)
469 have hθ₁ : (TopologicalFiberProduct.fst β₁ β₂).comp θ = φ₁ := by
470 ext k
471 rfl
472 have hθ₂ : (TopologicalFiberProduct.snd β₁ β₂).comp θ = φ₂ := by
473 ext k
474 rfl
475 refine ⟨(ContinuousMonoidHom.toContinuousMonoidHom e.symm).comp θ, ?_, ?_⟩
476 · constructor
477 · ext k
478 have hτ₁ : TopologicalFiberProduct.fst β₁ β₂ (τ (e.symm (θ k))) = α₁ (e.symm (θ k)) := by
479 simpa using congrArg (fun f : G →ₜ* H₁ => f (e.symm (θ k))) h₁
480 have hθ₁' : TopologicalFiberProduct.fst β₁ β₂ (θ k) = φ₁ k := by
481 simpa using congrArg (fun f : K →ₜ* H₁ => f k) hθ₁
482 calc
483 α₁ (e.symm (θ k)) = TopologicalFiberProduct.fst β₁ β₂ (τ (e.symm (θ k))) := by
484 simpa using hτ₁.symm
485 _ = TopologicalFiberProduct.fst β₁ β₂ (θ k) := by
486 rw [show τ (e.symm (θ k)) = θ k from e.apply_symm_apply (θ k)]
487 _ = φ₁ k := hθ₁'
488 · ext k
489 have hτ₂ : TopologicalFiberProduct.snd β₁ β₂ (τ (e.symm (θ k))) = α₂ (e.symm (θ k)) := by
490 simpa using congrArg (fun f : G →ₜ* H₂ => f (e.symm (θ k))) h₂
491 have hθ₂' : TopologicalFiberProduct.snd β₁ β₂ (θ k) = φ₂ k := by
492 simpa using congrArg (fun f : K →ₜ* H₂ => f k) hθ₂
493 calc
494 α₂ (e.symm (θ k)) = TopologicalFiberProduct.snd β₁ β₂ (τ (e.symm (θ k))) := by
495 simpa using hτ₂.symm
496 _ = TopologicalFiberProduct.snd β₁ β₂ (θ k) := by
497 rw [show τ (e.symm (θ k)) = θ k from e.apply_symm_apply (θ k)]
498 _ = φ₂ k := hθ₂'
499 · intro ψ hψ
500 have hcoord : τ.comp ψ = θ := by
501 apply TopologicalFiberProduct.hom_ext
502 · intro k
503 have hτ₁ : TopologicalFiberProduct.fst β₁ β₂ (τ (ψ k)) = α₁ (ψ k) := by
504 simpa using congrArg (fun f : G →ₜ* H₁ => f (ψ k)) h₁
505 have hψ₁ : α₁ (ψ k) = φ₁ k := by
506 simpa using congrArg (fun f : K →ₜ* H₁ => f k) hψ.1
507 have hθ₁' : TopologicalFiberProduct.fst β₁ β₂ (θ k) = φ₁ k := by
508 simpa using congrArg (fun f : K →ₜ* H₁ => f k) hθ₁
509 calc
510 TopologicalFiberProduct.fst β₁ β₂ ((τ.comp ψ) k) = α₁ (ψ k) := by
511 simpa using hτ₁
512 _ = φ₁ k := hψ₁
513 _ = TopologicalFiberProduct.fst β₁ β₂ (θ k) := hθ₁'.symm
514 · intro k
515 have hτ₂ : TopologicalFiberProduct.snd β₁ β₂ (τ (ψ k)) = α₂ (ψ k) := by
516 simpa using congrArg (fun f : G →ₜ* H₂ => f (ψ k)) h₂
517 have hψ₂ : α₂ (ψ k) = φ₂ k := by
518 simpa using congrArg (fun f : K →ₜ* H₂ => f k) hψ.2
519 have hθ₂' : TopologicalFiberProduct.snd β₁ β₂ (θ k) = φ₂ k := by
520 simpa using congrArg (fun f : K →ₜ* H₂ => f k) hθ₂
521 calc
522 TopologicalFiberProduct.snd β₁ β₂ ((τ.comp ψ) k) = α₂ (ψ k) := by
523 simpa using hτ₂
524 _ = φ₂ k := hψ₂
525 _ = TopologicalFiberProduct.snd β₁ β₂ (θ k) := hθ₂'.symm
526 ext k
527 apply hτ.1
528 calc
529 τ (ψ k) = (τ.comp ψ) k := by rfl
530 _ = θ k := by
531 exact congrArg (fun f : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ => f k) hcoord
532 _ = τ (((ContinuousMonoidHom.toContinuousMonoidHom e.symm).comp θ) k) := by
533 change θ k = τ (e.symm (θ k))
534 symm
535 exact e.apply_symm_apply (θ k)
538/--
539A continuous multiplicative equivalence with the concrete fiber product transports the
540profinite-source test property.
541-/
542theorem hasProfiniteTestPullbackProperty_of_equiv_toConcretePullback
543 [Group G] [Group H] [Group H₁] [Group H₂]
544 [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
545 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
546 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
547 (e : G ≃ₜ* TopologicalFiberProduct.carrier β₁ β₂)
548 (h₁ : (TopologicalFiberProduct.fst β₁ β₂).comp (ContinuousMonoidHom.toContinuousMonoidHom e)
549 = α₁)
550 (h₂ : (TopologicalFiberProduct.snd β₁ β₂).comp (ContinuousMonoidHom.toContinuousMonoidHom e)
551 = α₂) :
552 HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂ := by
553 refine ⟨?_, ?_⟩
554 · ext g
555 have h₁g : TopologicalFiberProduct.fst β₁ β₂ (e g) = α₁ g := by
556 simpa using congrArg (fun f : G →ₜ* H₁ => f g) h₁
557 have h₂g : TopologicalFiberProduct.snd β₁ β₂ (e g) = α₂ g := by
558 simpa using congrArg (fun f : G →ₜ* H₂ => f g) h₂
559 calc
560 β₁ (α₁ g) = β₁ (TopologicalFiberProduct.fst β₁ β₂ (e g)) := by rw [← h₁g]
561 _ = β₂ (TopologicalFiberProduct.snd β₁ β₂ (e g)) := (e g).2
562 _ = β₂ (α₂ g) := by rw [h₂g]
563 · intro K _ _ _ _ _ _ φ₁ φ₂ hφ
564 let θ : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
565 TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)
566 refine ⟨(ContinuousMonoidHom.toContinuousMonoidHom e.symm).comp θ, ?_, ?_⟩
567 · constructor
568 · ext k
569 have h₁k : TopologicalFiberProduct.fst β₁ β₂ (e (e.symm (θ k))) = α₁ (e.symm (θ k)) := by
570 simpa using congrArg (fun f : G →ₜ* H₁ => f (e.symm (θ k))) h₁
571 calc
572 α₁ (((ContinuousMonoidHom.toContinuousMonoidHom e.symm).comp θ) k) = α₁ (e.symm (θ k))
573 := rfl
574 _ = TopologicalFiberProduct.fst β₁ β₂ (e (e.symm (θ k))) := by
575 simpa using h₁k.symm
576 _ = TopologicalFiberProduct.fst β₁ β₂ (θ k) := by rw [e.apply_symm_apply]
577 _ = φ₁ k := by
578 change
579 TopologicalFiberProduct.fst β₁ β₂
580 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k) =
581 φ₁ k
582 rfl
583 · ext k
584 have h₂k : TopologicalFiberProduct.snd β₁ β₂ (e (e.symm (θ k))) = α₂ (e.symm (θ k)) := by
585 simpa using congrArg (fun f : G →ₜ* H₂ => f (e.symm (θ k))) h₂
586 calc
587 α₂ (((ContinuousMonoidHom.toContinuousMonoidHom e.symm).comp θ) k) = α₂ (e.symm (θ k))
588 := rfl
589 _ = TopologicalFiberProduct.snd β₁ β₂ (e (e.symm (θ k))) := by
590 simpa using h₂k.symm
591 _ = TopologicalFiberProduct.snd β₁ β₂ (θ k) := by rw [e.apply_symm_apply]
592 _ = φ₂ k := by
593 change
594 TopologicalFiberProduct.snd β₁ β₂
595 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k) =
596 φ₂ k
597 rfl
598 · intro ψ hψ
599 have hcoord : (ContinuousMonoidHom.toContinuousMonoidHom e).comp ψ = θ := by
600 apply TopologicalFiberProduct.hom_ext
601 · intro k
602 have h₁ψ : TopologicalFiberProduct.fst β₁ β₂ (e (ψ k)) = α₁ (ψ k) := by
603 simpa using congrArg (fun f : G →ₜ* H₁ => f (ψ k)) h₁
604 have hψ₁ : α₁ (ψ k) = φ₁ k := by
605 simpa using congrArg (fun f : K →ₜ* H₁ => f k) hψ.1
606 calc
607 TopologicalFiberProduct.fst β₁ β₂ (((ContinuousMonoidHom.toContinuousMonoidHom
608 e).comp ψ) k) = α₁ (ψ k) := by
609 simpa using h₁ψ
610 _ = φ₁ k := hψ₁
611 _ = TopologicalFiberProduct.fst β₁ β₂ (θ k) := by
612 change
613 φ₁ k =
614 TopologicalFiberProduct.fst β₁ β₂
615 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k)
616 rfl
617 · intro k
618 have h₂ψ : TopologicalFiberProduct.snd β₁ β₂ (e (ψ k)) = α₂ (ψ k) := by
619 simpa using congrArg (fun f : G →ₜ* H₂ => f (ψ k)) h₂
620 have hψ₂ : α₂ (ψ k) = φ₂ k := by
621 simpa using congrArg (fun f : K →ₜ* H₂ => f k) hψ.2
622 calc
623 TopologicalFiberProduct.snd β₁ β₂ (((ContinuousMonoidHom.toContinuousMonoidHom
624 e).comp ψ) k) = α₂ (ψ k) := by
625 simpa using h₂ψ
626 _ = φ₂ k := hψ₂
627 _ = TopologicalFiberProduct.snd β₁ β₂ (θ k) := by
628 change
629 φ₂ k =
630 TopologicalFiberProduct.snd β₁ β₂
631 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k)
632 rfl
633 ext k
634 apply e.injective
635 calc
636 e (ψ k) = ((ContinuousMonoidHom.toContinuousMonoidHom e).comp ψ) k := by rfl
637 _ = θ k := by
638 exact congrArg (fun f : K →ₜ* TopologicalFiberProduct.carrier β₁ β₂ => f k) hcoord
639 _ = e (e.symm (θ k)) := by rw [e.apply_symm_apply]
641/-- The continuous pullback lift is surjective exactly when the underlying composite kernel is
642contained in the supremum of the two underlying coordinate kernels. -/
643theorem pullbackLiftCont_surjective_iff_ker_comp_le_sup_ker
644 [Group A] [Group H] [Group H₁] [Group H₂]
645 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
646 {β₁ : H₁ →ₜ* H} (β₂ : H₂ →ₜ* H)
647 {φ₁ : A →ₜ* H₁} {φ₂ : A →ₜ* H₂}
648 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
649 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
650 Function.Surjective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂
651 (fun a => DFunLike.congr_fun hcomp a)) ↔
652 ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker ≤
653 ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔
654 ((φ₂ : A →ₜ* H₂).toMonoidHom).ker := by
655 have hcomp' :
656 ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)) =
657 ((β₂ : H₂ →* H).comp (φ₂ : A →* H₂)) := by
658 ext a
659 exact DFunLike.congr_fun hcomp a
660 change
661 Function.Surjective
662 (FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
663 (φ₁ : A →* H₁) (φ₂ : A →* H₂) _) ↔
664 ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)).ker ≤
665 (φ₁ : A →* H₁).ker ⊔ (φ₂ : A →* H₂).ker
666 exact pullbackLift_surjective_iff_ker_comp_le_sup_ker
667 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
668 (φ₁ := (φ₁ : A →* H₁)) (φ₂ := (φ₂ : A →* H₂))
669 hφ₁ hφ₂ hcomp'
671/-- Surjectivity of the continuous pullback lift is equivalent to the required kernel equality. -/
672theorem pullbackLiftCont_surjective_iff_ker_eq
673 [Group A] [Group H] [Group H₁] [Group H₂]
674 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
675 {β₁ : H₁ →ₜ* H} (β₂ : H₂ →ₜ* H)
676 {φ₁ : A →ₜ* H₁} {φ₂ : A →ₜ* H₂}
677 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
678 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
679 Function.Surjective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂
680 (fun a => DFunLike.congr_fun hcomp a)) ↔
681 ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker =
682 ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔
683 ((φ₂ : A →ₜ* H₂).toMonoidHom).ker := by
684 have hcomp' :
685 ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)) =
686 ((β₂ : H₂ →* H).comp (φ₂ : A →* H₂)) := by
687 ext a
688 exact DFunLike.congr_fun hcomp a
689 change
690 Function.Surjective
691 (FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
692 (φ₁ : A →* H₁) (φ₂ : A →* H₂) _) ↔
693 ((β₁ : H₁ →* H).comp (φ₁ : A →* H₁)).ker =
694 (φ₁ : A →* H₁).ker ⊔ (φ₂ : A →* H₂).ker
695 exact pullbackLift_surjective_iff_ker_eq
696 (β₁ := (β₁ : H₁ →* H)) (β₂ := (β₂ : H₂ →* H))
697 (φ₁ := (φ₁ : A →* H₁)) (φ₂ := (φ₂ : A →* H₂))
698 hφ₁ hφ₂ hcomp'
700/-- Surjective continuous coordinate maps whose underlying composite kernel is the supremum of
701their kernels induce a surjective continuous map into the fiber product. -/
702theorem surjective_pullbackLiftCont_of_ker_eq
703 [Group A] [Group H] [Group H₁] [Group H₂]
704 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
705 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
706 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
707 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
708 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
709 (hker : ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker =
710 ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔ ((φ₂ : A →ₜ* H₂).toMonoidHom).ker) :
711 Function.Surjective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
712 exact DFunLike.congr_fun hcomp a)) := by
713 exact (pullbackLiftCont_surjective_iff_ker_eq
714 (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁ hφ₂ hcomp).2 hker
716/--
717The continuous pullback lift is bijective when the left map is injective and the required kernel
718equality holds.
719-/
720theorem bijective_pullbackLiftCont_of_left_injective_of_ker_eq
721 [Group A] [Group H] [Group H₁] [Group H₂]
722 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
723 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
724 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
725 (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
726 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
727 (hker : ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker =
728 ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔ ((φ₂ : A →ₜ* H₂).toMonoidHom).ker)
729 (hφ₁inj : Function.Injective φ₁) :
730 Function.Bijective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
731 exact DFunLike.congr_fun hcomp a)) := by
732 refine ⟨?_, ?_⟩
733 · exact pullbackLiftCont_injective_of_left_injective β₁ β₂ φ₁ φ₂
734 (fun a => DFunLike.congr_fun hcomp a) hφ₁inj
735 · exact surjective_pullbackLiftCont_of_ker_eq β₁ β₂ φ₁ φ₂
736 hφ₁surj hφ₂surj hcomp hker
738/--
739The continuous pullback lift is bijective when the right map is injective and the required
740kernel equality holds.
741-/
742theorem bijective_pullbackLiftCont_of_right_injective_of_ker_eq
743 [Group A] [Group H] [Group H₁] [Group H₂]
744 [TopologicalSpace A] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
745 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
746 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
747 (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
748 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
749 (hker : ((β₁.comp φ₁ : A →ₜ* H).toMonoidHom).ker =
750 ((φ₁ : A →ₜ* H₁).toMonoidHom).ker ⊔ ((φ₂ : A →ₜ* H₂).toMonoidHom).ker)
751 (hφ₂inj : Function.Injective φ₂) :
752 Function.Bijective (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
753 exact DFunLike.congr_fun hcomp a)) := by
754 refine ⟨?_, ?_⟩
755 · exact pullbackLiftCont_injective_of_right_injective β₁ β₂ φ₁ φ₂
756 (fun a => DFunLike.congr_fun hcomp a) hφ₂inj
757 · exact surjective_pullbackLiftCont_of_ker_eq β₁ β₂ φ₁ φ₂
758 hφ₁surj hφ₂surj hcomp hker
760namespace TopologicalFiberProduct
762/-- Composing the first projection with a topological fiber-product lift gives the left map. -/
763@[simp] theorem fst_lift
764 [Group H] [Group H₁] [Group H₂] [Group K]
765 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
766 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
767 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
768 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
769 (fst β₁ β₂).comp (lift β₁ β₂ φ₁ φ₂ h) = φ₁ :=
770 pullbackFstCont_pullbackLiftCont β₁ β₂ φ₁ φ₂ h
772/-- Composing the second projection with a topological fiber-product lift gives the right map. -/
773@[simp] theorem snd_lift
774 [Group H] [Group H₁] [Group H₂] [Group K]
775 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
776 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
777 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
778 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
779 (snd β₁ β₂).comp (lift β₁ β₂ φ₁ φ₂ h) = φ₂ :=
780 pullbackSndCont_pullbackLiftCont β₁ β₂ φ₁ φ₂ h
782/-- The first projection of a lifted element is the value of the first coordinate map. -/
783@[simp] theorem fst_lift_apply
784 [Group H] [Group H₁] [Group H₂] [Group K]
785 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
786 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
787 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
788 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
789 fst β₁ β₂ (lift β₁ β₂ φ₁ φ₂ h k) = φ₁ k :=
790 rfl
792/-- The second projection of a lifted element is the value of the second coordinate map. -/
793@[simp] theorem snd_lift_apply
794 [Group H] [Group H₁] [Group H₂] [Group K]
795 [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace K]
796 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
797 (φ₁ : K →ₜ* H₁) (φ₂ : K →ₜ* H₂)
798 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
799 snd β₁ β₂ (lift β₁ β₂ φ₁ φ₂ h k) = φ₂ k :=
800 rfl
802end TopologicalFiberProduct
804end
808end ProCGroups.Categorical