Simple objects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
- mono_is_iso_iff_nonzero : ∀ {Y : C} (f : Y ⟶ X) [_inst_3 : category_theory.mono f], category_theory.is_iso f ↔ f ≠ 0
An object is simple if monomorphisms into it are (exclusively) either isomorphisms or zero.
Instances of this typeclass
A nonzero monomorphism to a simple object is an isomorphism.
A nonzero morphism f to a simple object is an epimorphism
(assuming f has an image, and C has equalizers).
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.
Any simple object in a preadditive category is indecomposable.
If X has subobject lattice {⊥, ⊤}, then X is simple.
X is simple iff it has subobject lattice {⊥, ⊤}.
A subobject is simple iff it is an atom in the subobject lattice.