Does the functor law about preserving identity follow from other laws? I've only recently picked up literature about category theory, but the definition of a functor on Wikipedia seems redundant to me. I've paraphrased it here:

Given categories $C$ and $D$, then a mapping $F : C \rightarrow D$ is a functor iff:
  
  
*
  
*$F$ assigns to every object $X \in C$ an object $F(X) \in D$, (left-total for objects)
  
*$F$ assigns to every arrow $f : X \rightarrow Y \in C$ an arrow $F(f) : F(X) \rightarrow F(Y) \in D$, (left-total for arrows)
  
*For all arrows $f : X \rightarrow Y$ and $g : Y \rightarrow Z$ in $C$, $F(g \circ f) = F(g) \circ F(f)$, (homomorphism) and
  
*For every identity arrow $1_X : X \rightarrow X$ in $C$, $F(1_X) = 1_{F(X)}$. (preservation of identity)
  

From what I understand, it can be proven that every identity arrow in a category is unique. Combined with this theorem, I think the following proof is correct:


*

*Reflexivity of equality: $\forall f\in C: f = f$

*Left-totality for arrows: $\forall f\in C: F(f) = F(f)$

*Introduce left-identity: $\forall f\in C: F(1_Y \circ f) = F(f)$ (given $f:X \rightarrow Y$)

*Homomorphism: $\forall f\in C: F(1_Y) \circ F(f) = F(f)$ (given $f:X \rightarrow Y$)

*Because of uniqueness of identity, $F(1_Y)$ must be the identity arrow for $F(Y)$, so it follows that $F(1_Y) = 1_{F(Y)}$.


Am I missing something here? Does preservation of identity follow from other laws?
 A: The problem with your argument is that you confuse $F(1_Y) \circ F(f) = F(f)$ for all $f$ with $F(1_Y) \circ g = g$ for all $g$.
For example, pick any object with an idempotent endomorphism $e$ on it, and map every morphism to $e$. Then $F(f) \circ F(g) = F(h)$ for all $f,g,h$, but $e$ need not be the identity.
Your argument does show that if the identity is in the image of your functor, say $1_{FY} = Fh$, then: $F(1_Y) = F(1_Y) \circ 1_{FY} = F(1_Y) \circ Fh = F(1_Y \circ h) = Fh = 1_{FY}$. Note that this proof requires $1_Y \circ h$ to make sense, so $h$ must have codomain $Y$: it's easy to see how you could modify the proof so it would still work if $h$ had domain $Y$ instead.
Stefan H, in the comments, provides an example to show that this condition is necessary: consider the functor $F$ from the category $\mathcal C$ with two objects $X$ and $Y$ (and only their identities as morphisms) to the category $\mathcal D$ with one object $Z$ and two morphisms, the identity $1_Z$ and some $f : Z \to Z$ with $f \circ f = f$. Then the mapping sending $1_X$ to $1_Z$ and $1_Y$ to $f$ is not a functor, because $f$ is not an identity, but is surjective on morphisms.
The problem here is subtle: though we can always say $F(g \circ h) = Fg \circ Fh$, it's not always correct to start from $Fg \circ Fh$ and say it must be equal to $F(g \circ h)$, because the latter might not typecheck!
Issues like this are why (for example) the definition of a full functor picks the objects in the source category first, and then says the functor action is surjective restricted to those, rather than just saying "every morphism is in the image". And indeed, this additional care means that a morphism mapping being full (and preserving composition) really does ensure it preserves identities. Note that in Stefan's counterexample, the functor mapping $\mathcal C(X,X) \to \mathcal D(FX,FX)$ is not surjective, since no morphism from $X$ to itself maps to $f$, so $F$ is not full, even though it is surjective.
A: Yes, the last step in your proof is incorrect. You can conclude that an arrow $e:X\rightarrow X$ is the identity on $X$ if for all arrows $f:X\rightarrow Y$ and all arrows $g:Z\rightarrow X$, $f\circ e = f$ and $e\circ g = g$.
You have shown that for all arrows of the form $F(f)$ we have $F(1_Y) \circ F(f) = F(f)$. This is not enough to conclude that $F(1_Y)$ is the identity.
Here is a counterexample: Let $C$ be a category with just one object, $X$, and just one arrow, $1_X$. 
Let $D$ be a category with just one object, $Y$, and two arrows: $\text{Hom}(Y,Y) = \{1_Y,f\}$, with composition defined so that $f\circ f = f$.
Now let $F$ be the "functor" (in quotes because it is not really a functor) sending $X$ to $Y$ and $1_X$ to $f$. $F$ preserves composition ($F(1_X\circ 1_X) = F(1_X) = f = f\circ f = F(1_X) \circ F(1_X)$), but it does not preserve identities.
A: You've shown that $F(1_Y) \circ F(f) = F(f)$ for each $\mathcal{C}$-arrow $f : X \to Y$. However, in order to show that $F(1_Y)=1_{FY}$ you need to show that $F(1_Y) \circ g = g$ for each $\mathcal{D}$-arrow $g:Z \to FY$. These two notions won't necessarily be the case unless every $\mathcal{D}$-arrow into $FY$ is of the form $F(f)$ for some $\mathcal{C}$-arrow $f$.
For instance, consider the categories $\mathcal{C}$ and $\mathcal{D}$, which both have just one object, the set $X=\{ 0,1 \}$, and


*

*$\mathcal{C}$ has only the identity function $1_X$ as an arrow

*$\mathcal{D}$ has as arrows the identity function $1_X$ and the constant function $f$ with value zero


Let $F : \mathcal{C} \to \mathcal{D}$ take $1_X$ to $f$. You'll see that all the axioms are satisfied except the requirement that $F(1_X)=1_{FX}=1_X$.
