mathlib documentation

category_theory.additive.basic

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]

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