Source: ProCGroups.Categorical.AlgebraicPullbacks

1import Mathlib.Algebra.Category.Grp.Limits

2import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

3import Mathlib.GroupTheory.QuotientGroup.Basic

5/-!

6# Pro C Groups / Categorical / Algebraic Pullbacks

8This module develops concrete fiber products of groups, identifies them with

9the categorical pullback in `GrpCat`, and proves comparison and kernel

10criteria for the associated lift maps.

11-/

13namespace ProCGroups.Categorical

15open CategoryTheory Limits

16open scoped Pointwise

18universe u v

20section

22variable {A G H H₁ H₂ : Type u} {K : Type v}

23variable [Group A] [Group G] [Group H] [Group H₁] [Group H₂] [Group K]

25/-- Concrete pullback subgroup of \(\beta_1\) and \(\beta_2\). -/

26def FiberProduct.subgroup (β₁ : H₁ →* H) (β₂ : H₂ →* H) : Subgroup (H₁ × H₂) where

27 carrier := { x | β₁ x.1 = β₂ x.2 }

28 one_mem' := by simp only [Set.mem_setOf_eq, Prod.fst_one, map_one, Prod.snd_one]

29 mul_mem' := by

30 intro x y hx hy

31 change β₁ x.1 = β₂ x.2 at hx

32 change β₁ y.1 = β₂ y.2 at hy

33 simpa [map_mul] using congrArg₂ (· * ·) hx hy

34 inv_mem' := by

35 intro x hx

36 simpa [map_inv, hx]

38/-- Concrete pullback attached to \(\beta_1\) and \(\beta_2\). -/

39abbrev FiberProduct.carrier (β₁ : H₁ →* H) (β₂ : H₂ →* H) :=

40 ↥(FiberProduct.subgroup β₁ β₂)

42/-- Membership in the pullback subgroup is equivalent to the displayed coordinate condition. -/

43@[simp] theorem mem_pullbackSubgroup_iff {β₁ : H₁ →* H} {β₂ : H₂ →* H}

44 {x : H₁ × H₂} :

45 x ∈ FiberProduct.subgroup β₁ β₂ ↔ β₁ x.1 = β₂ x.2 :=

46 Iff.rfl

48/-- The first projection from the concrete pullback. -/

49def FiberProduct.fst (β₁ : H₁ →* H) (β₂ : H₂ →* H) : FiberProduct.carrier β₁ β₂ →* H₁ where

50 toFun := fun x => x.1.1

51 map_one' := rfl

52 map_mul' := by

53 intro x y

54 rfl

56/-- The second projection from the concrete pullback. -/

57def FiberProduct.snd (β₁ : H₁ →* H) (β₂ : H₂ →* H) : FiberProduct.carrier β₁ β₂ →* H₂ where

58 toFun := fun x => x.1.2

59 map_one' := rfl

60 map_mul' := by

61 intro x y

62 rfl

64/-- The canonical homomorphism into the concrete pullback. -/

65def FiberProduct.lift (β₁ : H₁ →* H) (β₂ : H₂ →* H)

66 (φ₁ : K →* H₁) (φ₂ : K →* H₂)

67 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) : K →* FiberProduct.carrier β₁ β₂ where

68 toFun := fun k => ⟨(φ₁ k, φ₂ k), h k⟩

69 map_one' := by

70 apply Subtype.ext

71 simp only [map_one, OneMemClass.coe_one, Prod.mk_eq_one, and_self]

72 map_mul' := by

73 intro x y

74 apply Subtype.ext

75 simp only [map_mul, Subgroup.coe_mul, Prod.mk_mul_mk]

77/-- The concrete group pullback as a categorical pullback cone in GrpCat. -/

78def FiberProduct.cone (β₁ : H₁ →* H) (β₂ : H₂ →* H) :

79 PullbackCone (GrpCat.ofHom β₁) (GrpCat.ofHom β₂) :=

