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)
:
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
@[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 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 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 Y : C}
{f : X ⟶ Y}
:
@[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
@[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
@[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
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
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₁ 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
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
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
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
@[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
@[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
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
@[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
theorem
CategoryTheory.Functor.preservesTerminalObject_of_preservesZeroMorphisms
{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]
:
Preserving zero morphisms implies preserving terminal objects.
theorem
CategoryTheory.Functor.preservesInitialObject_of_preservesZeroMorphisms
{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]
:
Preserving zero morphisms implies preserving terminal objects.
theorem
CategoryTheory.Functor.preservesLimitsOfShape_of_isZero
{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]
:
A zero functor preserves limits.
theorem
CategoryTheory.Functor.preservesColimitsOfShape_of_isZero
{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]
:
A zero functor preserves colimits.
theorem
CategoryTheory.Functor.preservesLimitsOfSize_of_isZero
{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)
:
A zero functor preserves limits.
theorem
CategoryTheory.Functor.preservesColimitsOfSize_of_isZero
{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)
:
A zero functor preserves colimits.