equalizer in category cat

1. Proposition

Let 20240328-equalizer_in_category_cat_2d5d1c2bfbb1a2fca757f722875cd0787290c048.svg be small categories and

20240328-equalizer_in_category_cat_f46316c39782af3c65b9fcc8988698e7ad017509.svg

be a diagram.

Then the equalizer is given by the category containing

  1. objects 20240328-equalizer_in_category_cat_9453902b5544d418294ac20701cedecedad7f2aa.svg with 20240328-equalizer_in_category_cat_48e1415e40e77f9a4736faf08215508c16bc7b3b.svg
  2. morphisms 20240328-equalizer_in_category_cat_431e1d71fe609c795efa9b3448da6aff6281a3a1.svg with 20240328-equalizer_in_category_cat_c20e3e9504aec853dfa42b943768bc6b730b7939.svg

2. Proof

2.1. welldefined category

Associativity is inherited. Let 20240328-equalizer_in_category_cat_7bb8a0c8f5c8068c73d013d42e1822d623172b1c.svg

2.1.1. identity

Follows from

20240328-equalizer_in_category_cat_3b15b61be7ebd071ccd8bff996d8d232d2b66740.svg

2.1.2. composition

Suppose 20240328-equalizer_in_category_cat_abec79b5568a155d55f91a06a5776b0abbdfc885.svg with compatible domain/codomain. Then we get

20240328-equalizer_in_category_cat_1ac1ef287b1e4370951baf989ea9a4fe0a369c87.svg

2.2. universal property

Suppose there exists a category 20240328-equalizer_in_category_cat_7e27669eaf03480bc8270e46d054b5bee8696749.svg a fork

20240328-equalizer_in_category_cat_300ae860c0499340462bf50f3e2ccbaee0e243e8.svg

Then we define

20240328-equalizer_in_category_cat_fa29a28debd34bda7811c8c89b4dae582639a170.svg

where 20240328-equalizer_in_category_cat_2b375be442e53d71c191d68d88118f9172ffabee.svg is interpreted as subcategory.

This functor is welldefined, as TODO

Date: nil

Author: Anton Zakrewski

Created: 2024-10-15 Di 23:15