@[class]
structure
category_theory.simple
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
C → Type (max u v)
- mono_is_iso_equiv_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.
@[ext]
theorem
category_theory.simple.ext
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X : C}
{a b : category_theory.simple X} :
a = b
@[instance]
def
category_theory.subsingleton_simple
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
Equations
- _ = _
def
category_theory.is_iso_of_mono_of_nonzero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.simple Y]
{f : X ⟶ Y}
[category_theory.mono f] :
f ≠ 0 → category_theory.is_iso f
A nonzero monomorphism to a simple object is an isomorphism.
theorem
category_theory.kernel_zero_of_nonzero_from_simple
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.simple X]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f] :
f ≠ 0 → category_theory.limits.kernel.ι f = 0
theorem
category_theory.mono_to_simple_zero_of_not_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.simple Y]
{f : X ⟶ Y}
[category_theory.mono f] :
(category_theory.is_iso f → false) → f = 0
theorem
category_theory.id_nonzero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X : C)
[category_theory.simple X] :
theorem
category_theory.zero_not_simple
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
[category_theory.simple 0] :
We don't want the definition of 'simple' to include the zero object, so we check that here.
def
category_theory.simple_of_cosimple
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
(X : C) :
(Π {Z : C} (f : X ⟶ Z) [_inst_3 : category_theory.epi f], category_theory.is_iso f ≃ f ≠ 0) → category_theory.simple X
In an abelian category, an object satisfying the dual of the definition of a simple object is simple.
Equations
- category_theory.simple_of_cosimple X h = {mono_is_iso_equiv_nonzero := λ (Y : C) (f : Y ⟶ X) (I : category_theory.mono f), equiv_of_subsingleton_of_subsingleton _ (λ (hf : f ≠ 0), category_theory.abelian.is_iso_of_mono_of_epi f)}
def
category_theory.is_iso_of_epi_of_nonzero
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
{X Y : C}
[category_theory.simple X]
{f : X ⟶ Y}
[category_theory.epi f] :
f ≠ 0 → category_theory.is_iso f
A nonzero epimorphism from a simple object is an isomorphism.
theorem
category_theory.cokernel_zero_of_nonzero_to_simple
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
{X Y : C}
[category_theory.simple Y]
{f : X ⟶ Y}
[category_theory.limits.has_cokernel f] :
f ≠ 0 → category_theory.limits.cokernel.π f = 0
theorem
category_theory.epi_from_simple_zero_of_not_iso
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
{X Y : C}
[category_theory.simple X]
{f : X ⟶ Y}
[category_theory.epi f] :
(category_theory.is_iso f → false) → f = 0