Identity Functor is Functor
Jump to navigation
Jump to search
Theorem
Let $\mathbf C$ be a metacategory.
Let $\operatorname{id}_{\mathbf C}: \mathbf C \to \mathbf C$ be the identity functor on $\mathbf C$.
Then $\operatorname{id}_{\mathbf C}$ is a functor.
Proof
Let $f, g$ be morphisms of $\mathbf C$ such that $g \circ f$ is defined.
Then:
\(\ds \operatorname{id}_{\mathbf C} \left({g \circ f}\right)\) | \(=\) | \(\ds g \circ f\) | Definition of Identity Functor | |||||||||||
\(\ds \) | \(=\) | \(\ds \operatorname{id}_{\mathbf C} g \circ \operatorname{id}_{\mathbf C} f\) | Definition of Identity Functor |
Also, for any object $C$ of $\mathbf C$:
\(\ds \operatorname{id}_{\mathbf C} \operatorname{id}_C\) | \(=\) | \(\ds \operatorname{id}_C\) | Definition of Identity Functor | |||||||||||
\(\ds \) | \(=\) | \(\ds \operatorname{id}_{\operatorname{id}_{\mathbf C} C}\) | Definition of Identity Functor |
Hence $\operatorname{id}_{\mathbf C}$ is shown to be a functor.
$\blacksquare$