# mathlibdocumentation

category_theory.limits.preserves.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 preserve 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.
@[class]
structure category_theory.functor.preserves_zero_morphisms {C : Type u₁} {D : Type u₂} (F : C D) :
Prop
• map_zero' : (∀ (X Y : C), F.map 0 = 0) . "obviously"

A functor preserves zero morphisms if it sends zero morphisms to zero morphisms.

Instances of this typeclass
@[protected, simp]
theorem category_theory.functor.map_zero {C : Type u₁} {D : Type u₂} (F : C D) (X Y : C) :
F.map 0 = 0
theorem category_theory.functor.zero_of_map_zero {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : X Y) (h : F.map f = 0) :
f = 0
theorem category_theory.functor.map_eq_zero_iff {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} {f : X Y} :
F.map f = 0 f = 0
@[protected, instance]
@[protected, instance]
@[protected, instance]
def category_theory.functor.preserves_zero_morphisms_of_full {C : Type u₁} {D : Type u₂} (F : C D)  :
noncomputable def category_theory.functor.map_zero_object {C : Type u₁} {D : Type u₂} (F : C D)  :
F.obj 0 0

A functor that preserves zero morphisms also preserves the zero object.

Equations
@[simp]
theorem category_theory.functor.map_zero_object_hom {C : Type u₁} {D : Type u₂} (F : C D)  :
@[simp]
theorem category_theory.functor.map_zero_object_inv {C : Type u₁} {D : Type u₂} (F : C D)  :
theorem category_theory.functor.preserves_zero_morphisms_of_map_zero_object {C : Type u₁} {D : Type u₂} {F : C D} (i : F.obj 0 0) :
@[protected, instance]
@[protected, instance]

Preserving zero morphisms implies preserving terminal objects.

Equations

Preserving zero morphisms implies preserving terminal objects.

Equations