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} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (X : C) : Prop

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

• mono_isIso_iff_nonzero {Y : C} (f : Y ⟶ X) [Mono f] : IsIso f ↔ f ≠ 0

theorem CategoryTheory.isIso_of_mono_of_nonzero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} [Simple Y] {f : X ⟶ Y} [Mono f] (w : f ≠ 0) : IsIso f

A nonzero monomorphism to a simple object is an isomorphism.

theorem CategoryTheory.Simple.of_iso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} [Simple Y] (i : X ≅ Y) : Simple X

theorem CategoryTheory.Simple.iff_of_iso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} (i : X ≅ Y) : Simple X ↔ Simple Y

theorem CategoryTheory.kernel_zero_of_nonzero_from_simple {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} [Simple X] {f : X ⟶ Y} [Limits.HasKernel f] (w : f ≠ 0) : Limits.kernel.ι f = 0

theorem CategoryTheory.epi_of_nonzero_to_simple {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasEqualizers C] {X Y : C} [Simple Y] {f : X ⟶ Y} [Limits.HasImage f] (w : f ≠ 0) : Epi f

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} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} [Simple Y] {f : X ⟶ Y} [Mono f] (w : IsIso f → False) : f = 0

theorem CategoryTheory.id_nonzero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (X : C) [Simple X] : CategoryStruct.id X ≠ 0

instance CategoryTheory.instNontrivialEndOfSimple {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (X : C) [Simple X] : Nontrivial (End X)

theorem CategoryTheory.Simple.not_isZero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (X : C) [Simple X] : ¬Limits.IsZero X

theorem CategoryTheory.zero_not_simple (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Simple 0] : False

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} [Category.{v, u} C] [Abelian C] (X : C) (h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0) : Simple X

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} [Category.{v, u} C] [Abelian C] {X Y : C} [Simple X] {f : X ⟶ Y} [Epi f] (w : f ≠ 0) : IsIso f

A nonzero epimorphism from a simple object is an isomorphism.

theorem CategoryTheory.cokernel_zero_of_nonzero_to_simple {C : Type u} [Category.{v, u} C] [Abelian C] {X Y : C} [Simple Y] {f : X ⟶ Y} (w : f ≠ 0) : Limits.cokernel.π f = 0

theorem CategoryTheory.epi_from_simple_zero_of_not_iso {C : Type u} [Category.{v, u} C] [Abelian C] {X Y : C} [Simple X] {f : X ⟶ Y} [Epi f] (w : IsIso f → False) : f = 0

theorem CategoryTheory.Biprod.isIso_inl_iff_isZero {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] (X Y : C) : IsIso Limits.biprod.inl ↔ Limits.IsZero Y

theorem CategoryTheory.indecomposable_of_simple {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] (X : C) [Simple X] : Indecomposable X

Any simple object in a preadditive category is indecomposable.

instance CategoryTheory.instNontrivialSubobjectOfSimple {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {X : C} [Simple X] : Nontrivial (Subobject X)

instance CategoryTheory.instIsSimpleOrderSubobjectOfSimple {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {X : C} [Simple X] : IsSimpleOrder (Subobject X)

theorem CategoryTheory.simple_of_isSimpleOrder_subobject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (X : C) [IsSimpleOrder (Subobject X)] : Simple X

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

theorem CategoryTheory.simple_iff_subobject_isSimpleOrder {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (X : C) : Simple X ↔ IsSimpleOrder (Subobject X)

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

theorem CategoryTheory.subobject_simple_iff_isAtom {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {X : C} (Y : Subobject X) : Simple (Subobject.underlying.obj Y) ↔ IsAtom Y

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