80 PullbackCone.mk

81 (GrpCat.ofHom (FiberProduct.fst β₁ β₂))

82 (GrpCat.ofHom (FiberProduct.snd β₁ β₂))

83 (by

84 apply GrpCat.hom_ext

85 ext x

86 exact x.2)

88/-- The concrete group pullback cone is a limit cone in GrpCat. -/

89def FiberProduct.isLimitCone (β₁ : H₁ →* H) (β₂ : H₂ →* H) :

90 IsLimit (FiberProduct.cone β₁ β₂) := by

91 refine PullbackCone.IsLimit.mk (by

92 apply GrpCat.hom_ext

93 ext x

94 exact x.2) ?lift ?fac_left ?fac_right ?uniq

95 · intro s

96 exact GrpCat.ofHom <|

97 FiberProduct.lift β₁ β₂ s.fst.hom s.snd.hom (fun x => by

98 have hcondition :

99 (s.fst ≫ GrpCat.ofHom β₁).hom =

100 (s.snd ≫ GrpCat.ofHom β₂).hom :=

101 congrArg (fun f : s.pt ⟶ GrpCat.of H => f.hom) s.condition

102 exact DFunLike.congr_fun hcondition x)

103 · intro s

104 apply GrpCat.hom_ext

105 rfl

106 · intro s

107 apply GrpCat.hom_ext

108 rfl

109 · intro s m hfst hsnd

110 apply GrpCat.hom_ext

111 ext x

112 · have hfst' :

113 (m ≫ GrpCat.ofHom (FiberProduct.fst β₁ β₂)).hom = s.fst.hom :=

114 congrArg (fun f : s.pt ⟶ GrpCat.of H₁ => f.hom) hfst

115 exact DFunLike.congr_fun hfst' x

116 · have hsnd' :

117 (m ≫ GrpCat.ofHom (FiberProduct.snd β₁ β₂)).hom = s.snd.hom :=

118 congrArg (fun f : s.pt ⟶ GrpCat.of H₂ => f.hom) hsnd

119 exact DFunLike.congr_fun hsnd' x

120

121/-- The concrete group fiber product is a pullback in mathlib's bundled category of groups. -/

122theorem FiberProduct.isPullback (β₁ : H₁ →* H) (β₂ : H₂ →* H) :

123 CategoryTheory.IsPullback

124 (GrpCat.ofHom (FiberProduct.fst β₁ β₂))

125 (GrpCat.ofHom (FiberProduct.snd β₁ β₂))

126 (GrpCat.ofHom β₁) (GrpCat.ofHom β₂) :=

127 CategoryTheory.IsPullback.of_isLimit (FiberProduct.isLimitCone β₁ β₂)

128

129/--

130The kernel of the canonical map into a concrete pullback is the intersection of the two

131coordinate kernels.

132-/

133@[simp] theorem ker_pullbackLift (β₁ : H₁ →* H) (β₂ : H₂ →* H)

134 (φ₁ : K →* H₁) (φ₂ : K →* H₂)

135 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :

136 (FiberProduct.lift β₁ β₂ φ₁ φ₂ h).ker = φ₁.ker ⊓ φ₂.ker := by

137 ext k

138 change FiberProduct.lift β₁ β₂ φ₁ φ₂ h k = 1 ↔ φ₁ k = 1 ∧ φ₂ k = 1

139 constructor

140 · intro hk

141 exact ⟨congrArg (fun z => FiberProduct.fst β₁ β₂ z) hk,

142 congrArg (fun z => FiberProduct.snd β₁ β₂ z) hk⟩

143 · rintro ⟨h₁, h₂⟩

144 apply Subtype.ext

145 exact Prod.ext h₁ h₂

146

147/--

148The canonical map into a concrete pullback is injective iff the two coordinate kernels intersect

149trivially.

150-/

151theorem pullbackLift_injective_iff (β₁ : H₁ →* H) (β₂ : H₂ →* H)

