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

• [F. Borceux, Handbook of Categorical Algebra 2][borceux-vol2]

structure CategoryTheory.Limits.IsZero {C : Type u} [Category.{v, u} C] (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 HasZeroObject.

• 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

noncomputable def CategoryTheory.Limits.IsZero.to_ {C : Type u} [Category.{v, u} C] {X : C} (h : IsZero X) (Y : C) : X ⟶ Y

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

to is a reserved word, it was replaced by to_

theorem CategoryTheory.Limits.IsZero.eq_to {C : Type u} [Category.{v, u} C] {X Y : C} (h : IsZero X) (f : X ⟶ Y) : f = h.to_ Y

theorem CategoryTheory.Limits.IsZero.to_eq {C : Type u} [Category.{v, u} C] {X Y : C} (h : IsZero X) (f : X ⟶ Y) : h.to_ Y = f

noncomputable def CategoryTheory.Limits.IsZero.from_ {C : Type u} [Category.{v, u} C] {X : C} (h : IsZero X) (Y : C) : Y ⟶ X

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

from is a reserved word, it was replaced by from_

theorem CategoryTheory.Limits.IsZero.eq_from {C : Type u} [Category.{v, u} C] {X Y : C} (h : IsZero X) (f : Y ⟶ X) : f = h.from_ Y

theorem CategoryTheory.Limits.IsZero.from_eq {C : Type u} [Category.{v, u} C] {X Y : C} (h : IsZero X) (f : Y ⟶ X) : h.from_ Y = f

theorem CategoryTheory.Limits.IsZero.eq_of_src {C : Type u} [Category.{v, u} C] {X Y : C} (hX : IsZero X) (f g : X ⟶ Y) : f = g

theorem CategoryTheory.Limits.IsZero.eq_of_tgt {C : Type u} [Category.{v, u} C] {X Y : C} (hX : IsZero X) (f g : Y ⟶ X) : f = g

theorem CategoryTheory.Limits.IsZero.epi {C : Type u} [Category.{v, u} C] {X : C} (h : IsZero X) {Y : C} (f : Y ⟶ X) : Epi f

theorem CategoryTheory.Limits.IsZero.mono {C : Type u} [Category.{v, u} C] {X : C} (h : IsZero X) {Y : C} (f : X ⟶ Y) : Mono f

noncomputable def CategoryTheory.Limits.IsZero.iso {C : Type u} [Category.{v, u} C] {X Y : C} (hX : IsZero X) (hY : IsZero Y) : X ≅ Y

Any two zero objects are isomorphic.

theorem CategoryTheory.Limits.IsZero.isIso {C : Type u} [Category.{v, u} C] {X Y : C} (hX : IsZero X) (hY : IsZero Y) (f : X ⟶ Y) : IsIso f

noncomputable def CategoryTheory.Limits.IsZero.isInitial {C : Type u} [Category.{v, u} C] {X : C} (hX : IsZero X) : IsInitial X

A zero object is in particular initial.

noncomputable def CategoryTheory.Limits.IsZero.isTerminal {C : Type u} [Category.{v, u} C] {X : C} (hX : IsZero X) : IsTerminal X

A zero object is in particular terminal.

noncomputable def CategoryTheory.Limits.IsZero.isoIsInitial {C : Type u} [Category.{v, u} C] {X Y : C} (hX : IsZero X) (hY : IsInitial Y) : X ≅ Y

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

noncomputable def CategoryTheory.Limits.IsZero.isoIsTerminal {C : Type u} [Category.{v, u} C] {X Y : C} (hX : IsZero X) (hY : IsTerminal Y) : X ≅ Y

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

theorem CategoryTheory.Limits.IsZero.of_iso {C : Type u} [Category.{v, u} C] {X Y : C} (hY : IsZero Y) (e : X ≅ Y) : IsZero X

theorem CategoryTheory.Limits.IsZero.op {C : Type u} [Category.{v, u} C] {X : C} (h : IsZero X) : IsZero (Opposite.op X)

theorem CategoryTheory.Limits.IsZero.unop {C : Type u} [Category.{v, u} C] {X : Cᵒᵖ} (h : IsZero X) : IsZero (Opposite.unop X)

noncomputable def CategoryTheory.Limits.IsZero.retract {C : Type u} [Category.{v, u} C] {X : C} (Y : C) (h : IsZero X) : Retract X Y

A zero object is a retract of every object.

theorem CategoryTheory.Iso.isZero_iff {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) : Limits.IsZero X ↔ Limits.IsZero Y

theorem CategoryTheory.Functor.isZero {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) (hF : ∀ (X : C), Limits.IsZero (F.obj X)) : Limits.IsZero F

class CategoryTheory.Limits.HasZeroObject (C : Type u) [Category.{v, u} C] : Prop

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

• zero : ∃ (X : C), IsZero X

  there exists a zero object

instance CategoryTheory.Limits.hasZeroObject_pUnit : HasZeroObject (Discrete PUnit.{u_1 + 1})

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.HasZeroObject.zero' (C : Type u) [Category.{v, u} C] [HasZeroObject C] : Zero C

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

theorem CategoryTheory.Limits.isZero_zero (C : Type u) [Category.{v, u} C] [HasZeroObject C] : IsZero 0

instance CategoryTheory.Limits.hasZeroObject_op (C : Type u) [Category.{v, u} C] [HasZeroObject C] : HasZeroObject Cᵒᵖ

theorem CategoryTheory.Limits.hasZeroObject_unop (C : Type u) [Category.{v, u} C] [HasZeroObject Cᵒᵖ] : HasZeroObject C

theorem CategoryTheory.Limits.IsZero.hasZeroObject {C : Type u} [Category.{v, u} C] {X : C} (hX : IsZero X) : HasZeroObject C

noncomputable def CategoryTheory.Limits.IsZero.isoZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] {X : C} (hX : IsZero X) : X ≅ 0

