๐Ÿ“Category Theory: Product

tags
ยง Category Theory
\begin{tikzcd} & X \arrow[ld, "f_1", swap] \arrow[d, "f", dashed] \arrow[rd, "f_2"] & \\ A & P \arrow[l, "\pi_1"] \arrow[r, "\pi_2", swap] & B \end{tikzcd}

Universal construction:

P,ฯ€1,ฯ€2P, \pi_1, \pi_2 is the (categorical) product of AA and BB if ฯ€1:Pโ†’A\pi_1 : P \to A and ฯ€2:Pโ†’B\pi_2 : P \to B and โˆ€(X,f1:Xโ†’A,f2:Xโ†’B)โ€…โ€Šโˆƒ!f:Xโ†’Pโˆ‹ฯ€1โˆ˜f=f1,ฯ€2โˆ˜f=f2\forall(X, f_1 : X \to A, f_2 : X \to B)\; \exists! f : X \to P \ni \pi_1 \circ f = f_1, \pi_2 \circ f = f_2

Also:

  • PP is usually called Aร—BA\times B or in types: (A,B)(A,B)
  • ฯ€1\pi_1 and ฯ€2\pi_2 are called projections.

Terminal object is a unit value of categorical product (aร—()โ‰…aa\times() \cong a) (forming a Monoid and Cartesian monoidal category).

Backlinks