hasCoequalizers_of_hasPushouts_and_binary_coproducts

English

If a category C has binary coproducts and pushouts, then every pair of parallel arrows has a coequalizer.

Русский

Если в категории C существуют двоичные копроизведения и пушауты, то любая пара параллельных стрел имеет коэквалайзер.

LaTeX

$$$\text{HasCoequalizers}(C)$$$

Lean4

/-- Any category with pullbacks and binary products, has equalizers. -/
theorem hasCoequalizers_of_hasPushouts_and_binary_coproducts [HasBinaryCoproducts C] [HasPushouts C] :
    HasCoequalizers C :=
  {
    has_colimit := fun F =>
      HasColimit.mk
        { cocone := coequalizerCocone F
          isColimit := coequalizerCoconeIsColimit F } }

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