categorical product in Set

1. Proposition

Given the category set, 20231019-product_in_set_fa6f14d2189f93bebf4e94e9fcb80910dda0fde4.svg and sets 20231019-product_in_set_d1182d4a3ba380b69400d5d8977bc0b4de8dc8c5.svg for an indexing set 20231019-product_in_set_4b65189679eaf678e24e75492af582c55d269155.svg , the categorical product with the canonical projection is the Cartesian product 20231019-product_in_set_fa53d77dc26dc0eb446278f8087f4b57e8857c8c.svg

2. Proof

2.1. construction of a map

Let 20231019-product_in_set_9c8bdb9f6ad11c13881249483fa93b024273b477.svg be a set and

20231019-product_in_set_dc3f987531fa0c7a95d2f8eaea869135d9c6eb88.svg

be maps

Then let

20231019-product_in_set_d0ee267c569db02afc94d8b1678f5f585ef89dde.svg

Then by construction

20231019-product_in_set_a8ccd4a07008a27256e2cda2969f990ec95f2c59.svg

commutes

2.2. uniqueness

Let 20231019-product_in_set_5f965d0a56374955f8a17da7129fa95cde5a6603.svg be a map making the diagram

20231019-product_in_set_a2748def3aafeaa755806a746f070aa012b11175.svg

commute

Then for 20231019-product_in_set_83af3dec20aa987a651b514cef58029da7f94cda.svg it follows, that for the 20231019-product_in_set_6cf2f08af66400fd36f0183308ae35968f9ae29f.svg -th component

20231019-product_in_set_3e6d637285711673e4b0d30d898d3b42ae7c658d.svg

hence by construction of 20231019-product_in_set_c3c0fa799b269f511421ec5811c7c3ca70b26569.svg it follows, that

20231019-product_in_set_44ccf833eeb1e03051f1075ab932e7b6e31d13f0.svg

Thus

20231019-product_in_set_2591a301b16ef2a20ffb6f3129ed74fb91072e70.svg