Skip to main content
MathOverflow

Return to Answer

added 29 characters in body
Source Link
Martin Brandenburg
Martin Brandenburg
  • 63.1k
  • 12
  • 207
  • 424

As was mentioned in the comments, such general isomorphisms can be reduced by Yoneda to the case of sets, and in your example $((a,c),d) \mapsto (a,d)$ is an isomorphism, simply because $c$ is already determined by $d$. As for me, I always manipulate arrows without caring about single-use names and use Yoneda. This worked very good in the past years. For example, for every test object $T \in C$, we have canonical bijections

$\{T \to (A \times_B C) \times_C D\} = \{T \to A \times_B C \to C = T \to D \to C\}$ $= \{T \to A \to B = T \to C \to B, T \to C = T \to D \to C\}$ $=\{T \to A \to B = T \to D \to C \to B\} = \{T \to A \times_B D\}$

You may argue that it's not clear at all what is given etc., but there is only one plausible interpretation: Everything not given before belongs to the data of the morphism sets. Every equation is a condition on this data. It's even nicer to draw everything in commutative diagrams (I don't know how to draw them here). This method also works when you want to simplify a universal object without knowing the result. You just reduce the diagrams as above. Every step is almost forced. Of course, this is just another way of writing down the proof mentioned first.

Regarding your second question: Your intuition is absolutely correct. A sufficient and useful condition is that $f$ is a final functor. You can read about them in Mac Lane, Categories for the working mathematician, IX.3.

As was mentioned in the comments, such general isomorphisms can be reduced by Yoneda to the case of sets, and in your example $((a,c),d) \mapsto (a,d)$ is an isomorphism, simply because $c$ is already determined by $d$. As for me, I always manipulate arrows without caring about single-use names and use Yoneda. This worked very good in the past years. For example, for every test object $T \in C$, we have canonical bijections

$\{T \to (A \times_B C) \times_C D\} = \{T \to A \times_B C \to C = T \to D \to C\}$ $= \{T \to A \to B = T \to C \to B, T \to C = T \to D \to C\}$ $=\{T \to A \to B = T \to D \to C \to B\} = \{T \to A \times_B D\}$

You may argue that it's not clear at all what is given etc., but there is only one plausible interpretation: Everything not given before belongs to the data of the morphism sets. Every equation is a condition on this data. It's even nicer to draw everything in commutative diagrams (I don't know how to draw them here). This method also works when you want to simplify a universal object without knowing the result. You just reduce the diagrams as above. Of course, this is just another way of writing down the proof mentioned first.

Regarding your second question: Your intuition is absolutely correct. A sufficient and useful condition is that $f$ is a final functor. You can read about them in Mac Lane, Categories for the working mathematician, IX.3.

As was mentioned in the comments, such general isomorphisms can be reduced by Yoneda to the case of sets, and in your example $((a,c),d) \mapsto (a,d)$ is an isomorphism, simply because $c$ is already determined by $d$. As for me, I always manipulate arrows without caring about single-use names and use Yoneda. This worked very good in the past years. For example, for every test object $T \in C$, we have canonical bijections

$\{T \to (A \times_B C) \times_C D\} = \{T \to A \times_B C \to C = T \to D \to C\}$ $= \{T \to A \to B = T \to C \to B, T \to C = T \to D \to C\}$ $=\{T \to A \to B = T \to D \to C \to B\} = \{T \to A \times_B D\}$

You may argue that it's not clear at all what is given etc., but there is only one plausible interpretation: Everything not given before belongs to the data of the morphism sets. Every equation is a condition on this data. It's even nicer to draw everything in commutative diagrams (I don't know how to draw them here). This method also works when you want to simplify a universal object without knowing the result. You just reduce the diagrams as above. Every step is almost forced. Of course, this is just another way of writing down the proof mentioned first.

Regarding your second question: Your intuition is absolutely correct. A sufficient and useful condition is that $f$ is a final functor. You can read about them in Mac Lane, Categories for the working mathematician, IX.3.

Source Link
Martin Brandenburg
Martin Brandenburg
  • 63.1k
  • 12
  • 207
  • 424

As was mentioned in the comments, such general isomorphisms can be reduced by Yoneda to the case of sets, and in your example $((a,c),d) \mapsto (a,d)$ is an isomorphism, simply because $c$ is already determined by $d$. As for me, I always manipulate arrows without caring about single-use names and use Yoneda. This worked very good in the past years. For example, for every test object $T \in C$, we have canonical bijections

$\{T \to (A \times_B C) \times_C D\} = \{T \to A \times_B C \to C = T \to D \to C\}$ $= \{T \to A \to B = T \to C \to B, T \to C = T \to D \to C\}$ $=\{T \to A \to B = T \to D \to C \to B\} = \{T \to A \times_B D\}$

You may argue that it's not clear at all what is given etc., but there is only one plausible interpretation: Everything not given before belongs to the data of the morphism sets. Every equation is a condition on this data. It's even nicer to draw everything in commutative diagrams (I don't know how to draw them here). This method also works when you want to simplify a universal object without knowing the result. You just reduce the diagrams as above. Of course, this is just another way of writing down the proof mentioned first.

Regarding your second question: Your intuition is absolutely correct. A sufficient and useful condition is that $f$ is a final functor. You can read about them in Mac Lane, Categories for the working mathematician, IX.3.