152 {φ₁ : K →* H₁} {φ₂ : K →* H₂}

153 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :

154 Function.Injective (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) ↔ φ₁.ker ⊓ φ₂.ker = ⊥ := by

155 rw [← MonoidHom.ker_eq_bot_iff, ker_pullbackLift]

156

157/--

158The supremum of the two kernels is contained in the kernel of the composite when the composites

159agree.

160-/

161theorem ker_sup_le_ker_comp_of_comp_eq

162 (β₁ : H₁ →* H) (β₂ : H₂ →* H)

163 (φ₁ : K →* H₁) (φ₂ : K →* H₂)

164 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :

165 φ₁.ker ⊔ φ₂.ker ≤ (β₁.comp φ₁).ker := by

166 rw [sup_le_iff]

167 constructor

168 · intro k hk

169 change β₁ (φ₁ k) = 1

170 have hk' : φ₁ k = 1 := by simpa using hk

171 simp only [hk', map_one]

172 · intro k hk

173 calc

174 β₁ (φ₁ k) = β₂ (φ₂ k) := DFunLike.congr_fun hcomp k

175 _ = 1 := by

176 have hk' : φ₂ k = 1 := by simpa using hk

177 simp only [hk', map_one]

178

179/-- The algebraic pullback lift is surjective exactly when the composite kernel is contained in

180the supremum of the two coordinate kernels. -/

181theorem pullbackLift_surjective_iff_ker_comp_le_sup_ker

182 {β₁ : H₁ →* H} (β₂ : H₂ →* H)

183 {φ₁ : K →* H₁} {φ₂ : K →* H₂}

184 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)

185 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :

186 Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂

187 (fun k => DFunLike.congr_fun hcomp k)) ↔

188 (β₁.comp φ₁).ker ≤ φ₁.ker ⊔ φ₂.ker := by

189 constructor

190 · intro hsurj k hk

191 let z : FiberProduct.carrier β₁ β₂ :=

192 ⟨(φ₁ k, 1), by

193 change β₁ (φ₁ k) = β₂ 1

194 simpa using hk⟩

195 rcases hsurj z with ⟨a, ha⟩

196 have hφ₁a : φ₁ a = φ₁ k := by

197 exact congrArg (fun y => FiberProduct.fst β₁ β₂ y) ha

198 have hφ₂a : φ₂ a = 1 := by

199 exact congrArg (fun y => FiberProduct.snd β₁ β₂ y) ha

200 have ha_ker₂ : a ∈ φ₂.ker := by

201 simpa using hφ₂a

202 have ha_inv_mul_ker₁ : a⁻¹ * k ∈ φ₁.ker := by

203 change φ₁ (a⁻¹ * k) = 1

204 simp only [map_mul, map_inv, hφ₁a, inv_mul_cancel]

205 have hprod : a * (a⁻¹ * k) ∈ φ₁.ker ⊔ φ₂.ker :=

206 (φ₁.ker ⊔ φ₂.ker).mul_mem

207 ((le_sup_right : φ₂.ker ≤ φ₁.ker ⊔ φ₂.ker) ha_ker₂)

208 ((le_sup_left : φ₁.ker ≤ φ₁.ker ⊔ φ₂.ker) ha_inv_mul_ker₁)

209 simpa [mul_assoc] using hprod

210 · intro hker_le z

211 rcases hφ₁ z.1.1 with ⟨a₁, ha₁⟩

212 rcases hφ₂ z.1.2 with ⟨a₂, ha₂⟩

213 have hEq : β₁ (φ₁ a₁) = β₁ (φ₁ a₂) := by

214 calc

215 β₁ (φ₁ a₁) = β₁ z.1.1 := by simp only [ha₁]

216 _ = β₂ z.1.2 := z.2

217 _ = β₂ (φ₂ a₂) := by simp only [ha₂]

