一連の話題を小ネタに切り刻んで投稿しています。ココに書いたような事情です。
「等式的関手インスティチューション(概要)」で述べたように、等式的関手インスティチューションでは、指標Σに対するモデル圏*1 Model[Σ] を、関手圏*2として具体的に構成するのでした。
- Model[Σ] := [Σ◇, Set]
上記の右辺によりモデル圏が定義されますが、右辺に登場する (-)◇ と [-, -] の意味がハッキリしないと定義したことになりません。実際、これじゃ全然ハッキリしてません。
モデル圏の定義をハッキリさせようとすると、圏論では常につきまとう問題が顔を出します。
- 圏のサイズ〈大きさ〉の問題
- 圏の構造の弱さの問題
サイズと弱さを調整する〈折り合いをつける〉定番の方法はない*3ので、試行錯誤でやるしかありません。
まずサイズについては:
- 指標(パス同値関係を持った有向グラフ)は集合ベースの小さいものを考える。
- 指標から生成される圏も小さい圏を考える。
- モデルである関手が値を取る圏は集合圏なので大きい圏。
- 指標に対するモデル圏も大きな圏になる。
これは妥当な選択でしょう。これでいいとします。
次に、圏の構造の弱さを考えます。Σ◇やSetが持つ構造としては、デカルト・モノイド構造を要請します。考えるべき弱さは:
ここで、三番目のSetのデカルト・モノイド構造の弱さは既に決まっているので議論しません。Setは直積に関して弱い〈非厳密な〉モノイド圏になります。直積の結合律も単位律もup-to-isoでしか成立しません。
悩むのは、Σ◇のデカルト・モノイド構造の弱さです。Σ◇を弱い〈非厳密な〉モノイド圏だとすると、どうも面倒そうです(そんな気がする)。厳密モノイド圏になるようにしましょう。Σ◇の定義は:
- Σ◇ := FreeStrCartMonCat(Σ) = (Σから生成される、最小の厳密デカルト・モノイド圏)
指標の圏Sの射は、厳密モノイド関手(デカルト構造も厳密に保存する)にしてみましょう、とりあえず。そうすれば、指標圏Sは扱いやすくなります。ただし、条件が厳しすぎて実用上困るかも知れません。現時点ではどっちか分かりません。
Σのモデルとなる、Σ◇からSetへの射(関手)を厳密モノイド関手にしてしまうと、これはさすがに無理。身動き取れないので、関手圏 [Σ◇, Set] を構成する関手は、タイトなモノイド関手とします。タイトなモノイド関手に関しては、次の記事を見てください。
Σ◇やSetに限らず、一般に(小さいとは限らない)弱デカルト・モノイド圏とタイト・デカルト・モノイド関手と自然変換からなる2-圏をTightCartMonCATとします。[-, -]TightCartMonCAT は、2-圏TightCartMonCATの内部ホムです。
以上に説明した概念を使うと、
- Model[Σ] := [FreeStrCartMonCat(Σ), Set]TightCartMonCAT
という定義になります。
この選択(決めた約束ごと)では、指標圏は厳密〈strict〉なものにして、弱さはターゲット圏であるSetとモデルである関手のほうに担わせます。まだ不明確なところもあるでしょうし、この選択で具合がいい保証もありません。が、何かに決めないと何もできないので、こう決めます。