mathlib documentation


Additive Categories #

This file contains the definition of additive categories.

TODO: show that finite biproducts implies enriched over commutative monoids and what is missing additionally to have additivity is that identities have additive inverses, see

structure category_theory.additive_category (C : Type u) [category_theory.category C] :
Type (max u u_1)

A preadditive category C is called additive if it has all finite biproducts. See