Initial object
Object
| context | ${\bf C}$ … category |
| definiendum | $I:\mathrm{Ob}_{\bf C}$ |
| for all | $X:\mathrm{Ob}_{\bf C}$ |
| postulate | $\exists_!i.\ i:{\bf C}[I,X]$ |
Discussion
Alternative definitions
The initial object of ${\bf C}$ can be characterized by the initial morphism $\langle I,\mathrm{id}_\bullet\rangle$ from $\bullet:\mathrm{Ob}_{\bf 1}$ to the (unique) functor $U$ mapping to the discrete category ${\bf 1}$, which only has a single object. Because then $U(g)=f$ is trivially true for all $g:\mathrm{Mor}_{\bf C}$ and $f:\mathrm{Mor}_{\bf 1}$ (the latter is necessarily the identity), the initial morphisms definition reduces to the statement that ${\bf C}[I,X]$ has only one term:
$\forall X:\mathrm{Ob}_{\bf C}.\ \exists_!(g:{\bf C}[I,X]).\ true$
Reference
Wikipedia: Initial and terminal objects
Parents
Context
Requirements
Element of
Related
