What is the proof that there is only one homomorphism from an initial object to another object?
$\begingroup$
$\endgroup$
3
-
$\begingroup$ Oops, sorry. I completely misunderstood your question, I suppose! $\endgroup$– Daniel AponAug 21 '10 at 21:03
-
1$\begingroup$ en.wikipedia.org/wiki/Initial_and_terminal_objects $\endgroup$– Dave ClarkeAug 21 '10 at 23:02
-
$\begingroup$ Small correction: "morphism" instead of "homomorphism" is used in the context of category theory. $\endgroup$– beroalOct 25 '10 at 19:08
Add a comment
|
$\begingroup$
$\endgroup$
To add on top of finrod's answer: while the existence of an initial object guarantees the uniqueness of the aforesaid morphism, the initial object's existence is not guaranteed.
As you asked this question under the functional programming tag, perhaps you meant to ask how to establish the existence of initial algebras for a given algebraic type in a functional programming language.
The existence of an initial object is not entirely trivial, but if you know some domain theory then the proof is very similar to the least fixed point theorem for continuous functions over directed CPOs.
The canonical reference eludes me right now, but brief Googling/Wikipedia dig up Abramsky's and Jung's chapter on Domain Theory (section 5, this case is the example in 5.1.3) in the Handbook of Logic in CS.
$\begingroup$
$\endgroup$
1
As far as I remember (and my copy of Pierce's Basic Category Theory for Computer Scientists confirms this), the initial object is defined as an object with exactly one arrow to each object in the category.
-
$\begingroup$ Exactly. If there isn't exactly one morphism from the initial object to all objects, then it isn't initial :) $\endgroup$ Oct 20 '10 at 8:24