mathlib documentation


structure category_theory.simple {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] (X : C) :
Type (max u v)

An object is simple if monomorphisms into it are (exclusively) either isomorphisms or zero.

We don't want the definition of 'simple' to include the zero object, so we check that here.

In an abelian category, an object satisfying the dual of the definition of a simple object is simple.