ProCGroups/Categorical/AlgebraicPullbacks.lean
1import Mathlib.Algebra.Category.Grp.Limits
2import Mathlib.GroupTheory.QuotientGroup.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Categorical/AlgebraicPullbacks.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Pullbacks, pushouts, and quotient comparison
15Concrete algebraic and topological pullbacks and pushouts of groups and profinite groups, with comparison maps, universal properties, kernel criteria, and quotient pullback equivalences.
16-/
18namespace ProCGroups.Categorical
20open CategoryTheory Limits
21open scoped Pointwise
23universe u v
25section
27variable {A G H H₁ H₂ : Type u} {K : Type v}
28variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]
30/-- Concrete pullback subgroup of `β₁` and `β₂`.
31-/
32def FiberProduct.subgroup (β₁ : H₁ →* H) (β₂ : H₂ →* H) : Subgroup (H₁ × H₂) where
33 carrier := { x | β₁ x.1 = β₂ x.2 }
35 mul_mem' := by
36 intro x y hx hy
37 change β₁ x.1 = β₂ x.2 at hx
38 change β₁ y.1 = β₂ y.2 at hy
40 inv_mem' := by
41 intro x hx
42 simpa [map_inv, hx]
44/-- Concrete pullback attached to `β₁` and `β₂`.
45-/
46abbrev FiberProduct.carrier (β₁ : H₁ →* H) (β₂ : H₂ →* H) :=
47 ↥(FiberProduct.subgroup β₁ β₂)
49/-- Membership criterion for the concrete pullback subgroup. -/
50@[simp] theorem mem_pullbackSubgroup_iff {β₁ : H₁ →* H} {β₂ : H₂ →* H}
51 {x : H₁ × H₂} :
52 x ∈ FiberProduct.subgroup β₁ β₂ ↔ β₁ x.1 = β₂ x.2 :=
53 Iff.rfl
55/-- The first projection from the concrete pullback. -/
56def FiberProduct.fst (β₁ : H₁ →* H) (β₂ : H₂ →* H) : FiberProduct.carrier β₁ β₂ →* H₁ where
57 toFun := fun x => x.1.1
58 map_one' := rfl
59 map_mul' := by
60 intro x y
61 rfl
63/-- The second projection from the concrete pullback. -/
64def FiberProduct.snd (β₁ : H₁ →* H) (β₂ : H₂ →* H) : FiberProduct.carrier β₁ β₂ →* H₂ where
65 toFun := fun x => x.1.2
66 map_one' := rfl
67 map_mul' := by
68 intro x y
69 rfl
71/-- The canonical homomorphism into the concrete pullback. -/
72def FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
73 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
74 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) : K →* FiberProduct.carrier β₁ β₂ where
75 toFun := fun k => ⟨(φ₁ k, φ₂ k), h k⟩
76 map_one' := by
77 apply Subtype.ext
79 map_mul' := by
80 intro x y
81 apply Subtype.ext
84/-- The canonical pullback lift evaluates coordinatewise. -/
85@[simp] theorem pullbackLift_apply (β₁ : H₁ →* H) (β₂ : H₂ →* H)
86 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
87 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
88 FiberProduct.lift β₁ β₂ φ₁ φ₂ h k = ⟨(φ₁ k, φ₂ k), h k⟩ :=
89 rfl
91/-- The first coordinate of the canonical pullback lift. -/
92@[simp] theorem pullbackFst_pullbackLift_apply (β₁ : H₁ →* H) (β₂ : H₂ →* H)
93 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
94 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
95 FiberProduct.fst β₁ β₂ (FiberProduct.lift β₁ β₂ φ₁ φ₂ h k) = φ₁ k :=
96 rfl
98/-- The second coordinate of the canonical pullback lift. -/
99@[simp] theorem pullbackSnd_pullbackLift_apply (β₁ : H₁ →* H) (β₂ : H₂ →* H)
100 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
101 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
102 FiberProduct.snd β₁ β₂ (FiberProduct.lift β₁ β₂ φ₁ φ₂ h k) = φ₂ k :=
103 rfl
105/-- The concrete group pullback as a categorical pullback cone in `GrpCat`. -/
106def FiberProduct.cone (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
107 PullbackCone (GrpCat.ofHom β₁) (GrpCat.ofHom β₂) :=
108 PullbackCone.mk
109 (GrpCat.ofHom (FiberProduct.fst β₁ β₂))
110 (GrpCat.ofHom (FiberProduct.snd β₁ β₂))
111 (by
112 apply GrpCat.hom_ext
113 ext x
114 exact x.2)
116/-- The concrete group pullback cone is a limit cone in `GrpCat`. -/
117def FiberProduct.isLimitCone (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
118 IsLimit (FiberProduct.cone β₁ β₂) := by
119 refine PullbackCone.IsLimit.mk (by
120 apply GrpCat.hom_ext
121 ext x
123 · intro s
124 exact GrpCat.ofHom <|
125 FiberProduct.lift β₁ β₂ s.fst.hom s.snd.hom (fun x => by
126 have hcondition :
127 (s.fst ≫ GrpCat.ofHom β₁).hom =
128 (s.snd ≫ GrpCat.ofHom β₂).hom :=
129 congrArg (fun f : s.pt ⟶ GrpCat.of H => f.hom) s.condition
130 exact DFunLike.congr_fun hcondition x)
131 · intro s
132 apply GrpCat.hom_ext
133 rfl
134 · intro s
135 apply GrpCat.hom_ext
136 rfl
137 · intro s m hfst hsnd
138 apply GrpCat.hom_ext
139 ext x
140 · have hfst' :
141 (m ≫ GrpCat.ofHom (FiberProduct.fst β₁ β₂)).hom = s.fst.hom :=
142 congrArg (fun f : s.pt ⟶ GrpCat.of H₁ => f.hom) hfst
143 exact DFunLike.congr_fun hfst' x
144 · have hsnd' :
145 (m ≫ GrpCat.ofHom (FiberProduct.snd β₁ β₂)).hom = s.snd.hom :=
146 congrArg (fun f : s.pt ⟶ GrpCat.of H₂ => f.hom) hsnd
147 exact DFunLike.congr_fun hsnd' x
149/-- The kernel of the canonical map into a concrete pullback is the intersection of the two
150coordinate kernels. -/
151@[simp] theorem ker_pullbackLift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
152 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
153 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
155 ext k
156 change FiberProduct.lift β₁ β₂ φ₁ φ₂ h k = 1 ↔ φ₁ k = 1 ∧ φ₂ k = 1
157 constructor
158 · intro hk
159 exact ⟨congrArg (fun z => FiberProduct.fst β₁ β₂ z) hk,
160 congrArg (fun z => FiberProduct.snd β₁ β₂ z) hk⟩
161 · rintro ⟨h₁, h₂⟩
162 apply Subtype.ext
163 exact Prod.ext h₁ h₂
165/-- The canonical map into a concrete pullback is injective exactly when the coordinate kernels
166intersect trivially. -/
167theorem pullbackLift_injective_iff (β₁ : H₁ →* H) (β₂ : H₂ →* H)
168 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
169 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
170 Function.Injective (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) ↔ φ₁.ker ⊓ φ₂.ker = ⊥ := by
171 rw [← MonoidHom.ker_eq_bot_iff, ker_pullbackLift]
173/-- The sum of the coordinate kernels is always contained in the kernel of the common composite. -/
175 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
176 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
177 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
179 rw [sup_le_iff]
180 constructor
181 · intro k hk
182 change β₁ (φ₁ k) = 1
183 have hk' : φ₁ k = 1 := by simpa using hk
185 · intro k hk
186 calc
187 β₁ (φ₁ k) = β₂ (φ₂ k) := DFunLike.congr_fun hcomp k
188 _ = 1 := by
189 have hk' : φ₂ k = 1 := by simpa using hk
192/-- The standard kernel condition for surjectivity onto a pullback. -/
194 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
195 (φ₁ : K →* H₁) (φ₂ : K →* H₂) : Prop :=
198/-- The compatibility equality contained in `HasPullbackKernelCriterion`. -/
199theorem HasPullbackKernelCriterion.comp_eq
200 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
201 {φ₁ : K →* H₁} {φ₂ : K →* H₂}
202 (h : HasPullbackKernelCriterion β₁ β₂ φ₁ φ₂) :
203 β₁.comp φ₁ = β₂.comp φ₂ :=
204 h.1
206/-- The kernel equality contained in `HasPullbackKernelCriterion`. -/
207theorem HasPullbackKernelCriterion.ker_eq
208 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
209 {φ₁ : K →* H₁} {φ₂ : K →* H₂}
210 (h : HasPullbackKernelCriterion β₁ β₂ φ₁ φ₂) :
212 h.2
214/-- The canonical map into a concrete pullback is surjective exactly when the composite kernel is
215contained in the sum of the coordinate kernels. -/
217 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
218 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
219 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
220 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
221 Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂
222 (fun k => DFunLike.congr_fun hcomp k)) ↔
224 constructor
225 · intro hsurj k hk
226 let z : FiberProduct.carrier β₁ β₂ :=
227 ⟨(φ₁ k, 1), by
228 change β₁ (φ₁ k) = β₂ 1
229 simpa using hk⟩
230 rcases hsurj z with ⟨a, ha⟩
231 have hφ₁a : φ₁ a = φ₁ k := by
232 exact congrArg (fun y => FiberProduct.fst β₁ β₂ y) ha
233 have hφ₂a : φ₂ a = 1 := by
234 exact congrArg (fun y => FiberProduct.snd β₁ β₂ y) ha
235 have ha_ker₂ : a ∈ φ₂.ker := by
236 simpa using hφ₂a
237 have ha_inv_mul_ker₁ : a⁻¹ * k ∈ φ₁.ker := by
238 change φ₁ (a⁻¹ * k) = 1
240 have hprod : a * (a⁻¹ * k) ∈ φ₁.ker ⊔ φ₂.ker :=
241 (φ₁.ker ⊔ φ₂.ker).mul_mem
242 ((le_sup_right : φ₂.ker ≤ φ₁.ker ⊔ φ₂.ker) ha_ker₂)
243 ((le_sup_left : φ₁.ker ≤ φ₁.ker ⊔ φ₂.ker) ha_inv_mul_ker₁)
244 simpa [mul_assoc] using hprod
245 · intro hker_le z
246 rcases hφ₁ z.1.1 with ⟨a₁, ha₁⟩
247 rcases hφ₂ z.1.2 with ⟨a₂, ha₂⟩
248 have hEq : β₁ (φ₁ a₁) = β₁ (φ₁ a₂) := by
249 calc
250 β₁ (φ₁ a₁) = β₁ z.1.1 := by simp only [ha₁]
251 _ = β₂ z.1.2 := z.2
252 _ = β₂ (φ₂ a₂) := by simp only [ha₂]
253 _ = β₁ (φ₁ a₂) := by
254 exact (DFunLike.congr_fun hcomp a₂).symm
256 change β₁ (φ₁ (a₁ * a₂⁻¹)) = 1
258 have hgjoin : a₁ * a₂⁻¹ ∈ (φ₁.ker : Subgroup K) ⊔ (φ₂.ker : Subgroup K) :=
259 hker_le hgker
260 have hgjoin' : a₁ * a₂⁻¹ ∈ ((φ₁.ker : Set K) * (φ₂.ker : Set K)) := by
261 rw [← Subgroup.mul_normal (φ₁.ker) (φ₂.ker)]
262 simpa [SetLike.mem_coe] using hgjoin
263 rcases (show ∃ y ∈ (φ₁.ker : Set K), ∃ z ∈ (φ₂.ker : Set K),
264 y * z = a₁ * a₂⁻¹ from by
265 simpa [Set.mem_mul] using hgjoin') with ⟨k₁, hk₁, k₂, hk₂, hkprod⟩
266 have hk₁' : φ₁ k₁ = 1 := by simpa using hk₁
267 have hk₂' : φ₂ k₂ = 1 := by simpa using hk₂
268 have haeq : a₁ = k₁ * k₂ * a₂ := by
269 calc
270 a₁ = (a₁ * a₂⁻¹) * a₂ := by simp only [mul_assoc, inv_mul_cancel, mul_one]
271 _ = (k₁ * k₂) * a₂ := by rw [hkprod]
272 _ = k₁ * k₂ * a₂ := by simp only [mul_assoc]
273 refine ⟨k₂ * a₂, ?_⟩
274 apply Subtype.ext
275 apply Prod.ext
276 · calc
277 φ₁ (k₂ * a₂) = φ₁ (k₁ * k₂ * a₂) := by
279 _ = φ₁ a₁ := by rw [haeq]
280 _ = z.1.1 := ha₁
281 · calc
283 _ = 1 * φ₂ a₂ := by simp only [hk₂', one_mul]
284 _ = z.1.2 := by simp only [ha₂, one_mul]
286/-- The canonical map into a concrete pullback is surjective exactly when the composite kernel is
287the sum of the coordinate kernels. -/
289 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
290 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
291 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
292 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
293 Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂
294 (fun k => DFunLike.congr_fun hcomp k)) ↔
296 constructor
297 · intro hsurj
298 exact le_antisymm
300 β₁ β₂ φ₁ φ₂ hφ₁ hφ₂ hcomp).1 hsurj)
301 (ker_sup_le_ker_comp_of_comp_eq β₁ β₂ φ₁ φ₂ hcomp)
302 · intro hker
304 β₁ β₂ φ₁ φ₂ hφ₁ hφ₂ hcomp).2 (by
305 intro k hk
306 rw [← hker]
307 exact hk)
309/-- The named kernel criterion gives surjectivity of the canonical map into the pullback. -/
311 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
312 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
313 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
314 (hcrit : HasPullbackKernelCriterion β₁ β₂ φ₁ φ₂) :
315 Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂
316 (fun k => DFunLike.congr_fun hcrit.comp_eq k)) := by
318 β₁ β₂ φ₁ φ₂ hφ₁ hφ₂ hcrit.comp_eq).2 hcrit.ker_eq
320/-- The first projection composed with the canonical pullback lift is `φ₁`. -/
321@[simp] theorem pullbackFst_pullbackLift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
322 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
323 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
324 (FiberProduct.fst β₁ β₂).comp (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₁ := by
325 ext k
326 rfl
328/-- The second projection composed with the canonical pullback lift is `φ₂`. -/
329@[simp] theorem pullbackSnd_pullbackLift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
330 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
331 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
332 (FiberProduct.snd β₁ β₂).comp (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₂ := by
333 ext k
334 rfl
336/-- If `φ₁` is injective, then the canonical map into the concrete pullback is injective. -/
337theorem pullbackLift_injective_of_left_injective (β₁ : H₁ →* H) (β₂ : H₂ →* H)
338 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
339 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
340 (hφ₁ : Function.Injective φ₁) :
341 Function.Injective (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) := by
342 intro x y hxy
343 apply hφ₁
344 simpa using congrArg (fun z => FiberProduct.fst β₁ β₂ z) hxy
346/-- If `φ₂` is injective, then the canonical map into the concrete pullback is injective. -/
347theorem pullbackLift_injective_of_right_injective (β₁ : H₁ →* H) (β₂ : H₂ →* H)
348 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
349 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))
350 (hφ₂ : Function.Injective φ₂) :
351 Function.Injective (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) := by
352 intro x y hxy
353 apply hφ₂
354 simpa using congrArg (fun z => FiberProduct.snd β₁ β₂ z) hxy
356/-- FiberProduct.carrier squares in the category of groups.
357-/
358def IsPullbackSquare (α₁ : G →* H₁) (α₂ : G →* H₂)
359 (β₁ : H₁ →* H) (β₂ : H₂ →* H) : Prop :=
360 β₁.comp α₁ = β₂.comp α₂ ∧
361 ∀ ⦃K : Type v⦄ [Group K] (φ₁ : K →* H₁) (φ₂ : K →* H₂),
362 β₁.comp φ₁ = β₂.comp φ₂ →
363 ∃! φ : K →* G, α₁.comp φ = φ₁ ∧ α₂.comp φ = φ₂
365/-- A commutative square of groups as a categorical pullback cone in `GrpCat`. -/
366def groupPullbackSquareCone (α₁ : G →* H₁) (α₂ : G →* H₂)
367 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
368 (hcomm : β₁.comp α₁ = β₂.comp α₂) :
369 PullbackCone (GrpCat.ofHom β₁) (GrpCat.ofHom β₂) :=
370 PullbackCone.mk (GrpCat.ofHom α₁) (GrpCat.ofHom α₂) (by
371 apply GrpCat.hom_ext
372 exact hcomm)
374/-- Chosen morphism induced by the pullback universal property. -/
375noncomputable def IsPullbackSquare.desc
376 {α₁ : G →* H₁} {α₂ : G →* H₂}
377 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
378 {K : Type v} [Group K]
379 (hpb : IsPullbackSquare α₁ α₂ β₁ β₂)
380 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
381 (hφ : β₁.comp φ₁ = β₂.comp φ₂) : K →* G :=
382 Classical.choose (ExistsUnique.exists (hpb.2 φ₁ φ₂ hφ))
384/-- Specification of the chosen pullback descent map. -/
385theorem IsPullbackSquare.desc_spec
386 {α₁ : G →* H₁} {α₂ : G →* H₂}
387 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
388 {K : Type v} [Group K]
389 (hpb : IsPullbackSquare α₁ α₂ β₁ β₂)
390 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
391 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
392 α₁.comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ) = φ₁ ∧
393 α₂.comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ) = φ₂ :=
394 Classical.choose_spec (ExistsUnique.exists (hpb.2 φ₁ φ₂ hφ))
396/-- Left composite of the chosen pullback descent map. -/
397@[simp 900] theorem IsPullbackSquare.desc_left
398 {α₁ : G →* H₁} {α₂ : G →* H₂}
399 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
400 {K : Type v} [Group K]
401 (hpb : IsPullbackSquare α₁ α₂ β₁ β₂)
402 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
403 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
404 α₁.comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ) = φ₁ :=
405 (IsPullbackSquare.desc_spec hpb φ₁ φ₂ hφ).1
407/-- Right composite of the chosen pullback descent map. -/
408@[simp 900] theorem IsPullbackSquare.desc_right
409 {α₁ : G →* H₁} {α₂ : G →* H₂}
410 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
411 {K : Type v} [Group K]
412 (hpb : IsPullbackSquare α₁ α₂ β₁ β₂)
413 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
414 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
415 α₂.comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ) = φ₂ :=
416 (IsPullbackSquare.desc_spec hpb φ₁ φ₂ hφ).2
418/-- Uniqueness of the chosen pullback descent map. -/
419theorem IsPullbackSquare.desc_uniq
420 {α₁ : G →* H₁} {α₂ : G →* H₂}
421 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
422 {K : Type v} [Group K]
423 (hpb : IsPullbackSquare α₁ α₂ β₁ β₂)
424 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
425 (hφ : β₁.comp φ₁ = β₂.comp φ₂)
426 {ψ : K →* G}
427 (hψ : α₁.comp ψ = φ₁ ∧ α₂.comp ψ = φ₂) :
428 ψ = IsPullbackSquare.desc hpb φ₁ φ₂ hφ := by
429 rcases hpb.2 φ₁ φ₂ hφ with ⟨u, hu, huuniq⟩
430 have hψ' : ψ = u := huuniq _ hψ
431 have hdesc : IsPullbackSquare.desc hpb φ₁ φ₂ hφ = u :=
432 huuniq _ (IsPullbackSquare.desc_spec hpb φ₁ φ₂ hφ)
433 exact hψ'.trans hdesc.symm
435/-- The hand-written group pullback property gives a categorical `IsLimit` cone in `GrpCat`. -/
436noncomputable def isLimit_groupPullbackSquareCone_of_isPullbackSquare
437 {α₁ : G →* H₁} {α₂ : G →* H₂}
438 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
439 (hpb : IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂) :
440 IsLimit (groupPullbackSquareCone α₁ α₂ β₁ β₂ hpb.1) := by
441 refine PullbackCone.IsLimit.mk (by
442 apply GrpCat.hom_ext
444 · intro s
445 exact GrpCat.ofHom <|
446 IsPullbackSquare.desc hpb s.fst.hom s.snd.hom (by
447 exact congrArg (fun f : s.pt ⟶ GrpCat.of H => f.hom) s.condition)
448 · intro s
449 apply GrpCat.hom_ext
450 exact IsPullbackSquare.desc_left hpb s.fst.hom s.snd.hom
451 (by exact congrArg (fun f : s.pt ⟶ GrpCat.of H => f.hom) s.condition)
452 · intro s
453 apply GrpCat.hom_ext
454 exact IsPullbackSquare.desc_right hpb s.fst.hom s.snd.hom
455 (by exact congrArg (fun f : s.pt ⟶ GrpCat.of H => f.hom) s.condition)
456 · intro s m hfst hsnd
457 apply GrpCat.hom_ext
458 apply IsPullbackSquare.desc_uniq hpb s.fst.hom s.snd.hom
459 (by exact congrArg (fun f : s.pt ⟶ GrpCat.of H => f.hom) s.condition)
460 constructor
461 · exact congrArg (fun f : s.pt ⟶ GrpCat.of H₁ => f.hom) hfst
462 · exact congrArg (fun f : s.pt ⟶ GrpCat.of H₂ => f.hom) hsnd
464/-- A categorical `IsLimit` cone in `GrpCat` gives the hand-written group pullback property. -/
465noncomputable def isPullbackSquare_of_isLimit_groupPullbackSquareCone
466 {α₁ : G →* H₁} {α₂ : G →* H₂}
467 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
468 (hcomm : β₁.comp α₁ = β₂.comp α₂)
469 (hlim : IsLimit (groupPullbackSquareCone α₁ α₂ β₁ β₂ hcomm)) :
470 IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂ := by
471 refine ⟨hcomm, ?_⟩
472 intro K _ φ₁ φ₂ hφ
473 let s : PullbackCone (GrpCat.ofHom β₁) (GrpCat.ofHom β₂) :=
474 PullbackCone.mk (GrpCat.ofHom φ₁) (GrpCat.ofHom φ₂) (by
475 apply GrpCat.hom_ext
476 exact hφ)
477 let φ : K →* G := (PullbackCone.IsLimit.lift hlim (GrpCat.ofHom φ₁)
478 (GrpCat.ofHom φ₂) (by
479 apply GrpCat.hom_ext
480 exact hφ)).hom
481 refine ⟨φ, ?_, ?_⟩
482 · constructor
483 · exact congrArg (fun f : GrpCat.of K ⟶ GrpCat.of H₁ => f.hom)
484 (PullbackCone.IsLimit.lift_fst hlim (GrpCat.ofHom φ₁) (GrpCat.ofHom φ₂) (by
485 apply GrpCat.hom_ext
486 exact hφ))
487 · exact congrArg (fun f : GrpCat.of K ⟶ GrpCat.of H₂ => f.hom)
488 (PullbackCone.IsLimit.lift_snd hlim (GrpCat.ofHom φ₁) (GrpCat.ofHom φ₂) (by
489 apply GrpCat.hom_ext
490 exact hφ))
491 · intro ψ hψ
492 exact congrArg (fun f : GrpCat.of K ⟶ GrpCat.of G => f.hom) <| by
493 change GrpCat.ofHom ψ =
494 PullbackCone.IsLimit.lift hlim (GrpCat.ofHom φ₁) (GrpCat.ofHom φ₂) (by
495 apply GrpCat.hom_ext
496 exact hφ)
497 apply PullbackCone.IsLimit.hom_ext hlim
498 · apply GrpCat.hom_ext
499 calc
500 (GrpCat.ofHom ψ ≫ (groupPullbackSquareCone α₁ α₂ β₁ β₂ hcomm).fst).hom =
501 α₁.comp ψ := rfl
502 _ = φ₁ := hψ.1
503 _ = (GrpCat.ofHom φ₁).hom := rfl
504 _ =
505 (PullbackCone.IsLimit.lift hlim (GrpCat.ofHom φ₁) (GrpCat.ofHom φ₂) (by
506 apply GrpCat.hom_ext
507 exact hφ) ≫
508 (groupPullbackSquareCone α₁ α₂ β₁ β₂ hcomm).fst).hom := by
509 symm
510 exact congrArg (fun f : GrpCat.of K ⟶ GrpCat.of H₁ => f.hom)
511 (PullbackCone.IsLimit.lift_fst hlim (GrpCat.ofHom φ₁) (GrpCat.ofHom φ₂)
512 (by
513 apply GrpCat.hom_ext
514 exact hφ))
515 · apply GrpCat.hom_ext
516 calc
517 (GrpCat.ofHom ψ ≫ (groupPullbackSquareCone α₁ α₂ β₁ β₂ hcomm).snd).hom =
518 α₂.comp ψ := rfl
519 _ = φ₂ := hψ.2
520 _ = (GrpCat.ofHom φ₂).hom := rfl
521 _ =
522 (PullbackCone.IsLimit.lift hlim (GrpCat.ofHom φ₁) (GrpCat.ofHom φ₂) (by
523 apply GrpCat.hom_ext
524 exact hφ) ≫
525 (groupPullbackSquareCone α₁ α₂ β₁ β₂ hcomm).snd).hom := by
526 symm
527 exact congrArg (fun f : GrpCat.of K ⟶ GrpCat.of H₂ => f.hom)
528 (PullbackCone.IsLimit.lift_snd hlim (GrpCat.ofHom φ₁) (GrpCat.ofHom φ₂)
529 (by
530 apply GrpCat.hom_ext
531 exact hφ))
533/-- Same-universe hand-written group pullback squares are exactly categorical limit cones in
534`GrpCat`, up to the choice of `IsLimit` data. -/
536 {α₁ : G →* H₁} {α₂ : G →* H₂}
537 {β₁ : H₁ →* H} {β₂ : H₂ →* H}
538 (hcomm : β₁.comp α₁ = β₂.comp α₂) :
539 IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂ ↔
540 Nonempty (IsLimit (groupPullbackSquareCone α₁ α₂ β₁ β₂ hcomm)) := by
541 constructor
542 · intro hpb
544 · rintro ⟨hlim⟩
545 exact isPullbackSquare_of_isLimit_groupPullbackSquareCone hcomm hlim
547/-- Two homomorphisms into the concrete pullback are equal once both coordinates agree. -/
548theorem FiberProduct.hom_ext {β₁ : H₁ →* H} {β₂ : H₂ →* H}
549 {K : Type v} [Group K]
550 {ψ ψ' : K →* FiberProduct.carrier β₁ β₂}
551 (h₁ : ∀ k, FiberProduct.fst β₁ β₂ (ψ k) = FiberProduct.fst β₁ β₂ (ψ' k))
552 (h₂ : ∀ k, FiberProduct.snd β₁ β₂ (ψ k) = FiberProduct.snd β₁ β₂ (ψ' k)) :
553 ψ = ψ' := by
554 apply MonoidHom.ext
555 intro k
556 exact Subtype.ext <| Prod.ext (h₁ k) (h₂ k)
558namespace FiberProduct
560/-- Transport a concrete fiber product across equal cospan maps. -/
561def congr {β₁ β₁' : H₁ →* H} {β₂ β₂' : H₂ →* H}
562 (h₁ : β₁ = β₁') (h₂ : β₂ = β₂') :
563 carrier β₁ β₂ ≃* carrier β₁' β₂' := by
564 subst β₁'
565 subst β₂'
566 exact MulEquiv.refl _
568/-- The first projection composed with a fiber-product lift is the left map. -/
569@[simp 900] theorem fst_lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
570 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
571 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
572 (fst β₁ β₂).comp (lift β₁ β₂ φ₁ φ₂ h) = φ₁ :=
573 pullbackFst_pullbackLift β₁ β₂ φ₁ φ₂ h
575/-- The second projection composed with a fiber-product lift is the right map. -/
576@[simp 900] theorem snd_lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)
577 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
578 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :
579 (snd β₁ β₂).comp (lift β₁ β₂ φ₁ φ₂ h) = φ₂ :=
580 pullbackSnd_pullbackLift β₁ β₂ φ₁ φ₂ h
582@[simp 900] theorem fst_lift_apply (β₁ : H₁ →* H) (β₂ : H₂ →* H)
583 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
584 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
585 fst β₁ β₂ (lift β₁ β₂ φ₁ φ₂ h k) = φ₁ k :=
586 rfl
588@[simp 900] theorem snd_lift_apply (β₁ : H₁ →* H) (β₂ : H₂ →* H)
589 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
590 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) (k : K) :
591 snd β₁ β₂ (lift β₁ β₂ φ₁ φ₂ h k) = φ₂ k :=
592 rfl
594end FiberProduct
596/-- The concrete pullback is reconstructed from its two projections by the canonical lift. -/
597@[simp 900] theorem pullbackLift_eta {β₁ : H₁ →* H} {β₂ : H₂ →* H}
598 {K : Type v} [Group K]
599 (ψ : K →* FiberProduct.carrier β₁ β₂) :
600 FiberProduct.lift β₁ β₂
601 ((FiberProduct.fst β₁ β₂).comp ψ)
602 ((FiberProduct.snd β₁ β₂).comp ψ)
603 (fun k => by exact (ψ k).2) = ψ := by
604 apply FiberProduct.hom_ext
605 · intro k
606 rfl
607 · intro k
608 rfl
610/-- The concrete pullback satisfies the pullback universal property.
611-/
612theorem pullback_isPullback (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
613 IsPullbackSquare (FiberProduct.fst β₁ β₂) (FiberProduct.snd β₁ β₂) β₁ β₂ := by
614 refine ⟨?_, ?_⟩
615 · ext x
616 exact x.2
617 · intro K _ φ₁ φ₂ hφ
618 let hφfun : ∀ k : K, β₁ (φ₁ k) = β₂ (φ₂ k) := fun k =>
619 DFunLike.congr_fun hφ k
620 refine ⟨FiberProduct.lift (K := K) β₁ β₂ φ₁ φ₂ hφfun, ?_, ?_⟩
621 · exact ⟨pullbackFst_pullbackLift (K := K) β₁ β₂ φ₁ φ₂ hφfun,
622 pullbackSnd_pullbackLift (K := K) β₁ β₂ φ₁ φ₂ hφfun⟩
623 · intro ψ hψ
624 have hfst :
625 (FiberProduct.fst β₁ β₂).comp ψ =
626 (FiberProduct.fst β₁ β₂).comp
627 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
628 calc
629 (FiberProduct.fst β₁ β₂).comp ψ = φ₁ := hψ.1
630 _ =
631 (FiberProduct.fst β₁ β₂).comp
632 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
633 symm
634 exact pullbackFst_pullbackLift β₁ β₂ φ₁ φ₂
635 (fun k => DFunLike.congr_fun hφ k)
636 have hsnd :
637 (FiberProduct.snd β₁ β₂).comp ψ =
638 (FiberProduct.snd β₁ β₂).comp
639 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
640 calc
641 (FiberProduct.snd β₁ β₂).comp ψ = φ₂ := hψ.2
642 _ =
643 (FiberProduct.snd β₁ β₂).comp
644 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) := by
645 symm
646 exact pullbackSnd_pullbackLift β₁ β₂ φ₁ φ₂
647 (fun k => DFunLike.congr_fun hφ k)
648 exact FiberProduct.hom_ext
649 (fun k => by
650 exact congrArg (fun f : K →* H₁ => f k) hfst)
651 (fun k => by
652 exact congrArg (fun f : K →* H₂ => f k) hsnd)
654/-- Symmetry of the concrete pullback. -/
655def pullbackSwap (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
656 FiberProduct.carrier β₁ β₂ ≃* FiberProduct.carrier β₂ β₁ where
657 toFun := fun x => ⟨(x.1.2, x.1.1), x.2.symm⟩
658 invFun := fun x => ⟨(x.1.2, x.1.1), x.2.symm⟩
659 left_inv := by
660 intro x
661 apply Subtype.ext
662 rfl
663 right_inv := by
664 intro x
665 apply Subtype.ext
666 rfl
667 map_mul' := by
668 intro x y
669 apply Subtype.ext
670 rfl
672/-- The first projection after swapping equals the original second projection. -/
673@[simp] theorem pullbackFst_pullbackSwap (β₁ : H₁ →* H) (β₂ : H₂ →* H)
674 (x : FiberProduct.carrier β₁ β₂) :
675 FiberProduct.fst β₂ β₁ (pullbackSwap β₁ β₂ x) = FiberProduct.snd β₁ β₂ x :=
676 rfl
678/-- The second projection after swapping equals the original first projection. -/
679@[simp] theorem pullbackSnd_pullbackSwap (β₁ : H₁ →* H) (β₂ : H₂ →* H)
680 (x : FiberProduct.carrier β₁ β₂) :
681 FiberProduct.snd β₂ β₁ (pullbackSwap β₁ β₂ x) = FiberProduct.fst β₁ β₂ x :=
682 rfl
684/-- The symmetry equivalence is involutive. -/
685@[simp] theorem pullbackSwap_symm (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
686 (pullbackSwap β₁ β₂).symm = pullbackSwap β₂ β₁ :=
687 rfl
689/-- If `β₂` is surjective, then the first pullback projection is surjective. -/
691 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
692 (hβ₂ : Function.Surjective β₂) :
693 Function.Surjective (FiberProduct.fst β₁ β₂) := by
694 intro x
695 rcases hβ₂ (β₁ x) with ⟨y, hy⟩
696 refine ⟨⟨(x, y), ?_⟩, rfl⟩
697 simp only [mem_pullbackSubgroup_iff, hy]
699/-- If `β₁` is surjective, then the second pullback projection is surjective. -/
701 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
702 (hβ₁ : Function.Surjective β₁) :
703 Function.Surjective (FiberProduct.snd β₁ β₂) := by
704 intro y
705 rcases hβ₁ (β₂ y) with ⟨x, hx⟩
706 refine ⟨⟨(x, y), ?_⟩, rfl⟩
707 simp only [mem_pullbackSubgroup_iff, hx]
709/-- If `β₂` is injective, then the first pullback projection is injective. -/
711 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
712 (hβ₂ : Function.Injective β₂) :
713 Function.Injective (FiberProduct.fst β₁ β₂) := by
714 intro x y hxy
715 apply Subtype.ext
716 exact Prod.ext hxy <| hβ₂ <| by
717 calc
718 β₂ x.1.2 = β₁ x.1.1 := x.2.symm
719 _ = β₁ y.1.1 := by simpa using congrArg β₁ hxy
720 _ = β₂ y.1.2 := y.2
722/-- If `β₁` is injective, then the second pullback projection is injective. -/
724 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
725 (hβ₁ : Function.Injective β₁) :
726 Function.Injective (FiberProduct.snd β₁ β₂) := by
727 intro x y hxy
728 apply Subtype.ext
729 exact Prod.ext (hβ₁ <| by
730 calc
731 β₁ x.1.1 = β₂ x.1.2 := x.2
732 _ = β₂ y.1.2 := by simpa using congrArg β₂ hxy
733 _ = β₁ y.1.1 := y.2.symm) hxy
735/-- A square with a bijective comparison map to the concrete pullback is a pullback square. -/
737 (α₁ : G →* H₁) (α₂ : G →* H₂) (β₁ : H₁ →* H) (β₂ : H₂ →* H)
738 (τ : G →* FiberProduct.carrier β₁ β₂)
739 (hτ : Function.Bijective τ)
740 (h₁ : (FiberProduct.fst β₁ β₂).comp τ = α₁)
741 (h₂ : (FiberProduct.snd β₁ β₂).comp τ = α₂) :
742 IsPullbackSquare α₁ α₂ β₁ β₂ := by
743 classical
744 refine ⟨?_, ?_⟩
745 · ext g
746 have hτ₁ : FiberProduct.fst β₁ β₂ (τ g) = α₁ g := by
747 simpa using congrArg (fun f : G →* H₁ => f g) h₁
748 have hτ₂ : FiberProduct.snd β₁ β₂ (τ g) = α₂ g := by
749 simpa using congrArg (fun f : G →* H₂ => f g) h₂
750 calc
751 β₁ (α₁ g) = β₁ (FiberProduct.fst β₁ β₂ (τ g)) := by rw [← hτ₁]
752 _ = β₂ (FiberProduct.snd β₁ β₂ (τ g)) := (τ g).2
753 _ = β₂ (α₂ g) := by rw [hτ₂]
754 · intro K _ φ₁ φ₂ hφ
755 let e : G ≃* FiberProduct.carrier β₁ β₂ := MulEquiv.ofBijective τ hτ
756 let hφfun : ∀ k : K, β₁ (φ₁ k) = β₂ (φ₂ k) := fun k =>
757 DFunLike.congr_fun hφ k
758 let θ : K →* FiberProduct.carrier β₁ β₂ :=
759 FiberProduct.lift (K := K) β₁ β₂ φ₁ φ₂ hφfun
760 refine ⟨e.symm.toMonoidHom.comp θ, ?_, ?_⟩
761 · constructor
762 · ext k
763 have hτ₁ : FiberProduct.fst β₁ β₂ (τ (e.symm (θ k))) = α₁ (e.symm (θ k)) := by
764 simpa using congrArg (fun f : G →* H₁ => f (e.symm (θ k))) h₁
765 calc
766 α₁ (e.symm (θ k)) = FiberProduct.fst β₁ β₂ (τ (e.symm (θ k))) := by
767 simpa using hτ₁.symm
768 _ = FiberProduct.fst β₁ β₂ (θ k) := by
769 rw [show τ (e.symm (θ k)) = θ k from e.apply_symm_apply (θ k)]
770 _ = φ₁ k := by
771 change
772 FiberProduct.fst β₁ β₂
773 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k) = φ₁ k
774 rfl
775 · ext k
776 have hτ₂ : FiberProduct.snd β₁ β₂ (τ (e.symm (θ k))) = α₂ (e.symm (θ k)) := by
777 simpa using congrArg (fun f : G →* H₂ => f (e.symm (θ k))) h₂
778 calc
779 α₂ (e.symm (θ k)) = FiberProduct.snd β₁ β₂ (τ (e.symm (θ k))) := by
780 simpa using hτ₂.symm
781 _ = FiberProduct.snd β₁ β₂ (θ k) := by
782 rw [show τ (e.symm (θ k)) = θ k from e.apply_symm_apply (θ k)]
783 _ = φ₂ k := by
784 change
785 FiberProduct.snd β₁ β₂
786 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k) = φ₂ k
787 rfl
788 · intro ψ hψ
789 have hcoord : τ.comp ψ = θ := by
790 apply FiberProduct.hom_ext
791 · intro k
792 have hτ₁ : FiberProduct.fst β₁ β₂ (τ (ψ k)) = α₁ (ψ k) := by
793 simpa using congrArg (fun f : G →* H₁ => f (ψ k)) h₁
794 have hψ₁ : α₁ (ψ k) = φ₁ k := by
795 simpa using congrArg (fun f : K →* H₁ => f k) hψ.1
796 calc
797 FiberProduct.fst β₁ β₂ ((τ.comp ψ) k) = α₁ (ψ k) := by
798 simpa [MonoidHom.comp_apply] using hτ₁
799 _ = φ₁ k := hψ₁
800 _ = FiberProduct.fst β₁ β₂ (θ k) := by
801 change
802 φ₁ k =
803 FiberProduct.fst β₁ β₂
804 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k)
805 rfl
806 · intro k
807 have hτ₂ : FiberProduct.snd β₁ β₂ (τ (ψ k)) = α₂ (ψ k) := by
808 simpa using congrArg (fun f : G →* H₂ => f (ψ k)) h₂
809 have hψ₂ : α₂ (ψ k) = φ₂ k := by
810 simpa using congrArg (fun f : K →* H₂ => f k) hψ.2
811 calc
812 FiberProduct.snd β₁ β₂ ((τ.comp ψ) k) = α₂ (ψ k) := by
813 simpa [MonoidHom.comp_apply] using hτ₂
814 _ = φ₂ k := hψ₂
815 _ = FiberProduct.snd β₁ β₂ (θ k) := by
816 change
817 φ₂ k =
818 FiberProduct.snd β₁ β₂
819 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) k)
820 rfl
821 ext k
822 apply hτ.1
823 calc
824 τ (ψ k) = (τ.comp ψ) k := by rfl
825 _ = θ k := by
826 exact congrArg (fun f : K →* FiberProduct.carrier β₁ β₂ => f k) hcoord
827 _ = τ ((e.symm.toMonoidHom.comp θ) k) := by
828 change θ k = τ (e.symm (θ k))
829 symm
830 exact e.apply_symm_apply (θ k)
832/-- The canonical map from an abstract pullback square into the concrete subgroup pullback. -/
833def IsPullbackSquare.toConcretePullback
834 (α₁ : G →* H₁) (α₂ : G →* H₂) (β₁ : H₁ →* H) (β₂ : H₂ →* H)
835 (hpb : IsPullbackSquare α₁ α₂ β₁ β₂) :
836 G →* FiberProduct.carrier β₁ β₂ :=
837 FiberProduct.lift β₁ β₂ α₁ α₂ (fun g => by
838 exact DFunLike.congr_fun hpb.1 g)
840/-- The canonical comparison map from the concrete pullback to itself is the identity.
841-/
842@[simp 900] theorem IsPullbackSquare.toConcretePullback_self
843 (β₁ : H₁ →* H) (β₂ : H₂ →* H) :
844 IsPullbackSquare.toConcretePullback (FiberProduct.fst β₁ β₂) (FiberProduct.snd β₁ β₂) β₁ β₂
845 (pullback_isPullback.{u, u} β₁ β₂) =
846 MonoidHom.id (FiberProduct.carrier β₁ β₂) := by
847 simpa [IsPullbackSquare.toConcretePullback] using
848 (pullbackLift_eta (β₁ := β₁) (β₂ := β₂) (ψ := MonoidHom.id (FiberProduct.carrier β₁ β₂)))
850/-- The first coordinate of the canonical comparison map recovers `α₁`. -/
851@[simp 900] theorem IsPullbackSquare.fst_toConcretePullback
852 (α₁ : G →* H₁) (α₂ : G →* H₂) (β₁ : H₁ →* H) (β₂ : H₂ →* H)
853 (hpb : IsPullbackSquare α₁ α₂ β₁ β₂) :
854 (FiberProduct.fst β₁ β₂).comp (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb) = α₁ := by
855 ext g
856 rfl
858/-- The second coordinate of the canonical comparison map recovers `α₂`. -/
859@[simp 900] theorem IsPullbackSquare.snd_toConcretePullback
860 (α₁ : G →* H₁) (α₂ : G →* H₂) (β₁ : H₁ →* H) (β₂ : H₂ →* H)
861 (hpb : IsPullbackSquare α₁ α₂ β₁ β₂) :
862 (FiberProduct.snd β₁ β₂).comp (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb) = α₂ := by
863 ext g
864 rfl
866/-- Any abstract pullback square is canonically bijective to the concrete pullback. -/
867theorem IsPullbackSquare.bijective_toConcretePullback
868 (α₁ : G →* H₁) (α₂ : G →* H₂) (β₁ : H₁ →* H) (β₂ : H₂ →* H)
869 (hpb : IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂) :
870 Function.Bijective (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb) := by
871 let ψ : FiberProduct.carrier β₁ β₂ →* G :=
872 IsPullbackSquare.desc hpb (FiberProduct.fst β₁ β₂) (FiberProduct.snd β₁ β₂)
873 ((pullback_isPullback.{u, u} β₁ β₂).1)
874 have hψfst : α₁.comp ψ = FiberProduct.fst β₁ β₂ := by
875 change
876 α₁.comp
877 (IsPullbackSquare.desc hpb (FiberProduct.fst β₁ β₂) (FiberProduct.snd β₁ β₂)
878 ((pullback_isPullback.{u, u} β₁ β₂).1)) =
879 FiberProduct.fst β₁ β₂
880 exact IsPullbackSquare.desc_left hpb (FiberProduct.fst β₁ β₂) (FiberProduct.snd β₁ β₂)
881 ((pullback_isPullback.{u, u} β₁ β₂).1)
882 have hψsnd : α₂.comp ψ = FiberProduct.snd β₁ β₂ := by
883 change
884 α₂.comp
885 (IsPullbackSquare.desc hpb (FiberProduct.fst β₁ β₂) (FiberProduct.snd β₁ β₂)
886 ((pullback_isPullback.{u, u} β₁ β₂).1)) =
887 FiberProduct.snd β₁ β₂
888 exact IsPullbackSquare.desc_right hpb (FiberProduct.fst β₁ β₂) (FiberProduct.snd β₁ β₂)
889 ((pullback_isPullback.{u, u} β₁ β₂).1)
890 have hleft :
891 (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb).comp ψ =
892 MonoidHom.id (FiberProduct.carrier β₁ β₂) := by
893 apply FiberProduct.hom_ext
894 · intro x
895 calc
896 FiberProduct.fst β₁ β₂ ((IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb).comp ψ x)
897 = α₁ (ψ x) := by
898 rfl
899 _ = FiberProduct.fst β₁ β₂ x := by
900 exact congrArg (fun f : FiberProduct.carrier β₁ β₂ →* H₁ => f x) hψfst
901 · intro x
902 calc
903 FiberProduct.snd β₁ β₂ ((IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb).comp ψ x)
904 = α₂ (ψ x) := by
905 rfl
906 _ = FiberProduct.snd β₁ β₂ x := by
907 exact congrArg (fun f : FiberProduct.carrier β₁ β₂ →* H₂ => f x) hψsnd
908 have hright_desc :
909 ψ.comp (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb) =
910 IsPullbackSquare.desc hpb α₁ α₂ hpb.1 := by
911 apply IsPullbackSquare.desc_uniq hpb α₁ α₂ hpb.1
912 constructor
913 · ext g
914 calc
915 α₁ ((ψ.comp (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb)) g)
916 = FiberProduct.fst β₁ β₂ (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb g) := by
917 exact congrArg (fun f : FiberProduct.carrier β₁ β₂ →* H₁ =>
918 f (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb g)) hψfst
919 _ = α₁ g := by
920 rfl
921 · ext g
922 calc
923 α₂ ((ψ.comp (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb)) g)
924 = FiberProduct.snd β₁ β₂ (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb g) := by
925 exact congrArg (fun f : FiberProduct.carrier β₁ β₂ →* H₂ =>
926 f (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb g)) hψsnd
927 _ = α₂ g := by
928 rfl
929 have hself : IsPullbackSquare.desc hpb α₁ α₂ hpb.1 = MonoidHom.id G := by
930 symm
931 exact IsPullbackSquare.desc_uniq hpb α₁ α₂ hpb.1 (by simp only [MonoidHom.comp_id, and_self])
932 have hright :
933 ψ.comp (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb) = MonoidHom.id G := by
934 exact hright_desc.trans hself
935 refine ⟨?_, ?_⟩
936 · intro x y hxy
937 have hx : ψ (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb x) = x := by
938 simpa using congrArg (fun f : G →* G => f x) hright
939 have hy : ψ (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb y) = y := by
940 simpa using congrArg (fun f : G →* G => f y) hright
941 calc
942 x = ψ (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb x) := hx.symm
943 _ = ψ (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb y) := by simpa using congrArg ψ hxy
944 _ = y := hy
945 · intro x
946 refine ⟨ψ x, ?_⟩
947 simpa using congrArg (fun f : FiberProduct.carrier β₁ β₂ →* FiberProduct.carrier β₁ β₂ => f x) hleft
949/-- Any abstract pullback square is canonically isomorphic to the concrete pullback. -/
950noncomputable def IsPullbackSquare.concretePullbackEquiv
951 (α₁ : G →* H₁) (α₂ : G →* H₂) (β₁ : H₁ →* H) (β₂ : H₂ →* H)
952 (hpb : IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂) :
953 G ≃* FiberProduct.carrier β₁ β₂ :=
954 MulEquiv.ofBijective
955 (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb)
956 (IsPullbackSquare.bijective_toConcretePullback α₁ α₂ β₁ β₂ hpb)
958/-- The first coordinate of the pullback comparison equivalence is `α₁`. -/
959@[simp] theorem IsPullbackSquare.concretePullbackEquiv_fst
960 (α₁ : G →* H₁) (α₂ : G →* H₂) (β₁ : H₁ →* H) (β₂ : H₂ →* H)
961 (hpb : IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂) :
962 (FiberProduct.fst β₁ β₂).comp (IsPullbackSquare.concretePullbackEquiv α₁ α₂ β₁ β₂ hpb).toMonoidHom = α₁ := by
963 ext g
964 rfl
966/-- The second coordinate of the pullback comparison equivalence is `α₂`. -/
967@[simp] theorem IsPullbackSquare.concretePullbackEquiv_snd
968 (α₁ : G →* H₁) (α₂ : G →* H₂) (β₁ : H₁ →* H) (β₂ : H₂ →* H)
969 (hpb : IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂) :
970 (FiberProduct.snd β₁ β₂).comp (IsPullbackSquare.concretePullbackEquiv α₁ α₂ β₁ β₂ hpb).toMonoidHom = α₂ := by
971 ext g
972 rfl
974/-- A square is a pullback iff its canonical map to the concrete pullback is bijective. -/
976 {α₁ : G →* H₁} {α₂ : G →* H₂} {β₁ : H₁ →* H} {β₂ : H₂ →* H}
977 (hcomm : β₁.comp α₁ = β₂.comp α₂) :
978 IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂ ↔
979 Function.Bijective (FiberProduct.lift β₁ β₂ α₁ α₂ (fun g => by
980 exact DFunLike.congr_fun hcomm g)) := by
981 constructor
982 · intro hpb
983 simpa [IsPullbackSquare.toConcretePullback] using
984 (IsPullbackSquare.bijective_toConcretePullback α₁ α₂ β₁ β₂ hpb)
985 · intro hbij
987 α₁ α₂ β₁ β₂
988 (FiberProduct.lift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
989 hbij
990 (pullbackFst_pullbackLift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
991 (pullbackSnd_pullbackLift β₁ β₂ α₁ α₂ (fun g => DFunLike.congr_fun hcomm g))
993/-- The canonical comparison map sends the chosen pullback descent map to the concrete
994pullback lift. -/
995@[simp 900] theorem IsPullbackSquare.toConcretePullback_comp_desc
996 (α₁ : G →* H₁) (α₂ : G →* H₂)
997 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
998 (hpb : IsPullbackSquare α₁ α₂ β₁ β₂)
999 (φ₁ : K →* H₁) (φ₂ : K →* H₂)
1000 (hφ : β₁.comp φ₁ = β₂.comp φ₂) :
1001 (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb).comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ) =
1002 FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k) := by
1003 apply FiberProduct.hom_ext
1004 · intro k
1005 have hleft :
1006 (FiberProduct.fst β₁ β₂).comp
1007 ((IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb).comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ)) = φ₁ := by
1008 calc
1009 (FiberProduct.fst β₁ β₂).comp
1010 ((IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb).comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ))
1011 = ((FiberProduct.fst β₁ β₂).comp
1012 (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb)).comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ) := by
1013 rfl
1014 _ = α₁.comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ) := by
1015 rw [IsPullbackSquare.fst_toConcretePullback α₁ α₂ β₁ β₂ hpb]
1016 _ = φ₁ := IsPullbackSquare.desc_left hpb φ₁ φ₂ hφ
1017 have hright :
1018 (FiberProduct.fst β₁ β₂).comp
1019 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) = φ₁ :=
1020 pullbackFst_pullbackLift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)
1021 exact congrArg (fun f : K →* H₁ => f k) (hleft.trans hright.symm)
1022 · intro k
1023 have hleft :
1024 (FiberProduct.snd β₁ β₂).comp
1025 ((IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb).comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ)) = φ₂ := by
1026 calc
1027 (FiberProduct.snd β₁ β₂).comp
1028 ((IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb).comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ))
1029 = ((FiberProduct.snd β₁ β₂).comp
1030 (IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb)).comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ) := by
1031 rfl
1032 _ = α₂.comp (IsPullbackSquare.desc hpb φ₁ φ₂ hφ) := by
1033 rw [IsPullbackSquare.snd_toConcretePullback α₁ α₂ β₁ β₂ hpb]
1034 _ = φ₂ := IsPullbackSquare.desc_right hpb φ₁ φ₂ hφ
1035 have hright :
1036 (FiberProduct.snd β₁ β₂).comp
1037 (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)) = φ₂ :=
1038 pullbackSnd_pullbackLift β₁ β₂ φ₁ φ₂ (fun k => DFunLike.congr_fun hφ k)
1039 exact congrArg (fun f : K →* H₂ => f k) (hleft.trans hright.symm)
1041/-- For an abstract pullback square, surjectivity of the chosen descent map is equivalent to
1042surjectivity of the corresponding map into the concrete pullback. -/
1043theorem IsPullbackSquare.surjective_desc_iff_surjective_lift
1044 (α₁ : G →* H₁) (α₂ : G →* H₂)
1045 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
1046 (hpb : IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂)
1047 (φ₁ : A →* H₁) (φ₂ : A →* H₂)
1048 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :
1049 Function.Surjective (IsPullbackSquare.desc hpb φ₁ φ₂ hcomp) ↔
1050 Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂
1051 (fun a => DFunLike.congr_fun hcomp a)) := by
1052 let c : G →* FiberProduct.carrier β₁ β₂ := IsPullbackSquare.toConcretePullback α₁ α₂ β₁ β₂ hpb
1053 have hc : Function.Bijective c := IsPullbackSquare.bijective_toConcretePullback α₁ α₂ β₁ β₂ hpb
1054 have hcomm :
1055 c.comp (IsPullbackSquare.desc hpb φ₁ φ₂ hcomp) =
1056 FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hcomp a) := by
1057 simp only [toConcretePullback_comp_desc, c]
1058 constructor
1059 · intro hdesc z
1060 rcases hc.2 z with ⟨g, rfl⟩
1061 rcases hdesc g with ⟨a, rfl⟩
1062 exact ⟨a, (DFunLike.congr_fun hcomm a).symm⟩
1063 · intro hlift g
1064 rcases hlift (c g) with ⟨a, ha⟩
1065 refine ⟨a, ?_⟩
1066 apply hc.1
1067 calc
1068 c (IsPullbackSquare.desc hpb φ₁ φ₂ hcomp a) =
1069 FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => DFunLike.congr_fun hcomp a) a := by
1070 exact DFunLike.congr_fun hcomm a
1071 _ = c g := ha
1073/-- Algebraic abstract-pullback form of the surjectivity criterion. -/
1074theorem IsPullbackSquare.surjective_desc_of_ker_eq
1075 (α₁ : G →* H₁) (α₂ : G →* H₂)
1076 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
1077 (hpb : IsPullbackSquare.{u, u} α₁ α₂ β₁ β₂)
1078 (φ₁ : A →* H₁) (φ₂ : A →* H₂)
1079 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
1080 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
1082 Function.Surjective (IsPullbackSquare.desc hpb φ₁ φ₂ hcomp) := by
1083 exact (IsPullbackSquare.surjective_desc_iff_surjective_lift
1084 α₁ α₂ β₁ β₂ hpb φ₁ φ₂ hcomp).2
1085 ((pullbackLift_surjective_iff_ker_eq β₁ β₂ φ₁ φ₂ hφ₁ hφ₂ hcomp).2 hker)
1087/-- Algebraic surjectivity criterion for the canonical map into the pullback. -/
1089 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
1090 (φ₁ : A →* H₁) (φ₂ : A →* H₂)
1091 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)
1092 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
1094 Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
1095 exact DFunLike.congr_fun hcomp a)) := by
1096 exact (pullbackLift_surjective_iff_ker_eq β₁ β₂ φ₁ φ₂ hφ₁ hφ₂ hcomp).2 hker
1098/-- Reusable bijectivity package for the canonical pullback map, using injectivity of `φ₁`. -/
1100 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
1101 (φ₁ : A →* H₁) (φ₂ : A →* H₂)
1102 (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
1103 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
1105 (hφ₁inj : Function.Injective φ₁) :
1106 Function.Bijective (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
1107 exact DFunLike.congr_fun hcomp a)) := by
1108 refine ⟨?_, ?_⟩
1109 · exact pullbackLift_injective_of_left_injective β₁ β₂ φ₁ φ₂
1110 (fun a => DFunLike.congr_fun hcomp a) hφ₁inj
1111 · exact (pullbackLift_surjective_iff_ker_eq
1112 β₁ β₂ φ₁ φ₂ hφ₁surj hφ₂surj hcomp).2 hker
1114/-- Reusable bijectivity package for the canonical pullback map, using injectivity of `φ₂`. -/
1116 (β₁ : H₁ →* H) (β₂ : H₂ →* H)
1117 (φ₁ : A →* H₁) (φ₂ : A →* H₂)
1118 (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)
1119 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)
1121 (hφ₂inj : Function.Injective φ₂) :
1122 Function.Bijective (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by
1123 exact DFunLike.congr_fun hcomp a)) := by
1124 refine ⟨?_, ?_⟩
1125 · exact pullbackLift_injective_of_right_injective β₁ β₂ φ₁ φ₂
1126 (fun a => DFunLike.congr_fun hcomp a) hφ₂inj
1127 · exact (pullbackLift_surjective_iff_ker_eq
1128 β₁ β₂ φ₁ φ₂ hφ₁surj hφ₂surj hcomp).2 hker
1130end
1134end ProCGroups.Categorical