【新機能】作り忘れたまとめはありませんか?31日前まで期間指定してまとめが作れる高度な検索ができました。有料APIだからツイートの漏れはありません!
3
ログインして広告を非表示にする
alg_d @alg_d
今までlaxモノイダル関手ってどっち向きだよ(Fu⊗Fv→F(u⊗V)なのか? ←なのか?)って思ってたけど今回の更新で完全に覚えた
alg_d @alg_d
CがV-豊穣圏のときa, b∈Cに対してC(a, b)∈Vである。ここでもし関手F: V→WがあるとF(C(a, b))∈Vを考えることができる。そこでFC(a, b) := F(C(a, b)) と定義すれば新しい W-豊穣圏 FC が定義できそうな感じがする。
alg_d @alg_d
ところがその為には射の合成を与える射 FC(b, c)⊗FC(a, b) → FC(a, c) を与えなければならない。ここでもしFが「⊗と可換」であれば FC(b, c)⊗FC(a, b) = F(C(b, c)⊗C(a, b))となるから、Cの合成から自然にFCの合成を定義できる。
alg_d @alg_d
ところが実はFは「⊗と可換」とかいうめちゃくちゃ強い条件を満たす必要はなくて、実はu, v∈Vについて自然な射 Fu⊗Fv→F(u⊗v) が存在してさえいれば(同型である必要もない)、FCに合成を定義できる。これがlaxモノイダル関手の条件の一つ。
alg_d @alg_d
FCをW-豊穣圏にするには恒等射も定義しなくてはいけないが、そのために必要なのがlaxモノイダル関手のもう一つの条件。
alg_d @alg_d
これ覚えておくとlaxモノイダル関手の条件の向きはすぐ復元できると思う。
alg_d @alg_d
今述べたことをきちんと考えると、laxモノイダル関手 F: V→W からstrict 2-functor F: V-Cat→W-Cat が構成できるという定理になる(今回の更新の定理95)。
alg_d @alg_d
さてすると今度はlaxモノイダル関手による随伴 F-|G: V→W から随伴 F-|G V-Cat→W-Cat が構成できないかなということを考えたくなる(これはまあHTT見たことある人は似たような主張のモデル圏版を見たことがあると思うが、まあとりあえずモデル構造なしに証明してみようやという感じである)
alg_d @alg_d
その為にはモノイダル随伴というのを導入する必要がある。これはなんてことはなくて、FとGがlaxモノイダルなのだからunitとcounitにもlaxモノイダル関手の構造と可換になるという条件を入れようというだけである。
alg_d @alg_d
するとこれ凄くて、F-|G でFとGがlaxモノイダルでunitとcounitがモノイダル自然変換だとなんとFが自動的にstrongモノイダル関手(Fu⊗Fv ≅ F(u⊗v)が成り立つやつ)になる。これが結構重要でFがstrongモノイダルになってくれた結果最終的に(Cat-豊穣圏の)随伴 F-|G V-Cat→W-Cat が示せる。
alg_d @alg_d
ここまでが今回の更新でこのstrongになるところが一番難しかった(いや書いてみたら全部自明だけど)のだが、これ調べると2-monadの理論から自明とか言われるので完全にキレた(何読んでも大体最終的にKellyの『Doctrinal Adjunction』に飛ばされる)(結局証明は全部自分で書いた)
ぴあのん@さよ朝宣伝bot @piano2683
lax monoidal functor F: V→Wがstrict 2-functor F: V-Cat→W-Catを誘導することも証明したのか [ところでV-Catがstrict 2-categoryになることの証明はまだ???]
alg_d @alg_d
@piano2683 ペーパー氏に任せた()
alg_d @alg_d
@piano2683 まあそのうち書きますよ
ぴあのん@さよ朝宣伝bot @piano2683
あのalg_dでも挫折するレベルの豊穣圏の定理
alg_d @alg_d
@piano2683 いや挫折する前に証明しようともしていないので
alg_d @alg_d
てか、豊穣圏PDF更新したけど豊穣圏はクソだからやらない方がいいよ
alg_d @alg_d
豊穣圏PDFを紙に印刷して透かして見ると「#豊穣圏は射が取れないからクソ」と書いてあります

コメント

ログインして広告を非表示にする
ログインして広告を非表示にする