このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

等式的関手インスティチューションの作り方: 悩みどころ

一連の話題を小ネタに切り刻んで投稿しています。ココに書いたような事情です。

等式的関手インスティチューション(概要)」で述べたように、等式的関手インスティチューションでは、指標Σに対するモデル圏*1 Model[Σ] を、関手圏*2として具体的に構成するのでした。

  • Model[Σ] := [Σ, Set]

上記の右辺によりモデル圏が定義されますが、右辺に登場する (-) と [-, -] の意味がハッキリしないと定義したことになりません。実際、これじゃ全然ハッキリしてません。

モデル圏の定義をハッキリさせようとすると、圏論では常につきまとう問題が顔を出します。

  • 圏のサイズ〈大きさ〉の問題
  • 圏の構造の弱さの問題

サイズと弱さを調整する〈折り合いをつける〉定番の方法はない*3ので、試行錯誤でやるしかありません。

まずサイズについては:

  1. 指標(パス同値関係を持った有向グラフ)は集合ベースの小さいものを考える。
  2. 指標から生成される圏も小さい圏を考える。
  3. モデルである関手が値を取る圏は集合圏なので大きい圏。
  4. 指標に対するモデル圏も大きな圏になる。

これは妥当な選択でしょう。これでいいとします。

次に、圏の構造の弱さを考えます。ΣSetが持つ構造としては、デカルト・モノイド構造を要請します。考えるべき弱さは:

  1. Σデカルト・モノイド構造の弱さ
  2. ΣとΔのあいだの射(モノイド関手)の弱さ
  3. Setデカルト・モノイド構造の弱さ
  4. ΣSetのあいだの射(モノイド関手=モデル)の弱さ

ここで、三番目のSetデカルト・モノイド構造の弱さは既に決まっているので議論しません。Setは直積に関して弱い〈非厳密な〉モノイド圏になります。直積の結合律も単位律もup-to-isoでしか成立しません。

悩むのは、Σデカルト・モノイド構造の弱さです。Σを弱い〈非厳密な〉モノイド圏だとすると、どうも面倒そうです(そんな気がする)。厳密モノイド圏になるようにしましょう。Σの定義は:

  • Σ := FreeStrCartMonCat(Σ) = (Σから生成される、最小の厳密デカルト・モノイド圏)

指標の圏Sの射は、厳密モノイド関手(デカルト構造も厳密に保存する)にしてみましょう、とりあえず。そうすれば、指標圏Sは扱いやすくなります。ただし、条件が厳しすぎて実用上困るかも知れません。現時点ではどっちか分かりません。

Σのモデルとなる、ΣからSetへの射(関手)を厳密モノイド関手にしてしまうと、これはさすがに無理。身動き取れないので、関手圏 [Σ, Set] を構成する関手は、タイトなモノイド関手とします。タイトなモノイド関手に関しては、次の記事を見てください。

ΣSetに限らず、一般に(小さいとは限らない)弱デカルト・モノイド圏とタイト・デカルト・モノイド関手と自然変換からなる2-圏をTightCartMonCATとします。[-, -]TightCartMonCAT は、2-圏TightCartMonCATの内部ホムです。

以上に説明した概念を使うと、

  • Model[Σ] := [FreeStrCartMonCat(Σ), Set]TightCartMonCAT

という定義になります。

この選択(決めた約束ごと)では、指標圏は厳密〈strict〉なものにして、弱さはターゲット圏であるSetとモデルである関手のほうに担わせます。まだ不明確なところもあるでしょうし、この選択で具合がいい保証もありません。が、何かに決めないと何もできないので、こう決めます。

*1:ホモトピー論では、モデル構造を持つ圏をモデル圏といいますが、ここでのモデル圏は、指標のモデルを対象とする圏です。

*2:関手が対象で、自然変換が射である圏が関手圏です。

*3:僕が知らないだけ、という可能性もあります。あったら教えてください。