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 https://ncatlab.org/nlab/show/biproduct#BiproductsImplyEnrichment
@[class]
structure
category_theory.additive_category
(C : Type u)
[category_theory.category C] :
Type (max u u_1)
- to_preadditive : category_theory.preadditive C
- to_has_finite_biproducts : category_theory.limits.has_finite_biproducts C
A preadditive category C is called additive if it has all finite biproducts.
See https://stacks.math.columbia.edu/tag/0104.
Instances of this typeclass
Instances of other typeclasses for category_theory.additive_category
- category_theory.additive_category.has_sizeof_inst