米田埋め込みの繰り返しと淡中再構成 - 檜山正幸のキマイラ飼育記 (はてなBlog)

ここ最近、米田の補題に関連する記事を幾つか書いています。

動機はなんなのかと言うと；淡中再構成〈Tannaka reconstruction〉を、米田の補題の直接的で簡単な応用として記述したい、ということです。米田の補題を知っていれば、（古典的・初等的な）淡中再構成は当たり前に見えるようにしたい、と。

そのためには、米田の補題を次の形にしたいのです。

$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\hyp}{\text{－}}
%
%
\quad よ * よ^\vee \cong た`$

記号の説明をすると：

$`よ = ({^\cat{C} よ}) \;: \cat{C} \to \cat{C}^\wedge`$ は米田埋め込み。$`(\hyp)^\wedge`$ は前層の圏を作るオペレーター。
$`よ^\vee = ({^{\cat{C}^\wedge} よ^\vee}) \;: (\cat{C}^\wedge)^\op \to (\cat{C}^\wedge)^\vee`$ は余米田埋め込み。$`(\hyp)^\vee`$ は余前層の圏を作るオペレーター。
'$`*`$' は関手の図式順結合の演算子記号。
$`た = ({^\cat{C} た}) \;: \cat{C}^\op \to (\cat{C}^\wedge)^\vee`$ は淡中埋め込み（「高階関手の計算：米田と淡中の周辺 // 評価関手と淡中埋め込み」を参照）。
$`\cong`$ は関手圏における同型（関手の自然同型）。

ところが、$`よ * よ^\vee \cong た`$ という単純な形は許されず、色々と細工したりゴタゴタと断り書きを付けたりする必要があります。僕は、細工や断り書きにウンザリしています。単純明快・ストレートな記述を阻んでいる“なにか”がありそうです。

$`よ * よ^\vee \cong た`$ が許されない事情を書いてみると：

関手 $`よ`$ の余域は $`\cat{C}^\wedge`$ であり、一方の関手 $`よ^\vee`$ の余域は $`(\cat{C}^\wedge)^\op`$ なので、結合はできない。
仮に $`よ * よ^\vee`$ 相当の関手を細工して作ったにしても、その域は $`\cat{C}`$ であり、一方の関手 $`た`$ の域は $`\cat{C}^\op`$ だから、自然同型で比較はできない。

$`{^\op}`$ が付いたり付かなかったりが、関手の自由な結合と比較を邪魔しているのです。$`{^\op}`$ を使う主たる理由は、反変関手を共変化するためです。となると、「反変関手の共変化がよろしくない」と見当が付きます。

現代の主流の圏論では、ほんとの反変関手〈genuine contravariant functor〉を扱うことを避けて、代理となる共変関手を使っています。それが反変関手と呼ぶ共変関手です。

反変関手を共変化して、すべてを共変関手として扱うことは多くの場合便利で、議論を単純化します。しかし、米田埋め込みを繰り返すような場合は、議論を複雑化させてしまいます。要するに、反変関手の共変化は万能ではなくて、不向きな状況もある、ということです。

$`よ * よ^\vee \cong た`$ を、単純明快・ストレートに記述するためには：

$`よ * よ^\vee \cong た`$ が単純明快・ストレートに記述できれば、淡中再構成はワンステップで出てきます。