English
The pullback of two monomorphisms exists in a Normal Mono category with finite products and kernels.
Русский
Пулбек двух моно-морфизмов существует в нормальной монокатегории с конечными произведениями и ядрами.
LaTeX
$$$\forall X,Y,Z\, (a:X\to Z)\,(b:Y\to Z)\,[Mono\ a][Mono\ b]\;:\; HasLimit(\mathrm{cospan}\ a\ b)$$$
Lean4
/-- The pullback of two monomorphisms exists. -/
theorem pullback_of_mono {X Y Z : C} (a : X ⟶ Z) (b : Y ⟶ Z) [Mono a] [Mono b] : HasLimit (cospan a b) :=
let ⟨P, f, haf, i⟩ := normalMonoOfMono a
let ⟨Q, g, hbg, i'⟩ := normalMonoOfMono b
let ⟨a', ha'⟩ :=
KernelFork.IsLimit.lift' i (kernel.ι (prod.lift f g)) <|
calc
kernel.ι (prod.lift f g) ≫ f
_ = kernel.ι (prod.lift f g) ≫ prod.lift f g ≫ Limits.prod.fst := by rw [prod.lift_fst]
_ = (0 : kernel (prod.lift f g) ⟶ P ⨯ Q) ≫ Limits.prod.fst := by rw [kernel.condition_assoc]
_ = 0 := zero_comp
let ⟨b', hb'⟩ :=
KernelFork.IsLimit.lift' i' (kernel.ι (prod.lift f g)) <|
calc
kernel.ι (prod.lift f g) ≫ g
_ = kernel.ι (prod.lift f g) ≫ prod.lift f g ≫ Limits.prod.snd := by rw [prod.lift_snd]
_ = (0 : kernel (prod.lift f g) ⟶ P ⨯ Q) ≫ Limits.prod.snd := by rw [kernel.condition_assoc]
_ = 0 := zero_comp
HasLimit.mk
{ cone :=
PullbackCone.mk a' b' <|
by
simp? at ha' hb' says simp only [parallelPair_obj_zero, Fork.ofι_pt, Fork.ι_ofι] at ha' hb'
rw [ha', hb']
isLimit :=
PullbackCone.IsLimit.mk _
(fun s =>
kernel.lift (prod.lift f g) (PullbackCone.snd s ≫ b) <|
Limits.prod.hom_ext
(calc
((PullbackCone.snd s ≫ b) ≫ prod.lift f g) ≫ Limits.prod.fst = PullbackCone.snd s ≫ b ≫ f := by
simp only [prod.lift_fst, Category.assoc]
_ = PullbackCone.fst s ≫ a ≫ f := by rw [PullbackCone.condition_assoc]
_ = PullbackCone.fst s ≫ 0 := by rw [haf]
_ = 0 ≫ Limits.prod.fst := by rw [comp_zero, zero_comp])
(calc
((PullbackCone.snd s ≫ b) ≫ prod.lift f g) ≫ Limits.prod.snd = PullbackCone.snd s ≫ b ≫ g := by
simp only [prod.lift_snd, Category.assoc]
_ = PullbackCone.snd s ≫ 0 := by rw [hbg]
_ = 0 ≫ Limits.prod.snd := by rw [comp_zero, zero_comp]))
(fun s =>
(cancel_mono a).1 <| by
rw [KernelFork.ι_ofι] at ha'
simp [ha', PullbackCone.condition s])
(fun s =>
(cancel_mono b).1 <| by
rw [KernelFork.ι_ofι] at hb'
simp [hb'])
fun s m h₁ _ =>
(cancel_mono (kernel.ι (prod.lift f g))).1 <|
calc
m ≫ kernel.ι (prod.lift f g) = m ≫ a' ≫ a := by
congr
exact ha'.symm
_ = PullbackCone.fst s ≫ a := by rw [← Category.assoc, h₁]
_ = PullbackCone.snd s ≫ b := (PullbackCone.condition s)
_ = kernel.lift (prod.lift f g) (PullbackCone.snd s ≫ b) _ ≫ kernel.ι (prod.lift f g) := by
rw [kernel.lift_ι] }
