hasFiniteCoproducts_of_hasFiniteBiproducts

English

If a category C has finite biproducts, then it has finite coproducts (dually to finite biproducts).

Русский

Если в категории C существуют конечные бипродукты, то существуют и конечные копродукты.

LaTeX

$$$\text{HasFiniteBiproducts}(C) \Rightarrow \text{HasFiniteCoproducts}(C)$$$

Lean4

instance (priority := 100) hasFiniteCoproducts_of_hasFiniteBiproducts [HasFiniteBiproducts C] : HasFiniteCoproducts C
    where out _ := ⟨fun _ => hasColimit_of_iso Discrete.natIsoFunctor⟩

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