hasBinaryCoproducts_of_hasInitial_and_pushouts

English

Any category with an initial object and pushouts has binary coproducts.

Русский

Любая категория с начальным объектом и пушаутами имеет бинарные копродукты.

LaTeX

$$$\\forall C:\\,\\text{Category},\\ HasInitial C\\,\\land\\ HasPushouts C\\Rightarrow\\ HasBinaryCoproducts C$$$

Lean4

/-- Any category with pushouts and initial object has binary coproducts. -/
theorem hasBinaryCoproducts_of_hasInitial_and_pushouts [HasInitial C] [HasPushouts C] : HasBinaryCoproducts C :=
  { has_colimit := fun F => HasColimit.mk (colimitCoconeOfInitialAndPushouts F) }

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