hasBinaryBiproducts_of_finite_biproducts

English

A category with finite biproducts has binary biproducts. The construction uses biproducts of pairs via the biproduct data for the pair function.

Русский

Категория, имеющая конечные би-произведения, обладает бинарными би-произведениями. Конструкция использует би-произведения пары через пары функций.

LaTeX

$$$ \text{HasFiniteBiproducts } C \Rightarrow \text{HasBinaryBiproducts } C. $$$

Lean4

/-- A category with finite biproducts has binary biproducts.

This is not an instance as typically in concrete categories there will be
an alternative construction with nicer definitional properties. -/
theorem hasBinaryBiproducts_of_finite_biproducts [HasFiniteBiproducts C] : HasBinaryBiproducts C :=
  {
    has_binary_biproduct := fun P Q =>
      HasBinaryBiproduct.mk
        { bicone := (biproduct.bicone (pairFunction P Q)).toBinaryBicone
          isBilimit := (Bicone.toBinaryBiconeIsBilimit _).symm (biproduct.isBilimit _) } }

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