mathlibdocumentation

category_theory.limits.shapes.zero_objects

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 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.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]
noncomputable def category_theory.limits.has_zero_object.has_zero (C : Type u)  :

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
theorem category_theory.limits.is_zero.has_zero_object {C : Type u} {X : C}  :
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]
def category_theory.limits.has_zero_object.category_theory.epi {C : Type u} {X : C} (f : X 0) :
@[protected, instance]
noncomputable def category_theory.limits.has_zero_object.zero_is_initial {C : Type u}  :

A zero object is in particular initial.

Equations
noncomputable def category_theory.limits.has_zero_object.zero_is_terminal {C : Type u}  :

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
noncomputable def category_theory.limits.has_zero_object.zero_iso_initial {C : Type u}  :
0 ⊥_ C

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

Equations
noncomputable def category_theory.limits.has_zero_object.zero_iso_terminal {C : Type u}  :
0 ⊤_ C

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