feat(category_theory/.../zero): if a zero morphism is a mono, the sou…

…rce is zero (#7462)

Some simple lemmas about zero morphisms.





Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/limits/shapes/zero.lean

@@ -211,6 +211,18 @@ has_initial_of_unique 0
 lemma has_terminal : has_terminal C :=
 has_terminal_of_unique 0
 
+local attribute [instance] has_zero_object.has_zero
+
+instance {B : Type*} [category B] [has_zero_morphisms C] : has_zero_object (B ⥤ C) :=
+{ zero := { obj := λ X, 0, map := λ X Y f, 0, },
+  unique_to := λ F, ⟨⟨{ app := λ X, 0, }⟩, by tidy⟩,
+  unique_from := λ F, ⟨⟨{ app := λ X, 0, }⟩, by tidy⟩ }
+
+@[simp] lemma functor.zero_obj {B : Type*} [category B] [has_zero_morphisms C] (X : B) :
+  (0 : B ⥤ C).obj X = 0 := rfl
+@[simp] lemma functor.zero_map {B : Type*} [category B] [has_zero_morphisms C]
+  {X Y : B} (f : X ⟶ Y) : (0 : B ⥤ C).map f = 0 := rfl
+
 end has_zero_object
 
 section
@@ -272,6 +284,20 @@ lemma id_zero_equiv_iso_zero_apply_hom (X : C) (h : 𝟙 X = 0) :
 lemma id_zero_equiv_iso_zero_apply_inv (X : C) (h : 𝟙 X = 0) :
   ((id_zero_equiv_iso_zero X) h).inv = 0 := rfl
 
+/-- If `0 : X ⟶ Y` is an monomorphism, then `X ≅ 0`. -/
+@[simps]
+def iso_zero_of_mono_zero {X Y : C} (h : mono (0 : X ⟶ Y)) : X ≅ 0 :=
+{ hom := 0,
+  inv := 0,
+  hom_inv_id' := (cancel_mono (0 : X ⟶ Y)).mp (by simp) }
+
+/-- If `0 : X ⟶ Y` is an epimorphism, then `Y ≅ 0`. -/
+@[simps]
+def iso_zero_of_epi_zero {X Y : C} (h : epi (0 : X ⟶ Y)) : Y ≅ 0 :=
+{ hom := 0,
+  inv := 0,
+  hom_inv_id' := (cancel_epi (0 : X ⟶ Y)).mp (by simp) }
+
 /-- If an object `X` is isomorphic to 0, there's no need to use choice to construct
 an explicit isomorphism: the zero morphism suffices. -/
 def iso_of_is_isomorphic_zero {X : C} (P : is_isomorphic X 0) : X ≅ 0 :=
@@ -333,6 +359,12 @@ begin
   { tidy, },
 end
 
+lemma is_iso_of_source_target_iso_zero {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) (j : Y ≅ 0) : is_iso f :=
+begin
+  rw zero_of_source_iso_zero f i,
+  exact (is_iso_zero_equiv_iso_zero _ _).inv_fun ⟨i, j⟩,
+end
+
 /--
 A zero morphism `0 : X ⟶ X` is an isomorphism if and only if
 `X` is isomorphic to the zero object.