Definition:Product Functor
Jump to navigation
Jump to search
Definition
Let $\mathbf C$ be a metacategory with binary products.
Let $\mathbf C \times \mathbf C$ be the product category of $\mathbf C$ with itself.
The product functor on $\mathbf C$ is the functor $\times: \mathbf C \times \mathbf C \to \mathbf C$ defined by:
Object functor: | \(\ds \map \times {C, D} := C \times D \) | ||||||||
Morphism functor: | \(\ds \map \times {f, f'} := f \times f' \) |
where $C \times D$ is a binary product of $C$ and $D$, and $f \times f'$ is the product of $f$ and $f'$.
That it is in fact a functor is shown on Product Functor is Functor.
Sources
- 2010: Steve Awodey: Category Theory (2nd ed.) ... (previous) ... (next): $\S 2.6$