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)

Instances

source

theorem CategoryTheory.Functor.PreservesZeroMorphisms.map_zero {C : Type u₁} :

∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {F : CategoryTheory.Functor C D} [self : F.PreservesZeroMorphisms] (X Y : C), F.map 0 = 0

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

source

@[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

source

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)

source

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

source

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

source

@[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

⋯ = ⋯

source

@[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

⋯ = ⋯

source

@[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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

source

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

⋯ = ⋯

source

instance CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj {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 D] [CategoryTheory.Limits.HasZeroMorphisms E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) [∀ (X : C), (F.obj X).PreservesZeroMorphisms] :

F.flip.PreservesZeroMorphisms

Equations

⋯ = ⋯

source

instance CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip {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 E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) [F.PreservesZeroMorphisms] (Y : D) :

(F.flip.obj Y).PreservesZeroMorphisms

Equations

⋯ = ⋯

source

@[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

source

@[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

source

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 := ⋯ }

Instances For

source

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

source

@[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

⋯ = ⋯

source

@[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

⋯ = ⋯

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.62} [CategoryTheory.Category.{?u.63, ?u.62} J] => G.preservesLimitsOfShapeOfIsZero hG J }

Instances For

source

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.62} [CategoryTheory.Category.{?u.63, ?u.62} J] => G.preservesColimitsOfShapeOfIsZero hG J }

Instances For

HepLean Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Preservation of zero objects and zero morphisms #

Main results #