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

theorem CategoryTheory.Functor.PreservesZeroMorphisms.map_zero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} [self : F.PreservesZeroMorphisms] (X : C) (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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (X : C) (Y : C) : F.map 0 = 0

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

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

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

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.mapZeroObject {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.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 := ⋯ }

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

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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

Preserving zero morphisms implies preserving terminal objects.

Equations

• One or more equations did not get rendered due to their size.

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

Preserving zero morphisms implies preserving terminal objects.

Equations

• One or more equations did not get rendered due to their size.

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

A zero functor preserves limits.

Equations

• One or more equations did not get rendered due to their size.

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

A zero functor preserves colimits.

Equations

• One or more equations did not get rendered due to their size.

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

A zero functor preserves limits.

Equations

• G.preservesLimitsOfSizeOfIsZero hG = { preservesLimitsOfShape := fun {J : Type u} [CategoryTheory.Category.{v, u} J] => G.preservesLimitsOfShapeOfIsZero hG J }

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

A zero functor preserves colimits.

Equations

• G.preservesColimitsOfSizeOfIsZero hG = { preservesColimitsOfShape := fun {J : Type u} [CategoryTheory.Category.{v, u} J] => G.preservesColimitsOfShapeOfIsZero hG J }