feat(category_theory/limits): preservation of zero morphisms (#12068)

Author: TwoFX

src/category_theory/differential_object.lean

@@ -219,7 +219,7 @@ def shift_functor (n : ℤ) : differential_object C ⥤ differential_object C :=
   { X := X.X⟦n⟧,
     d := X.d⟦n⟧' ≫ (shift_comm _ _ _).hom,
     d_squared' := by rw [functor.map_comp, category.assoc, shift_comm_hom_comp_assoc,
-        ←functor.map_comp_assoc, X.d_squared, is_equivalence_preserves_zero_morphisms, zero_comp] },
+        ←functor.map_comp_assoc, X.d_squared, functor.map_zero, zero_comp] },
   map := λ X Y f,
   { f := f.f⟦n⟧',
     comm' := by { dsimp, rw [category.assoc, shift_comm_hom_comp, ← functor.map_comp_assoc,

src/category_theory/limits/preserves/shapes/zero.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2022 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import category_theory.limits.preserves.shapes.terminal
+import category_theory.limits.shapes.zero
+
+/-!
+# Preservation of zero objects and zero morphisms
+
+We define the class `preserves_zero_morphisms` and show basic properties.
+
+## Main results
+
+We provide the following results:
+* Left adjoints and right adjoints preserve zero morphisms;
+* full functors preserves zero morphisms;
+* if both categories involved have a zero object, then a functor preserves zero morphisms if and
+  only if it preserves the zero object;
+* functors which preserve initial or terminal objects preserve zero morphisms.
+
+-/
+
+universes v₁ v₂ u₁ u₂
+
+noncomputable theory
+
+open category_theory
+open category_theory.limits
+
+namespace category_theory.functor
+variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
+
+section zero_morphisms
+variables [has_zero_morphisms C] [has_zero_morphisms D]
+
+/-- A functor preserves zero morphisms if it sends zero morphisms to zero morphisms. -/
+class preserves_zero_morphisms (F : C ⥤ D) : Prop :=
+(map_zero' : ∀ (X Y : C), F.map (0 : X ⟶ Y) = 0 . obviously)
+
+@[simp]
+protected lemma map_zero (F : C ⥤ D) [preserves_zero_morphisms F] (X Y : C) :
+  F.map (0 : X ⟶ Y) = 0 :=
+preserves_zero_morphisms.map_zero' _ _
+
+@[priority 100]
+instance preserves_zero_morphisms_of_is_left_adjoint (F : C ⥤ D) [is_left_adjoint F] :
+  preserves_zero_morphisms F :=
+{ map_zero' := λ X Y, let adj := adjunction.of_left_adjoint F in
+  begin
+    calc F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) : _
+    ... = F.map 0 ≫ F.map ((right_adjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) : _
+    ... = 0 : _,
+    { rw adjunction.left_triangle_components, exact (category.comp_id _).symm },
+    { simp only [← category.assoc, ← F.map_comp, zero_comp] },
+    { simp only [adjunction.counit_naturality, comp_zero] }
+  end }
+
+@[priority 100]
+instance preserves_zero_morphisms_of_is_right_adjoint (G : C ⥤ D) [is_right_adjoint G] :
+  preserves_zero_morphisms G :=
+{ map_zero' := λ X Y, let adj := adjunction.of_right_adjoint G in
+  begin
+    calc G.map (0 : X ⟶ Y) = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 : _
+    ... = adj.unit.app (G.obj X) ≫ G.map ((left_adjoint G).map (0 : _ ⟶ G.obj X)) ≫ G.map 0 : _
+    ... = 0 : _,
+    { rw adjunction.right_triangle_components_assoc },
+    { simp only [← G.map_comp, comp_zero] },
+    { simp only [adjunction.unit_naturality_assoc, zero_comp] }
+  end }
+
+@[priority 100]
+instance preserves_zero_morphisms_of_full (F : C ⥤ D) [full F] : preserves_zero_morphisms F :=
+{ map_zero' := λ X Y, calc
+  F.map (0 : X ⟶ Y) = F.map (0 ≫ (F.preimage (0 : F.obj Y ⟶ F.obj Y))) : by rw zero_comp
+                ... = 0 : by rw [F.map_comp, F.image_preimage, comp_zero] }
+
+end zero_morphisms
+
+section zero_object
+variables [has_zero_object C] [has_zero_object D]
+
+open_locale zero_object
+
+variables [has_zero_morphisms C] [has_zero_morphisms D] (F : C ⥤ D)
+
+/-- A functor that preserves zero morphisms also preserves the zero object. -/
+@[simps] def map_zero_object [preserves_zero_morphisms F] : F.obj 0 ≅ 0 :=
+{ hom := 0,
+  inv := 0,
+  hom_inv_id' := by rw [← F.map_id, id_zero, F.map_zero, zero_comp],
+  inv_hom_id' := by rw [id_zero, comp_zero] }
+
+variables {F}
+
+lemma preserves_zero_morphisms_of_map_zero_object (i : F.obj 0 ≅ 0) : preserves_zero_morphisms F :=
+{ map_zero' := λ X Y, calc
+  F.map (0 : X ⟶ Y) = F.map (0 : X ⟶ 0) ≫ F.map 0 : by rw [← functor.map_comp, comp_zero]
+                ... = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0
+                        : by rw [iso.hom_inv_id, category.id_comp]
+                ... = 0 : by simp only [zero_of_to_zero i.hom, zero_comp, comp_zero] }
+
+@[priority 100]
+instance preserves_zero_morphisms_of_preserves_initial_object
+  [preserves_colimit (functor.empty.{v₁} C) F] : preserves_zero_morphisms F :=
+preserves_zero_morphisms_of_map_zero_object $ (F.map_iso has_zero_object.zero_iso_initial).trans $
+  (preserves_initial.iso F).trans has_zero_object.zero_iso_initial.symm
+
+@[priority 100]
+instance preserves_zero_morphisms_of_preserves_terminal_object
+  [preserves_limit (functor.empty.{v₁} C) F] : preserves_zero_morphisms F :=
+preserves_zero_morphisms_of_map_zero_object $ (F.map_iso has_zero_object.zero_iso_terminal).trans $
+    (preserves_terminal.iso F).trans has_zero_object.zero_iso_terminal.symm
+
+end zero_object
+
+end category_theory.functor

src/category_theory/limits/shapes/kernels.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Markus Himmel
 -/
-import category_theory.limits.shapes.zero
+import category_theory.limits.preserves.shapes.zero
 
 /-!
 # Kernels and cokernels

src/category_theory/limits/shapes/terminal.lean

@@ -266,6 +266,14 @@ by tidy
   initial.to P ≫ f = initial.to Q :=
 by tidy
 
+/-- The (unique) isomorphism between the chosen initial object and any other initial object. -/
+@[simp] def initial_iso_is_initial [has_initial C] {P : C} (t : is_initial P) : ⊥_ C ≅ P :=
+initial_is_initial.unique_up_to_iso t
+
+/-- The (unique) isomorphism between the chosen terminal object and any other terminal object. -/
+@[simp] def terminal_iso_is_terminal [has_terminal C] {P : C}  (t : is_terminal P) : ⊤_ C ≅ P :=
+terminal_is_terminal.unique_up_to_iso t
+
 /-- Any morphism from a terminal object is split mono. -/
 instance terminal.split_mono_from {Y : C} [has_terminal C] (f : ⊤_ C ⟶ Y) : split_mono f :=
 is_terminal.split_mono_from terminal_is_terminal _

src/category_theory/limits/shapes/zero.lean

@@ -129,24 +129,6 @@ instance : has_zero_morphisms (C ⥤ D) :=
 
 @[simp] lemma zero_app (F G : C ⥤ D) (j : C) : (0 : F ⟶ G).app j = 0 := rfl
 
-variables [has_zero_morphisms C]
-
-lemma equivalence_preserves_zero_morphisms (F : C ≌ D) (X Y : C) :
-  F.functor.map (0 : X ⟶ Y) = (0 : F.functor.obj X ⟶ F.functor.obj Y) :=
-begin
-  have t : F.functor.map (0 : X ⟶ Y) =
-    F.functor.map (0 : X ⟶ Y) ≫ (0 : F.functor.obj Y ⟶ F.functor.obj Y),
-  { apply faithful.map_injective (F.inverse),
-    rw [functor.map_comp, equivalence.inv_fun_map],
-    dsimp,
-    rw [zero_comp, comp_zero, zero_comp], },
-  exact t.trans (by simp)
-end
-
-@[simp] lemma is_equivalence_preserves_zero_morphisms (F : C ⥤ D) [is_equivalence F] (X Y : C) :
-  F.map (0 : X ⟶ Y) = 0 :=
-by rw [←functor.as_equivalence_functor F, equivalence_preserves_zero_morphisms]
-
 end
 
 variables (C)
@@ -225,6 +207,55 @@ has_initial_of_unique 0
 instance has_terminal : has_terminal C :=
 has_terminal_of_unique 0
 
+/-- The (unique) isomorphism between any initial object and the zero object. -/
+def zero_iso_is_initial {X : C} (t : is_initial X) : 0 ≅ X :=
+zero_is_initial.unique_up_to_iso t
+
+/-- The (unique) isomorphism between any terminal object and the zero object. -/
+def zero_iso_is_terminal {X : C} (t : is_terminal X) : 0 ≅ X :=
+zero_is_terminal.unique_up_to_iso t
+
+/-- The (unique) isomorphism between the chosen initial object and the chosen zero object. -/
+def zero_iso_initial [has_initial C] : 0 ≅ ⊥_ C :=
+zero_is_initial.unique_up_to_iso initial_is_initial
+
+/-- The (unique) isomorphism between the chosen terminal object and the chosen zero object. -/
+def zero_iso_terminal [has_terminal C] : 0 ≅ ⊤_ C :=
+zero_is_terminal.unique_up_to_iso terminal_is_terminal
+
+section has_zero_morphisms
+variables [has_zero_morphisms C]
+
+@[simp] lemma zero_iso_is_initial_hom {X : C} (t : is_initial X) :
+  (zero_iso_is_initial t).hom = 0 :=
+by ext
+
+@[simp] lemma zero_iso_is_initial_inv {X : C} (t : is_initial X) :
+  (zero_iso_is_initial t).inv = 0 :=
+by ext
+
+@[simp] lemma zero_iso_is_terminal_hom {X : C} (t : is_terminal X) :
+  (zero_iso_is_terminal t).hom = 0 :=
+by ext
+
+@[simp] lemma zero_iso_is_terminal_inv {X : C} (t : is_terminal X) :
+  (zero_iso_is_terminal t).inv = 0 :=
+by ext
+
+@[simp] lemma zero_iso_initial_hom [has_initial C] : zero_iso_initial.hom = (0 : 0 ⟶ ⊥_ C) :=
+by ext
+
+@[simp] lemma zero_iso_initial_inv [has_initial C] : zero_iso_initial.inv = (0 : ⊥_ C ⟶ 0) :=
+by ext
+
+@[simp] lemma zero_iso_terminal_hom [has_terminal C] : zero_iso_terminal.hom = (0 : 0 ⟶ ⊤_ C) :=
+by ext
+
+@[simp] lemma zero_iso_terminal_inv [has_terminal C] : zero_iso_terminal.inv = (0 : ⊤_ C ⟶ 0) :=
+by ext
+
+end has_zero_morphisms
+
 @[priority 100]
 instance has_strict_initial : initial_mono_class C :=
 initial_mono_class.of_is_initial zero_is_initial (λ X, category_theory.mono _)

src/category_theory/preadditive/additive_functor.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz, Scott Morrison
 -/
 import category_theory.preadditive
+import category_theory.limits.preserves.shapes.zero
 import category_theory.limits.shapes.biproducts
 
 /-!
@@ -54,9 +55,9 @@ add_monoid_hom.mk' (λ f, F.map f) (λ f g, F.map_add)
 
 lemma coe_map_add_hom {X Y : C} : ⇑(F.map_add_hom : (X ⟶ Y) →+ _) = @map C _ D _ F X Y := rfl
 
-@[simp]
-lemma map_zero {X Y : C} : F.map (0 : X ⟶ Y) = 0 :=
-F.map_add_hom.map_zero
+@[priority 100]
+instance preserves_zero_morphisms_of_additive : preserves_zero_morphisms F :=
+{ map_zero' := λ X Y, F.map_add_hom.map_zero }
 
 instance : additive (𝟭 C) :=
 {}
@@ -84,16 +85,6 @@ lemma map_sum {X Y : C} {α : Type*} (f : α → (X ⟶ Y)) (s : finset α) :
   F.map (∑ a in s, f a) = ∑ a in s, F.map (f a) :=
 (F.map_add_hom : (X ⟶ Y) →+ _).map_sum f s
 
-open category_theory.limits
-open_locale zero_object
-
-/-- An additive functor takes the zero object to the zero object (up to isomorphism). -/
-@[simps]
-def map_zero_object [has_zero_object C] [has_zero_object D] : F.obj 0 ≅ 0 :=
-{ hom := 0,
-  inv := 0,
-  hom_inv_id' := by { rw ←F.map_id, simp, } }
-
 end
 
 section induced_category

src/category_theory/shift.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johan Commelin, Andrew Yang
 -/
-import category_theory.limits.shapes.zero
+import category_theory.limits.preserves.shapes.zero
 import category_theory.monoidal.End
 import category_theory.monoidal.discrete
 
@@ -309,9 +309,8 @@ open category_theory.limits
 
 variables [has_zero_morphisms C]
 
-@[simp]
 lemma shift_zero_eq_zero (X Y : C) (n : A) : (0 : X ⟶ Y)⟦n⟧' = (0 : X⟦n⟧ ⟶ Y⟦n⟧) :=
-by apply is_equivalence_preserves_zero_morphisms _ (shift_functor C n)
+category_theory.functor.map_zero _ _ _
 
 end add_group