# mathlibdocumentation

category_theory.simple

# 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]
structure category_theory.simple {C : Type u} (X : C) :
Prop
• mono_is_iso_iff_nonzero : ∀ {Y : C} (f : Y X) [_inst_3 : , f 0

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

Instances of this typeclass
theorem category_theory.is_iso_of_mono_of_nonzero {C : Type u} {X Y : C} {f : X Y} (w : f 0) :

A nonzero monomorphism to a simple object is an isomorphism.

theorem category_theory.simple.of_iso {C : Type u} {X Y : C} (i : X Y) :
theorem category_theory.kernel_zero_of_nonzero_from_simple {C : Type u} {X Y : C} {f : X Y} (w : f 0) :
theorem category_theory.epi_of_nonzero_to_simple {C : Type u} {X 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 category_theory.mono_to_simple_zero_of_not_iso {C : Type u} {X Y : C} {f : X Y} (w : false) :
f = 0
theorem category_theory.id_nonzero {C : Type u} (X : C)  :
𝟙 X 0
@[protected, instance]
def category_theory.End.nontrivial {C : Type u} (X : C)  :
theorem category_theory.simple.not_is_zero {C : Type u} (X : C)  :

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

theorem category_theory.simple_of_cosimple {C : Type u} (X : C) (h : ∀ {Z : C} (f : X Z) [_inst_3 : , f 0) :

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

theorem category_theory.is_iso_of_epi_of_nonzero {C : Type u} {X Y : C} {f : X Y} (w : f 0) :

A nonzero epimorphism from a simple object is an isomorphism.

theorem category_theory.cokernel_zero_of_nonzero_to_simple {C : Type u} {X Y : C} {f : X Y} (w : f 0) :
theorem category_theory.epi_from_simple_zero_of_not_iso {C : Type u} {X Y : C} {f : X Y} (w : false) :
f = 0

Any simple object in a preadditive category is indecomposable.

@[protected, instance]
@[protected, instance]

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

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

theorem category_theory.subobject_simple_iff_is_atom {C : Type u} {X : C}  :

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