Preservation of zero objects and zero morphisms

We define the class PreservesZeroMorphisms 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 CategoryTheory.Functor.PreservesZeroMorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) : Prop

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

• map_zero (X Y : C) : F.map 0 = 0

  For any pair objects F (0: X ⟶ Y) = (0 : F X ⟶ F Y)

@[simp]

theorem CategoryTheory.Functor.map_zero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) : F.map 0 = 0

theorem CategoryTheory.Functor.map_isZero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X : C} (hX : Limits.IsZero X) : Limits.IsZero (F.obj X)

theorem CategoryTheory.Functor.zero_of_map_zero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] {X Y : C} (f : X ⟶ Y) (h : F.map f = 0) : f = 0

theorem CategoryTheory.Functor.map_eq_zero_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] {X Y : C} {f : X ⟶ Y} : F.map f = 0 ↔ f = 0

@[instance 100]

instance CategoryTheory.Functor.preservesZeroMorphisms_of_isLeftAdjoint {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.IsLeftAdjoint] : F.PreservesZeroMorphisms

@[instance 100]

instance CategoryTheory.Functor.preservesZeroMorphisms_of_isRightAdjoint {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (G : Functor C D) [G.IsRightAdjoint] : G.PreservesZeroMorphisms

@[instance 100]

instance CategoryTheory.Functor.preservesZeroMorphisms_of_full {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.Full] : F.PreservesZeroMorphisms

instance CategoryTheory.Functor.preservesZeroMorphisms_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [Limits.HasZeroMorphisms E] (F : Functor C D) (G : Functor D E) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] : (F.comp G).PreservesZeroMorphisms

theorem CategoryTheory.Functor.preservesZeroMorphisms_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {F₁ F₂ : Functor C D} [F₁.PreservesZeroMorphisms] (e : F₁ ≅ F₂) : F₂.PreservesZeroMorphisms

instance CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] (j : D) : ((evaluation D C).obj j).PreservesZeroMorphisms

instance CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] [Limits.HasZeroMorphisms D] [Limits.HasZeroMorphisms E] (F : Functor C (Functor D E)) [∀ (X : C), (F.obj X).PreservesZeroMorphisms] : F.flip.PreservesZeroMorphisms

instance CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms E] (F : Functor C (Functor D E)) [F.PreservesZeroMorphisms] (Y : D) : (F.flip.obj Y).PreservesZeroMorphisms

@[simp]

theorem CategoryTheory.Functor.whiskerRight_zero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] [Limits.HasZeroMorphisms D] [Limits.HasZeroMorphisms E] {F G : Functor C D} (H : Functor D E) [H.PreservesZeroMorphisms] : whiskerRight 0 H = 0

theorem CategoryTheory.Functor.FullyFaithful.preservesZeroMorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (F : Functor C D) (hF : F.FullyFaithful) : F.PreservesZeroMorphisms

noncomputable def CategoryTheory.Functor.mapZeroObject {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] : F.obj 0 ≅ 0

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

Equations

• F.mapZeroObject = { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapZeroObject_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] : F.mapZeroObject.hom = 0

@[simp]

theorem CategoryTheory.Functor.mapZeroObject_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] : F.mapZeroObject.inv = 0

theorem CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {F : Functor C D} (i : F.obj 0 ≅ 0) : F.PreservesZeroMorphisms

@[instance 100]

instance CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {F : Functor C D} [Limits.PreservesColimit (empty C) F] : F.PreservesZeroMorphisms

@[instance 100]

instance CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {F : Functor C D} [Limits.PreservesLimit (empty C) F] : F.PreservesZeroMorphisms

theorem CategoryTheory.Functor.preservesTerminalObject_of_preservesZeroMorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] : Limits.PreservesLimit (empty C) F

Preserving zero morphisms implies preserving terminal objects.

theorem CategoryTheory.Functor.preservesInitialObject_of_preservesZeroMorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] : Limits.PreservesColimit (empty C) F

Preserving zero morphisms implies preserving terminal objects.

theorem CategoryTheory.Functor.preservesLimitsOfShape_of_isZero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms D] (G : Functor C D) (hG : Limits.IsZero G) (J : Type u_1) [Category.{v_1, u_1} J] : Limits.PreservesLimitsOfShape J G

A zero functor preserves limits.

theorem CategoryTheory.Functor.preservesColimitsOfShape_of_isZero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms D] (G : Functor C D) (hG : Limits.IsZero G) (J : Type u_1) [Category.{v_1, u_1} J] : Limits.PreservesColimitsOfShape J G

A zero functor preserves colimits.

theorem CategoryTheory.Functor.preservesLimitsOfSize_of_isZero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms D] (G : Functor C D) (hG : Limits.IsZero G) : Limits.PreservesLimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G

A zero functor preserves limits.

theorem CategoryTheory.Functor.preservesColimitsOfSize_of_isZero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms D] (G : Functor C D) (hG : Limits.IsZero G) : Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G

A zero functor preserves colimits.