Skip to main content
added 47 characters in body
Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

Let us first consider a slightly simpler situation. The cartesian product of sets $A$ and $B$ is a set $C$ with two maps $p_1 : C \to A$ and $p_2 : C \to B$ such that ... (familiar condition inserted here). All cartesian products of $A$ and $B$ are canonically isomorphic, and among them there is a particular one, denoted $A \times B$, which is specifically defined as $A \times B = \lbrace\lbrace\lbrace x,y \rbrace, \lbrace y\rbrace\rbrace \mid x \in A \land y \in B\rbrace$.

This is a familiar situation. Often a construction is determined up to canonical isomorphism, but we have a specific one that we can use as an operation, like $(A,B) \mapsto A \times B$ above.

Awodey does the same thing in his book. "Being a pullback" is a property, but we can turn it into structure, i.e., an operation which takes a pair of arrows $f : A \to C$ and $g : B \to C$ and gives a pullback square. You may wonder whether there always is such an operation. If you believe in the axiom of choice then the answer is positive, because we may always choose particular pullbacks among the canonically isomorphic ones. In concrete examples you will usually find chosen pullbacks easily, so this is not problematic.

But thereThere is a small catch. Awodey saysWhile for $h : A \to B$ it is the case that pullbacks form$h^{*}$ is a functor. For this from $\mathcal{C}/B$ to be$\mathcal{C}/A$, the caseassignment $h \mapsto h^\ast$ tends to be a certain coherence condition has"functor up to hold, and itisomorphism" only. This is so because composition of chosen pullbacks need not obvious that we can always choose thebe a chosen pullback operation so that the condition holds. It(but is a good exercisecanonically isomprhic to work this out by yourselfit).

Let us first consider a slightly simpler situation. The cartesian product of sets $A$ and $B$ is a set $C$ with two maps $p_1 : C \to A$ and $p_2 : C \to B$ such that ... (familiar condition inserted here). All cartesian products of $A$ and $B$ are canonically isomorphic, and among them there is a particular one, denoted $A \times B$, which is specifically defined as $A \times B = \lbrace\lbrace\lbrace x,y \rbrace, \lbrace y\rbrace\rbrace \mid x \in A \land y \in B\rbrace$.

This is a familiar situation. Often a construction is determined up to canonical isomorphism, but we have a specific one that we can use as an operation, like $(A,B) \mapsto A \times B$ above.

Awodey does the same thing in his book. "Being a pullback" is a property, but we can turn it into structure, i.e., an operation which takes a pair of arrows $f : A \to C$ and $g : B \to C$ and gives a pullback square. You may wonder whether there always is such an operation. If you believe in the axiom of choice then the answer is positive, because we may always choose particular pullbacks among the canonically isomorphic ones. In concrete examples you will usually find chosen pullbacks easily, so this is not problematic.

But there is a catch. Awodey says that pullbacks form a functor. For this to be the case a certain coherence condition has to hold, and it is not obvious that we can always choose the pullback operation so that the condition holds. It is a good exercise to work this out by yourself.

Let us first consider a slightly simpler situation. The cartesian product of sets $A$ and $B$ is a set $C$ with two maps $p_1 : C \to A$ and $p_2 : C \to B$ such that ... (familiar condition inserted here). All cartesian products of $A$ and $B$ are canonically isomorphic, and among them there is a particular one, denoted $A \times B$, which is specifically defined as $A \times B = \lbrace\lbrace\lbrace x,y \rbrace, \lbrace y\rbrace\rbrace \mid x \in A \land y \in B\rbrace$.

This is a familiar situation. Often a construction is determined up to canonical isomorphism, but we have a specific one that we can use as an operation, like $(A,B) \mapsto A \times B$ above.

Awodey does the same thing in his book. "Being a pullback" is a property, but we can turn it into structure, i.e., an operation which takes a pair of arrows $f : A \to C$ and $g : B \to C$ and gives a pullback square. You may wonder whether there always is such an operation. If you believe in the axiom of choice then the answer is positive, because we may always choose particular pullbacks among the canonically isomorphic ones. In concrete examples you will usually find chosen pullbacks easily, so this is not problematic.

There is a small catch. While for $h : A \to B$ it is the case that $h^{*}$ is a functor from $\mathcal{C}/B$ to $\mathcal{C}/A$, the assignment $h \mapsto h^\ast$ tends to be a "functor up to isomorphism" only. This is so because composition of chosen pullbacks need not be a chosen pullback (but is canonically isomprhic to it).

Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

Let us first consider a slightly simpler situation. The cartesian product of sets $A$ and $B$ is a set $C$ with two maps $p_1 : C \to A$ and $p_2 : C \to B$ such that ... (familiar condition inserted here). All cartesian products of $A$ and $B$ are canonically isomorphic, and among them there is a particular one, denoted $A \times B$, which is specifically defined as $A \times B = \lbrace\lbrace\lbrace x,y \rbrace, \lbrace y\rbrace\rbrace \mid x \in A \land y \in B\rbrace$.

This is a familiar situation. Often a construction is determined up to canonical isomorphism, but we have a specific one that we can use as an operation, like $(A,B) \mapsto A \times B$ above.

Awodey does the same thing in his book. "Being a pullback" is a property, but we can turn it into structure, i.e., an operation which takes a pair of arrows $f : A \to C$ and $g : B \to C$ and gives a pullback square. You may wonder whether there always is such an operation. If you believe in the axiom of choice then the answer is positive, because we may always choose particular pullbacks among the canonically isomorphic ones. In concrete examples you will usually find chosen pullbacks easily, so this is not problematic.

But there is a catch. Awodey says that pullbacks form a functor. For this to be the case a certain coherence condition has to hold, and it is not obvious that we can always choose the pullback operation so that the condition holds. It is a good exercise to work this out by yourself.