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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
(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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Faithful F]
{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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Faithful F]
{X : C}
{Y : C}
{f : X ⟶ Y}
:
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)
[CategoryTheory.IsLeftAdjoint F]
:
Equations
- ⋯ = ⋯
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)
[CategoryTheory.IsRightAdjoint G]
:
Equations
- ⋯ = ⋯
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)
[CategoryTheory.Full F]
:
Equations
- ⋯ = ⋯
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)
:
Equations
- ⋯ = ⋯
@[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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
:
(CategoryTheory.Functor.mapZeroObject F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
:
(CategoryTheory.Functor.mapZeroObject F).inv = 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
:
F.obj 0 ≅ 0
A functor that preserves zero morphisms also preserves the zero object.
Equations
- CategoryTheory.Functor.mapZeroObject F = { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
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)
:
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]
:
Equations
- ⋯ = ⋯
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]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
:
Preserving zero morphisms implies preserving terminal objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
:
Preserving zero morphisms implies preserving terminal objects.
Equations
- One or more equations did not get rendered due to their size.