# Zero objects #

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 CategoryTheory.Limits.Shapes.ZeroMorphisms.

## References #

structure CategoryTheory.Limits.IsZero {C : Type u} (X : C) :

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.

• unique_to : ∀ (Y : C), Nonempty (Unique (X Y))

there are unique morphisms to the object

• unique_from : ∀ (Y : C), Nonempty (Unique (Y X))

there are unique morphisms from the object

Instances For
theorem CategoryTheory.Limits.IsZero.unique_to {C : Type u} {X : C} (self : ) (Y : C) :

there are unique morphisms to the object

theorem CategoryTheory.Limits.IsZero.unique_from {C : Type u} {X : C} (self : ) (Y : C) :

there are unique morphisms from the object

def CategoryTheory.Limits.IsZero.to_ {C : Type u} {X : C} (h : ) (Y : C) :
X Y

If h : IsZero X, then h.to_ Y is a choice of unique morphism X → Y.

Equations
• h.to_ Y = default
Instances For
theorem CategoryTheory.Limits.IsZero.eq_to {C : Type u} {X : C} {Y : C} (h : ) (f : X Y) :
f = h.to_ Y
theorem CategoryTheory.Limits.IsZero.to_eq {C : Type u} {X : C} {Y : C} (h : ) (f : X Y) :
h.to_ Y = f
def CategoryTheory.Limits.IsZero.from_ {C : Type u} {X : C} (h : ) (Y : C) :
Y X

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

Equations
• h.from_ Y = default
Instances For
theorem CategoryTheory.Limits.IsZero.eq_from {C : Type u} {X : C} {Y : C} (h : ) (f : Y X) :
f = h.from_ Y
theorem CategoryTheory.Limits.IsZero.from_eq {C : Type u} {X : C} {Y : C} (h : ) (f : Y X) :
h.from_ Y = f
theorem CategoryTheory.Limits.IsZero.eq_of_src {C : Type u} {X : C} {Y : C} (hX : ) (f : X Y) (g : X Y) :
f = g
theorem CategoryTheory.Limits.IsZero.eq_of_tgt {C : Type u} {X : C} {Y : C} (hX : ) (f : Y X) (g : Y X) :
f = g
def CategoryTheory.Limits.IsZero.iso {C : Type u} {X : C} {Y : C} (hX : ) (hY : ) :
X Y

Any two zero objects are isomorphic.

Equations
• hX.iso hY = { hom := hX.to_ Y, inv := hX.from_ Y, hom_inv_id := , inv_hom_id := }
Instances For
def CategoryTheory.Limits.IsZero.isInitial {C : Type u} {X : C} (hX : ) :

A zero object is in particular initial.

Equations
• hX.isInitial =
Instances For
def CategoryTheory.Limits.IsZero.isTerminal {C : Type u} {X : C} (hX : ) :

A zero object is in particular terminal.

Equations
• hX.isTerminal =
Instances For
def CategoryTheory.Limits.IsZero.isoIsInitial {C : Type u} {X : C} {Y : C} (hX : ) (hY : ) :
X Y

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

Equations
• hX.isoIsInitial hY = hX.isInitial.uniqueUpToIso hY
Instances For
def CategoryTheory.Limits.IsZero.isoIsTerminal {C : Type u} {X : C} {Y : C} (hX : ) (hY : ) :
X Y

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

Equations
• hX.isoIsTerminal hY = hX.isTerminal.uniqueUpToIso hY
Instances For
theorem CategoryTheory.Limits.IsZero.of_iso {C : Type u} {X : C} {Y : C} (hY : ) (e : X Y) :
theorem CategoryTheory.Limits.IsZero.op {C : Type u} {X : C} (h : ) :
theorem CategoryTheory.Limits.IsZero.unop {C : Type u} {X : Cᵒᵖ} (h : ) :
theorem CategoryTheory.Iso.isZero_iff {C : Type u} {X : C} {Y : C} (e : X Y) :
theorem CategoryTheory.Functor.isZero {C : Type u} {D : Type u'} [] (F : ) (hF : ∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)) :

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

• zero : ∃ (X : C),

there exists a zero object

Instances
theorem CategoryTheory.Limits.HasZeroObject.zero {C : Type u} [self : ] :
∃ (X : C),

there exists a zero object

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

Equations
• = { zero := .choose }
Instances For
Equations
• =
theorem CategoryTheory.Limits.IsZero.hasZeroObject {C : Type u} {X : C} (hX : ) :
def CategoryTheory.Limits.IsZero.isoZero {C : Type u} {X : C} (hX : ) :
X 0

Every zero object is isomorphic to the zero object.

Equations
• hX.isoZero = hX.iso
Instances For
theorem CategoryTheory.Limits.IsZero.obj {C : Type u} {D : Type u'} [] {F : } (hF : ) (X : C) :

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

Equations
Instances For

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

Equations
Instances For
theorem CategoryTheory.Limits.HasZeroObject.to_zero_ext_iff {C : Type u} {X : C} {f : X 0} {g : X 0} :
f = g True
theorem CategoryTheory.Limits.HasZeroObject.to_zero_ext {C : Type u} {X : C} (f : X 0) (g : X 0) :
f = g
theorem CategoryTheory.Limits.HasZeroObject.from_zero_ext_iff {C : Type u} {X : C} {f : 0 X} {g : 0 X} :
f = g True
theorem CategoryTheory.Limits.HasZeroObject.from_zero_ext {C : Type u} {X : C} (f : 0 X) (g : 0 X) :
f = g
instance CategoryTheory.Limits.HasZeroObject.instMono {C : Type u} {X : C} (f : 0 X) :
Equations
• =
instance CategoryTheory.Limits.HasZeroObject.instEpi {C : Type u} {X : C} (f : X 0) :
Equations
• =
Equations
• =

A zero object is in particular initial.

Equations
• CategoryTheory.Limits.HasZeroObject.zeroIsInitial = .isInitial
Instances For

A zero object is in particular terminal.

Equations
• CategoryTheory.Limits.HasZeroObject.zeroIsTerminal = .isTerminal
Instances For
@[instance 10]

A zero object is in particular initial.

Equations
• =
@[instance 10]

A zero object is in particular terminal.

Equations
• =

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

Equations
• = CategoryTheory.Limits.HasZeroObject.zeroIsInitial.uniqueUpToIso t
Instances For

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

Equations
• = CategoryTheory.Limits.HasZeroObject.zeroIsTerminal.uniqueUpToIso t
Instances For

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

Equations
• CategoryTheory.Limits.HasZeroObject.zeroIsoInitial = CategoryTheory.Limits.HasZeroObject.zeroIsInitial.uniqueUpToIso CategoryTheory.Limits.initialIsInitial
Instances For

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

Equations
• CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal = CategoryTheory.Limits.HasZeroObject.zeroIsTerminal.uniqueUpToIso CategoryTheory.Limits.terminalIsTerminal
Instances For
@[instance 100]
Equations
• =
theorem CategoryTheory.Functor.isZero_iff {C : Type u} {D : Type u'} [] (F : ) :
∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)