Lex ComonadでRight Kanへ帰着

## Trigger Notion「研究テーマ」DBの `When is a finite presheaf category a topos?`（優先度 Active、進行状況 ●●○、共著 Jeremie Marques）に残っていた手法のメモから瓶化した。原文は「Lex Comonadを用いて，Right Kan extensionの存在に帰着する．」。 既存の [[tk8psy]] は「\(\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 性の判定条件を、[[tk8psy]] にある十分条件「すべての slice \(\mathcal C/c\) が essentially finite」より広い形で与える。少なくとも、帰着が成立する条件そのものを特定する。 ## Personal context [[tk8psy]] は旧HP Problems 6.0.1 由来の公開問題で dormant のまま残っていた。こちらは同じ問いへの攻め口を手法として切り出したものである。Burnside rieg 由来の動機は [[suw4hw]] に繋がる。 ## 訂正（2026-08-16） 本文で Jeremie Marques を「共著」と書いたのは誤りである。Notion の `coresearcher` 欄の記載をそのまま共著と解釈したが、洞の確認により、この欄は共著者・議論した相手・謝辞に載せる人を区別せず含むことが分かった。[[tk8psy]] にも「Jeremie Marques と議論され」とある。**Jeremie Marques は議論した相手であり、論文の著者に名を連ねる関係ではない。**