# 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 #

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.

• zero : (X Y : C) → Zero (X Y)

Every morphism space has zero

• comp_zero : ∀ {X Y : C} (f : X Y) (Z : C),

f composed with 0 is 0

• zero_comp : ∀ (X : C) {Y Z : C} (f : Y Z),

0 composed with f is 0

Instances
theorem CategoryTheory.Limits.HasZeroMorphisms.comp_zero {C : Type u} [self : ] {X : C} {Y : C} (f : X Y) (Z : C) :

f composed with 0 is 0

theorem CategoryTheory.Limits.HasZeroMorphisms.zero_comp {C : Type u} [self : ] (X : C) {Y : C} {Z : C} (f : Y Z) :

0 composed with f is 0

@[simp]
theorem CategoryTheory.Limits.comp_zero {C : Type u} {X : C} {Y : C} {f : X Y} {Z : C} :
@[simp]
theorem CategoryTheory.Limits.zero_comp {C : Type u} {X : C} {Y : C} {Z : C} {f : Y Z} :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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 HasZeroMorphisms to exist at all.

See, particularly, the note on zeroMorphismsOfZeroObject below.

Equations
• =
Equations
• CategoryTheory.Limits.hasZeroMorphismsOpposite =
@[simp]
theorem CategoryTheory.Limits.op_zero {C : Type u} (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.Limits.unop_zero {C : Type u} (X : Cᵒᵖ) (Y : Cᵒᵖ) :
theorem CategoryTheory.Limits.zero_of_comp_mono {C : Type u} {X : C} {Y : C} {Z : C} {f : X Y} (g : Y Z) (h : ) :
f = 0
theorem CategoryTheory.Limits.zero_of_epi_comp {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) {g : Y Z} (h : ) :
g = 0
theorem CategoryTheory.Limits.eq_zero_of_image_eq_zero {C : Type u} {X : C} {Y : C} {f : X Y} (w : ) :
f = 0
theorem CategoryTheory.Limits.nonzero_image_of_nonzero {C : Type u} {X : C} {Y : C} {f : X Y} (w : f 0) :
Equations
@[simp]
theorem CategoryTheory.Limits.zero_app {C : Type u} (D : Type u') [] (F : ) (G : ) (j : C) :
theorem CategoryTheory.Limits.IsZero.eq_zero_of_src {C : Type u} {X : C} {Y : C} (o : ) (f : X Y) :
f = 0
theorem CategoryTheory.Limits.IsZero.eq_zero_of_tgt {C : Type u} {X : C} {Y : C} (o : ) (f : X Y) :
f = 0
theorem CategoryTheory.Limits.IsZero.of_mono_zero {C : Type u} (X : C) (Y : C) :
theorem CategoryTheory.Limits.IsZero.of_epi_zero {C : Type u} (X : C) (Y : C) :
theorem CategoryTheory.Limits.IsZero.of_mono_eq_zero {C : Type u} {X : C} {Y : C} (f : X Y) (h : f = 0) :
theorem CategoryTheory.Limits.IsZero.of_epi_eq_zero {C : Type u} {X : C} {Y : C} (f : X Y) (h : f = 0) :
theorem CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.IsZero.of_mono {C : Type u} {X : C} {Y : C} (f : X Y) (i : ) :
theorem CategoryTheory.Limits.IsZero.of_epi {C : Type u} {X : C} {Y : C} (f : X Y) (i : ) :

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 zeroMorphismsOfZeroObject will then be incompatible with these categories because the HasZeroMorphisms instances will not be definitionally equal. For this reason library code should generally ask for an instance of HasZeroMorphisms separately, even if it already asks for an instance of HasZeroObjects.

Equations
• hO.hasZeroMorphisms =
Instances For

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 zeroMorphismsOfZeroObject 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 HasZeroMorphisms separately, even if it already asks for an instance of HasZeroObjects.

Equations
• CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject =
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_hom {C : Type u} :
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.hom = 0
@[simp]
theorem CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_inv {C : Type u} :
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.inv = 0
@[simp]
theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_hom {C : Type u} :
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.hom = 0
@[simp]
theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_inv {C : Type u} :
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.inv = 0
Equations
• =
@[simp]
theorem CategoryTheory.Limits.IsZero.map {C : Type u} {D : Type u'} [] {F : } (hF : ) {X : C} {Y : C} (f : X Y) :
F.map f = 0
@[simp]
theorem CategoryTheory.Functor.zero_obj {C : Type u} {D : Type u'} [] (X : C) :
@[simp]
theorem CategoryTheory.zero_map {C : Type u} {D : Type u'} [] {X : C} {Y : C} (f : X Y) :
f = 0
@[simp]
theorem CategoryTheory.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 CategoryTheory.Limits.zero_of_target_iso_zero {C : Type u} {X : C} {Y : C} (f : X Y) (i : Y 0) :
f = 0
theorem CategoryTheory.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 CategoryTheory.Limits.zero_of_source_iso_zero {C : Type u} {X : C} {Y : C} (f : X Y) (i : X 0) :
f = 0
theorem CategoryTheory.Limits.zero_of_source_iso_zero' {C : Type u} {X : C} {Y : C} (f : X Y) (i : ) :
f = 0
theorem CategoryTheory.Limits.zero_of_target_iso_zero' {C : Type u} {X : C} {Y : C} (f : X Y) (i : ) :
f = 0
theorem CategoryTheory.Limits.mono_of_source_iso_zero {C : Type u} {X : C} {Y : C} (f : X Y) (i : X 0) :
theorem CategoryTheory.Limits.epi_of_target_iso_zero {C : Type u} {X : C} {Y : C} (f : X Y) (i : Y 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom {C : Type u} (X : C) (h : ) :
.hom = 0
@[simp]
theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv {C : Type u} (X : C) (h : ) :
.inv = 0
@[simp]
theorem CategoryTheory.Limits.isoZeroOfMonoZero_inv {C : Type u} {X : C} {Y : C} (h : ) :
@[simp]
theorem CategoryTheory.Limits.isoZeroOfMonoZero_hom {C : Type u} {X : C} {Y : C} (h : ) :
def CategoryTheory.Limits.isoZeroOfMonoZero {C : Type u} {X : C} {Y : C} (h : ) :
X 0

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

Equations
• = { hom := 0, inv := 0, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Limits.isoZeroOfEpiZero_inv {C : Type u} {X : C} {Y : C} (h : ) :
@[simp]
theorem CategoryTheory.Limits.isoZeroOfEpiZero_hom {C : Type u} {X : C} {Y : C} (h : ) :
def CategoryTheory.Limits.isoZeroOfEpiZero {C : Type u} {X : C} {Y : C} (h : ) :
Y 0

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

Equations
• = { hom := 0, inv := 0, hom_inv_id := , inv_hom_id := }
Instances For
def CategoryTheory.Limits.isoZeroOfMonoEqZero {C : Type u} {X : C} {Y : C} {f : X Y} (h : f = 0) :
X 0

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.isoZeroOfEpiEqZero {C : Type u} {X : C} {Y : C} {f : X Y} (h : f = 0) :
Y 0

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.isoOfIsIsomorphicZero {C : Type u} {X : C} (P : ) :
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
• = { hom := 0, inv := 0, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Limits.isIsoZeroEquiv_symm_apply {C : Type u} (X : C) (Y : C) (h : ) :
=
@[simp]
theorem CategoryTheory.Limits.isIsoZeroEquiv_apply {C : Type u} (X : C) (Y : C) (i : ) :
=
def CategoryTheory.Limits.isIsoZeroEquiv {C : Type u} (X : C) (Y : C) :

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

Equations
• = { toFun := , invFun := , left_inv := , right_inv := }
Instances For

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

Equations
Instances For
def CategoryTheory.Limits.isIsoZeroEquivIsoZero {C : Type u} (X : C) (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
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.isIso_of_source_target_iso_zero {C : Type u} {X : C} {Y : C} (f : X Y) (i : X 0) (j : Y 0) :

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

Equations
• = .trans subsingletonProdSelfEquiv
Instances For

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 CategoryTheory.Limits.image_ι_comp_eq_zero {C : Type u} {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} (h : ) :
theorem CategoryTheory.Limits.comp_factorThruImage_eq_zero {C : Type u} {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} (h : ) :
@[simp]
theorem CategoryTheory.Limits.monoFactorisationZero_m {C : Type u} (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.Limits.monoFactorisationZero_I {C : Type u} (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.Limits.monoFactorisationZero_e {C : Type u} (X : C) (Y : C) :

The zero morphism has a MonoFactorisation through the zero object.

Equations
Instances For

The factorisation through the zero object is an image factorisation.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Limits.hasImage_zero {C : Type u} {X : C} {Y : C} :
Equations
• =
def CategoryTheory.Limits.imageZero {C : Type u} {X : C} {Y : C} :

The image of a zero morphism is the zero object.

Equations
• CategoryTheory.Limits.imageZero = .isoExt .isImage
Instances For
def CategoryTheory.Limits.imageZero' {C : Type u} {X : C} {Y : C} {f : X Y} (h : f = 0) :

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

Equations
• = ≪≫ CategoryTheory.Limits.imageZero
Instances For
@[simp]
theorem CategoryTheory.Limits.image.ι_zero {C : Type u} {X : C} {Y : C} :
@[simp]
theorem CategoryTheory.Limits.image.ι_zero' {C : Type u} {X : C} {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.

instance CategoryTheory.Limits.isSplitMono_sigma_ι {C : Type u} {β : Type u'} (f : βC) (b : β) :

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

Equations
• =
instance CategoryTheory.Limits.isSplitEpi_pi_π {C : Type u} {β : Type u'} (f : βC) (b : β) :

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

Equations
• =
instance CategoryTheory.Limits.isSplitMono_coprod_inl {C : Type u} {X : C} {Y : C} :
CategoryTheory.IsSplitMono CategoryTheory.Limits.coprod.inl

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

Equations
• =
instance CategoryTheory.Limits.isSplitMono_coprod_inr {C : Type u} {X : C} {Y : C} :
CategoryTheory.IsSplitMono CategoryTheory.Limits.coprod.inr

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

Equations
• =
instance CategoryTheory.Limits.isSplitEpi_prod_fst {C : Type u} {X : C} {Y : C} :
CategoryTheory.IsSplitEpi CategoryTheory.Limits.prod.fst

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

Equations
• =
instance CategoryTheory.Limits.isSplitEpi_prod_snd {C : Type u} {X : C} {Y : C} :
CategoryTheory.IsSplitEpi CategoryTheory.Limits.prod.snd

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

Equations
• =
def CategoryTheory.Limits.IsLimit.ofIsZero {C : Type u} {D : Type u'} [] {F : } (c : ) (hF : ) (hc : ) :

If a functor F is zero, then any cone for F with a zero point is limit.

Equations
• = { lift := fun (x : ) => 0, fac := , uniq := }
Instances For
def CategoryTheory.Limits.IsColimit.ofIsZero {C : Type u} {D : Type u'} [] {F : } (c : ) (hF : ) (hc : ) :

If a functor F is zero, then any cocone for F with a zero point is colimit.

Equations
• = { desc := fun (x : ) => 0, fac := , uniq := }
Instances For
theorem CategoryTheory.Limits.IsLimit.isZero_pt {C : Type u} {D : Type u'} [] {F : } {c : } (hc : ) (hF : ) :
theorem CategoryTheory.Limits.IsColimit.isZero_pt {C : Type u} {D : Type u'} [] {F : } {c : } (hc : ) (hF : ) :
theorem CategoryTheory.Limits.IsTerminal.isZero {C : Type u} {X : C} (hX : ) :
theorem CategoryTheory.Limits.IsInitial.isZero {C : Type u} {X : C} (hX : ) :