Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Preservation of zero objects and zero morphisms #

We define the class PreservesZeroMorphisms and show basic properties.

Main results #

We provide the following results:

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

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

    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

    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