Structures · Category theory

CategoryTheory.NonPreadditiveAbelian

We call a category NonPreadditiveAbelian if it has a zero object, kernels, cokernels, finite products and coproducts, and every monomorphism and every epimorphism is normal. Notice that every such category is abelian (see CategoryTheory.NonPreadditiveAbelian.preadditive), so in practice it is preferable to work directly with Abelian.

Defined in

Mathlib.CategoryTheory.Abelian.NonPreadditive

Shape

One type argument · adds has_zero_object, has_kernels, has_cokernels, has_finite_products, has_finite_coproducts