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} [CategoryTheory.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 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

theorem CategoryTheory.Limits.IsZero.unique_to {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (self : CategoryTheory.Limits.IsZero X) (Y : C) : Nonempty (Unique (X ⟶ Y))

there are unique morphisms to the object

theorem CategoryTheory.Limits.IsZero.unique_from {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (self : CategoryTheory.Limits.IsZero X) (Y : C) : Nonempty (Unique (Y ⟶ X))

there are unique morphisms from the object

def CategoryTheory.Limits.IsZero.to_ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsZero X) (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

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

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

def CategoryTheory.Limits.IsZero.from_ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsZero X) (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

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

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

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

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

def CategoryTheory.Limits.IsZero.iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (hX : CategoryTheory.Limits.IsZero X) (hY : CategoryTheory.Limits.IsZero Y) : 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 := ⋯ }

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

A zero object is in particular initial.

Equations

• hX.isInitial = CategoryTheory.Limits.IsInitial.ofUnique X

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

A zero object is in particular terminal.

Equations

• hX.isTerminal = CategoryTheory.Limits.IsTerminal.ofUnique X

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

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

Equations

• hX.isoIsInitial hY = hX.isInitial.uniqueUpToIso hY

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

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

Equations

• hX.isoIsTerminal hY = hX.isTerminal.uniqueUpToIso hY

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

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

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

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

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

class CategoryTheory.Limits.HasZeroObject (C : Type u) [CategoryTheory.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), CategoryTheory.Limits.IsZero X

  there exists a zero object

theorem CategoryTheory.Limits.HasZeroObject.zero {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasZeroObject C], ∃ (X : C), CategoryTheory.Limits.IsZero X

there exists a zero object

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

Equations

• CategoryTheory.Limits.hasZeroObject_pUnit = ⋯

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

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

• CategoryTheory.Limits.HasZeroObject.zero' C = { zero := ⋯.choose }

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

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

Equations

• ⋯ = ⋯

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

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

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

Every zero object is isomorphic to the zero object.

Equations

• hX.isoZero = hX.iso ⋯

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

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

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

Equations

• CategoryTheory.Limits.HasZeroObject.uniqueTo X = ⋯.some

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

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

Equations

• CategoryTheory.Limits.HasZeroObject.uniqueFrom X = ⋯.some

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

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

A zero object is in particular initial.

Equations

• CategoryTheory.Limits.HasZeroObject.zeroIsInitial = ⋯.isInitial

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

A zero object is in particular terminal.

Equations

• CategoryTheory.Limits.HasZeroObject.zeroIsTerminal = ⋯.isTerminal

@[instance 10]

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

A zero object is in particular initial.

Equations

• ⋯ = ⋯

@[instance 10]

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

A zero object is in particular terminal.

Equations

• ⋯ = ⋯

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

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

Equations

• CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial t = CategoryTheory.Limits.HasZeroObject.zeroIsInitial.uniqueUpToIso t

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

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

Equations

• CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal t = CategoryTheory.Limits.HasZeroObject.zeroIsTerminal.uniqueUpToIso t

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

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

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

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

@[instance 100]

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

Equations

• ⋯ = ⋯

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