Return to Question

I am reading "Category Theory" (2nd ed.) of Awodey, and I'm stuck at page 96 (proposition 5.12) when pullbacks are presented as functors:

The pullback under question corresponds to this square:

$$\begin{matrix} C' \times_C A & \xrightarrow{h'} & A \\[1ex] \downarrow \rlap{\scriptstyle{\alpha'}} & & \downarrow\rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

Here is the statement of Awodey's book that I do not understand:

Pullback is a functor. That is, for fixed $C' \rightarrow_h C$ in a category $\mathbf{C}$ with pullbacks, there is a functor

$h^* : \mathbf{C}/C \rightarrow \mathbf{C}/C'$

defined by

$(A\rightarrow_\alpha C) \mapsto (C'\times_C A \rightarrow_{\alpha'} C')$

where $\alpha'$ is the pullback of $\alpha$ along h

The problem that I see is that, given initially:

$$\begin{matrix} & & A \\[1ex] & & \downarrow \rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

there can be several pullbacks on it, for example, in addition to $(\alpha',h')$, there could be $(\alpha_2',h_2')$, and the unique condition is that there exists an isomorphism i such that $\alpha_2' = \alpha\circ i$ and $h_2' = h'\circ i$. Worse, given a pullback $(\alpha',h')$, one can build as many as pullbacks as there exist isomorphisms, as given any isomorphism j (with domain $C' \times_C A \rightarrow_{h'}$) the two arrows $(\alpha'\circ j,h' \circ j)$ form a new pullback.

So, how could we build a functor if the image arrow is only defined up to an arbitrary isomorphism?

I am reading "Category Theory" (2nd ed.) of Awodey, and I'm stuck at page 96 (proposition 5.12) when pullbacks are presented as functors:

The pullback under question corresponds to this square:

$$\begin{matrix} C' \times_C A & \xrightarrow{h'} & A \\[1ex] \downarrow \rlap{\scriptstyle{\alpha'}} & & \downarrow\rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

Here is the statement of Awodey's book that I do not understand:

Pullback is a functor. That is, for fixed $C' \rightarrow_h C$ in a category $\mathbf{C}$ with pullbacks, there is a functor

$h^* : \mathbf{C}/C \rightarrow \mathbf{C}/C'$

defined by

$(A\rightarrow_\alpha C) \mapsto (C'\times_C A \rightarrow_{\alpha'} C')$

where $\alpha'$ is the pullback of $\alpha$ along h

The problem that I see is that, given initially:

$$\begin{matrix} & & A \\[1ex] & & \downarrow \rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

there can be several pullbacks on it, for example, in addition to $(\alpha',h')$, there could be $(\alpha_2',h_2')$, and the unique condition is that there exists an isomorphism $i$ such that $\alpha_2' = \alpha\circ i$ and $h_2' = h'\circ i$. Worse, given a pullback $(\alpha',h')$, one can build as many as pullbacks as there exist isomorphisms, as given any isomorphism $j$ (with domain $C' \times_C A \rightarrow_{h'}$) the two arrows $(\alpha'\circ j,h' \circ j)$ form a new pullback.

So, how could we build a functor if the image arrow is only defined up to an arbitrary isomorphism?

I am reading "Category Theory" (2nd ed.) of Awodey, and I'm stuck at page 96 (proposition 5.12) when pullbacks are presented as functors:

The pullback under question corresponds to this square:

$$\begin{matrix} C' \times_C A & \xrightarrow{h'} & A \\[1ex] \downarrow \rlap{\scriptstyle{\alpha'}} & & \downarrow\rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

Here is the statement of Awodey's book that I do not understand:

Pullback is a functor. That is, for fixed $C' \rightarrow_h C$ in a category $\mathbf{C}$ with pullbacks, there is a functor

$h^* : \mathbf{C}/C \rightarrow \mathbf{C}/C'$

defined by

$(A\rightarrow_\alpha C) \mapsto (C'\times_C A \rightarrow_{\alpha'} C')$

where $\alpha'$ is the pullback of $\alpha$ along h

The problem that I see is that, given initially:

$$\begin{matrix} & & A \\[1ex] & & \downarrow \rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

there can be several pullbacks on it, for example, in addition to $(\alpha',h')$, there could be $(\alpha_2',h_2')$, and the unique condition is that there exist an isomorphism i such that $\alpha_2' = \alpha\circ i$ and $h_2' = h'\circ i$. Worse, given a pullback $(\alpha',h')$, one can build as many as pullbacks as there exist isomorphisms, as given any isomorphism j (with domain $C' \times_C A \rightarrow_{h'}$) the two arrows $(\alpha'\circ j,h' \circ j)$ form a new pullback.

So, how could we build a functor if the image arrow is only defined up to an arbitrary isomorphism?

I am reading "Category Theory" (2nd ed.) of Awodey, and I'm stuck at page 96 (proposition 5.12) when pullbacks are presented as functors:

The pullback under question corresponds to this square:

$$\begin{matrix} C' \times_C A & \xrightarrow{h'} & A \\[1ex] \downarrow \rlap{\scriptstyle{\alpha'}} & & \downarrow\rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

Here is the statement of Awodey's book that I do not understand:

Pullback is a functor. That is, for fixed $C' \rightarrow_h C$ in a category $\mathbf{C}$ with pullbacks, there is a functor

$h^* : \mathbf{C}/C \rightarrow \mathbf{C}/C'$

defined by

$(A\rightarrow_\alpha C) \mapsto (C'\times_C A \rightarrow_{\alpha'} C')$

where $\alpha'$ is the pullback of $\alpha$ along h

The problem that I see is that, given initially:

$$\begin{matrix} & & A \\[1ex] & & \downarrow \rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

there can be several pullbacks on it, for example, in addition to $(\alpha',h')$, there could be $(\alpha_2',h_2')$, and the unique condition is that there exists an isomorphism i such that $\alpha_2' = \alpha\circ i$ and $h_2' = h'\circ i$. Worse, given a pullback $(\alpha',h')$, one can build as many as pullbacks as there exist isomorphisms, as given any isomorphism j (with domain $C' \times_C A \rightarrow_{h'}$) the two arrows $(\alpha'\circ j,h' \circ j)$ form a new pullback.

So, how could we build a functor if the image arrow is only defined up to an arbitrary isomorphism?

I am reading "Category Theory" (2nd ed.) of Awodey, and I'm stuck at page 96 (proposition 5.12) when pullbacks are presented as functors:

The pullback under question corresponds to this square:

$$\begin{matrix} C' \times_C A & \xrightarrow{h'} & A \\[1ex] \downarrow \rlap{\scriptstyle{\alpha'}} & & \downarrow\rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

Here is the statement of Awodey's book that I do not understand:

Pullback is a functor. That is, for fixed $C' \rightarrow_h C$ in a category $\mathbf{C}$ with pullbacks, there is a functor

$h^* : \mathbf{C}/C \rightarrow \mathbf{C}/C'$

defined by

$(A\rightarrow_\alpha C) \mapsto (C'\times_C A \rightarrow_{\alpha'} C')$

where $\alpha'$ is the pullback of $\alpha$ along h

The problem that I see is that, given initially:

$$\begin{matrix} & & A \\[1ex] & & \downarrow \rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

there can be several pullbacks on it, for example, in addition to $(\alpha',h')$, there could be $(\alpha_2',h_2')$, and the unique condition is that there exist an isomorphism i such that $\alpha_2' = \alpha\circ i$ and $h_2' = h'\circ i$. Worse, given a pullback $(\alpha',h')$, one can build as much as pullbacks as there exist isomorphisms, as given any isomorphism j (with domain $C' \times_C A \rightarrow_{h'}$) the two arrows $(\alpha'\circ j,h' \circ j)$ form a new pullback.

So, how could we build a functor if the image arrow is only defined up to an arbitrary isomorphism?

I am reading "Category Theory" (2nd ed.) of Awodey, and I'm stuck at page 96 (proposition 5.12) when pullbacks are presented as functors:

The pullback under question corresponds to this square:

$$\begin{matrix} C' \times_C A & \xrightarrow{h'} & A \\[1ex] \downarrow \rlap{\scriptstyle{\alpha'}} & & \downarrow\rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

Here is the statement of Awodey's book that I do not understand:

Pullback is a functor. That is, for fixed $C' \rightarrow_h C$ in a category $\mathbf{C}$ with pullbacks, there is a functor

$h^* : \mathbf{C}/C \rightarrow \mathbf{C}/C'$

defined by

$(A\rightarrow_\alpha C) \mapsto (C'\times_C A \rightarrow_{\alpha'} C')$

where $\alpha'$ is the pullback of $\alpha$ along h

The problem that I see is that, given initially:

$$\begin{matrix} & & A \\[1ex] & & \downarrow \rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

there can be several pullbacks on it, for example, in addition to $(\alpha',h')$, there could be $(\alpha_2',h_2')$, and the unique condition is that there exist an isomorphism i such that $\alpha_2' = \alpha\circ i$ and $h_2' = h'\circ i$. Worse, given a pullback $(\alpha',h')$, one can build as many as pullbacks as there exist isomorphisms, as given any isomorphism j (with domain $C' \times_C A \rightarrow_{h'}$) the two arrows $(\alpha'\circ j,h' \circ j)$ form a new pullback.

So, how could we build a functor if the image arrow is only defined up to an arbitrary isomorphism?