Structures · Category theory

CategoryTheory.Abelian

A (preadditive) category C is called abelian if it has all finite products, all kernels and cokernels, and if every monomorphism is the kernel of some morphism and every epimorphism is the cokernel of some morphism. (This definition implies the existence of zero objects: finite products give a terminal object, and in a preadditive category any terminal object is a zero object.)

Defined in

Mathlib.CategoryTheory.Abelian.Basic

Shape

One type argument · adds has_finite_products, has_kernels, has_cokernels