hasCoequalizers_of_hasColimit_parallelPair

English

If every diagram parallelPair f g has a colimit in C, then C has all coequalizers.

Русский

Если для каждой пары стрел f,g существуют колимиты диаграммы parallelPair в C, тогда C имеет все коэквалайзеры.

LaTeX

$$$ [\\forall X,Y,f,g, \\ HasColimit( parallelPair f g )] \\Rightarrow HasCoequalizers C $$$

Lean4

/-- If `C` has all colimits of diagrams `parallelPair f g`, then it has all coequalizers -/
theorem hasCoequalizers_of_hasColimit_parallelPair [∀ {X Y : C} {f g : X ⟶ Y}, HasColimit (parallelPair f g)] :
    HasCoequalizers C :=
  { has_colimit := fun F => hasColimit_of_iso (diagramIsoParallelPair F) }

Похожие утверждения