# mathlibdocumentation

category_theory.limits.shapes.zero_morphisms

# Zero morphisms and zero objects #

A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space, and compositions of zero morphisms with anything give the zero morphism. (Notice this is extra structure, not merely a property.)

A category "has a zero object" if it has an object which is both initial and terminal. Having a zero object provides zero morphisms, as the unique morphisms factoring through the zero object.

## References #

@[class]
structure category_theory.limits.has_zero_morphisms (C : Type u)  :
Type (max u v)
• has_zero : Π (X Y : C), has_zero (X Y)
• comp_zero' : (∀ {X Y : C} (f : X Y) (Z : C), f 0 = 0) . "obviously"
• zero_comp' : (∀ (X : C) {Y Z : C} (f : Y Z), 0 f = 0) . "obviously"

A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space, and compositions of zero morphisms with anything give the zero morphism.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.has_zero_morphisms
theorem category_theory.limits.has_zero_morphisms.comp_zero {C : Type u} {X Y : C} (f : X Y) (Z : C) :
f 0 = 0
theorem category_theory.limits.has_zero_morphisms.zero_comp {C : Type u} (X : C) {Y Z : C} (f : Y Z) :
0 f = 0
@[simp]
theorem category_theory.limits.comp_zero {C : Type u} {X Y : C} {f : X Y} {Z : C} :
f 0 = 0
@[simp]
theorem category_theory.limits.zero_comp {C : Type u} {X Y Z : C} {f : Y Z} :
0 f = 0
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem category_theory.limits.has_zero_morphisms.ext {C : Type u}  :
I = J

If you're tempted to use this lemma "in the wild", you should probably carefully consider whether you've made a mistake in allowing two instances of has_zero_morphisms to exist at all.

See, particularly, the note on zero_morphisms_of_zero_object below.

