「バンドル-ファミリー対応を簡潔に書く」で導入した簡潔な記法（(-1)乗の書き方）により、随伴トリプルを記述してみます。
内容：
バンドルの随伴トリプル
次はプルバック四角形です。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\o}[1]{\overline{#1} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
\newcommand{\FProd}{\mathop{\underline{\times}}}
`$
$`\quad \xymatrix{
\cdot \ar[r] \ar[d]_{f^\# t}
\ar@{}[dr]|{\text{p.b.}}
&\cdot \ar[d]^t
\\
A \ar[r]_f
&B
}\\
\quad \In \mbf{Set}
`$
$`t\mapsto f^\# t`$ という対応は、次のような関手に仕立てることができます。
$`\quad f^\# : \mbf{Set}/B \to \mbf{Set}/A \In \mbf{CAT}`$
$`\mbf{Set}/\hyp`$ は、集合圏のオーバー圏〈スライス圏〉です。
関手 $`f^\#`$ には左随伴関手と右随伴関手が存在します。それを、$`f_\wedge, f_\#`$ と書くことにします。すると：
$`\quad f_\wedge \dashv f^\# \dashv f_\#\\
\text{where}\\
\quad f_\wedge : \mbf{Set}/A \to \mbf{Set}/B\\
\quad f_\# : \mbf{Set}/A \to \mbf{Set}/B
`$
オーバー圏〈スライス圏〉は、ベース集合を固定したバンドル達の圏でした。次が成立します。
$`\quad \mbf{Set}/A = \mbf{Bun}[A]\\
\quad \mbf{Set}/B = \mbf{Bun}[B]\\
\quad f_\wedge, f_\# : \mbf{Bun}[A] \to \mbf{Bun}[B]
`$
バンドル-ファミリー対応により、ファミリー側にも次の随伴トリプルがあります。
$`\quad f_! \dashv f^* \dashv f_*\\
\text{where}\\
\quad f_! : \mbf{Fam}[A] \to \mbf{Fam}[B]\\
\quad f_* : \mbf{Fam}[A] \to \mbf{Fam}[B]
`$
$`f_!, f_*`$ のほうが具体的な定義をしやすいので、次節で $`f_!, f_*`$ を定義します。
ファミリーの随伴トリプル
関数（一般的には射） $`f`$ から誘導される関手を $`f^*`$ と書き*1、その左随伴関手を $`f_!`$ 、右随伴関手を $`f_*`$ と書くのは比較的によく使われる記法です。バンドルの場合もこの記法がそのまま使われることが多いでしょう（ここでは区別して $`f^\#, f_\wedge`$ を使いましたが）。
別な書き方として、次があります。
$`\quad \Sigma_f \dashv \Delta_f \dashv \Pi_f`$
左右は、シグマ型（集合族の総和）とパイ型（集合族のセクション空間）にちなみます。実際、シグマ型とパイ型を使って $`\Sigma_f, \Pi_f`$ を書けます。
ここから先、ギリシャ文字大文字の $`\Sigma, \Pi`$ と、総和記号 $`\sum`$ 、総積記号 $`\prod`$ は次のように使い分けます。
- $`\Sigma_f`$ は、$`\Delta_f = f^*`$ の左随伴関手
- $`\Pi_f`$ は、$`\Delta_f = f^*`$ の右随伴関手
- $`\sum(x\in A \mid H(x))`$ は、集合族 $`H`$ のシグマ型（総和）
- $`\prod(x\in A \mid H(x))`$ は、集合族 $`H`$ のパイ型（総積）
まず、$`f:A \to B`$ に対する $`\Delta_f`$ は次のように定義されます。
$`\text{For }G \in |\mbf{Fam}[B]|\\
\text{For }a \in A\\
\quad (\Delta_f G)(a) := G(f(a))
`$
これは対象に対する定義ですが、$`\mbf{Fam}[B]`$ の射に対しても適切に定義します。
図式では：
$`\quad \xymatrix{
{}
&{}
\\
A \ar[r]_{f} \ar@{~>}[ur]^{\Delta_f G}
&B \ar@{~>}[u]_{G}
}
`$
$`\Sigma_f`$ の具体的な定義は次のようです。
$`\text{For }F \in |\mbf{Fam}[A]|\\
\text{For }b \in B\\
\quad (\Sigma_f F)(b) := \sum( x \in f^{-1}(b) \mid F(x))
`$
ここでの $`f^{-1}`$ は要素の逆像です。$`\mbf{Fam}[A]`$ の射に対しても適切に定義します。
$`\Pi_f`$ の具体的な定義は次のようです。
$`\text{For }F \in |\mbf{Fam}[A]|\\
\text{For }b \in B\\
\quad (\Pi_f F)(b) := \prod( x \in f^{-1}(b) \mid F(x))
`$
$`\mbf{Fam}[A]`$ の射に対しても適切に定義します。
これらは随伴関手ペアなので、次のホムセット同型が成立します。
$`\quad \mbf{Fam}[B](\Sigma_f F, G)\cong \mbf{Fam}[A]( F, \Delta_f G)
`$
$`\quad \mbf{Fam}[A](\Delta_f G, F)\cong \mbf{Fam}[B]( G, \Pi_f F)
`$
ちなみに、述語論理の場合なら、対象が述語〈predicate〉で証明が射（ホムセットの要素）である圏を考えて次のようになります。
$`\quad \mbf{Pred}[B](\exists_f P, Q)\cong \mbf{Pred}[A]( P, \diamondsuit_f Q)
`$
$`\quad \mbf{Pred}[A](\diamondsuit_f Q, P)\cong \mbf{Pred}[B]( Q, \forall_f P)
`$
$`\diamondsuit`$ については「型を命題にクラッシュさせる： ダイアモンド・オペレーターの由来」を参照してください。過去記事では、$`\mbf{Pred}[\hyp]`$ ではなくて $`\mrm{Pred}(\hyp)`$ と書いているので注意してください。
バンドルとファミリー
前節で、ファミリーに対して次の関手を定義しました。
- $`f^* = \Delta_f\; : \mbf{Fam}[B] \to \mbf{Fam}[A]\In \mbf{CAT}`$
- $`f_! = \Sigma_f\; : \mbf{Fam}[A] \to \mbf{Fam}[B]\In \mbf{CAT}`$
- $`f_* = \Pi_f\; : \mbf{Fam}[A] \to \mbf{Fam}[B]\In \mbf{CAT}`$
バンドルに対する関手達 $`f^\#, f_\wedge, f_\#`$ は、ファミリーに対する関手を使って次のように定義できます。以下で、$`\hyp^{-1}`$ はバンドルに対応するファミリーです。
$`\text{For }t \in |\mbf{Bun}[B]|\\
\quad f^\# t := {^\pi (f^* (t^{-1}) )}
`$
$`\text{For }s \in |\mbf{Bun}[A]|\\
\quad f_\wedge s := {^\pi (f_! (s^{-1}) ) }
`$
$`\text{For }s \in |\mbf{Bun}[A]|\\
\quad f_\# s := {^\pi (f_* (s^{-1}) ) }
`$
以上の定義で、バンドル達の世界の随伴トリプルを定義できます。
バンドル達の世界とファミリー達の世界は、細部まで対応が成立するソックリな世界なので、随伴トリプルのような繊細な構造も「別な世界に素材を持って行って、組み立てて戻って来る」という手法が使えます。
*1:僕もしばしば混乱するのですが、$`f \mapsto f^*`$ は反変的対応ですが、$`f^*`$ 自体は共変関手です。
