hasBinaryCoproducts_of_hasBinaryBiproducts

English

Let C be a category with binary biproducts for every pair of objects. Then C has binary coproducts.

Русский

Пусть C — категория, в которой для любых пар объектов существуют двоичные би-произведения. Тогда C имеет двоичные копродукты.

LaTeX

$$$\operatorname{HasBinaryBiproducts}(\mathcal{C}) \Rightarrow \operatorname{HasBinaryCoproducts}(\mathcal{C})$$$

Lean4

instance (priority := 100) hasBinaryCoproducts_of_hasBinaryBiproducts [HasBinaryBiproducts C] : HasBinaryCoproducts C
    where has_colimit F := hasColimit_of_iso (diagramIsoPair F)

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