colimits commute with colimits
1. Proposition
2. Proof
2.1. adjoint
2.2. hands on
Suppose there exist a diagram
Then for and
we get objects
with possible arrows
Then consider
and
Suppose there exists an object and morphisms
Then as a morphism out of a colimit corresponds to morphisms out of the diagram (by precomposition with the 's), we get morphisms
Then note, there exists a unique morphism
and furthermore
Thus it remains to show, that with
makes the diagram commute, hence by uniqueness
todo:
- construct morphisms to colimit
- show that those commute
- show that
commutes