English
In a Normal Mono category with finite products and kernels, the equalizer of two morphisms f and g exists, i.e., HasLimit(parallelPair f g).
Русский
В нормальной моно-категории с конечными произведениями и ядрами равнитель двух морфизмов f и g существует.
LaTeX
$$$\forall X,Y: C\, (f,g: X\to Y)\; HasLimit(\text{parallelPair } f\ g)$$$
Lean4
/-- The equalizer of `f` and `g` exists. -/
theorem hasLimit_parallelPair {X Y : C} (f g : X ⟶ Y) : HasLimit (parallelPair f g) :=
have huv : (pullback.fst _ _ : P f g ⟶ X) = pullback.snd _ _ :=
calc
(pullback.fst _ _ : P f g ⟶ X) = pullback.fst _ _ ≫ 𝟙 _ := Eq.symm <| Category.comp_id _
_ = pullback.fst _ _ ≫ prod.lift (𝟙 X) f ≫ Limits.prod.fst := by rw [prod.lift_fst]
_ = pullback.snd _ _ ≫ prod.lift (𝟙 X) g ≫ Limits.prod.fst := by rw [pullback.condition_assoc]
_ = pullback.snd _ _ := by rw [prod.lift_fst, Category.comp_id]
have hvu : (pullback.fst _ _ : P f g ⟶ X) ≫ f = pullback.snd _ _ ≫ g :=
calc
(pullback.fst _ _ : P f g ⟶ X) ≫ f = pullback.fst _ _ ≫ prod.lift (𝟙 X) f ≫ Limits.prod.snd := by
rw [prod.lift_snd]
_ = pullback.snd _ _ ≫ prod.lift (𝟙 X) g ≫ Limits.prod.snd := by rw [pullback.condition_assoc]
_ = pullback.snd _ _ ≫ g := by rw [prod.lift_snd]
have huu : (pullback.fst _ _ : P f g ⟶ X) ≫ f = pullback.fst _ _ ≫ g := by rw [hvu, ← huv]
HasLimit.mk
{ cone := Fork.ofι (pullback.fst _ _) huu
isLimit :=
Fork.IsLimit.mk _
(fun s =>
pullback.lift (Fork.ι s) (Fork.ι s) <|
Limits.prod.hom_ext (by simp only [prod.lift_fst, Category.assoc])
(by simp only [prod.comp_lift, Fork.condition s]))
(fun s => by simp) fun s m h =>
pullback.hom_ext (by simpa only [pullback.lift_fst] using h)
(by simpa only [huv.symm, pullback.lift_fst] using h) }
