Sunday, 8 September 2013

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日かかったりしないだろうな。
Post a Comment