haskell-jp / math #10

函手 F, G: C ↝ D に対して、自然変換 F ⇒ G は、任意の f: a → b in C に函手をそれぞれ適用し、
Ff: Fa → Fb in D および Gf: Ga → Gb in D に可換図式 θb . Ff = Gf . θa を満たす射の族 θ_ を考えることで与えられますよね

これを直観的に解釈したいと考えたときに：
1. 自然変換によって、函手によって D に移された対象の対応関係を知ることができる
2. 自然変換によって、函手によって D に移された射の対応関係を知ることができる
という捉え方ができないかを考察しています (その方が函手と函手の対応っぽく見えるので)

1. に関しては自明で、そもそも任意の C の対象 a に対して θa: Fa → Ga が言えるわけですから、
これは自然変換と任意の Fa から、Ga を知ることができると言ってよいでしょう

対して、2. に関しては θ_ が常に同型射となる制約 (自然同型) であれば、
逆射であることを ' をつけて表せば、Gf = θb . Ff . θa' が言えるので、
自然変換と Ff から、Gf を知ることができると言って良いでしょうが、実際はそこまで強い制約は課さないわけですよね

少なくとも可換図式 θb . Ff = Gf . θa が言える以上、Fa を固定して、Fa および θa から Ga (すなわち dom(Gf)) に、
Fa，Ff および θb から Gb (すなわち cod(Gf)) に辿るつけることは言えて、任意の2対象から適当に射を取り出すようなこと考えれば、
Gf とドメイン・コドメインを共通にする Gf† なる射の存在は言えそうなのかなと
(もちろん、一般に任意の2対象の間に射が存在するとは限りませんが、今回は少なくとも Gf が存在しているので、Hom(Ga, Gb) ≠ Φ)

あとは Gf と Gf† は等しいとは言えないまでも、同型であることを言えれば、
「自然変換と任意の Ff から、Gf を知ることができる」という直観的な主張をできると思うのですが、はたしてと… :thinking_face:

あー、でも可換図式 θb . Ff = Gf . θa をそもそも射圏で捉えてしまえば、射 θ: Ff → Gf と 対象 Ff がわかって、Gf† も同様な可換図式を満たすとすれば、同じ対象 Ff から同じ射 θ を使ってたどり着く先が Gf と Gf† と言えて、これが同型でないということはあり得ないで良いんですかね :innocent:

@HiB has joined the channel

詳しくないので、間違っていたらすみません。

自然同型について触れられているとおり、
j = θ_a, k = θ_b . Ff, x = Gf としたとき、
j と k から x が一意に定まるか、と捉えた場合、
x . j = k かつ x' . j = k ならば x = x'
は一般にはいえなかったと思います。
(これが成り立つ j をエピ射といったと思います。)

逆にたとえば j が右零射なら、任意の射 x, x' に対して x . j = x' . j となるので、
そのような j = θ_a を成分とする自然変換の場合、
Ff から Gf が決まらないことがいえると思います。

具体例としては、

関手 F, G : Vect_k -> Vect_k、
関手 F は、任意の対象を零ベクトル空間 0 に、任意の射を 0 の恒等射に写す
関手 G は、恒等関手

を考えたときに、自然変換 θ: F ⇒ G を
θ_a : 0 -> a は 0 から a への埋め込み 0_{0,a}
で定義すれば、
( Gf . θ_a = θ_b . Ff = 0_{0,b} となって可換 )
f : a -> b の像は、
Ff = id_0
に対して、
Gf = f
で、
f が複数ある場合、Ff からは Gf は一意に決まらないと思います。

上記が正しい場合、射の対応をあきらめて、おっしゃるような
射 Ff に対応する射集合 Gf†={ g | g . θ_a = θ_b . Ff }
といったことを考えることはできると思いますが、
それは結局、
射 Ff に対応する射集合 {f'|Ff' = Ff} から射集合 {Gf'|Ff' = Ff} を知る、
ということなので、自然変換はもはや関係なくて、
単に任意のfに対するFfとGfがどう対応しているかという話になっている気がします。
(そういう意味では1.と同じような意味で自明なのかもしれないです。)

たとえば j が右零射

あー、たしかにこのパターンは完全にアウトですね :pray:

@skaribe has joined the channel

@ has joined the channel

@ysys13 has joined the channel

@ has joined the channel

@Roki has joined the channel

@Shota has joined the channel

@kaorun343 has left the channel

@SF has joined the channel

@niszet has joined the channel

@knight-rose has joined the channel

:随伴: や :adjunction: で :adjunction: が出せるようにしたり、
:compose: や :合成: で :compose: が出せるようにしました。
他にも :id: で :id: が出せたり、emojiには圏論が溢れています :smirk:

@mds_boy has joined the channel

@ has joined the channel

@Jonas has joined the channel

Haskellと直接関係がないっぽいのでこちらへ。知らなかった: https://github.com/liuxinyu95/unplugged

Haskellのコード例が結構書かれているみたいです（詳細は読んでません）。
HaskellのRedditや、haskell-cafe MLでも案内があったようです:slightly_smiling_face:
https://www.reddit.com/r/haskell/comments/jdyxee/haskellcafe_release_a_book_about_math_and/

えぇ、私が知ったのもHaskell Cafeでした。が、なるほどやっぱりサンプルにHaskell :haskell: が、と。

こちらの本、少し前に本を持ってる方にチラ見せしてもらいました。リポジトリがあったとは知りませんでした…

@ has joined the channel

@yuki2501 has joined the channel

@Yasuhiro has joined the channel

@Yudai Tanabe has joined the channel

@sh9 has joined the channel

@Jaeseung Han has joined the channel

@sirkerf has joined the channel

@ has joined the channel

@rozaki has joined the channel

@Aumy has joined the channel

@KXing has joined the channel

@Masaya(M_simplifier) has joined the channel

@ has left the channel

@ has joined the channel

@さんたむ has joined the channel

@Benjamin Bray has joined the channel

英語版ウィキペディアの「米田の補題」に Haskell の Coyoneda 型の原理になる同型が書いてあった

@ has joined the channel

@TH has joined the channel

@juxtapose has joined the channel

@ddd has joined the channel

@ has joined the channel

@Tomo has joined the channel

@Kouji Okamoto has joined the channel

@K.Hirata has joined the channel

@ has joined the channel

@HA has joined the channel