まずは集合の積を考える。集合 A と B があるとき、A と B のデカルト積は順序対 (ordered pairs) の集合となる
A × B = {(a, b)| a ∈ A, b ∈ B}

2つの座標射影 (coordinate projection) があって:
coordinate projections

これは以下の条件を満たす:

この積という考えは case class やタプルの基底 trait である scala.Product にも関連する。

任意の要素 c ∈ A × B に対して、c = (fst ∘ c, snd ∘ c) ということができる。

15日目に出てきたが、明示的に単集合 1 を導入することで要素という概念を一般化できる。

product of sets

これをすこしきれいに直すと、積の圏論的な定義を得ることができる:

定義 2.15. 任意の圏 C において、対象 A と B の積の図式は対象 P と射 p1 と p2 から構成され
product diagram
以下の UMP を満たす:

この形となる任意の図式があるとき
product definition
次の図式
product of objects
が可換となる (つまり、x1 = p1 u かつ x2 = p2 u が成立する) 一意の射 u: X => P が存在する。

「一意の射」と出てきたら UMP だなと見当がつく。

積の一意性 

Sets に立ち返ると、型A と型B があるとき、(A, B) を返す一意の関数があると言っているだけだ。しかし、これが全ての圏に当てはまるかどう証明すればいいだろう? 使って良いのはアルファベットと矢印だけだ。

命題 2.17 積は同型を除いて一意である。

PQ が対象 AB の積であるとする。

uniqueness of products

  1. P は積であるため、p1 = q1 ∘ i かつ p2 = q2 ∘ i を満たす一意の i: P => Q が存在する。
  2. Q は積であるため、q1 = p1 ∘ j かつ q2 = p2 ∘ j を満たす一意の j: Q => P が存在する。
  3. ij を合成することで 1P = j ∘ i が得られる。
  4. 同様にして 1Q = i ∘ j
  5. i は同型射、P ≅ Q である。∎

全ての積は同型であるため、一つを取って A × B と表記する。また、射 u: X => A × B⟨x1, x2 と表記する。

Contents

猫番