hasCoproduct_of_hasBiproduct — Mathlib

English

From HasBiproduct F, obtain HasCoproduct F by taking the biproduct cone as a cocone.

Русский

Из HasBiproduct F получаем HasCoproduct F, рассматривая биконус как кокон.

LaTeX

$$$$ \\text{HasCoproduct}(F) := \\text{HasColimit}(F) \\text{ with cocone given by } (biproduct.bicone F).toCocone. $$$$

Lean4

instance (priority := 100) hasCoproduct_of_hasBiproduct [HasBiproduct F] : HasCoproduct F :=
  HasColimit.mk
    { cocone := (biproduct.bicone F).toCocone
      isColimit := biproduct.isColimit F }

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