圏論の「積の定義」について考える

 Youtubeの圏論勉強会１回目で対（積）の定義が最初に出てくる。正しいのかどうか、いまいち自信はないが、自分なりに少し考えてみた。

　型A,Bの対とは、型P　,　関数first:P→A　,　second:P→B　からなり、任意の型Xと任意の関数f:X→A , g:X→B に対して　,　以下の図式が可換となるような u:X→Pが　唯一つ存在するものである。　というのが定義らしい。

　　　　　　　　　　 　 X
                     　 f↙        ↓ u       ↘ g

　　　　　  　A　 ←　 　P　→　 　B
                           first         second

public class Pair<T, U>

{
    public T First { get; set; }
    public U Second { get; set; }
 
    public Pair(T first, U second) {
        this.First = first;
        this.Second = second;
    }
.............   こんな感じで、プログラミング言語でP(x,y)などpairはよく使うが。

　単に、１つめか、２つめか指定すればそれを取り出せるような仕組みのことだけれど、それを圏論的に定義すると上記のようなことになるらしい。

PはA,B型のデータを得る特定の関数を備えていて　図式で表現すると（中身を詳しく説明せず、矢印と対象だけで表現するのが圏論）

　　　　　  　A　 ←　 　P　→　 　B

                           first         second

しかし、これだけでは、A,B型への関数をもつデータ型は、Pair以外にもいろいろある（何らかの計算や処理が入っている場合もこの定義を満たす）ので、十分とはいえない。関数もいろいろある。

そこで、上記のような可換図式を使う。

　合成関数で考えると　frist 〇 u = f       second 〇 u = g　①　だが、定義がこれだけでは不足している。uの唯一性というのがポイントらしい。

　例えば、uが余分なデータを付け足してfirst,secondがそれを捨てる場合などでも、可換にできるが、それでは、first,secondの働きを正しく表していない。（あくまで、first,secondの働きはただ取り出すだけ、というふうに定義したいわけなので）

 　余分なデータをつけたす(first,secondがそれを捨てる）→uは唯一に定まらない

対偶は　　uが唯一　→　余分なデータはつけたさない(first,secondはただ取り出すのみ)

　ということで、uの唯一性があると、うまくPairを定義できたことになるということらしい。　こういうのを、普遍性による定義というらしい。

　ここのところが、非常にわかりにくい。uが一意に定まると、自動的に射影しかありえなくなるのはなぜか？ 　射影だと、どんなX,f,gであっても、唯一u(x)=(f(x),g(x))というものさえあればいいわけだから、これでいいような気はする。

　どんなX,f,gであっても、唯一決まるパターンとは、first,secondが射影の場合とu(x)=(f(x),g(x))の組み合わせしかないということ？だろうか。射影のところになんらかの別の射の要素が入り込むと、u(x)=(f(x),g(x))とは違うものが必要になってくる。定義の文章をよく読むと、u(x)は任意のX,f,gに対してきまるとしており、first,secondからも影響を受けることは想定してないということなのかもしれない。