Theorems · Inductive type · category theory

CategoryTheory.Abelian

(C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)

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

Cited by

1,753 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category