# mathlibdocumentation

category_theory.limits.shapes.zero

# 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
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
@[instance]
Equations
@[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.

@[instance]
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) :
@[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.equivalence_preserves_zero_morphisms {C : Type u} (D : Type u') (F : C D) (X Y : C) :
F.functor.map 0 = 0
@[simp]
theorem category_theory.limits.is_equivalence_preserves_zero_morphisms {C : Type u} (D : Type u') (F : C D) (X Y : C) :
F.map 0 = 0
@[class]
structure category_theory.limits.has_zero_object (C : Type u)  :
Type (max u v)
• zero : C
• unique_to : Π (X : C),
• unique_from : Π (X : C),

A category "has a zero object" if it has an object which is both initial and terminal.

Instances
@[instance]
Equations

Construct a has_zero C for a category with a zero object. This can not be a global instance as it will trigger for every has_zero C typeclass search.

Equations
@[ext]
theorem category_theory.limits.has_zero_object.to_zero_ext {C : Type u} {X : C} (f g : X 0) :
f = g
@[ext]
theorem category_theory.limits.has_zero_object.from_zero_ext {C : Type u} {X : C} (f g : 0 X) :
f = g
@[instance]
@[instance]
def category_theory.limits.has_zero_object.category_theory.epi {C : Type u} {X : C} (f : X 0) :

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 zero object is in particular initial.

A zero object is in particular terminal.

@[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) :
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) :
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
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

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

Equations
@[instance]

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

Equations
@[instance]

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

Equations
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) :
@[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) :

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) :

The factorisation through the zero object is an image factorisation.

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

The image of a zero morphism is the zero object.

Equations
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.

@[instance]
def category_theory.limits.split_mono_sigma_ι {C : Type u} {β : Type v} [decidable_eq β] (f : β → C) (b : β) :

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

Equations
@[instance]
def category_theory.limits.split_epi_pi_π {C : Type u} {β : Type v} [decidable_eq β] (f : β → C) (b : β) :

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

Equations
@[instance]

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

Equations
@[instance]

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

Equations
@[instance]

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

Equations
@[instance]

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

Equations