mathlib documentation

category_theory.preadditive.of_biproducts

Constructing a semiadditive structure from binary biproducts #

We show that any category with zero morphisms and binary biproducts is enriched over the category of commutative monoids.

@[simp]

f +ₗ g is the composite X ⟶ Y ⊞ Y ⟶ Y, where the first map is (f, g) and the second map is (𝟙 𝟙).

Equations
@[simp]

f +ᵣ g is the composite X ⟶ X ⊞ X ⟶ Y, where the first map is (𝟙, 𝟙) and the second map is (f g).

Equations