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

@@ -28,14 +28,19 @@ 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.
 -/
 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
 

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