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

ProCGroups/Categorical/PullbackComparison.lean

1import ProCGroups.Categorical.ProfinitePullbacks
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/Categorical/PullbackComparison.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Pullbacks, pushouts, and quotient comparison
14Concrete algebraic and topological pullbacks and pushouts of groups and profinite groups, with comparison maps, universal properties, kernel criteria, and quotient pullback equivalences.
15-/
17namespace ProCGroups.Categorical
19universe u
21section
23open ContinuousMonoidHom
25variable {G H H₁ H₂ : Type u}
26variable [Group G] [Group H] [Group H₁] [Group H₂]
27variable [TopologicalSpace G] [TopologicalSpace H] [TopologicalSpace H₁] [TopologicalSpace H₂]
28variable
29 [IsTopologicalGroup G] [IsTopologicalGroup H]
30 [IsTopologicalGroup H₁] [IsTopologicalGroup H₂]
32/--
33Canonical comparison map from an abstract profinite pullback square to the concrete
34pullback.
35-/
37 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
38 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
39 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
40 G →ₜ* TopologicalFiberProduct.carrier β₁ β₂ :=
41 TopologicalFiberProduct.lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hpb.1 g)
43omit [IsTopologicalGroup H] [IsTopologicalGroup H₁] [IsTopologicalGroup H₂] in
44/-- The canonical comparison map from the concrete profinite pullback to itself is the identity. -/
46 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H) :
47 toContinuousPullbackOfIsPullback (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂) β₁ β₂
48 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂) =
49 ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂) := by
50 change
51 TopologicalFiberProduct.lift β₁ β₂ (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
52 (fun g => DFunLike.congr_fun (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1 g) =
53 ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂)
54 exact pullbackLiftCont_eta (β₁ := β₁) (β₂ := β₂)
55 (ψ := ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂))
57omit [IsTopologicalGroup G] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
58 [IsTopologicalGroup H₂] in
59/--
60The first coordinate of the canonical comparison map recovers the first leg of the square.
61-/
62@[simp] theorem TopologicalFiberProduct.fst_toContinuousPullbackOfIsPullback
63 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
64 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
65 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
66 (TopologicalFiberProduct.fst β₁ β₂).comp (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) = α₁ := by
67 ext g
68 rfl
70omit [IsTopologicalGroup G] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
71 [IsTopologicalGroup H₂] in
72/--
73The second coordinate of the canonical comparison map recovers the second leg of the
74square.
75-/
76@[simp] theorem TopologicalFiberProduct.snd_toContinuousPullbackOfIsPullback
77 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
78 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
79 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
80 (TopologicalFiberProduct.snd β₁ β₂).comp (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) = α₂ := by
81 ext g
82 rfl
84/--
85Canonical inverse comparison map from the concrete pullback to an abstract profinite
86pullback square.
87-/
89 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
90 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
91 (hH₁ : IsProfiniteGroup H₁)
92 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
93 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
94 TopologicalFiberProduct.carrier β₁ β₂ →ₜ* G :=
96 (TopologicalFiberProduct.isProfiniteGroup β₁ β₂ hH₁ hH₂ hH)
97 (TopologicalFiberProduct.fst β₁ β₂)
98 (TopologicalFiberProduct.snd β₁ β₂)
99 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1
101omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
102/-- Specification of the inverse comparison map from the concrete pullback. -/
104 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
105 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
106 (hH₁ : IsProfiniteGroup H₁)
107 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
108 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
109 α₁.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb) =
110 TopologicalFiberProduct.fst β₁ β₂ ∧
111 α₂.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb) =
112 TopologicalFiberProduct.snd β₁ β₂ := by
113 change
114 α₁.comp
116 (TopologicalFiberProduct.isProfiniteGroup β₁ β₂ hH₁ hH₂ hH)
117 (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
118 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1) =
119 TopologicalFiberProduct.fst β₁ β₂ ∧
120 α₂.comp
122 (TopologicalFiberProduct.isProfiniteGroup β₁ β₂ hH₁ hH₂ hH)
123 (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
124 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1) =
125 TopologicalFiberProduct.snd β₁ β₂
127 (TopologicalFiberProduct.isProfiniteGroup β₁ β₂ hH₁ hH₂ hH)
128 (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
129 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1
131omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
132/-- Uniqueness of the inverse comparison map from the concrete pullback. -/
134 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
135 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
136 (hH₁ : IsProfiniteGroup H₁)
137 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
138 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
139 {ψ : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* G}
140 (hψ : α₁.comp ψ = TopologicalFiberProduct.fst β₁ β₂ ∧ α₂.comp ψ = TopologicalFiberProduct.snd β₁ β₂) :
141 ψ = fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb := by
144 (TopologicalFiberProduct.isProfiniteGroup β₁ β₂ hH₁ hH₂ hH)
145 (TopologicalFiberProduct.fst β₁ β₂) (TopologicalFiberProduct.snd β₁ β₂)
146 (TopologicalFiberProduct.hasProfiniteTestPullbackProperty β₁ β₂).1
147 (ψ := ψ) hψ)
149omit [IsTopologicalGroup H] in
150/-- The inverse comparison map composed with the canonical map is the identity. -/
152 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
153 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
154 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
155 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
156 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
157 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).comp
158 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
159 ContinuousMonoidHom.id G := by
160 have hdesc :
161 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).comp
162 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) =
163 pullbackDescCont hpb hG α₁ α₂ hpb.1 := by
164 apply pullbackDescCont_uniq hpb hG α₁ α₂ hpb.1
165 constructor
166 · ext g
167 calc
168 α₁ ((fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).comp
169 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) g)
170 = TopologicalFiberProduct.fst β₁ β₂
171 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g) := by
172 simpa using congrArg
173 (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₁ =>
174 f (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g))
175 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).1
176 _ = α₁ g := by
177 rfl
178 · ext g
179 calc
180 α₂ ((fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).comp
181 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) g)
182 = TopologicalFiberProduct.snd β₁ β₂
183 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g) := by
184 simpa using congrArg
185 (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₂ =>
186 f (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g))
187 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).2
188 _ = α₂ g := by
189 rfl
190 have hself :
191 pullbackDescCont hpb hG α₁ α₂ hpb.1 = ContinuousMonoidHom.id G := by
192 symm
193 exact pullbackDescCont_uniq hpb hG α₁ α₂ hpb.1
194 (ψ := ContinuousMonoidHom.id G) (by
195 constructor <;> ext g <;> rfl)
196 exact hdesc.trans hself
198omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
199/-- The canonical map composed with the inverse comparison map is the identity. -/
201 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
202 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
203 (hH₁ : IsProfiniteGroup H₁)
204 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
205 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
206 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
207 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb) =
208 ContinuousMonoidHom.id (TopologicalFiberProduct.carrier β₁ β₂) := by
209 apply TopologicalFiberProduct.hom_ext
210 · intro x
211 calc
212 TopologicalFiberProduct.fst β₁ β₂
213 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
214 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb) x)
215 = α₁ (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb x) := by
216 rfl
217 _ = TopologicalFiberProduct.fst β₁ β₂ x := by
218 simpa using congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₁ => f x)
219 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).1
220 · intro x
221 calc
222 TopologicalFiberProduct.snd β₁ β₂
223 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
224 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb) x)
225 = α₂ (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb x) := by
226 rfl
227 _ = TopologicalFiberProduct.snd β₁ β₂ x := by
228 simpa using congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₂ => f x)
229 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).2
231omit [IsTopologicalGroup H] in
232/-- Pointwise left-inverse formula for the canonical comparison maps. -/
234 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
235 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
236 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
237 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
238 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (g : G) :
239 fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb
240 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g) = g := by
241 simpa using congrArg (fun f : G →ₜ* G => f g)
242 (fromContinuousPullback_comp_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb)
244omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
245/-- Pointwise right-inverse formula for the canonical comparison maps. -/
247 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
248 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
249 (hH₁ : IsProfiniteGroup H₁)
250 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
251 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (x : TopologicalFiberProduct.carrier β₁ β₂) :
252 toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
253 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb x) = x := by
254 simpa using congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* TopologicalFiberProduct.carrier β₁ β₂ => f x)
255 (toContinuousPullback_comp_fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb)
257omit [IsTopologicalGroup H] in
258/-- The canonical comparison map from an abstract profinite pullback square is bijective. -/
260 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
261 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
262 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
263 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
264 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
265 Function.Bijective (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) := by
266 have hleft :
267 Function.LeftInverse
268 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb)
269 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) := by
270 intro g
272 α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb g
273 have hright :
274 Function.RightInverse
275 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb)
276 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) := by
277 intro x
279 α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb x
280 exact ⟨hleft.injective, hright.surjective⟩
283omit [IsTopologicalGroup G] [IsTopologicalGroup H] [IsTopologicalGroup H₁]
284 [IsTopologicalGroup H₂] in
285/-- The canonical comparison map sends the chosen pullback descent map to the concrete
286continuous pullback lift. -/
288 {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
289 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
290 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
291 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
293 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
294 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
295 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
296 (pullbackDescCont hpb hA φ₁ φ₂ hφ) =
297 TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a) := by
298 apply TopologicalFiberProduct.hom_ext
299 · intro a
300 have hleft :
301 (TopologicalFiberProduct.fst β₁ β₂).comp
302 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
303 (pullbackDescCont hpb hA φ₁ φ₂ hφ)) = φ₁ := by
304 calc
305 (TopologicalFiberProduct.fst β₁ β₂).comp
306 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
307 (pullbackDescCont hpb hA φ₁ φ₂ hφ)) =
308 ((TopologicalFiberProduct.fst β₁ β₂).comp
309 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)).comp
310 (pullbackDescCont hpb hA φ₁ φ₂ hφ) := by
311 rfl
312 _ = α₁.comp (pullbackDescCont hpb hA φ₁ φ₂ hφ) := by
313 rw [TopologicalFiberProduct.fst_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb]
314 _ = φ₁ := pullbackDescCont_left hpb hA φ₁ φ₂ hφ
315 have hright :
316 (TopologicalFiberProduct.fst β₁ β₂).comp
317 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)) = φ₁ :=
318 TopologicalFiberProduct.fst_lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)
319 exact congrArg (fun f : A →ₜ* H₁ => f a) (hleft.trans hright.symm)
320 · intro a
321 have hleft :
322 (TopologicalFiberProduct.snd β₁ β₂).comp
323 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
324 (pullbackDescCont hpb hA φ₁ φ₂ hφ)) = φ₂ := by
325 calc
326 (TopologicalFiberProduct.snd β₁ β₂).comp
327 ((toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).comp
328 (pullbackDescCont hpb hA φ₁ φ₂ hφ)) =
329 ((TopologicalFiberProduct.snd β₁ β₂).comp
330 (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb)).comp
331 (pullbackDescCont hpb hA φ₁ φ₂ hφ) := by
332 rfl
333 _ = α₂.comp (pullbackDescCont hpb hA φ₁ φ₂ hφ) := by
334 rw [TopologicalFiberProduct.snd_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb]
335 _ = φ₂ := pullbackDescCont_right hpb hA φ₁ φ₂ hφ
336 have hright :
337 (TopologicalFiberProduct.snd β₁ β₂).comp
338 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)) = φ₂ :=
339 TopologicalFiberProduct.snd_lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hφ a)
340 exact congrArg (fun f : A →ₜ* H₂ => f a) (hleft.trans hright.symm)
342omit [IsTopologicalGroup H] in
343/-- Exact abstract-pullback form of the continuous surjectivity criterion. -/
345 {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
346 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
347 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
349 (hH₁ : IsProfiniteGroup H₁)
350 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
351 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂)
352 (φ₁ : A →ₜ* H₁) (φ₂ : A →ₜ* H₂)
353 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
354 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
355 (hker : (β₁.comp φ₁).toMonoidHom.ker = φ₁.toMonoidHom.ker ⊔ φ₂.toMonoidHom.ker) :
356 Function.Surjective (pullbackDescCont hpb hA φ₁ φ₂ hcomp) := by
357 have hbij : Function.Bijective (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb) :=
358 bijective_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb
359 have hsurjLift :
360 Function.Surjective
361 (TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hcomp a)) :=
362 surjective_pullbackLiftCont_of_ker_eq β₁ β₂ φ₁ φ₂ hφ₁ hφ₂ hcomp hker
363 intro g
364 let z : TopologicalFiberProduct.carrier β₁ β₂ := toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g
365 rcases hsurjLift z with ⟨a, ha⟩
366 refine ⟨a, ?_⟩
367 apply hbij.1
368 calc
369 toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb (pullbackDescCont hpb hA φ₁ φ₂ hcomp a)
370 = TopologicalFiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hcomp k) a := by
371 exact congrArg (fun f : A →ₜ* TopologicalFiberProduct.carrier β₁ β₂ => f a)
373 α₁ α₂ β₁ β₂ hpb hA φ₁ φ₂ hcomp)
374 _ = z := ha
375 _ = toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb g := rfl
377/-- Any profinite pullback square is canonically isomorphic to the concrete pullback. -/
379 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
380 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
381 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
382 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
383 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
384 G ≃ₜ* TopologicalFiberProduct.carrier β₁ β₂ where
385 toMulEquiv :=
386 { toFun := toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb
387 invFun := fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb
388 left_inv := by
389 intro g
390 exact congrArg (fun f : G →ₜ* G => f g)
391 (fromContinuousPullback_comp_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb)
392 right_inv := by
393 intro x
394 exact congrArg
395 (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* TopologicalFiberProduct.carrier β₁ β₂ => f x)
396 (toContinuousPullback_comp_fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb)
397 map_mul' := by
398 intro x y
399 exact (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).map_mul x y }
400 continuous_toFun := (toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hpb).continuous_toFun
401 continuous_invFun :=
402 (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).continuous_toFun
404omit [IsTopologicalGroup H] in
405/-- Forgetting continuity from the inverse of the canonical pullback equivalence recovers the
406inverse comparison map. -/
408 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
409 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
410 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
411 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
412 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
413 (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb).symm.toContinuousMonoidHom =
414 fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb := by
415 rfl
418omit [IsTopologicalGroup H] in
419/-- The first coordinate of the canonical pullback equivalence recovers `α₁`. -/
421 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
422 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
423 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
424 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
425 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
426 (TopologicalFiberProduct.fst β₁ β₂).comp
427 (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb).toContinuousMonoidHom =
428 α₁ := by
429 rfl
431omit [IsTopologicalGroup H] in
432/-- The second coordinate of the canonical pullback equivalence recovers `α₂`. -/
434 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
435 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
436 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
437 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
438 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) :
439 (TopologicalFiberProduct.snd β₁ β₂).comp
440 (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb).toContinuousMonoidHom =
441 α₂ := by
442 rfl
444omit [IsTopologicalGroup H] in
445/--
446Pointwise first-coordinate formula for the inverse of the canonical pullback equivalence.
447-/
449 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
450 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
451 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
452 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
453 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (x : TopologicalFiberProduct.carrier β₁ β₂) :
454 α₁ ((pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb).symm x) =
455 TopologicalFiberProduct.fst β₁ β₂ x := by
456 have hfst :
457 α₁.comp
458 (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb).symm.toContinuousMonoidHom =
459 TopologicalFiberProduct.fst β₁ β₂ := by
460 calc
461 α₁.comp
462 (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb).symm.toContinuousMonoidHom =
463 α₁.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb) := by
465 _ = TopologicalFiberProduct.fst β₁ β₂ := by
466 simpa using
467 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).1
468 exact congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₁ => f x) hfst
470omit [IsTopologicalGroup H] in
471/--
472Pointwise second-coordinate formula for the inverse of the canonical pullback equivalence.
473-/
475 (α₁ : G →ₜ* H₁) (α₂ : G →ₜ* H₂)
476 (β₁ : H₁ →ₜ* H) (β₂ : H₂ →ₜ* H)
477 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
478 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
479 (hpb : HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂) (x : TopologicalFiberProduct.carrier β₁ β₂) :
480 α₂ ((pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb).symm x) =
481 TopologicalFiberProduct.snd β₁ β₂ x := by
482 have hsnd :
483 α₂.comp
484 (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb).symm.toContinuousMonoidHom =
485 TopologicalFiberProduct.snd β₁ β₂ := by
486 calc
487 α₂.comp
488 (pullbackContEquivOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb).symm.toContinuousMonoidHom =
489 α₂.comp (fromContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb) := by
491 _ = TopologicalFiberProduct.snd β₁ β₂ := by
492 simpa using
493 (fromContinuousPullbackOfIsPullback_spec α₁ α₂ β₁ β₂ hH₁ hH₂ hH hpb).2
494 exact congrArg (fun f : TopologicalFiberProduct.carrier β₁ β₂ →ₜ* H₂ => f x) hsnd
496omit [IsTopologicalGroup H] in
497/-- A profinite square is a pullback iff its canonical comparison map to the concrete pullback is
498bijective. -/
500 {α₁ : G →ₜ* H₁} {α₂ : G →ₜ* H₂}
501 {β₁ : H₁ →ₜ* H} {β₂ : H₂ →ₜ* H}
502 (hG : IsProfiniteGroup G) (hH₁ : IsProfiniteGroup H₁)
503 (hH₂ : IsProfiniteGroup H₂) (hH : IsProfiniteGroup H)
504 (hcomm : β₁.comp α₁ = β₂.comp α₂) :
505 HasProfiniteTestPullbackProperty α₁ α₂ β₁ β₂ ↔
506 Function.Bijective
507 (TopologicalFiberProduct.lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g)) := by
508 constructor
509 · intro hpb
511 (bijective_toContinuousPullbackOfIsPullback α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH hpb)
512 · intro hbij
514 α₁ α₂ β₁ β₂ hG hH₁ hH₂ hH
515 (TopologicalFiberProduct.lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
516 hbij
517 (TopologicalFiberProduct.fst_lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
518 (TopologicalFiberProduct.snd_lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
520end
523end ProCGroups.Categorical