Fibre product and coproduct

Fibre product is the equalizer of a product

Suppose products and equalizers exist in and we have a diagram

Then the fibre product exists and is given by in the commutative diagram cat

where is the equalizer of . Conversely, any such fibre product gives as the equalizer of .¹

Proof

Let

such that , so where

Now there exists so that . Thus

Given an alternate with the property , then so , and since the equalizer is monic .

---

tidy | en | sembr

Footnotes

1. 2010. Category theory, ¶5.5, pp. 93–94 ↩