CatDat

binary products

A category has binary products if every pair A,BA,B of objects has a product A×BA \times B.

Relevant implications

  • finite products is equivalent to   terminal object and  binary products
    The non-trivial direction follows since finite products can be constructed recursively via X1××Xn+1=(X1××Xn)×Xn+1X_1 \times \cdots \times X_{n+1} = (X_1 \times \cdots \times X_n) \times X_{n+1}.
  • binary products and  equalizers implies   pullbacks
    The pullback of f:XSf : X \to S and g:YSg : Y \to S is the equalizer of p1f,p2g:X×YSp_1 \circ f, \, p_2 \circ g : X \times Y \rightrightarrows S.
  • binary products and  pullbacks implies   equalizers
    The equalizer of f,g:XYf,g : X \rightrightarrows Y is the pullback of (f,g):XY×Y(f,g) : X \to Y \times Y with the diagonal YY×YY \to Y \times Y.
  • pullbacks and  terminal object implies   binary products
    If 11 is a terminal object, then X×1Y=X×YX \times_1 Y = X \times Y.
  • binary products and  inhabited implies   connected
    For any two objects A,BA,B we have the zig-zag AA×BBA \to A \times B \to B.
  • groupoid and  binary products and  inhabited implies   trivial
    Let C\mathcal{C} be an inhabited groupoid with binary products. Then it is connected, so we may assume C=BG\mathcal{C}=BG for a group GG with unique object *. But then ×=* \times * = *, so there are p,qGp,q \in G such that GG×GG \to G \times G, x(px,qx)x \mapsto (px,qx) is bijective. From here it is an easy exercise to deduce G=1G=1.
  • self-dual and  binary products implies   binary coproducts
    trivial by self-duality
  • self-dual and  binary coproducts implies   binary products
    trivial by self-duality

Examples

Counterexamples

Unknown

For these categories the database has no info if they satisfy this property or not.