Picture speaks a thousand words:
C | c -a→ d
Set | P(c) -P(a)→ P(d)
Set | u ∈ P(c) -P(a)→ d ∋ P(a)(u)
el P | (c∈C, u∈P(c))
el P | (c∈C, u∈P(c)) -el a→ (d∈C, P(a)(u)∈P(d))
- So, this category gives us a way to "locate ourselves" within the set , which will be instrumental in creating the arrows (natural transformations) of the form , as asked of us by the cocone.
- This also hints at why we use colimis and not limits: because the yoneda goes from the to , we can only conjure arrows into via Yoneda, thereby forcing us to use a colimit.
- We claim that we should choose the diagram category as , with the diagram functor given by .
- This embeds where is a way to locate 's view of as a Hom-set .
- To give the natural transformation from the image of the diagram to the apex of the cocone , we use Yoneda: We need an arrow , which we know is in bijection with elements of through yoneda.
- Luckily, we have to invoke yoneda, so we build the arrows from to , given by applying Yoneda to .
- Thus, we can at least form a cocone. Whether the arrows of the "base" of the cocone commute with the apex-pointing arrows, and whether this is universal is to be checked next.
- Given some other cocone , with co-cone morphisms , we need to create a natural transformation . Let's do this pointwise.
- For some , we need to build a map . Since the domain and codomain are pointwise, let's pick some element .
- See that this can be seen as an element which is an element of the category .
- But, recall that this was our index category . Thus, there is going to be an arrow since is a cocone.
- But since , it's an element of . We have thus found a way to map into by "pulling back" into the index category and then "pushing forward" via Yoneda. [What the fuck is actually happening here? ]
§ Simplified construction of
- Recall that consisted of a pair . We know from Yoneda that set elements of are in bijection with natural transformations .
- Thus consists of all natural transformations [for all objects ].
- The arrows in between and are pushforwards of arrow (given by ) which make the diagram commute:
Hom(-, x) >------->P
| \h -> f.h / μ
- Consider the functor which sends each natural transformation to just (ie, forget the mapping, just keep the domain of the natural transformation.
- We claim that is the cocone of the functor . So we must have mappings from each into .
- These mappings from into are given by "un-forgetting" the data we forgot when mapping . These commute by the construction of .
- (Are these the only choices of maps? Maybe there are others, not just the ones we "un-forgot"!)
- Next we need to check that is universal. Consider some other . We must show a map (ie, the cocone factorizes through , or is initial cocone.).
- Let's do this pointwise. So we want to define a family .
- Pick some element . This corresponds to some natural transformation . We know that we have a corresponding . this is some element . So we are forced to set when we try to map to .
- This works for arbitrary , so the entire map is determined. This proves that is terminal cocone.