Equalizer

バンド関係ではありません。圏の射の積みたいなものですね。二つの射 f,g から定義されて、それを e(f,g) とすると、

         e(f,g)             f

     c ----------> a -------------> b

                     ------------->

                            g

f h = g h なら、f e k = g e k かつ h = e k となる k がただ一つある

みたいな定義です。一意対応とか上への写像とかと関係するらしいです。積も同じような感じで定義されるんだよね。

f : a → q , g : b → q があると、f = e1 k, g = e2 k となる k : (p,q) → q がただ一つある

           f                g   

     a -----------> q <-------------  b

     |              ^                 |

     |              |k                |

     v     e1       |       e2        v

     +----------> (p,q) <-------------+

みたいな感じ。

Equalizer の定義は [ f h = g h なら ] という等式以外のものが入っていて、これを取り除いて等式のみで
定義した Burroni という人がいたらしい。

本読んでもピンと来なかったので、そこを Agda で書いていくわけですが、B1からB4の等式を、仮定した Equalizer の性質で証明していくのですが、
B1-B3 までは、数時間でできたらしい。なのだが、B4 が全然できない。いや、いいところまで行くのだが、

＊　どうどう巡りする

equalizer には、e と、解の k の二つがあるのだが、e から k を出して k から e 出すと元に戻る。あららら。

どうも、e = e' を証明する辺りでけっつまづいているので、「二つのEqualizer は、isomorphism の分を除いて同じ」ってのを調べてみる。 これは、

e = left e', e' = right e で、left right = id, right left = id

つまり、行って帰ると元に戻る射があるというわけだ。これが、また、全然証明できない。行きは良いのだが帰りが全然ダメ。その辺りで5日ぐらいつぶれました。

そういえば、c って f, g から決まるのかという昔からの疑問があった。悩んでいるのは e = e' だから、c が任意に決められるなら、e = e' と勝手に決めて良い。 どうも、そうすると証明できるっぽい! そこか! というのが昨日の深夜。そこから朝まででだいたいできました。

Agda での定義の違いは、

    record Equalizer { c c � : Level} ( A : Category c c � )  {c a b : Obj A} (f g : Hom A a b)  : Set  (�  (c  c)) where

       field

          equalizer : Hom A c a

          fe=ge : A [ A [ f o e ]  A [ g o e ] ]

          k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ]  A [ g  o h ] ] → Hom A d c

          ek=h : {d : Obj A}  → ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ]  A [ g  o h ] ] } →  A [ A [ e  o k {d} h eq ]  h ]

          uniqueness : {d : Obj A} →  ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ]  A [ g  o h ] ] } →  {k' : Hom A d c } →

                  A [ A [ e  o k' ]  h ] → A [ k {d} h eq   k' ]

と、

    record Equalizer { c c � : Level} ( A : Category c c � )  {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b)  : Set  (�  (c  c)) where

       field

          fe=ge : A [ A [ f o e ]  A [ g o e ] ]

          k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ]  A [ g  o h ] ] → Hom A d c

          ek=h : {d : Obj A}  → ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ]  A [ g  o h ] ] } →  A [ A [ e  o k {d} h eq ]  h ]

          uniqueness : {d : Obj A} →  ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ]  A [ g  o h ] ] } →  {k' : Hom A d c } →

                  A [ A [ e  o k' ]  h ] → A [ k {d} h eq   k' ]

       equalizer : Hom A c a

       equalizer = e

だけだ。証明も影響は限定的。k, ek=h, uniqueness は変わってないし。この手の命題間の依存関係が低いのは圏論の良い所だな。

record の field にするのか、record の parameter にするのかは、結構大きな違いがあるらしいというのがわかりました。

＊　parameter は、外から指定できる

＊　field は、存在を仮定されてしまう

みたいな感じ。implicit parameter を指定してやることで同等なはずだと思っていたのですが、結構差があるのね。

Equalizer を record { equalizer = hoge; ... } みたいに作っていくと差がないけど、「 とにかく Equalizer があって」という場合に e を指定できるかできないかの差があるようですね。後出しで「e は、実は、e' だったことにしよう」ってのも可能。この辺りは、Unification だから Prolog　的だ。

まだ、ちょっと残ってますが、片付いてうれしいです。Burroni から Equalizer を導くところが三箇所。また、5日かかったりしないだろうな。