Lex ComonadでRight Kanへ帰着

Trigger

Notion「研究テーマ」DBの When is a finite presheaf category a topos?（優先度 Active、進行状況 ●●○、共著 Jeremie Marques）に残っていた手法のメモから瓶化した。原文は「Lex Comonadを用いて，Right Kan extensionの存在に帰着する．」。

既存の Finite presheaf topoi は「$\mathbf{fPSh}(\mathcal C)$ がいつ elementary topos になるか」という問いそのものを述べるが、その判定を Right Kan extension の存在へ帰着させるという手法は入っていない。洞の判断で独立した瓶として立てる。

Idea

small category $\mathcal C$ に対し、有限前層のなす圏 $\mathbf{fPSh}(\mathcal C)$ が elementary topos（あるいは locally cartesian closed）になる条件を判定したい。

原メモの手法は、この判定を Lex Comonad を経由して Right Kan extension の存在問題へ帰着させるというものである。ここでどの comonad を指すか、また帰着の具体的な経路は原メモからは確定できない。想定される筋は、包含 $\mathbf{fPSh}(\mathcal C)\hookrightarrow \mathbf{PSh}(\mathcal C)$ に沿った右随伴の有限性保存に exponential の存在を帰着させる形だが、これは瓶化時の補完であって原メモの主張ではない。

原メモが同じ場所に並べている材料は次の二つ。

• 前層圏の subobject classifier がその圏に住んでいるかで、どこまで判定できるか。$\omega$ や simplex では住まないのではないか
• $\mathbf{FinSet}$ で必ず limit を持つような圏のクラスを考え、コンマ圏がその形になるという条件を課す

Goal

Lex Comonad と Right Kan extension による帰着を明示し、$\mathbf{fPSh}(\mathcal C)$ の topos 性の判定条件を、Finite presheaf topoi にある十分条件「すべての slice $\mathcal C/c$ が essentially finite」より広い形で与える。少なくとも、帰着が成立する条件そのものを特定する。

Personal context

Finite presheaf topoi は旧HP Problems 6.0.1 由来の公開問題で dormant のまま残っていた。こちらは同じ問いへの攻め口を手法として切り出したものである。Burnside rieg 由来の動機は Rieg theory: the research programme に繋がる。

訂正（2026-08-16）

本文で Jeremie Marques を「共著」と書いたのは誤りである。Notion の coresearcher 欄の記載をそのまま共著と解釈したが、洞の確認により、この欄は共著者・議論した相手・謝辞に載せる人を区別せず含むことが分かった。Finite presheaf topoi にも「Jeremie Marques と議論され」とある。Jeremie Marques は議論した相手であり、論文の著者に名を連ねる関係ではない。

@misc{sumire:2609.00007:8:v2,
  author = {hora},
  title = {{Lex ComonadでRight Kanへ帰着}},
  year = {2026},
  note = {SUMIRE:2609.00007/8, v2},
  url = {https://sumire.aiformath.jp/p/2609.00007/n/8/v/2}
}