Preservation of zero objects and zero morphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define the class preserves_zero_morphisms 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]
structure
category_theory.functor.preserves_zero_morphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D) :
Prop
A functor preserves zero morphisms if it sends zero morphisms to zero morphisms.
Instances of this typeclass
- category_theory.functor.preserves_zero_morphisms_of_is_left_adjoint
- category_theory.functor.preserves_zero_morphisms_of_is_right_adjoint
- category_theory.functor.preserves_zero_morphisms_of_full
- category_theory.functor.preserves_zero_morphisms_of_preserves_initial_object
- category_theory.functor.preserves_zero_morphisms_of_preserves_terminal_object
- category_theory.functor.preserves_zero_morphisms_of_additive
@[protected, simp]
theorem
category_theory.functor.map_zero
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C) :
theorem
category_theory.functor.zero_of_map_zero
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.faithful F]
{X Y : C}
(f : X ⟶ Y)
(h : F.map f = 0) :
f = 0
theorem
category_theory.functor.map_eq_zero_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.faithful F]
{X Y : C}
{f : X ⟶ Y} :
@[protected, instance]
def
category_theory.functor.preserves_zero_morphisms_of_is_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[category_theory.is_left_adjoint F] :
@[protected, instance]
def
category_theory.functor.preserves_zero_morphisms_of_is_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(G : C ⥤ D)
[category_theory.is_right_adjoint G] :
@[protected, instance]
def
category_theory.functor.preserves_zero_morphisms_of_full
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[category_theory.full F] :
noncomputable
def
category_theory.functor.map_zero_object
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
A functor that preserves zero morphisms also preserves the zero object.
Equations
- F.map_zero_object = {hom := 0, inv := 0, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.functor.map_zero_object_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
F.map_zero_object.hom = 0
@[simp]
theorem
category_theory.functor.map_zero_object_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
F.map_zero_object.inv = 0
theorem
category_theory.functor.preserves_zero_morphisms_of_map_zero_object
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{F : C ⥤ D}
(i : F.obj 0 ≅ 0) :
@[protected, instance]
def
category_theory.functor.preserves_zero_morphisms_of_preserves_initial_object
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{F : C ⥤ D}
[category_theory.limits.preserves_colimit (category_theory.functor.empty C) F] :
@[protected, instance]
def
category_theory.functor.preserves_zero_morphisms_of_preserves_terminal_object
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{F : C ⥤ D}
[category_theory.limits.preserves_limit (category_theory.functor.empty C) F] :
noncomputable
def
category_theory.functor.preserves_terminal_object_of_preserves_zero_morphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Preserving zero morphisms implies preserving terminal objects.
noncomputable
def
category_theory.functor.preserves_initial_object_of_preserves_zero_morphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Preserving zero morphisms implies preserving terminal objects.