# mathlib3documentation

category_theory.limits.shapes.zero_objects

# Zero objects #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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; see category_theory.limits.shapes.zero_morphisms.

## References #

structure category_theory.limits.is_zero {C : Type u} (X : C) :
Prop

An object X in a category is a zero object if for every object Y there is a unique morphism to : X → Y and a unique morphism from : Y → X.

This is a characteristic predicate for has_zero_object.

@[protected]
noncomputable def category_theory.limits.is_zero.to {C : Type u} {X : C} (Y : C) :
X Y

If h : is_zero X, then h.to Y is a choice of unique morphism X → Y.

Equations
theorem category_theory.limits.is_zero.eq_to {C : Type u} {X Y : C} (f : X Y) :
f = h.to Y
theorem category_theory.limits.is_zero.to_eq {C : Type u} {X Y : C} (f : X Y) :
h.to Y = f
@[protected]
noncomputable def category_theory.limits.is_zero.from {C : Type u} {X : C} (Y : C) :
Y X

If h : is_zero X, then h.from Y is a choice of unique morphism Y → X.

Equations
theorem category_theory.limits.is_zero.eq_from {C : Type u} {X Y : C} (f : Y X) :
f = h.from Y
theorem category_theory.limits.is_zero.from_eq {C : Type u} {X Y : C} (f : Y X) :
h.from Y = f
theorem category_theory.limits.is_zero.eq_of_src {C : Type u} {X Y : C} (f g : X Y) :
f = g
theorem category_theory.limits.is_zero.eq_of_tgt {C : Type u} {X Y : C} (f g : Y X) :
f = g
noncomputable def category_theory.limits.is_zero.iso {C : Type u} {X Y : C}  :
X Y

Any two zero objects are isomorphic.

Equations
@[protected]
noncomputable def category_theory.limits.is_zero.is_initial {C : Type u} {X : C}  :

A zero object is in particular initial.

Equations
@[protected]
noncomputable def category_theory.limits.is_zero.is_terminal {C : Type u} {X : C}  :

A zero object is in particular terminal.

Equations
noncomputable def category_theory.limits.is_zero.iso_is_initial {C : Type u} {X Y : C}  :
X Y

The (unique) isomorphism between any initial object and the zero object.

Equations
noncomputable def category_theory.limits.is_zero.iso_is_terminal {C : Type u} {X Y : C}  :
X Y

The (unique) isomorphism between any terminal object and the zero object.

Equations
theorem category_theory.limits.is_zero.of_iso {C : Type u} {X Y : C} (e : X Y) :
theorem category_theory.limits.is_zero.op {C : Type u} {X : C}  :
theorem category_theory.iso.is_zero_iff {C : Type u} {X Y : C} (e : X Y) :
theorem category_theory.functor.is_zero {C : Type u} {D : Type u'} (F : C D) (hF : (X : C), ) :
@[class]
structure category_theory.limits.has_zero_object (C : Type u)  :
Prop
• zero : (X : C),

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

Instances of this typeclass
@[protected, instance]
@[protected]

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
@[protected, instance]
noncomputable def category_theory.limits.is_zero.iso_zero {C : Type u} {X : C}  :
X 0

Every zero object is isomorphic to the zero object.

Equations
theorem category_theory.limits.is_zero.obj {C : Type u} {D : Type u'} {F : C D} (X : C) :
@[protected]
noncomputable def category_theory.limits.has_zero_object.unique_to {C : Type u} (X : C) :
unique (0 X)

There is a unique morphism from the zero object to any object X.

Equations
@[protected]
noncomputable def category_theory.limits.has_zero_object.unique_from {C : Type u} (X : C) :
unique (X 0)

There is a unique morphism from any object X to the zero object.

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
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

A zero object is in particular initial.

Equations

A zero object is in particular terminal.

Equations
@[protected, instance]

A zero object is in particular initial.

@[protected, instance]

A zero object is in particular terminal.

noncomputable def category_theory.limits.has_zero_object.zero_iso_is_initial {C : Type u} {X : C}  :
0 X

The (unique) isomorphism between any initial object and the zero object.

Equations
noncomputable def category_theory.limits.has_zero_object.zero_iso_is_terminal {C : Type u} {X : C}  :
0 X

The (unique) isomorphism between any terminal object and the zero object.

Equations

The (unique) isomorphism between the chosen initial object and the chosen zero object.

Equations

The (unique) isomorphism between the chosen terminal object and the chosen zero object.

Equations
@[protected, instance]
theorem category_theory.functor.is_zero_iff {C : Type u} {D : Type u'} (F : C D) :
(X : C),