昨日の記事「述語論理： 二重圏的ハイパードクトリン」で、二重圏的ハイパードクトリンという概念を出しました。二重圏的ハイパードクトリンを定義するために、シード付き二重圏を定義したのですが、どうも安直過ぎました。シード付き二重圏を再定義します。$`\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\In}{\text{ in } }
`$
内容：
ハブ記事：
二重圏的ハイパードクトリン
ハイパードクトリンは、ベース圏 $`\cat{C}`$ と、ベース圏の各対象に（圏とみなした）論理代数を対応させるインデックス付き圏 $`\cat{P}:\cat{C} \to {\bf Cat}`$ からなります。その他の構成素もありますし、色々な条件が付きますが、主役は $`\cat{P}:\cat{C} \to {\bf Cat}`$ です。
二重圏的ハイパードクトリン〈double categorical hyperdoctrine〉とは、ハイパードクトリンにおける主役を置き換える試みです。二重圏 $`\cat{D}`$ を構成し、二重圏からの2つの二重関手
$`\quad \cat{P}_\exists : \cat{D} \to {\bf AdjDC}\\
\quad \cat{P}_\forall : \cat{D} \to {\bf AdjDC}`$
を主役に据えたいのです。ここで、$`{\bf AdjDC}`$ は随伴系（関手の随伴ペア）の二重圏です。
$`\cat{D}`$ と $`\cat{P}_\exists, \cat{P}_\forall`$ を導入したからといって、$`\cat{C}`$ と $`\cat{P}`$ が不要になるわけではありません。新しい主役を下支えする存在として $`\cat{C}, \cat{P}`$ は重要です。
シード付き二重圏
ハイパードクトリンの新しい定義で使用する二重圏 $`\cat{D}`$ を、「述語論理： 二重圏的ハイパードクトリン」ではシード付き二重圏〈double category with seeds〉と呼ぶことにしました。この呼称は使い続けますが、「シード」の意味を変更します。
二重圏 $`\cat{D}`$ の横1-射〈水平射 | horizontal 1-morphism〉を射とする圏を $`\cat{D}_\mrm{H}`$ 、$`\cat{D}`$ の縦1-射〈鉛直射 | vertical 1-morphism〉を射とする圏を $`\cat{D}_\mrm{V}`$ とします。シードは次のような関手であるとします。
$`\quad S_\mrm{H} : \cat{D}_\mrm{H} \to \cat{C}\\
\quad S_\mrm{V} : \cat{D}_\mrm{V} \to \cat{C}`$
$`S_\mrm{H}`$ を横シード関手〈水平シード関手 | horizontal seed functor〉、$`S_\mrm{V}`$ を縦シード関手〈鉛直シード関手 | vertical seed functor〉と呼びます。
シードであるための条件があります。
- $`(S_\mrm{H})_\mrm{obj} = (S_\mrm{V})_\mrm{obj}`$
つまり、横シード関手と縦シード関手の対象パートは一致します。対象〈0-射〉 $`A\in |\cat{D}|`$ に対しては、$`S(A) = S_\mrm{H}(A) = S_\mrm{V}(A)`$ と書くことにします。
二重圏 $`\cat{D}`$ の二重2-射を $`\alpha`$ として、その境界四角形は次の形だとします。
$`\require{AMScd}
\begin{CD}
A @>s>> A'\\
@V{f}VV @VV{g}V\\
B @>t>> B'
\end{CD}`$
この境界四角形を $`S_\mrm{H}, S_\mrm{V}`$ で $`\cat{C}`$ に移すと以下の四角形ができます。
$`\require{AMScd}
\begin{CD}
S(A) @>{S_\mrm{H}(s) }>> S(A')\\
@V{S_\mrm{V}(f) }VV @VV{S_\mrm{V}(g) }V\\
S(B) @>{S_\mrm{H} (t)}>> S(B')
\end{CD}`$
$`\cat{C}`$ 内のこの四角形は可換であることを要求します。
二重圏 $`\cat{D}`$ の二重2-射はそんなにたくさんはないことも仮定します。横1-射と縦1-射で作られた四角形があるとき、その四角形を境界とする二重2-射はたかだか1つしかないとします。二重圏 $`\cat{D}`$ は“やせた二重圏”と言えます。
訂正・変更
昨日の記事「述語論理： 二重圏的ハイパードクトリン」を直接に訂正はしないで、ここで訂正・変更すべき箇所を指摘します。（元記事に注釈の追記はするかも知れませんが。）
昨日記事では、二重圏 $`\cat{D}`$ は、圏 $`\cat{C}`$ とその部分圏 $`\cat{S}`$ から簡単に構成できる前提でした。それは安直過ぎるので、二重圏 $`\cat{D}`$ は独立に与えられると変更します。しかし、$`\cat{D}`$ と $`\cat{C}`$ は密接に関係していて、その関係性が横シード関手／縦シード関手で与えられます。
昨日記事の部分圏 $`\cat{S}`$ は、横シード射の像である部分圏ですが、もはや強調する意味はありません。二重圏 $`\cat{D}`$ の横1-射の圏 $`\cat{D}_\mrm{H}`$ は、$`\cat{C}`$ の部分圏になるとは限りません。
それと、昨日記事では、二重圏の縦横の区別が曖昧です。シード射（昨日の意味）の方向が横のつもりなのですが、僕の不注意から、シード射の方向を縦に描いている図があります。縦横の区別に関しては、述語論理のモデルにおいて、述語論理系（の随伴トリプル）が横方向になるように決めます。縦方向に見た二重2-射は、述語論理系の変換になります。ハイパードクトリンの定義がうまくいくように決めます。
昨日の記事の“シード付き二重圏”ではダメだ、と思ったのは、伝統的述語論理のハイパードクトリンの記述がうまくいかなかったからです。伝統的述語論理を、二重圏的ハイパードクトリンで定式化するのが最初の目標です。