218 _ = β₁ (φ₁ a₂) := by

219 exact (DFunLike.congr_fun hcomp a₂).symm

220 have hgker : a₁ * a₂⁻¹ ∈ (β₁.comp φ₁).ker := by

221 change β₁ (φ₁ (a₁ * a₂⁻¹)) = 1

222 simp only [map_mul, map_inv, hEq, mul_inv_cancel]

223 have hgjoin : a₁ * a₂⁻¹ ∈ (φ₁.ker : Subgroup K) ⊔ (φ₂.ker : Subgroup K) :=

224 hker_le hgker

225 have hgjoin' : a₁ * a₂⁻¹ ∈ ((φ₁.ker : Set K) * (φ₂.ker : Set K)) := by

226 rw [← Subgroup.mul_normal (φ₁.ker) (φ₂.ker)]

227 simpa [SetLike.mem_coe] using hgjoin

228 rcases (show ∃ y ∈ (φ₁.ker : Set K), ∃ z ∈ (φ₂.ker : Set K),

229 y * z = a₁ * a₂⁻¹ from by

230 simpa [Set.mem_mul] using hgjoin') with ⟨k₁, hk₁, k₂, hk₂, hkprod⟩

231 have hk₁' : φ₁ k₁ = 1 := by simpa using hk₁

232 have hk₂' : φ₂ k₂ = 1 := by simpa using hk₂

233 have haeq : a₁ = k₁ * k₂ * a₂ := by

234 calc

235 a₁ = (a₁ * a₂⁻¹) * a₂ := by simp only [mul_assoc, inv_mul_cancel, mul_one]

236 _ = (k₁ * k₂) * a₂ := by rw [hkprod]

237 _ = k₁ * k₂ * a₂ := by simp only [mul_assoc]

238 refine ⟨k₂ * a₂, ?_⟩

239 apply Subtype.ext

240 apply Prod.ext

241 · calc

242 φ₁ (k₂ * a₂) = φ₁ (k₁ * k₂ * a₂) := by

243 simp only [map_mul, mul_assoc, hk₁', one_mul]

244 _ = φ₁ a₁ := by rw [haeq]

245 _ = z.1.1 := ha₁

246 · calc

247 φ₂ (k₂ * a₂) = φ₂ k₂ * φ₂ a₂ := by rw [map_mul]

248 _ = 1 * φ₂ a₂ := by simp only [hk₂', one_mul]

249 _ = z.1.2 := by simp only [ha₂, one_mul]

250

251/-- Surjectivity of the algebraic pullback lift is equivalent to the required kernel equality. -/

252theorem pullbackLift_surjective_iff_ker_eq

253 {β₁ : H₁ →* H} (β₂ : H₂ →* H)

254 {φ₁ : K →* H₁} {φ₂ : K →* H₂}

255 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)

256 (hcomp : β₁.comp φ₁ = β₂.comp φ₂) :

257 Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂

258 (fun k => DFunLike.congr_fun hcomp k)) ↔

259 (β₁.comp φ₁).ker = φ₁.ker ⊔ φ₂.ker := by

260 constructor

261 · intro hsurj

262 exact le_antisymm

263 ((pullbackLift_surjective_iff_ker_comp_le_sup_ker

264 (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁ hφ₂ hcomp).1 hsurj)

265 (ker_sup_le_ker_comp_of_comp_eq β₁ β₂ φ₁ φ₂ hcomp)

266 · intro hker

267 exact (pullbackLift_surjective_iff_ker_comp_le_sup_ker

268 (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁ hφ₂ hcomp).2 (by

269 intro k hk

270 rw [← hker]

271 exact hk)

272

273/-- Composing the first projection with the canonical pullback lift gives \(\varphi_1\). -/

274@[simp] theorem pullbackFst_pullbackLift (β₁ : H₁ →* H) (β₂ : H₂ →* H)

275 (φ₁ : K →* H₁) (φ₂ : K →* H₂)

276 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :

277 (FiberProduct.fst β₁ β₂).comp (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₁ := by

278 ext k

279 rfl

280

281/-- Composing the second projection with the canonical pullback lift gives \(\varphi_2\). -/

282@[simp] theorem pullbackSnd_pullbackLift (β₁ : H₁ →* H) (β₂ : H₂ →* H)

283 (φ₁ : K →* H₁) (φ₂ : K →* H₂)

284 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k)) :

285 (FiberProduct.snd β₁ β₂).comp (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) = φ₂ := by

286 ext k

287 rfl

288

289/--

290If \(\varphi_1\) is injective, then the canonical map into the concrete pullback is injective.

291-/

292theorem pullbackLift_injective_of_left_injective (β₁ : H₁ →* H) (β₂ : H₂ →* H)

293 (φ₁ : K →* H₁) (φ₂ : K →* H₂)

294 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))

