English
Let f,g: X ⟶ Y be parallel morphisms in a category that has zero morphisms, finite coproducts, cokernels, and is a Normal Epi category. Then the coequalizer (the coequalizing object) of f and g exists.
Русский
Пусть f, g: X ⟶ Y — пара параллельных стрелок в категории, которая имеет нулевые морфизмы, конечные копродукты, коточкако, и является категорией с нормальным эпиморсом. Тогда существует коэквалент пары f и g.
LaTeX
$$$\mathrm{HasColimit}\big(\mathrm{parallelPair}(f,g)\big)$$$
Lean4
/-- The coequalizer of `f` and `g` exists. -/
theorem hasColimit_parallelPair {X Y : C} (f g : X ⟶ Y) : HasColimit (parallelPair f g) :=
have huv : (pushout.inl _ _ : Y ⟶ Q f g) = pushout.inr _ _ :=
calc
(pushout.inl _ _ : Y ⟶ Q f g) = 𝟙 _ ≫ pushout.inl _ _ := Eq.symm <| Category.id_comp _
_ = (coprod.inl ≫ coprod.desc (𝟙 Y) f) ≫ pushout.inl _ _ := by rw [coprod.inl_desc]
_ = (coprod.inl ≫ coprod.desc (𝟙 Y) g) ≫ pushout.inr _ _ := by simp only [Category.assoc, pushout.condition]
_ = pushout.inr _ _ := by rw [coprod.inl_desc, Category.id_comp]
have hvu : f ≫ (pushout.inl _ _ : Y ⟶ Q f g) = g ≫ pushout.inr _ _ :=
calc
f ≫ (pushout.inl _ _ : Y ⟶ Q f g) = (coprod.inr ≫ coprod.desc (𝟙 Y) f) ≫ pushout.inl _ _ := by
rw [coprod.inr_desc]
_ = (coprod.inr ≫ coprod.desc (𝟙 Y) g) ≫ pushout.inr _ _ := by simp only [Category.assoc, pushout.condition]
_ = g ≫ pushout.inr _ _ := by rw [coprod.inr_desc]
have huu : f ≫ (pushout.inl _ _ : Y ⟶ Q f g) = g ≫ pushout.inl _ _ := by rw [hvu, huv]
HasColimit.mk
{ cocone := Cofork.ofπ (pushout.inl _ _) huu
isColimit :=
Cofork.IsColimit.mk _
(fun s =>
pushout.desc (Cofork.π s) (Cofork.π s) <|
coprod.hom_ext (by simp only [coprod.inl_desc_assoc])
(by simp only [coprod.desc_comp, Cofork.condition s]))
(fun s => by simp only [pushout.inl_desc, Cofork.π_ofπ]) fun s m h =>
pushout.hom_ext (by simpa only [pushout.inl_desc] using h)
(by simpa only [huv.symm, pushout.inl_desc] using h) }