Every zero object is isomorphic to the zero object.

theorem CategoryTheory.Limits.IsZero.obj {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroObject D] {F : Functor C D} (hF : IsZero F) (X : C) : IsZero (F.obj X)

theorem CategoryTheory.Limits.IsZero.of_full_of_faithful_of_isZero {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) [F.Full] [F.Faithful] (X : C) (hX : IsZero (F.obj X)) : IsZero X

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.HasZeroObject.uniqueTo {C : Type u} [Category.{v, u} C] [HasZeroObject C] (X : C) : Unique (0 ⟶ X)

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

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.HasZeroObject.uniqueFrom {C : Type u} [Category.{v, u} C] [HasZeroObject C] (X : C) : Unique (X ⟶ 0)

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

theorem CategoryTheory.Limits.HasZeroObject.to_zero_ext {C : Type u} [Category.{v, u} C] [HasZeroObject C] {X : C} (f g : X ⟶ 0) : f = g

theorem CategoryTheory.Limits.HasZeroObject.to_zero_ext_iff {C : Type u} [Category.{v, u} C] [HasZeroObject C] {X : C} {f g : X ⟶ 0} : f = g ↔ True

theorem CategoryTheory.Limits.HasZeroObject.from_zero_ext {C : Type u} [Category.{v, u} C] [HasZeroObject C] {X : C} (f g : 0 ⟶ X) : f = g

theorem CategoryTheory.Limits.HasZeroObject.from_zero_ext_iff {C : Type u} [Category.{v, u} C] [HasZeroObject C] {X : C} {f g : 0 ⟶ X} : f = g ↔ True

instance CategoryTheory.Limits.HasZeroObject.instSubsingletonIsoOfNat {C : Type u} [Category.{v, u} C] [HasZeroObject C] (X : C) : Subsingleton (X ≅ 0)

instance CategoryTheory.Limits.HasZeroObject.instMono {C : Type u} [Category.{v, u} C] [HasZeroObject C] {X : C} (f : 0 ⟶ X) : Mono f

instance CategoryTheory.Limits.HasZeroObject.instEpi {C : Type u} [Category.{v, u} C] [HasZeroObject C] {X : C} (f : X ⟶ 0) : Epi f

instance CategoryTheory.Limits.HasZeroObject.zero_to_zero_isIso {C : Type u} [Category.{v, u} C] [HasZeroObject C] (f : 0 ⟶ 0) : IsIso f

noncomputable def CategoryTheory.Limits.HasZeroObject.zeroIsInitial {C : Type u} [Category.{v, u} C] [HasZeroObject C] : IsInitial 0

A zero object is in particular initial.

noncomputable def CategoryTheory.Limits.HasZeroObject.zeroIsTerminal {C : Type u} [Category.{v, u} C] [HasZeroObject C] : IsTerminal 0

A zero object is in particular terminal.

@[instance 10]

instance CategoryTheory.Limits.HasZeroObject.hasInitial {C : Type u} [Category.{v, u} C] [HasZeroObject C] : HasInitial C

A zero object is in particular initial.

@[instance 10]

instance CategoryTheory.Limits.HasZeroObject.hasTerminal {C : Type u} [Category.{v, u} C] [HasZeroObject C] : HasTerminal C

A zero object is in particular terminal.

noncomputable def CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial {C : Type u} [Category.{v, u} C] [HasZeroObject C] {X : C} (t : IsInitial X) : 0 ≅ X

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

noncomputable def CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal {C : Type u} [Category.{v, u} C] [HasZeroObject C] {X : C} (t : IsTerminal X) : 0 ≅ X

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

noncomputable def CategoryTheory.Limits.HasZeroObject.zeroIsoInitial {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasInitial C] : 0 ≅ ⊥_ C

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

noncomputable def CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasTerminal C] : 0 ≅ ⊤_ C

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

@[instance 100]

instance CategoryTheory.Limits.HasZeroObject.initialMonoClass {C : Type u} [Category.{v, u} C] [HasZeroObject C] : InitialMonoClass C

theorem CategoryTheory.Functor.isZero_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroObject D] (F : Functor C D) : Limits.IsZero F ↔ ∀ (X : C), Limits.IsZero (F.obj X)