hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers

English

If a category has binary coproducts and coequalizers, then it has all pushouts.

Русский

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

LaTeX

$$$$\text{HasPushouts } C\,,$$$$

Lean4

/-- If a category has all binary coproducts and all coequalizers, then it also has all pushouts.
As usual, this is not an instance, since there may be a more direct way to construct pushouts. -/
theorem hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers (C : Type u) [Category.{v} C] [HasBinaryCoproducts C]
    [HasCoequalizers C] : HasPushouts C :=
  hasPushouts_of_hasColimit_span C

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