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

• 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

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.

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

• CategoryTheory.Limits.IsZero.to_ h 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 = CategoryTheory.Limits.IsZero.to_ h 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) : CategoryTheory.Limits.IsZero.to_ h 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

• CategoryTheory.Limits.IsZero.from_ h 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 = CategoryTheory.Limits.IsZero.from_ h 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) : CategoryTheory.Limits.IsZero.from_ h 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

• CategoryTheory.Limits.IsZero.iso hX hY = CategoryTheory.Iso.mk (CategoryTheory.Limits.IsZero.to_ hX Y) (CategoryTheory.Limits.IsZero.from_ hX Y)

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

• CategoryTheory.Limits.IsZero.isInitial hX = 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

• CategoryTheory.Limits.IsZero.isTerminal hX = 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

• CategoryTheory.Limits.IsZero.isoIsInitial hX hY = CategoryTheory.Limits.IsInitial.uniqueUpToIso (CategoryTheory.Limits.IsZero.isInitial hX) 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

• CategoryTheory.Limits.IsZero.isoIsTerminal hX hY = CategoryTheory.Limits.IsTerminal.uniqueUpToIso (CategoryTheory.Limits.IsZero.isTerminal hX) 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 X.unop

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

• zero : ∃ X, CategoryTheory.Limits.IsZero X

  there exists a zero object

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

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

Equations

• CategoryTheory.Limits.hasZeroObject_pUnit = CategoryTheory.Limits.hasZeroObject_pUnit.proof_1

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 := Exists.choose (_ : ∃ X, CategoryTheory.Limits.IsZero X) }

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

• CategoryTheory.Limits.hasZeroObject_op = CategoryTheory.Limits.hasZeroObject_op.proof_1

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

• CategoryTheory.Limits.IsZero.isoZero hX = CategoryTheory.Limits.IsZero.iso hX (_ : CategoryTheory.Limits.IsZero 0)

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 = Nonempty.some (_ : Nonempty (Unique (0 ⟶ X)))

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 = Nonempty.some (_ : Nonempty (Unique (X ⟶ 0)))

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 {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.instSubsingletonIsoOfNatToOfNat0Zero' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] (X : C) : Subsingleton (X ≅ 0)

Equations

• @CategoryTheory.Limits.HasZeroObject.instSubsingletonIsoOfNatToOfNat0Zero' = @CategoryTheory.Limits.HasZeroObject.instSubsingletonIsoOfNatToOfNat0Zero'.proof_1

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

Equations

• @CategoryTheory.Limits.HasZeroObject.instMonoOfNat = @CategoryTheory.Limits.HasZeroObject.instMonoOfNat.proof_1

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

Equations

• @CategoryTheory.Limits.HasZeroObject.instEpiOfNatToOfNat0Zero' = @CategoryTheory.Limits.HasZeroObject.instEpiOfNatToOfNat0Zero'.proof_1

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

• @CategoryTheory.Limits.HasZeroObject.zero_to_zero_isIso = @CategoryTheory.Limits.HasZeroObject.zero_to_zero_isIso.proof_1

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 = CategoryTheory.Limits.IsZero.isInitial (_ : CategoryTheory.Limits.IsZero 0)

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 = CategoryTheory.Limits.IsZero.isTerminal (_ : CategoryTheory.Limits.IsZero 0)

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

• @CategoryTheory.Limits.HasZeroObject.hasInitial = @CategoryTheory.Limits.HasZeroObject.hasInitial.proof_1

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

• @CategoryTheory.Limits.HasZeroObject.hasTerminal = @CategoryTheory.Limits.HasZeroObject.hasTerminal.proof_1

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.IsInitial.uniqueUpToIso CategoryTheory.Limits.HasZeroObject.zeroIsInitial 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.IsTerminal.uniqueUpToIso CategoryTheory.Limits.HasZeroObject.zeroIsTerminal 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.IsInitial.uniqueUpToIso CategoryTheory.Limits.HasZeroObject.zeroIsInitial 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.IsTerminal.uniqueUpToIso CategoryTheory.Limits.HasZeroObject.zeroIsTerminal CategoryTheory.Limits.terminalIsTerminal

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

Equations

• @CategoryTheory.Limits.HasZeroObject.initialMonoClass = @CategoryTheory.Limits.HasZeroObject.initialMonoClass.proof_1

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)