295 (hφ₁ : Function.Injective φ₁) :

296 Function.Injective (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) := by

297 intro x y hxy

298 apply hφ₁

299 exact congrArg (fun z => FiberProduct.fst β₁ β₂ z) hxy

300

301/--

302If \(\varphi_2\) is injective, then the canonical map into the concrete pullback is injective.

303-/

304theorem pullbackLift_injective_of_right_injective (β₁ : H₁ →* H) (β₂ : H₂ →* H)

305 (φ₁ : K →* H₁) (φ₂ : K →* H₂)

306 (h : ∀ k, β₁ (φ₁ k) = β₂ (φ₂ k))

307 (hφ₂ : Function.Injective φ₂) :

308 Function.Injective (FiberProduct.lift β₁ β₂ φ₁ φ₂ h) := by

309 intro x y hxy

310 apply hφ₂

311 exact congrArg (fun z => FiberProduct.snd β₁ β₂ z) hxy

312

313/-- Two homomorphisms into the concrete pullback are equal once both coordinates agree. -/

314theorem FiberProduct.hom_ext {β₁ : H₁ →* H} {β₂ : H₂ →* H}

315 {K : Type v} [Group K]

316 {ψ ψ' : K →* FiberProduct.carrier β₁ β₂}

317 (h₁ : ∀ k, FiberProduct.fst β₁ β₂ (ψ k) = FiberProduct.fst β₁ β₂ (ψ' k))

318 (h₂ : ∀ k, FiberProduct.snd β₁ β₂ (ψ k) = FiberProduct.snd β₁ β₂ (ψ' k)) :

319 ψ = ψ' := by

320 apply MonoidHom.ext

321 intro k

322 exact Subtype.ext <| Prod.ext (h₁ k) (h₂ k)

323

324namespace FiberProduct

325

326/-- Transport a concrete fiber product across equal cospan maps. -/

327def congr {β₁ β₁' : H₁ →* H} {β₂ β₂' : H₂ →* H}

328 (h₁ : β₁ = β₁') (h₂ : β₂ = β₂') :

329 carrier β₁ β₂ ≃* carrier β₁' β₂' := by

330 subst β₁'

331 subst β₂'

332 exact MulEquiv.refl _

333

334end FiberProduct

335

336/-- The concrete pullback is reconstructed from its two projections by the canonical lift. -/

337@[simp 900] theorem pullbackLift_eta {β₁ : H₁ →* H} {β₂ : H₂ →* H}

338 {K : Type v} [Group K]

339 (ψ : K →* FiberProduct.carrier β₁ β₂) :

340 FiberProduct.lift β₁ β₂

341 ((FiberProduct.fst β₁ β₂).comp ψ)

342 ((FiberProduct.snd β₁ β₂).comp ψ)

343 (fun k => by exact (ψ k).2) = ψ := by

344 apply FiberProduct.hom_ext

345 · intro k

346 rfl

347 · intro k

348 rfl

349

350/-- Symmetry of the concrete pullback. -/

351def pullbackSwap (β₁ : H₁ →* H) (β₂ : H₂ →* H) :

352 FiberProduct.carrier β₁ β₂ ≃* FiberProduct.carrier β₂ β₁ where

353 toFun := fun x => ⟨(x.1.2, x.1.1), x.2.symm⟩

354 invFun := fun x => ⟨(x.1.2, x.1.1), x.2.symm⟩

355 left_inv := by

356 intro x

357 apply Subtype.ext

358 rfl

359 right_inv := by

360 intro x

361 apply Subtype.ext

362 rfl

363 map_mul' := by

364 intro x y

365 apply Subtype.ext

366 rfl

367

368/-- The first projection after swapping equals the original second projection. -/

369@[simp] theorem pullbackFst_pullbackSwap (β₁ : H₁ →* H) (β₂ : H₂ →* H)

370 (x : FiberProduct.carrier β₁ β₂) :

371 FiberProduct.fst β₂ β₁ (pullbackSwap β₁ β₂ x) = FiberProduct.snd β₁ β₂ x :=

372 rfl

373

374/-- The second projection after swapping equals the original first projection. -/

375@[simp] theorem pullbackSnd_pullbackSwap (β₁ : H₁ →* H) (β₂ : H₂ →* H)

376 (x : FiberProduct.carrier β₁ β₂) :

377 FiberProduct.snd β₂ β₁ (pullbackSwap β₁ β₂ x) = FiberProduct.fst β₁ β₂ x :=

378 rfl

379

380/--

381The symmetry map for the algebraic pullback is inverse to the corresponding swapped pullback

382comparison.

383-/

384@[simp] theorem pullbackSwap_symm (β₁ : H₁ →* H) (β₂ : H₂ →* H) :

385 (pullbackSwap β₁ β₂).symm = pullbackSwap β₂ β₁ :=

386 rfl

387

388/-- If the right cospan map is surjective, then the first projection from the fiber product is

389surjective. -/

390theorem pullbackFst_surjective_of_right_surjective

391 (β₁ : H₁ →* H) (β₂ : H₂ →* H)

392 (hβ₂ : Function.Surjective β₂) :

393 Function.Surjective (FiberProduct.fst β₁ β₂) := by

394 intro x

395 rcases hβ₂ (β₁ x) with ⟨y, hy⟩

396 refine ⟨⟨(x, y), ?_⟩, rfl⟩

397 simp only [mem_pullbackSubgroup_iff, hy]

398

399/-- If the left cospan map is surjective, then the second projection from the fiber product is

400surjective. -/

401theorem pullbackSnd_surjective_of_left_surjective

402 (β₁ : H₁ →* H) (β₂ : H₂ →* H)

403 (hβ₁ : Function.Surjective β₁) :

404 Function.Surjective (FiberProduct.snd β₁ β₂) := by

405 intro y

406 rcases hβ₁ (β₂ y) with ⟨x, hx⟩

407 refine ⟨⟨(x, y), ?_⟩, rfl⟩

408 simp only [mem_pullbackSubgroup_iff, hx]

409

410/-- If \(\beta_2\) is injective, then the first pullback projection is injective. -/

411theorem pullbackFst_injective_of_right_injective

412 (β₁ : H₁ →* H) (β₂ : H₂ →* H)

413 (hβ₂ : Function.Injective β₂) :

414 Function.Injective (FiberProduct.fst β₁ β₂) := by

415 intro x y hxy

416 apply Subtype.ext

417 exact Prod.ext hxy <| hβ₂ <| by

418 calc

419 β₂ x.1.2 = β₁ x.1.1 := x.2.symm

420 _ = β₁ y.1.1 := by

421 have h := congrArg β₁ hxy

422 change β₁ x.1.1 = β₁ y.1.1 at h

423 exact h

424 _ = β₂ y.1.2 := y.2

425

426/-- If \(\beta_1\) is injective, then the second pullback projection is injective. -/

427theorem pullbackSnd_injective_of_left_injective

428 (β₁ : H₁ →* H) (β₂ : H₂ →* H)

429 (hβ₁ : Function.Injective β₁) :

430 Function.Injective (FiberProduct.snd β₁ β₂) := by

431 intro x y hxy

432 apply Subtype.ext

433 exact Prod.ext (hβ₁ <| by

434 calc

435 β₁ x.1.1 = β₂ x.1.2 := x.2

436 _ = β₂ y.1.2 := by

437 have h := congrArg β₂ hxy

438 change β₂ x.1.2 = β₂ y.1.2 at h

439 exact h

440 _ = β₁ y.1.1 := y.2.symm) hxy

441

442/-- Surjective coordinate maps whose composite kernel is the supremum of their kernels induce a

443surjective map into the concrete fiber product. -/

444theorem surjective_pullbackLift_of_ker_eq

445 (β₁ : H₁ →* H) (β₂ : H₂ →* H)

446 (φ₁ : A →* H₁) (φ₂ : A →* H₂)

447 (hφ₁ : Function.Surjective φ₁) (hφ₂ : Function.Surjective φ₂)

448 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)

449 (hker : (β₁.comp φ₁).ker = φ₁.ker ⊔ φ₂.ker) :

450 Function.Surjective (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by

451 exact DFunLike.congr_fun hcomp a)) := by

452 exact (pullbackLift_surjective_iff_ker_eq (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁ hφ₂

453 hcomp).2 hker

454

455/--

456The algebraic pullback lift is bijective when the left map is injective and the required kernel

457equality holds.

458-/

459theorem bijective_pullbackLift_of_left_injective_of_ker_eq

460 (β₁ : H₁ →* H) (β₂ : H₂ →* H)

461 (φ₁ : A →* H₁) (φ₂ : A →* H₂)

462 (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)

463 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)

464 (hker : (β₁.comp φ₁).ker = φ₁.ker ⊔ φ₂.ker)

465 (hφ₁inj : Function.Injective φ₁) :

466 Function.Bijective (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by

467 exact DFunLike.congr_fun hcomp a)) := by

468 refine ⟨?_, ?_⟩

469 · exact pullbackLift_injective_of_left_injective β₁ β₂ φ₁ φ₂

470 (fun a => DFunLike.congr_fun hcomp a) hφ₁inj

471 · exact (pullbackLift_surjective_iff_ker_eq

472 (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁surj hφ₂surj hcomp).2 hker

473

474/--

475The algebraic pullback lift is bijective when the right map is injective and the required kernel

476equality holds.

477-/

478theorem bijective_pullbackLift_of_right_injective_of_ker_eq

479 (β₁ : H₁ →* H) (β₂ : H₂ →* H)

480 (φ₁ : A →* H₁) (φ₂ : A →* H₂)

481 (hφ₁surj : Function.Surjective φ₁) (hφ₂surj : Function.Surjective φ₂)

482 (hcomp : β₁.comp φ₁ = β₂.comp φ₂)

483 (hker : (β₁.comp φ₁).ker = φ₁.ker ⊔ φ₂.ker)

484 (hφ₂inj : Function.Injective φ₂) :

485 Function.Bijective (FiberProduct.lift β₁ β₂ φ₁ φ₂ (fun a => by

486 exact DFunLike.congr_fun hcomp a)) := by

487 refine ⟨?_, ?_⟩

488 · exact pullbackLift_injective_of_right_injective β₁ β₂ φ₁ φ₂

489 (fun a => DFunLike.congr_fun hcomp a) hφ₂inj

490 · exact (pullbackLift_surjective_iff_ker_eq

491 (β₁ := β₁) (β₂ := β₂) (φ₁ := φ₁) (φ₂ := φ₂) hφ₁surj hφ₂surj hcomp).2 hker

493end

497end ProCGroups.Categorical