From 098ab17f68a4533aae57771d2bfc3058a6165de6 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Wed, 4 May 2022 07:50:58 +0000
Subject: [PATCH] feat(category_theory/simple): nonzero morphisms to/from a
 simple are epi/mono (#13905)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
---
 src/category_theory/preadditive/schur.lean |  7 ++++++-
 src/category_theory/simple.lean            | 13 +++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/category_theory/preadditive/schur.lean b/src/category_theory/preadditive/schur.lean
index 22566b9338844..e37533d9f1990 100644
--- a/src/category_theory/preadditive/schur.lean
+++ b/src/category_theory/preadditive/schur.lean
@@ -28,6 +28,11 @@ open category_theory.limits
 variables {C : Type*} [category C]
 variables [preadditive C]
 
+-- See also `epi_of_nonzero_to_simple`, which does not require `preadditive C`.
+lemma mono_of_nonzero_from_simple [has_kernels C] {X Y : C} [simple X] {f : X ⟶ Y} (w : f ≠ 0) :
+  mono f :=
+preadditive.mono_of_kernel_zero (kernel_zero_of_nonzero_from_simple w)
+
 /--
 The part of **Schur's lemma** that holds in any preadditive category with kernels:
 that a nonzero morphism between simple objects is an isomorphism.
@@ -35,7 +40,7 @@ that a nonzero morphism between simple objects is an isomorphism.
 lemma is_iso_of_hom_simple [has_kernels C] {X Y : C} [simple X] [simple Y] {f : X ⟶ Y} (w : f ≠ 0) :
   is_iso f :=
 begin
-  haveI : mono f := preadditive.mono_of_kernel_zero (kernel_zero_of_nonzero_from_simple w),
+  haveI := mono_of_nonzero_from_simple w,
   exact is_iso_of_mono_of_nonzero w
 end
 
diff --git a/src/category_theory/simple.lean b/src/category_theory/simple.lean
index a19205474b3bc..7d5fa5786e259 100644
--- a/src/category_theory/simple.lean
+++ b/src/category_theory/simple.lean
@@ -79,6 +79,19 @@ begin
   exact w (eq_zero_of_epi_kernel f),
 end
 
+/--
+A nonzero morphism `f` to a simple object is an epimorphism
+(assuming `f` has an image, and `C` has equalizers).
+-/
+-- See also `mono_of_nonzero_from_simple`, which requires `preadditive C`.
+lemma epi_of_nonzero_to_simple [has_equalizers C] {X Y : C} [simple Y]
+  {f : X ⟶ Y} [has_image f] (w : f ≠ 0) : epi f :=
+begin
+  rw ←image.fac f,
+  haveI : is_iso (image.ι f) := is_iso_of_mono_of_nonzero (λ h, w (eq_zero_of_image_eq_zero h)),
+  apply epi_comp,
+end
+
 lemma mono_to_simple_zero_of_not_iso
   {X Y : C} [simple Y] {f : X ⟶ Y} [mono f] (w : is_iso f → false) : f = 0 :=
 begin