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)
:
A functor preserves zero morphisms if it sends zero morphisms to zero morphisms.
For any pair objects
F (0: X ⟶ Y) = (0 : F X ⟶ F Y)
Instances
- CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj
- CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip
- CategoryTheory.Functor.preservesZeroMorphisms_comp
- CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj
- CategoryTheory.Functor.preservesZeroMorphisms_of_full
- CategoryTheory.Functor.preservesZeroMorphisms_of_isLeftAdjoint
- CategoryTheory.Functor.preservesZeroMorphisms_of_isRightAdjoint
- CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object
- CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object
@[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)
:
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)
:
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}
:
@[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]
:
@[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]
:
@[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]
:
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₂)
:
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]
:
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
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]
:
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]
:
@[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]
:
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)
:
@[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]
:
@[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]
:
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.{u_2, u_1} J]
:
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.{u_2, u_1} J]
:
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)
:
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)
:
A zero functor preserves colimits.