# 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.

In some contexts, especially representation theory, simple objects are called "irreducibles".

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.

We show that any simple object is indecomposable.

class CategoryTheory.Simple {C : Type u} (X : C) :

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

• mono_isIso_iff_nonzero : ∀ {Y : C} (f : Y X) [inst : ], f 0
Instances
theorem CategoryTheory.Simple.mono_isIso_iff_nonzero {C : Type u} {X : C} [self : ] {Y : C} (f : Y X) :
f 0
theorem CategoryTheory.isIso_of_mono_of_nonzero {C : Type u} {X : C} {Y : C} {f : X Y} (w : f 0) :

A nonzero monomorphism to a simple object is an isomorphism.

theorem CategoryTheory.Simple.of_iso {C : Type u} {X : C} {Y : C} (i : X Y) :
theorem CategoryTheory.Simple.iff_of_iso {C : Type u} {X : C} {Y : C} (i : X Y) :
theorem CategoryTheory.kernel_zero_of_nonzero_from_simple {C : Type u} {X : C} {Y : C} {f : X Y} (w : f 0) :
theorem CategoryTheory.epi_of_nonzero_to_simple {C : Type u} {X : C} {Y : C} {f : X Y} (w : f 0) :

A nonzero morphism f to a simple object is an epimorphism (assuming f has an image, and C has equalizers).

theorem CategoryTheory.mono_to_simple_zero_of_not_iso {C : Type u} {X : C} {Y : C} {f : X Y} (w : ) :
f = 0
theorem CategoryTheory.id_nonzero {C : Type u} (X : C) :
Equations
• =

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

theorem CategoryTheory.simple_of_cosimple {C : Type u} (X : C) (h : ∀ {Z : C} (f : X Z) [inst : ], f 0) :

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

theorem CategoryTheory.isIso_of_epi_of_nonzero {C : Type u} {X : C} {Y : C} {f : X Y} (w : f 0) :

A nonzero epimorphism from a simple object is an isomorphism.

theorem CategoryTheory.cokernel_zero_of_nonzero_to_simple {C : Type u} {X : C} {Y : C} {f : X Y} (w : f 0) :
theorem CategoryTheory.epi_from_simple_zero_of_not_iso {C : Type u} {X : C} {Y : C} {f : X Y} (w : ) :
f = 0
theorem CategoryTheory.Biprod.isIso_inl_iff_isZero {C : Type u} (X : C) (Y : C) :
CategoryTheory.IsIso CategoryTheory.Limits.biprod.inl

Any simple object in a preadditive category is indecomposable.

Equations
• =
Equations
• =

If X has subobject lattice {⊥, ⊤}, then X is simple.

X is simple iff it has subobject lattice {⊥, ⊤}.

theorem CategoryTheory.subobject_simple_iff_isAtom {C : Type u} {X : C} (Y : ) :
CategoryTheory.Simple (CategoryTheory.Subobject.underlying.obj Y)

A subobject is simple iff it is an atom in the subobject lattice.