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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.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) [CategoryTheory.Mono f] : CategoryTheory.IsIso f ↔ f ≠ 0

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

A nonzero monomorphism to a simple object is an isomorphism.

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

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

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

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

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

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

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

theorem CategoryTheory.zero_not_simple (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) (h : ∀ {Z : C} (f : X ⟶ Z) [inst : CategoryTheory.Epi f], CategoryTheory.IsIso f ↔ f ≠ 0) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} [CategoryTheory.Simple X] {f : X ⟶ Y} [CategoryTheory.Epi f] (w : f ≠ 0) : CategoryTheory.IsIso f

A nonzero epimorphism from a simple object is an isomorphism.

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

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

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

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

Any simple object in a preadditive category is indecomposable.

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

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

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

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

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

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

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

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