Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

CategoryTheory.Limits.IsZero structure

(X : C)

Full source

/-- 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`. -/
structure IsZero (X : C) : Prop where
  /-- there are unique morphisms to the object -/
  unique_to : ∀ Y, Nonempty (Unique (X ⟶ Y))
  /-- there are unique morphisms from the object -/
  unique_from : ∀ Y, Nonempty (Unique (Y ⟶ X))

Zero object in a category

Informal description

An object $ X $ in a category $ C $ is called a *zero object* if for every object $ Y $ in $ C $, there exists a unique morphism $ X \to Y $ and a unique morphism $ Y \to X $. This property characterizes whether a category has a zero object.

CategoryTheory.Limits.IsZero.to_ definition

(h : IsZero X) (Y : C) : X ⟶ Y

Full source

/-- If `h : IsZero X`, then `h.to_ Y` is a choice of unique morphism `X → Y`. -/
protected def to_ (h : IsZero X) (Y : C) : X ⟶ Y :=
  @default _ <| (h.unique_to Y).some.toInhabited

Unique morphism from a zero object

Informal description

Given an object $ X $ in a category $ C $ that is a zero object (i.e., `h : IsZero X` holds), the function `h.to_ Y` provides a choice of the unique morphism from $ X $ to any other object $ Y $ in $ C $.

CategoryTheory.Limits.IsZero.to_eq theorem

(h : IsZero X) (f : X ⟶ Y) : h.to_ Y = f

Full source

theorem to_eq (h : IsZero X) (f : X ⟶ Y) : h.to_ Y = f :=
  (h.eq_to f).symm

Uniqueness of Morphisms from a Zero Object

Informal description

Given an object $X$ in a category $C$ that is a zero object (i.e., $h : \text{IsZero}\,X$ holds), for any morphism $f : X \to Y$, the unique morphism $h.\text{to}_\,Y$ from $X$ to $Y$ equals $f$.

CategoryTheory.Limits.IsZero.from_ definition

(h : IsZero X) (Y : C) : Y ⟶ X

Full source

/-- If `h : is_zero X`, then `h.from_ Y` is a choice of unique morphism `Y → X`. -/
protected def from_ (h : IsZero X) (Y : C) : Y ⟶ X :=
  @default _ <| (h.unique_from Y).some.toInhabited

Unique morphism to a zero object

Informal description

Given an object $ X $ in a category $ C $ that is a zero object (i.e., `h : IsZero X` holds), the morphism `h.from_ Y` is the unique morphism from any object $ Y $ in $ C $ to $ X $.

CategoryTheory.Limits.IsZero.from_eq theorem

(h : IsZero X) (f : Y ⟶ X) : h.from_ Y = f

Full source

theorem from_eq (h : IsZero X) (f : Y ⟶ X) : h.from_ Y = f :=
  (h.eq_from f).symm

Uniqueness of Morphisms to a Zero Object

Informal description

Given an object $X$ in a category $C$ that is a zero object (i.e., $h : \text{IsZero}\, X$ holds), for any morphism $f : Y \to X$, the unique morphism $h.\text{from}_\, Y$ equals $f$.

CategoryTheory.Limits.IsZero.epi theorem

(h : IsZero X) {Y : C} (f : Y ⟶ X) : Epi f

Full source

lemma epi (h : IsZero X) {Y : C} (f : Y ⟶ X) : Epi f where
  left_cancellation _ _ _ := h.eq_of_src _ _

Morphisms to a Zero Object are Epimorphisms

Informal description

Let $ X $ be a zero object in a category $ C $. Then for any object $ Y $ in $ C $, any morphism $ f : Y \to X $ is an epimorphism.

CategoryTheory.Limits.IsZero.mono theorem

(h : IsZero X) {Y : C} (f : X ⟶ Y) : Mono f

Full source

lemma mono (h : IsZero X) {Y : C} (f : X ⟶ Y) : Mono f where
  right_cancellation _ _ _ := h.eq_of_tgt _ _

Morphisms from a Zero Object are Monomorphisms

Informal description

Let $X$ be a zero object in a category $C$. Then for any object $Y$ in $C$, any morphism $f : X \to Y$ is a monomorphism.

CategoryTheory.Limits.IsZero.iso definition

(hX : IsZero X) (hY : IsZero Y) : X ≅ Y

Full source

/-- Any two zero objects are isomorphic. -/
def iso (hX : IsZero X) (hY : IsZero Y) : X ≅ Y where
  hom := hX.to_ Y
  inv := hX.from_ Y
  hom_inv_id := hX.eq_of_src _ _
  inv_hom_id := hY.eq_of_src _ _

Isomorphism between zero objects

Informal description

Given two objects $ X $ and $ Y $ in a category $ C $, if both $ X $ and $ Y $ are zero objects (i.e., `hX : IsZero X` and `hY : IsZero Y` hold), then there exists a unique isomorphism between $ X $ and $ Y $. The isomorphism is given by the unique morphisms `hX.to_ Y` and `hX.from_ Y`, and their compositions satisfy the identity conditions.

CategoryTheory.Limits.IsZero.isInitial definition

(hX : IsZero X) : IsInitial X

Full source

/-- A zero object is in particular initial. -/
protected def isInitial (hX : IsZero X) : IsInitial X :=
  @IsInitial.ofUnique _ _ X fun Y => (hX.unique_to Y).some

Zero object implies initial object

Informal description

If an object $ X $ in a category $ C $ is a zero object (i.e., it is both initial and terminal), then it is in particular an initial object. This means that for every object $ Y $ in $ C $, there exists a unique morphism from $ X $ to $ Y $.

CategoryTheory.Limits.IsZero.isTerminal definition

(hX : IsZero X) : IsTerminal X

Full source

/-- A zero object is in particular terminal. -/
protected def isTerminal (hX : IsZero X) : IsTerminal X :=
  @IsTerminal.ofUnique _ _ X fun Y => (hX.unique_from Y).some

Zero object implies terminal object

Informal description

If an object $ X $ in a category $ \mathcal{C} $ is a zero object (i.e., it is both initial and terminal), then it is in particular a terminal object. This means that for every object $ Y $ in $ \mathcal{C} $, there exists a unique morphism from $ Y $ to $ X $.

CategoryTheory.Limits.IsZero.isoIsInitial definition

(hX : IsZero X) (hY : IsInitial Y) : X ≅ Y

Full source

/-- The (unique) isomorphism between any initial object and the zero object. -/
def isoIsInitial (hX : IsZero X) (hY : IsInitial Y) : X ≅ Y :=
  IsInitial.uniqueUpToIso hX.isInitial hY

Isomorphism between zero object and initial object

Informal description

Given a zero object $ X $ and an initial object $ Y $ in a category $ \mathcal{C} $, there exists a unique isomorphism between $ X $ and $ Y $. This isomorphism is constructed using the unique morphisms provided by the universal properties of zero and initial objects.

CategoryTheory.Limits.IsZero.isoIsTerminal definition

(hX : IsZero X) (hY : IsTerminal Y) : X ≅ Y

Full source

/-- The (unique) isomorphism between any terminal object and the zero object. -/
def isoIsTerminal (hX : IsZero X) (hY : IsTerminal Y) : X ≅ Y :=
  IsTerminal.uniqueUpToIso hX.isTerminal hY

Isomorphism between zero object and terminal object

Informal description

Given a zero object $ X $ and a terminal object $ Y $ in a category $ \mathcal{C} $, there exists a unique isomorphism between $ X $ and $ Y $. This isomorphism is constructed using the unique morphisms provided by the universal properties of zero and terminal objects.

CategoryTheory.Limits.IsZero.of_iso theorem

(hY : IsZero Y) (e : X ≅ Y) : IsZero X

Full source

theorem of_iso (hY : IsZero Y) (e : X ≅ Y) : IsZero X := by
  refine ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => ?_⟩⟩,
    fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => ?_⟩⟩⟩
  · rw [← cancel_epi e.inv]
    apply hY.eq_of_src
  · rw [← cancel_mono e.hom]
    apply hY.eq_of_tgt

Isomorphism preserves zero objects

Informal description

Let $\mathcal{C}$ be a category, and let $X$ and $Y$ be objects in $\mathcal{C}$. If $Y$ is a zero object (i.e., $h_Y : \text{IsZero}\, Y$ holds) and there exists an isomorphism $e : X \cong Y$, then $X$ is also a zero object.

CategoryTheory.Limits.IsZero.op theorem

(h : IsZero X) : IsZero (Opposite.op X)

Full source

theorem op (h : IsZero X) : IsZero (Opposite.op X) :=
  ⟨fun Y => ⟨⟨⟨(h.from_ (Opposite.unop Y)).op⟩, fun _ => Quiver.Hom.unop_inj (h.eq_of_tgt _ _)⟩⟩,
    fun Y => ⟨⟨⟨(h.to_ (Opposite.unop Y)).op⟩, fun _ => Quiver.Hom.unop_inj (h.eq_of_src _ _)⟩⟩⟩

Opposite of a Zero Object is Zero

Informal description

If an object $X$ in a category $C$ is a zero object, then its opposite $\mathrm{op}\, X$ in the opposite category $C^{\mathrm{op}}$ is also a zero object.

CategoryTheory.Limits.IsZero.unop theorem

{X : Cᵒᵖ} (h : IsZero X) : IsZero (Opposite.unop X)

Full source

theorem unop {X : Cᵒᵖ} (h : IsZero X) : IsZero (Opposite.unop X) :=
  ⟨fun Y => ⟨⟨⟨(h.from_ (Opposite.op Y)).unop⟩, fun _ => Quiver.Hom.op_inj (h.eq_of_tgt _ _)⟩⟩,
    fun Y => ⟨⟨⟨(h.to_ (Opposite.op Y)).unop⟩, fun _ => Quiver.Hom.op_inj (h.eq_of_src _ _)⟩⟩⟩

Unopposite of a Zero Object is Zero

Informal description

Let $C$ be a category and $X$ an object in its opposite category $C^{\mathrm{op}}$. If $X$ is a zero object in $C^{\mathrm{op}}$, then its unopposite $\mathrm{unop}\, X$ is a zero object in $C$.

CategoryTheory.Iso.isZero_iff theorem

{X Y : C} (e : X ≅ Y) : IsZero X ↔ IsZero Y

Full source

theorem Iso.isZero_iff {X Y : C} (e : X ≅ Y) : IsZeroIsZero X ↔ IsZero Y :=
  ⟨fun h => h.of_iso e.symm, fun h => h.of_iso e⟩

Isomorphism Preserves Zero Object Property

Informal description

Given an isomorphism $e \colon X \cong Y$ between objects $X$ and $Y$ in a category $\mathcal{C}$, the object $X$ is a zero object if and only if $Y$ is a zero object.

CategoryTheory.Functor.isZero theorem

(F : C ⥤ D) (hF : ∀ X, IsZero (F.obj X)) : IsZero F

Full source

theorem Functor.isZero (F : C ⥤ D) (hF : ∀ X, IsZero (F.obj X)) : IsZero F := by
  constructor <;> intro G <;> refine ⟨⟨⟨?_⟩, ?_⟩⟩
  · refine
      { app := fun X => (hF _).to_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_src _ _
  · intro f
    ext
    apply (hF _).eq_of_src _ _
  · refine
      { app := fun X => (hF _).from_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_tgt _ _
  · intro f
    ext
    apply (hF _).eq_of_tgt _ _

Functor to Zero Objects is Zero in Functor Category

Informal description

Let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor between categories. If for every object $X$ in $\mathcal{C}$, the object $F(X)$ is a zero object in $\mathcal{D}$, then $F$ itself is a zero object in the functor category $\mathcal{C} \to \mathcal{D}$.

CategoryTheory.Limits.HasZeroObject structure

Full source

/-- A category "has a zero object" if it has an object which is both initial and terminal. -/
class HasZeroObject : Prop where
  /-- there exists a zero object -/
  zero : ∃ X : C, IsZero X

Category with Zero Object

Informal description

A category $ C $ has a zero object if there exists an object in $ C $ that is both initial and terminal. This means there is an object $ 0 $ such that for every object $ X $ in $ C $, there exists a unique morphism $ 0 \to X $ and a unique morphism $ X \to 0 $.

CategoryTheory.Limits.hasZeroObject_pUnit instance

: HasZeroObject (Discrete PUnit)

Full source

instance hasZeroObject_pUnit : HasZeroObject (Discrete PUnit) where zero :=
  ⟨⟨⟨⟩⟩,
    { unique_to := fun ⟨⟨⟩⟩ =>
      ⟨{ default := 𝟙 _,
          uniq := by subsingleton }⟩
      unique_from := fun ⟨⟨⟩⟩ =>
      ⟨{ default := 𝟙 _,
          uniq := by subsingleton }⟩}⟩

The Discrete Singleton Category has a Zero Object

Informal description

The discrete category on the singleton type `PUnit` has a zero object. Specifically, the unique object in this category serves as both an initial and terminal object, making it a zero object.

CategoryTheory.Limits.HasZeroObject.zero' definition

: Zero C

Full source

/-- 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.
-/
protected def HasZeroObject.zero' : Zero C where zero := HasZeroObject.zero.choose

Zero object in a category with zero objects

Informal description

Given a category $ C $ with a zero object, this constructs a `Zero C` instance where the zero element is the chosen zero object of the category. This cannot be a global instance to avoid unnecessary typeclass searches.

CategoryTheory.Limits.isZero_zero theorem

: IsZero (0 : C)

Full source

theorem isZero_zero : IsZero (0 : C) :=
  HasZeroObject.zero.choose_spec

The Zero Object is Initial and Terminal

Informal description

In a category $C$ with a zero object, the object $0$ is a zero object, meaning it is both initial and terminal. That is, for every object $X$ in $C$, there exists a unique morphism $0 \to X$ and a unique morphism $X \to 0$.

CategoryTheory.Limits.hasZeroObject_op instance

: HasZeroObject Cᵒᵖ

Full source

instance hasZeroObject_op : HasZeroObject Cᵒᵖ :=
  ⟨⟨Opposite.op 0, IsZero.op (isZero_zero C)⟩⟩

Opposite Category Preserves Zero Object

Informal description

The opposite category $C^{\mathrm{op}}$ of a category $C$ with a zero object also has a zero object.

CategoryTheory.Limits.hasZeroObject_unop theorem

[HasZeroObject Cᵒᵖ] : HasZeroObject C

Full source

theorem hasZeroObject_unop [HasZeroObject Cᵒᵖ] : HasZeroObject C :=
  ⟨⟨Opposite.unop 0, IsZero.unop (isZero_zero Cᵒᵖ)⟩⟩

Existence of Zero Object in Category from Opposite Category

Informal description

If the opposite category $C^{\mathrm{op}}$ has a zero object, then the original category $C$ also has a zero object.

CategoryTheory.Limits.IsZero.hasZeroObject theorem

{X : C} (hX : IsZero X) : HasZeroObject C

Full source

theorem IsZero.hasZeroObject {X : C} (hX : IsZero X) : HasZeroObject C :=
  ⟨⟨X, hX⟩⟩

Existence of Zero Object from Zero Object Property

Informal description

If an object $X$ in a category $C$ is a zero object (i.e., for every object $Y$ in $C$, there exists a unique morphism $X \to Y$ and a unique morphism $Y \to X$), then the category $C$ has a zero object.

CategoryTheory.Limits.IsZero.isoZero definition

[HasZeroObject C] {X : C} (hX : IsZero X) : X ≅ 0

Full source

/-- Every zero object is isomorphic to *the* zero object. -/
def IsZero.isoZero [HasZeroObject C] {X : C} (hX : IsZero X) : X ≅ 0 :=
  hX.iso (isZero_zero C)

Isomorphism between a zero object and the zero object of the category

Informal description

Given a category $ C $ with a zero object and an object $ X $ in $ C $ that is a zero object (i.e., `hX : IsZero X` holds), there exists a unique isomorphism between $ X $ and the zero object $ 0 $ of $ C $.

CategoryTheory.Limits.IsZero.obj theorem

[HasZeroObject D] {F : C ⥤ D} (hF : IsZero F) (X : C) : IsZero (F.obj X)

Full source

theorem IsZero.obj [HasZeroObject D] {F : C ⥤ D} (hF : IsZero F) (X : C) : IsZero (F.obj X) := by
  let G : C ⥤ D := (CategoryTheory.Functor.const C).obj 0
  have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _
  let e : F ≅ G := hF.iso hG
  exact (isZero_zero _).of_iso (e.app X)

Zero Functor Maps to Zero Objects

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with $\mathcal{D}$ having a zero object. If a functor $F \colon \mathcal{C} \to \mathcal{D}$ is a zero object in the functor category $\mathcal{C} \to \mathcal{D}$ (i.e., $h_F : \text{IsZero}\, F$ holds), then for every object $X$ in $\mathcal{C}$, the object $F(X)$ is a zero object in $\mathcal{D}$.

CategoryTheory.Limits.HasZeroObject.uniqueTo definition

(X : C) : Unique (0 ⟶ X)

Full source

/-- There is a unique morphism from the zero object to any object `X`. -/
protected def uniqueTo (X : C) : Unique (0 ⟶ X) :=
  ((isZero_zero C).unique_to X).some

Unique morphism from zero object

Informal description

For any object $ X $ in a category $ C $ with a zero object, there is a unique morphism from the zero object to $ X $.

CategoryTheory.Limits.HasZeroObject.uniqueFrom definition

(X : C) : Unique (X ⟶ 0)

Full source

/-- There is a unique morphism from any object `X` to the zero object. -/
protected def uniqueFrom (X : C) : Unique (X ⟶ 0) :=
  ((isZero_zero C).unique_from X).some

Unique morphism to zero object

Informal description

For any object $ X $ in a category $ C $ with a zero object, there is a unique morphism from $ X $ to the zero object.

CategoryTheory.Limits.HasZeroObject.to_zero_ext theorem

{X : C} (f g : X ⟶ 0) : f = g

Full source

@[ext]
theorem to_zero_ext {X : C} (f g : X ⟶ 0) : f = g :=
  (isZero_zero C).eq_of_tgt _ _

Uniqueness of morphisms to zero object

Informal description

In a category $C$ with a zero object, any two morphisms $f, g : X \to 0$ from an object $X$ to the zero object are equal.

CategoryTheory.Limits.HasZeroObject.from_zero_ext theorem

{X : C} (f g : 0 ⟶ X) : f = g

Full source

@[ext]
theorem from_zero_ext {X : C} (f g : 0 ⟶ X) : f = g :=
  (isZero_zero C).eq_of_src _ _

Uniqueness of Morphisms from Zero Object

Informal description

In a category $C$ with a zero object, any two morphisms $f, g$ from the zero object $0$ to an object $X$ in $C$ are equal, i.e., $f = g$.

CategoryTheory.Limits.HasZeroObject.instSubsingletonIsoOfNat instance

(X : C) : Subsingleton (X ≅ 0)

Full source

instance (X : C) : Subsingleton (X ≅ 0) := ⟨fun f g => by ext⟩

Uniqueness of Isomorphisms to Zero Object

Informal description

For any object $X$ in a category $\mathcal{C}$ with a zero object, the collection of isomorphisms between $X$ and the zero object is a subsingleton (i.e., has at most one element up to equality).

CategoryTheory.Limits.HasZeroObject.instMono instance

{X : C} (f : 0 ⟶ X) : Mono f

Full source

instance {X : C} (f : 0 ⟶ X) : Mono f where right_cancellation g h _ := by ext

Morphisms from Zero Object are Monomorphisms

Informal description

In a category $\mathcal{C}$ with a zero object, every morphism $f : 0 \to X$ from the zero object to any object $X$ is a monomorphism.

CategoryTheory.Limits.HasZeroObject.instEpi instance

{X : C} (f : X ⟶ 0) : Epi f

Full source

instance {X : C} (f : X ⟶ 0) : Epi f where left_cancellation g h _ := by ext

Morphisms to Zero Objects are Epimorphisms

Informal description

In a category $\mathcal{C}$ with a zero object, any morphism $f : X \to 0$ from an object $X$ to the zero object is an epimorphism.

CategoryTheory.Limits.HasZeroObject.zero_to_zero_isIso instance

(f : (0 : C) ⟶ 0) : IsIso f

Full source

instance zero_to_zero_isIso (f : (0 : C) ⟶ 0) : IsIso f := by
  convert show IsIso (𝟙 (0 : C)) by infer_instance
  subsingleton

Morphisms Between Zero Objects are Isomorphisms

Informal description

In a category $\mathcal{C}$ with a zero object, any morphism $f : 0 \to 0$ between zero objects is an isomorphism.

CategoryTheory.Limits.HasZeroObject.zeroIsInitial definition

: IsInitial (0 : C)

Full source

/-- A zero object is in particular initial. -/
def zeroIsInitial : IsInitial (0 : C) :=
  (isZero_zero C).isInitial

Zero object is initial

Informal description

In a category $ C $ with a zero object, the zero object $ 0 $ is initial. That is, for every object $ X $ in $ C $, there exists a unique morphism $ 0 \to X $.

CategoryTheory.Limits.HasZeroObject.zeroIsTerminal definition

: IsTerminal (0 : C)

Full source

/-- A zero object is in particular terminal. -/
def zeroIsTerminal : IsTerminal (0 : C) :=
  (isZero_zero C).isTerminal

Zero object is terminal

Informal description

The zero object $0$ in a category $C$ is a terminal object. That is, for every object $X$ in $C$, there exists a unique morphism from $X$ to $0$.

CategoryTheory.Limits.HasZeroObject.hasInitial instance

: HasInitial C

Full source

/-- A zero object is in particular initial. -/
instance (priority := 10) hasInitial : HasInitial C :=
  hasInitial_of_unique 0

Existence of Initial Object in Categories with Zero Object

Informal description

Every category with a zero object has an initial object.

CategoryTheory.Limits.HasZeroObject.hasTerminal instance

: HasTerminal C

Full source

/-- A zero object is in particular terminal. -/
instance (priority := 10) hasTerminal : HasTerminal C :=
  hasTerminal_of_unique 0

Existence of Terminal Object in Categories with Zero Object

Informal description

Every category with a zero object has a terminal object.

CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial definition

{X : C} (t : IsInitial X) : 0 ≅ X

Full source

/-- The (unique) isomorphism between any initial object and the zero object. -/
def zeroIsoIsInitial {X : C} (t : IsInitial X) : 0 ≅ X :=
  zeroIsInitial.uniqueUpToIso t

Isomorphism between zero object and initial object

Informal description

Given an initial object $X$ in a category $\mathcal{C}$ with a zero object, there is a unique isomorphism between the zero object $0$ and $X$.

CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal definition

{X : C} (t : IsTerminal X) : 0 ≅ X

Full source

/-- The (unique) isomorphism between any terminal object and the zero object. -/
def zeroIsoIsTerminal {X : C} (t : IsTerminal X) : 0 ≅ X :=
  zeroIsTerminal.uniqueUpToIso t

Isomorphism between zero object and terminal object

Informal description

Given a terminal object $X$ in a category $\mathcal{C}$ with a zero object, there is a unique isomorphism between the zero object $0$ and $X$.

CategoryTheory.Limits.HasZeroObject.zeroIsoInitial definition

[HasInitial C] : 0 ≅ ⊥_ C

Full source

/-- The (unique) isomorphism between the chosen initial object and the chosen zero object. -/
def zeroIsoInitial [HasInitial C] : 0 ≅ ⊥_ C :=
  zeroIsInitial.uniqueUpToIso initialIsInitial

Isomorphism between zero object and initial object

Informal description

The unique isomorphism between the zero object $0$ and the initial object $\bot_{\mathcal{C}}$ in a category $\mathcal{C}$ that has both a zero object and an initial object.

CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal definition

[HasTerminal C] : 0 ≅ ⊤_ C

Full source

/-- The (unique) isomorphism between the chosen terminal object and the chosen zero object. -/
def zeroIsoTerminal [HasTerminal C] : 0 ≅ ⊤_ C :=
  zeroIsTerminal.uniqueUpToIso terminalIsTerminal

Isomorphism between zero object and terminal object

Informal description

The unique isomorphism between the zero object $0$ and the terminal object $\top_{\mathcal{C}}$ in a category $\mathcal{C}$ that has both a zero object and a terminal object.

CategoryTheory.Limits.HasZeroObject.initialMonoClass instance

: InitialMonoClass C

Full source

instance (priority := 100) initialMonoClass : InitialMonoClass C :=
  InitialMonoClass.of_isInitial zeroIsInitial fun X => by infer_instance

Categories with Zero Objects are Initial Mono Classes

Informal description

Every category $\mathcal{C}$ with a zero object is an `InitialMonoClass`, meaning that for any initial object $I$ in $\mathcal{C}$, the unique morphism from $I$ to any other object $X$ is a monomorphism.

CategoryTheory.Functor.isZero_iff theorem

[HasZeroObject D] (F : C ⥤ D) : IsZero F ↔ ∀ X, IsZero (F.obj X)

Full source

theorem Functor.isZero_iff [HasZeroObject D] (F : C ⥤ D) : IsZeroIsZero F ↔ ∀ X, IsZero (F.obj X) :=
  ⟨fun hF X => hF.obj X, Functor.isZero _⟩

Characterization of Zero Functors via Zero Objects

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with $\mathcal{D}$ having a zero object. A functor $F \colon \mathcal{C} \to \mathcal{D}$ is a zero object in the functor category $\mathcal{C} \to \mathcal{D}$ if and only if for every object $X$ in $\mathcal{C}$, the object $F(X)$ is a zero object in $\mathcal{D}$.

References