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 #m/thm/cat

c|https://q.uiver.app/#q=WzAsNSxbNCw0LCJDIl0sWzIsNCwiQSJdLFs0LDIsIkIiXSxbMiwyLCJBIFxcdGltZXMgQiJdLFswLDAsIkUiXSxbMiwwLCJnIl0sWzEsMCwiZiIsMl0sWzQsMywiXFxtYXRocm17ZXF9Il0sWzQsMSwicF8xIiwyLHsiY3VydmUiOjF9XSxbNCwyLCJwXzIiLDAseyJjdXJ2ZSI6LTF9XSxbMywyLCJcXHBpXzIiXSxbMywxLCJcXHBpXzEiLDJdXQ==

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

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 .

Dually, the fibre coproduct is the coëqualizer of a coproduct.

#state/tidy | #lang/en | #SemBr

Footnotes

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