テレスコープのための関手意味論フレームワーク

$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\Within}{ \sqsubseteq }
`$

  • $`\cat{Sign}`$ 指標の圏
  • $`\cat{Alg}`$ 代数の圏
  • $`\mathbb{F}:\cat{Sign} \dashv \cat{Alg} : \mathbb{U}`$ 自由忘却随伴系
  • $`J:\cat{Alg} \to {\bf Cat}`$ 代数の圏解釈(小さい圏とみなす)
  • $`\cat{T} \in |{\bf CAT}|`$ (モデルの)ターゲット圏

モデル関手は次のように定義できる。

$`\quad \mrm{Model}(S) := [J(\mathbb{F}(S)), \cat{T}]_{\bf CAT}`$

これは、インデックス付き圏になる。

標準モナド〈canonical monad〉は次のように定義する。

$`\quad \mathbb{M} := \mathbb{F}*\mathbb{U}`$

手続きの圏は次のように定義できる。

$`\quad \mrm{Proc} := (\mrm{Kl}( \mathbb{M}/\cat{Sign}) )^\mrm{op}`$

フレームワーク全体を $`\mathscr{F}`$ で表すと、フレームワーク、定義されたモデル関手、標準モナド、手続きの圏は次のように書ける。

  • $`\mathscr{F} = (\mathbb{F}:\cat{Sign} \dashv \cat{Alg} : \mathbb{U}, J, \cat{T} )`$
  • $`\mrm{Model}_{\mathscr{F}}`$
  • $`\mathbb{M}_{\mathscr{F}}`$
  • $`\mrm{Proc}_{\mathscr{F}}`$

テレスコープを定義するには、指標の圏 $`\cat{Sign}`$ に包含構造〈inclusive structure〉が入る。