colimits commute with colimits

1. Proposition

2. Proof

2.2. hands on

Suppose there exist a diagram

20231125-colimits_commute_with_colimits_9bc70cbb36ae6e5f287e28ea8a501b0becbe2e71.svg

Then for 20231125-colimits_commute_with_colimits_8919a9b063343116b7454f4c4f8e87262c97c893.svg and 20231125-colimits_commute_with_colimits_b95ee67f1c1c2ebd7beabf496719d948c86cb162.svg we get objects 20231125-colimits_commute_with_colimits_309203fb27242279745fc7ba0a92218d2f79ed01.svg with possible arrows

20231125-colimits_commute_with_colimits_ccf349aec1e7f200a1c8e50a30ea23d5ab28ffcf.svg

Then consider

20231125-colimits_commute_with_colimits_53274b34f51a9b2ffd1d0ca4c32f06e709dff403.svg

and

20231125-colimits_commute_with_colimits_1435d6d96f0260ab2593757fe979dc2d741b1946.svg

Suppose there exists an object 20231125-colimits_commute_with_colimits_73eed9b29d43fbfeded6554d9fef135ba7ec0f7b.svg and morphisms 20231125-colimits_commute_with_colimits_224d198a9d1ee929ceb57023ee4604378cd9aad9.svg

20231125-colimits_commute_with_colimits_ceddc8ab65fb3ab56285b48766c5961ac182b075.svg

Then as a morphism out of a colimit corresponds to morphisms out of the diagram (by precomposition with the 20231125-colimits_commute_with_colimits_6a4813ced87bc153459c197bb383e1f2897f3d1e.svg's), we get morphisms

20231125-colimits_commute_with_colimits_eb98639b8d8bc801a9efdd703c9e949e1d97c39a.svg

Then note, there exists a unique morphism

20231125-colimits_commute_with_colimits_f61e71beeb1a42410fd090817f31f0f962d2da32.svg

and furthermore

20231125-colimits_commute_with_colimits_37649de65909553ba04030cc246d643c7f17e2af.svg

Thus it remains to show, that 20231125-colimits_commute_with_colimits_6a4813ced87bc153459c197bb383e1f2897f3d1e.svg with 20231125-colimits_commute_with_colimits_3f5793eaa5cfd0f6b4bdfceb6ca9d38b38b4bfe8.svg makes the diagram commute, hence by uniqueness

todo:

  • construct morphisms to colimit
  • show that those commute
  • show that 20231125-colimits_commute_with_colimits_6a4813ced87bc153459c197bb383e1f2897f3d1e.svg commutes

Date: nil

Author: Anton Zakrewski

Created: 2024-10-13 So 19:27