mathlib documentation


Simple objects #

We define simple objects in any category with zero morphisms. A simple object is an object Y such that any monomorphism f : X ⟶ Y is either an isomorphism or zero (but not both).

This is formalized as a Prop valued typeclass simple X.

If a morphism f out of a simple object is nonzero and has a kernel, then that kernel is zero. (We state this as kernel.ι f = 0, but should add kernel f ≅ 0.)

When the category is abelian, being simple is the same as being cosimple (although we do not state a separate typeclass for this). As a consequence, any nonzero epimorphism out of a simple object is an isomorphism, and any nonzero morphism into a simple object has trivial cokernel.


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

A nonzero monomorphism to a simple object is an isomorphism.

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.

A nonzero epimorphism from a simple object is an isomorphism.