Category theory Notes 2

Epis and monos

In any category $C$, an arrow $f: A → B$ is called a monomorphism if for any $g, h: C → A$, $f\cdot g = f\cdot h$ implies $g = h$.

We usually write $f: A ↣ B$ if $f$ is a monomorphism.

Similarly, an arrow $f: A → B$ is called an epimorphism (or $f$ is monic) if for any $g, h: B → D$, $g \cdot f = h \cdot f$ implies $g = h$.

We usually write $f: A ↠ B$ if $f$ is an epimorphism.

Initial and terminal objects

In any category $C$, an object 0¹ is initial if for any object A there is a unique morphism

$$ 0→A $$

Or in other words:

The initial object is the object that has one and only one morphism going to any object in the category. —— Category Theory for Programmers, Bartosz Milewski

Similarly, in any category $C$, an object $1$² is terminal if for any object $A$ there is a unique morphism

$$ A→1 $$

Or in other words:

The terminal object is the object with one and only one morphism coming to it from any object in the category. —— Category Theory for Programmers, Bartosz Milewski

Initial (terminal) objects are unique up to isomorphism.

In agda, the definition of initial (terminal is similar) object is something like:

record IsInitial (⊥ : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    ! : {A : Obj} → (⊥ ⇒ A)
    !-unique : ∀ {A} → (f : ⊥ ⇒ A) → ! ≈ f

record Initial : Set (o ⊔ ℓ ⊔ e) where
  field
    ⊥ : Obj
    ⊥-is-initial : IsInitial ⊥

Here ! is the morphism from ⊥ to A. And !-unique is the proof of the uniqueness, while the definition of ≈, which means isomorphism equal, is defined here.

Products and Coproducts

In category theory, the product of two (or more) objects in a category is a notion designed to capture the essence behind constructions in other areas of mathematics such as ... Essentially, the product of a family of objects is the "most general" object which admits a morphism to each of the given objects. —— Wikipedia

In other words:

A product of two objects $X_1$ and $X_2$ is the object $X_1\times X_2$ equipped with two projections such that for any other object $Y$ equipped with two projections there is a unique morphism $f$ from $Y$ to $X_1\times X_2$ that factorizes those projections.

Similarly, we can define coproducts:

The coproduct of a family of objects is essentially the "least specific" object to which each object in the family admits a morphism. It is the category-theoretic dual notion to the categorical product, which means the definition is the same as the product but with all arrows reversed. —— Wikipedia

In other words:

A coproduct of two objects $X_1$ and $X_2$ is the object $X_1 + X_2$ equipped with two injections such that for any other object $Y$ equipped with two injections there is a unique morphism $f$ from $X_1 + X_2$ to $Y$ that factorizes those injections.