Product

Before introducing the product

Product in CT is somewhat related to products from arithmetic. So, in arithmetic, e.g. 6 = 2 3, means that 2 and 3 are factors of 6, either 2 or 3 factorizes 6. Similarly, in 6 = x 3 and with x restricted to ℕ domain, there may be a nat that factorizes 6, or there may not be. If it exists, then it must satisfy the given equation.

If we know that a category C has a product object, P, then we know there will be two crucial arrows, both emerging from the product object but each going to some other, distinct, object, f: P -> A and g: P -> B in the category.

So, in the entire category, which may have a gazillion objects and arrows, we are looking for a pattern involving 3 objects and 2 arrows; such that two arrows emerge from the same object, P, and then one arrow goes to an object A and the other arrows goes to an object B (and all 3 objects are distinct).

         P'
         o
        /↑\
       / | \
      /  |  \
   f'/   |   \g'
    /    |    \
   /     |     \
  /      |      \
 ↙   f   |   g   ↘
o <----- o -----> o
A        P        B

Products

The concepts of product corresponds to Cartesian products.

(Definition) A product of objects a and b in a category 𝒞 consists of a product object a × b, and projection morphisms π₁ ∶ a × b → a and π₂ ∶ a × b → b, such that, for all objects c, and morphisms f ∶ c → a and g ∶ c → b, there is a unique morphism ⟨f, g⟩ ∶ c → a × b such that π₁ ∘ ⟨f, g⟩ = f and π₂ ∘ ⟨f, g⟩ = g.

In Hask, tuples are products and the two projection functions are fst and snd:

data (,) a b = (,) a b

fst :: (a,b) -> a
fst (a,b) = a

snd :: (a,b) -> b
snd (a,b) = b

fork :: (c -> a) -> (c -> b) -> c -> (a, b)
fork f g z = (f z, g z)

The fork function is required to show that tuples are indeed products.

In Set, the product of two sets 𝐴 and 𝐵 consists of the Cartesian product 𝐴 × 𝐵 = {(𝑥, 𝑦) ∣ 𝑥 ∈ 𝐴 and 𝑦 ∈ 𝐵} and two projection functions π₁ ∶ 𝐴 × 𝐵 → 𝐴 and π₂ ∶ 𝐴 × 𝐵 → 𝐵 such that, for all (𝑥, 𝑦) ∈ 𝐴 × 𝐵, π₁(𝑥, 𝑦) = 𝑥 and π₂(𝑥, 𝑦) = 𝑦.

Given a set 𝐶, and two functions 𝑓 ∶ 𝐶 → 𝐴 and 𝑔 ∶ 𝐶 → 𝐵, there is a unique function ⟨𝑓, 𝑔⟩ ∶ 𝐶 → 𝐴 × 𝐵 defined by ⟨𝑓, 𝑔⟩(𝑧) = (𝑓(𝑧), 𝑔(𝑧)) for all 𝑧 ∈ 𝐶.