Source: ProCGroups.Categorical.PullbackComparison
1import ProCGroups.Categorical.ProfinitePullbacks
3/-!
4# Pro C Groups / Categorical / Pullback Comparison
6This module compares a profinite-tested continuous pullback square with its
7concrete fiber product and transports bijectivity and kernel criteria across
8the canonical comparison map.
9-/
11namespace ProCGroups.Categorical
13universe u
15section
17open ContinuousMonoidHom
19variable {G H H₁ H₂ : Type u}
20variable [Group G] [Group H] [Group H₁] [Group H₂]
21variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
22variable
23 [IsTopologicalGroup G] [IsTopologicalGroup H]
24 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
25variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
26variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
27variable [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
28variable [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂]
30/--
31The canonical comparison map from a profinite-tested pullback square to the concrete continuous
32fiber product.
33-/
34def toContinuousPullbackOfIsPullback
35 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
36 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
37 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
38 G →ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
39 TopologicalFiberProduct.lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hpb.1 g)
41omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
42 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
43 [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
44 [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂] in
45/--
46The canonical comparison map from the concrete continuous fiber product to itself is the
47identity.
48-/
49@[simp] theorem toContinuousPullbackOfIsPullback_self
50 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
51 toContinuousPullbackOfIsPullback (TopologicalFiberProduct.fst β₁ β₂)
52 (TopologicalFiberProduct.snd β₁ β₂) β₁ β₂
53 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂) =
54 ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂) := by
55 change
56 TopologicalFiberProduct.lift β₁ β₂ (TopologicalFiberProduct.fst β₁ β₂)
57 (TopologicalFiberProduct.snd β₁ β₂)
58 (fun g => DFunLike.congr_fun (TopologicalFiberProduct.hasProfiniteTestPullbackProperty
59 β₁ β₂).1 g) =
60 ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂)
61 exact pullbackLiftCont_eta (β₁ := β₁) (β₂ := β₂)
62 (ψ := ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂))
64omit [IsTopologicalGroup G] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
65 [IsTopologicalGroup H₂]
66 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
67 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
68 [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
69 [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂] in
70/-- The first coordinate of the canonical comparison map recovers the first leg of the square. -/
71@[simp] theorem TopologicalFiberProduct.fst_toContinuousPullbackOfIsPullback
72 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
73 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
74 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
75 (TopologicalFiberProduct.fst β₁ β₂).comp (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
76 = α₁ := by
77 ext g
78 rfl
80omit [IsTopologicalGroup G] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
81 [IsTopologicalGroup H₂]
82 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
83 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
84 [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
85 [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂] in
86/-- The second coordinate of the canonical comparison map recovers the second leg of the square. -/
87@[simp] theorem TopologicalFiberProduct.snd_toContinuousPullbackOfIsPullback
88 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
89 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
90 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
91 (TopologicalFiberProduct.snd β₁ β₂).comp (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
92 = α₂ := by
93 ext g
94 rfl
96/--
97The canonical inverse comparison map from the concrete continuous fiber product to a
98profinite-tested pullback square.
99-/
100noncomputable def fromContinuousPullbackOfIsPullback
101 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
102 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
103 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
104 TopologicalFiberProduct.carrier β₁ β₂ →ₜ* G :=
105 pullbackDescCont hpb
106 (TopologicalFiberProduct.fst β₁ β₂)
107 (TopologicalFiberProduct.snd β₁ β₂)
108 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1
110omit [IsTopologicalGroup G] [IsTopologicalGroup H]
111 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
112 [CompactSpace H] [TotallyDisconnectedSpace H] in
113/-- Specification of the inverse comparison map from the concrete pullback. -/
114theorem fromContinuousPullbackOfIsPullback_spec
115 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
116 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
117 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
118 α₁.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
119 TopologicalFiberProduct.fst β₁ β₂ ∧
120 α₂.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
121 TopologicalFiberProduct.snd β₁ β₂ := by
122 change
123 α₁.comp
124 (pullbackDescCont hpb
125 (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
126 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1) =
127 TopologicalFiberProduct.fst β₁ β₂ ∧
128 α₂.comp
129 (pullbackDescCont hpb
130 (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
131 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1) =
132 TopologicalFiberProduct.snd β₁ β₂
133 exact pullbackDescCont_spec hpb
134 (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
135 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1
137omit [IsTopologicalGroup G] [IsTopologicalGroup H]
138 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
139 [CompactSpace H] [TotallyDisconnectedSpace H] in
140/-- Uniqueness of the inverse comparison map from the concrete pullback. -/
141theorem fromContinuousPullbackOfIsPullback_uniq
142 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
143 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
144 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
145 {ψ : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* G}
146 (hψ : α₁.comp ψ = TopologicalFiberProduct.fst β₁ β₂ ∧ α₂.comp ψ =
147 TopologicalFiberProduct.snd β₁ β₂) :
148 ψ = fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb := by
149 simpa [fromContinuousPullbackOfIsPullback] using
150 (pullbackDescCont_uniq hpb
151 (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
152 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1
153 (ψ := ψ) hψ)
155omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in
156/-- Composing the inverse comparison map with the canonical map gives the identity. -/
157theorem fromContinuousPullback_comp_toContinuousPullbackOfIsPullback
158 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
159 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
160 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
161 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
162 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
163 ContinuousMonoidHom.id G := by
164 have hdesc :
165 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
166 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
167 pullbackDescCont hpb α₁ α₂ hpb.1 := by
168 apply pullbackDescCont_uniq hpb α₁ α₂ hpb.1
169 constructor
170 · ext g
171 calc
172 α₁ ((fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
173 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) g)
174 = TopologicalFiberProduct.fst β₁ β₂
175 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g) := by
176 simpa using congrArg
177 (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₁ =>
178 f (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g))
179 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hpb).1
180 _ = α₁ g := by
181 rfl
182 · ext g
183 calc
184 α₂ ((fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
185 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) g)
186 = TopologicalFiberProduct.snd β₁ β₂
187 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g) := by
188 simpa using congrArg
189 (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₂ =>
190 f (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g))
191 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hpb).2
192 _ = α₂ g := by
193 rfl
194 have hself :
195 pullbackDescCont hpb α₁ α₂ hpb.1 = ContinuousMonoidHom.id G := by
196 symm
197 exact pullbackDescCont_uniq hpb α₁ α₂ hpb.1
198 (ψ := ContinuousMonoidHom.id G) (by
199 constructor <;> ext g <;> rfl)
200 exact hdesc.trans hself
202omit [IsTopologicalGroup G] [IsTopologicalGroup H]
203 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
204 [CompactSpace H] [TotallyDisconnectedSpace H] in
205/-- Composing the canonical map with the inverse comparison map gives the identity. -/
206theorem toContinuousPullback_comp_fromContinuousPullbackOfIsPullback
207 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
208 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
209 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
210 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
211 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
212 ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂) := by
213 apply TopologicalFiberProduct.hom_ext
214 · intro x
215 calc
216 TopologicalFiberProduct.fst β₁ β₂
217 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
218 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) x)
219 = α₁ (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb x) := by
220 rfl
221 _ = TopologicalFiberProduct.fst β₁ β₂ x := by
222 simpa using congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₁ => f x)
223 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hpb).1
224 · intro x
225 calc
226 TopologicalFiberProduct.snd β₁ β₂
227 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
228 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) x)
229 = α₂ (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb x) := by
230 rfl
231 _ = TopologicalFiberProduct.snd β₁ β₂ x := by
232 simpa using congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₂ => f x)
233 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hpb).2
235omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in
236/-- Pointwise left-inverse formula for the canonical comparison maps. -/
237@[simp] theorem fromContinuousPullbackOfIsPullback_toContinuousPullbackOfIsPullback_apply
238 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
239 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
240 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (g : G) :
241 fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
242 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g) = g := by
243 simpa using congrArg (fun f : G →ₜ* G => f g)
244 (fromContinuousPullback_comp_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
246omit [IsTopologicalGroup G] [IsTopologicalGroup H]
247 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
248 [CompactSpace H] [TotallyDisconnectedSpace H] in
249/-- Pointwise right-inverse formula for the canonical comparison maps. -/
250@[simp] theorem toContinuousPullbackOfIsPullback_fromContinuousPullbackOfIsPullback_apply
251 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
252 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
253 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (x : TopologicalFiberProduct.carrier β₁
254 β₂) :
255 toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
256 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb x) = x := by
257 simpa using congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ*
258 TopologicalFiberProduct.carrier β₁ β₂ => f x)
259 (toContinuousPullback_comp_fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
261omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in
262/-- The canonical comparison map from a profinite-tested pullback square is bijective. -/
263theorem bijective_toContinuousPullbackOfIsPullback
264 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
265 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
266 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
267 Function.Bijective (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) := by
268 have hleft :
269 Function.LeftInverse
270 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
271 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) := by
272 intro g
273 exact fromContinuousPullbackOfIsPullback_toContinuousPullbackOfIsPullback_apply
274 α₁ α₂ β₁ β₂ hpb g
275 have hright :
276 Function.RightInverse
277 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
278 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) := by
279 intro x
280 exact toContinuousPullbackOfIsPullback_fromContinuousPullbackOfIsPullback_apply
281 α₁ α₂ β₁ β₂ hpb x
282 exact ⟨hleft.injective, hright.surjective⟩
285omit [IsTopologicalGroup G] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
286 [IsTopologicalGroup H₂]
287 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
288 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
289 [CompactSpace H₁] [T2Space H₁] [TotallyDisconnectedSpace H₁]
290 [CompactSpace H₂] [T2Space H₂] [TotallyDisconnectedSpace H₂] in
291/--
292The canonical comparison map sends the chosen pullback descent map to the concrete continuous
293pullback lift.
294-/
295@[simp 900] theorem toContinuousPullbackOfIsPullback_comp_pullbackDescCont
296 {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
297 [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
298 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
299 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
300 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
301 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
302 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
303 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
304 (pullbackDescCont hpb φ₁ φ₂ hφ) =
305 TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a) := by
306 apply TopologicalFiberProduct.hom_ext
307 · intro a
308 have hleft :
309 (TopologicalFiberProduct.fst β₁ β₂).comp
310 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
311 (pullbackDescCont hpb φ₁ φ₂ hφ)) = φ₁ := by
312 calc
313 (TopologicalFiberProduct.fst β₁ β₂).comp
314 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
315 (pullbackDescCont hpb φ₁ φ₂ hφ)) =
316 ((TopologicalFiberProduct.fst β₁ β₂).comp
317 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)).comp
318 (pullbackDescCont hpb φ₁ φ₂ hφ) := by
319 rfl
320 _ = α₁.comp (pullbackDescCont hpb φ₁ φ₂ hφ) := by
321 rw [TopologicalFiberProduct.fst_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb]
322 _ = φ₁ := pullbackDescCont_left hpb φ₁ φ₂ hφ
323 have hright :
324 (TopologicalFiberProduct.fst β₁ β₂).comp
325 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)) = φ₁ :=
326 TopologicalFiberProduct.fst_lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)
327 exact congrArg (fun f : A →ₜ* H₁ => f a) (hleft.trans hright.symm)
328 · intro a
329 have hleft :
330 (TopologicalFiberProduct.snd β₁ β₂).comp
331 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
332 (pullbackDescCont hpb φ₁ φ₂ hφ)) = φ₂ := by
333 calc
334 (TopologicalFiberProduct.snd β₁ β₂).comp
335 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
336 (pullbackDescCont hpb φ₁ φ₂ hφ)) =
337 ((TopologicalFiberProduct.snd β₁ β₂).comp
338 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)).comp
339 (pullbackDescCont hpb φ₁ φ₂ hφ) := by
340 rfl
341 _ = α₂.comp (pullbackDescCont hpb φ₁ φ₂ hφ) := by
342 rw [TopologicalFiberProduct.snd_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb]
343 _ = φ₂ := pullbackDescCont_right hpb φ₁ φ₂ hφ
344 have hright :
345 (TopologicalFiberProduct.snd β₁ β₂).comp
346 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)) = φ₂ :=
347 TopologicalFiberProduct.snd_lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)
348 exact congrArg (fun f : A →ₜ* H₂ => f a) (hleft.trans hright.symm)
350omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in
351/-- Surjective coordinate maps whose underlying composite kernel is the supremum of their kernels
352induce a surjective descent map for a profinite-tested pullback square. -/
353theorem surjective_pullbackDescCont_of_ker_eq
354 {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
355 [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
356 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
357 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
358 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
359 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
360 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
361 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
362 (hker : (β₁.comp φ₁).toMonoidHom.ker = φ₁.toMonoidHom.ker ⊔ φ₂.toMonoidHom.ker) :
363 Function.Surjective (pullbackDescCont hpb φ₁ φ₂ hcomp) := by
364 have hbij : Function.Bijective (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) :=
365 bijective_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
366 have hsurjLift :
367 Function.Surjective
368 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hcomp a)) :=
369 surjective_pullbackLiftCont_of_ker_eq β₁ β₂ φ₁ φ₂ hφ₁ hφ₂ hcomp hker
370 intro g
371 let z : TopologicalFiberProduct.carrier β₁ β₂ := toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂
372 hpb g
373 rcases hsurjLift z with ⟨a, ha⟩
374 refine ⟨a, ?_⟩
375 apply hbij.1
376 calc
377 toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb (pullbackDescCont hpb φ₁ φ₂ hcomp a)
378 = TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hcomp k) a := by
379 exact congrArg (fun f : A →ₜ* TopologicalFiberProduct.carrier β₁ β₂ => f a)
380 (toContinuousPullbackOfIsPullback_comp_pullbackDescCont
381 α₁ α₂ β₁ β₂ hpb φ₁ φ₂ hcomp)
382 _ = z := ha
383 _ = toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g := rfl
385/--
386Any profinite-tested pullback square is canonically isomorphic to the concrete continuous fiber
387product.
388-/
389noncomputable def pullbackContEquivOfIsPullback
390 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
391 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
392 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
393 G ≃ₜ* TopologicalFiberProduct.carrier β₁ β₂ where
394 toMulEquiv :=
395 { toFun := toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
396 invFun := fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
397 left_inv := by
398 intro g
399 exact congrArg (fun f : G →ₜ* G => f g)
400 (fromContinuousPullback_comp_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
401 right_inv := by
402 intro x
403 exact congrArg
404 (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* TopologicalFiberProduct.carrier β₁
405 β₂ => f x)
406 (toContinuousPullback_comp_fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
407 map_mul' := by
408 intro x y
409 exact (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).map_mul x y }
410 continuous_toFun := (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).continuous_toFun
411 continuous_invFun :=
412 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).continuous_toFun
414omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in
415/--
416Forgetting continuity from the inverse of the canonical pullback equivalence recovers the
417inverse comparison map.
418-/
419@[simp] theorem pullbackContEquivOfIsPullback_symm_toContinuousMonoidHom
420 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
421 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
422 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
423 (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
424 hpb).symm) =
425 fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb := by
426 rfl
429omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in
430/-- The first coordinate of the canonical pullback equivalence recovers \(\alpha_1\). -/
431@[simp] theorem pullbackContEquivOfIsPullback_fst
432 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
433 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
434 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
435 (TopologicalFiberProduct.fst β₁ β₂).comp
436 (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
437 hpb)) =
438 α₁ := by
439 rfl
441omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in
442/-- The second coordinate of the canonical pullback equivalence recovers \(\alpha_2\). -/
443@[simp] theorem pullbackContEquivOfIsPullback_snd
444 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
445 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
446 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
447 (TopologicalFiberProduct.snd β₁ β₂).comp
448 (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
449 hpb)) =
450 α₂ := by
451 rfl
453omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in
454/-- Pointwise first-coordinate formula for the inverse of the canonical pullback equivalence. -/
455@[simp 900] theorem pullbackContEquivOfIsPullback_symm_fst_apply
456 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
457 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
458 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (x : TopologicalFiberProduct.carrier β₁
459 β₂) :
460 α₁ ((pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hpb).symm x) =
461 TopologicalFiberProduct.fst β₁ β₂ x := by
462 have hfst :
463 α₁.comp
464 (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
465 hpb).symm) =
466 TopologicalFiberProduct.fst β₁ β₂ := by
467 calc
468 α₁.comp
469 (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
470 hpb).symm) =
471 α₁.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) := by
472 rw [pullbackContEquivOfIsPullback_symm_toContinuousMonoidHom]
473 _ = TopologicalFiberProduct.fst β₁ β₂ := by
474 simpa using
475 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hpb).1
476 exact congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₁ => f x) hfst
478omit [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] in
479/-- Pointwise second-coordinate formula for the inverse of the canonical pullback equivalence. -/
480@[simp 900] theorem pullbackContEquivOfIsPullback_symm_snd_apply
481 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
482 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
483 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (x : TopologicalFiberProduct.carrier β₁
484 β₂) :
485 α₂ ((pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hpb).symm x) =
486 TopologicalFiberProduct.snd β₁ β₂ x := by
487 have hsnd :
488 α₂.comp
489 (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
490 hpb).symm) =
491 TopologicalFiberProduct.snd β₁ β₂ := by
492 calc
493 α₂.comp
494 (ContinuousMonoidHom.toContinuousMonoidHom (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂
495 hpb).symm) =
496 α₂.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) := by
497 rw [pullbackContEquivOfIsPullback_symm_toContinuousMonoidHom]
498 _ = TopologicalFiberProduct.snd β₁ β₂ := by
499 simpa using
500 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hpb).2
501 exact congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₂ => f x) hsnd
503omit [IsTopologicalGroup H] in
504/-- A commutative square has the universal property against profinite source groups if and only if
505its canonical comparison map to the concrete continuous fiber product is bijective. -/
506theorem hasProfiniteTestPullbackProperty_iff_bijective_toConcretePullback
507 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
508 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
509 (hcomm : β₁.comp α₁ = β₂.comp α₂) :
510 HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂ ↔
511 Function.Bijective
512 (TopologicalFiberProduct.lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g)) := by
513 constructor
514 · intro hpb
515 simpa [toContinuousPullbackOfIsPullback] using
516 (bijective_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)
517 · intro hbij
518 exact hasProfiniteTestPullbackProperty_of_bijective_toConcretePullback
519 α₁ α₂ β₁ β₂
520 (TopologicalFiberProduct.lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
521 hbij
522 (TopologicalFiberProduct.fst_lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
523 (TopologicalFiberProduct.snd_lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
525end
528end ProCGroups.Categorical