@[protected, instance]
@[protected, instance]
Equations
theorem category_theory.limits.zero_of_comp_mono {C : Type u} {X Y Z : C} {f : X Y} (g : Y Z) (h : f g = 0) :
f = 0
theorem category_theory.limits.zero_of_epi_comp {C : Type u} {X Y Z : C} (f : X Y) {g : Y Z} (h : f g = 0) :
g = 0
theorem category_theory.limits.eq_zero_of_image_eq_zero {C : Type u} {X Y : C} {f : X Y} (w : = 0) :
f = 0
theorem category_theory.limits.nonzero_image_of_nonzero {C : Type u} {X Y : C} {f : X Y} (w : f 0) :
@[protected, instance]
Equations
@[simp]
theorem category_theory.limits.zero_app {C : Type u} (D : Type u') (F G : C D) (j : C) :
0.app j = 0
theorem category_theory.limits.is_zero.eq_zero_of_src {C : Type u} {X Y : C} (f : X Y) :
f = 0
theorem category_theory.limits.is_zero.eq_zero_of_tgt {C : Type u} {X Y : C} (f : X Y) :
f = 0
theorem category_theory.limits.is_zero.iff_id_eq_zero {C : Type u} (X : C) :
theorem category_theory.limits.is_zero.of_mono_zero {C : Type u} (X Y : C)  :
theorem category_theory.limits.is_zero.of_epi_zero {C : Type u} (X Y : C)  :
theorem category_theory.limits.is_zero.of_mono_eq_zero {C : Type u} {X Y : C} (f : X Y) (h : f = 0) :
theorem category_theory.limits.is_zero.of_epi_eq_zero {C : Type u} {X Y : C} (f : X Y) (h : f = 0) :
theorem category_theory.limits.is_zero.iff_is_split_mono_eq_zero {C : Type u} {X Y : C} (f : X Y)  :
theorem category_theory.limits.is_zero.iff_is_split_epi_eq_zero {C : Type u} {X Y : C} (f : X Y)  :
theorem category_theory.limits.is_zero.of_mono {C : Type u} {X Y : C} (f : X Y)  :
theorem category_theory.limits.is_zero.of_epi {C : Type u} {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.is_zero.has_zero_morphisms {C : Type u} {O : C}  :

A category with a zero object has zero morphisms.

It is rarely a good idea to use this. Many categories that have a zero object have zero morphisms for some other reason, for example from additivity. Library code that uses zero_morphisms_of_zero_object will then be incompatible with these categories because the has_zero_morphisms instances will not be definitionally equal. For this reason library code should generally ask for an instance of has_zero_morphisms separately, even if it already asks for an instance of has_zero_objects.

Equations

A category with a zero object has zero morphisms.

It is rarely a good idea to use this. Many categories that have a zero object have zero morphisms for some other reason, for example from additivity. Library code that uses zero_morphisms_of_zero_object will then be incompatible with these categories because the has_zero_morphisms instances will not be definitionally equal. For this reason library code should generally ask for an instance of has_zero_morphisms separately, even if it already asks for an instance of has_zero_objects.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
@[simp]
theorem category_theory.limits.is_zero.map {C : Type u} {D : Type u'} {F : C D} {X Y : C} (f : X Y) :
F.map f = 0
@[simp]
theorem category_theory.functor.zero_obj {C : Type u} {D : Type u'} (X : C) :
@[simp]
theorem category_theory.zero_map {C : Type u} {D : Type u'} {X Y : C} (f : X Y) :
0.map f = 0
@[simp]
theorem category_theory.limits.id_zero {C : Type u}  :
𝟙 0 = 0
theorem category_theory.limits.zero_of_to_zero {C : Type u} {X : C} (f : X 0) :
f = 0

An arrow ending in the zero object is zero

theorem category_theory.limits.zero_of_target_iso_zero {C : Type u} {X Y : C} (f : X Y) (i : Y 0) :
f = 0
theorem category_theory.limits.zero_of_from_zero {C : Type u} {X : C} (f : 0 X) :
f = 0

An arrow starting at the zero object is zero

theorem category_theory.limits.zero_of_source_iso_zero {C : Type u} {X Y : C} (f : X Y) (i : X 0) :
f = 0
theorem category_theory.limits.zero_of_source_iso_zero' {C : Type u} {X Y : C} (f : X Y) (i : 0) :
f = 0
theorem category_theory.limits.zero_of_target_iso_zero' {C : Type u} {X Y : C} (f : X Y) (i : 0) :
f = 0
theorem category_theory.limits.mono_of_source_iso_zero {C : Type u} {X Y : C} (f : X Y) (i : X 0) :
theorem category_theory.limits.epi_of_target_iso_zero {C : Type u} {X Y : C} (f : X Y) (i : Y 0) :
noncomputable def category_theory.limits.id_zero_equiv_iso_zero {C : Type u} (X : C) :
𝟙 X = 0 (X 0)

An object X has 𝟙 X = 0 if and only if it is isomorphic to the zero object.

Because X ≅ 0 contains data (even if a subsingleton), we express this ↔ as an ≃.

Equations
@[simp]
theorem category_theory.limits.id_zero_equiv_iso_zero_apply_hom {C : Type u} (X : C) (h : 𝟙 X = 0) :
@[simp]
theorem category_theory.limits.id_zero_equiv_iso_zero_apply_inv {C : Type u} (X : C) (h : 𝟙 X = 0) :
noncomputable def category_theory.limits.iso_zero_of_mono_zero {C : Type u} {X Y : C} (h : category_theory.mono 0) :
X 0

If 0 : X ⟶ Y is an monomorphism, then X ≅ 0.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.limits.iso_zero_of_epi_zero_inv {C : Type u} {X Y : C} (h : category_theory.epi 0) :
@[simp]
theorem category_theory.limits.iso_zero_of_epi_zero_hom {C : Type u} {X Y : C} (h : category_theory.epi 0) :
noncomputable def category_theory.limits.iso_zero_of_epi_zero {C : Type u} {X Y : C} (h : category_theory.epi 0) :
Y 0

If 0 : X ⟶ Y is an epimorphism, then Y ≅ 0.

Equations
noncomputable def category_theory.limits.iso_zero_of_mono_eq_zero {C : Type u} {X Y : C} {f : X Y} (h : f = 0) :
X 0

If a monomorphism out of X is zero, then X ≅ 0.

Equations
• = eq.rec (λ [_inst_5 : , _
noncomputable def category_theory.limits.iso_zero_of_epi_eq_zero {C : Type u} {X Y : C} {f : X Y} (h : f = 0) :
Y 0

If an epimorphism in to Y is zero, then Y ≅ 0.

Equations
• = eq.rec (λ [_inst_5 : , _
noncomputable def category_theory.limits.iso_of_is_isomorphic_zero {C : Type u} {X : C} (P : 0) :
X 0

If an object X is isomorphic to 0, there's no need to use choice to construct an explicit isomorphism: the zero morphism suffices.

Equations
@[simp]
theorem category_theory.limits.is_iso_zero_equiv_symm_apply {C : Type u} (X Y : C) (h : 𝟙 X = 0 𝟙 Y = 0) :
_ = _
def category_theory.limits.is_iso_zero_equiv {C : Type u} (X Y : C) :
𝟙 X = 0 𝟙 Y = 0

A zero morphism 0 : X ⟶ Y is an isomorphism if and only if the identities on both X and Y are zero.

Equations
@[simp]
theorem category_theory.limits.is_iso_zero_equiv_apply {C : Type u} (X Y : C) (i : category_theory.is_iso 0) :
_ = _
def category_theory.limits.is_iso_zero_self_equiv {C : Type u} (X : C) :
𝟙 X = 0

A zero morphism 0 : X ⟶ X is an isomorphism if and only if the identity on X is zero.

Equations
noncomputable def category_theory.limits.is_iso_zero_equiv_iso_zero {C : Type u} (X Y : C) :
(X 0) × (Y 0)

A zero morphism 0 : X ⟶ Y is an isomorphism if and only if X and Y are isomorphic to the zero object.

Equations
theorem category_theory.limits.is_iso_of_source_target_iso_zero {C : Type u} {X Y : C} (f : X Y) (i : X 0) (j : Y 0) :
noncomputable def category_theory.limits.is_iso_zero_self_equiv_iso_zero {C : Type u} (X : C) :
(X 0)

A zero morphism 0 : X ⟶ X is an isomorphism if and only if X is isomorphic to the zero object.

Equations

If there are zero morphisms, any initial object is a zero object.

If there are zero morphisms, any terminal object is a zero object.

theorem category_theory.limits.image_ι_comp_eq_zero {C : Type u} {X Y Z : C} {f : X Y} {g : Y Z} (h : f g = 0) :
theorem category_theory.limits.comp_factor_thru_image_eq_zero {C : Type u} {X Y Z : C} {f : X Y} {g : Y Z} (h : f g = 0) :
@[simp]
theorem category_theory.limits.mono_factorisation_zero_m {C : Type u} (X Y : C) :
@[simp]
theorem category_theory.limits.mono_factorisation_zero_I {C : Type u} (X Y : C) :
noncomputable def category_theory.limits.mono_factorisation_zero {C : Type u} (X Y : C) :

The zero morphism has a mono_factorisation through the zero object.

Equations
@[simp]
theorem category_theory.limits.mono_factorisation_zero_e {C : Type u} (X Y : C) :
noncomputable def category_theory.limits.image_factorisation_zero {C : Type u} (X Y : C) :

The factorisation through the zero object is an image factorisation.

Equations
@[protected, instance]
noncomputable def category_theory.limits.image_zero {C : Type u} {X Y : C} :

The image of a zero morphism is the zero object.

Equations
noncomputable def category_theory.limits.image_zero' {C : Type u} {X Y : C} {f : X Y} (h : f = 0)  :

The image of a morphism which is equal to zero is the zero object.

Equations
@[simp]
@[simp]
theorem category_theory.limits.image.ι_zero' {C : Type u} {X Y : C} {f : X Y} (h : f = 0)  :

If we know f = 0, it requires a little work to conclude image.ι f = 0, because f = g only implies image f ≅ image g.

@[protected, instance]
def category_theory.limits.is_split_mono_sigma_ι {C : Type u} {β : Type u'} (f : β → C) (b : β) :

In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.

@[protected, instance]
def category_theory.limits.is_split_epi_pi_π {C : Type u} {β : Type u'} (f : β → C) (b : β) :

In the presence of zero morphisms, projections into a product are (split) epimorphisms.

@[protected, instance]

In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.

@[protected, instance]

In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.

@[protected, instance]

In the presence of zero morphisms, projections into a product are (split) epimorphisms.

@[protected, instance]

In the presence of zero morphisms, projections into a product are (split) epimorphisms.