English
In an abelian category, an object satisfying the dual condition of simplicity is simple.
Русский
В абелевой категории объект, удовлетворяющий двойственному условию простоты, является простым.
LaTeX
$$$ (\forall Z, \forall f: X \to Z) [\mathrm{Epi}(f)], (IsIso(f) \iff f \neq 0) \Rightarrow Simple(X). $$$
Lean4
/-- In an abelian category, an object satisfying the dual of the definition of a simple object is
simple. -/
theorem simple_of_cosimple (X : C) (h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0) : Simple X :=
⟨fun {Y} f I => by
classical
fconstructor
· intros
have hx := cokernel.π_of_epi f
by_contra h
subst h
exact (h _).mp (cokernel.π_of_zero _ _) hx
· intro hf
suffices Epi f by exact isIso_of_mono_of_epi _
apply Preadditive.epi_of_cokernel_zero
by_contra h'
exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')⟩
