双連続観測の一点評価
## Trigger
Kobin 全体の横断監査で，[[etdzdy]] の「独裁は表現可能性」と [[bpjn8j]] の「認識論的再構成」を，前層圏から集合への双連続な observer の分類として定理化した．
## Result
**定理（双連続観測の一点評価）．** 小さい Cauchy complete category \(\mathcal C\) と前層圏
\[
\widehat{\mathcal C}=[\mathcal C^{\mathrm{op}},\mathbf{Set}]
\]
を取る．すべての小極限とすべての小余極限を保つ関手
\[
F:\widehat{\mathcal C}\longrightarrow\mathbf{Set}
\]
は，ある \(c\in\mathcal C\) における evaluation と自然同型である：
\[
F(X)\cong X(c).
\]
\(\mathcal C\) が Cauchy complete でない場合，\(c\) は \(\operatorname{Kar}(\mathcal C)\) の対象として取れる．
## Proof
\(\widehat{\mathcal C}\) と \(\mathbf{Set}\) は locally presentable である．\(F\) は全余極限を保つので accessible であり，全極限も保つので adjoint functor theorem により左随伴
\[
L:\mathbf{Set}\rightleftarrows\widehat{\mathcal C}:F
\]
を持つ．\(P=L(1)\) と置けば
\[
F(X)\cong\mathbf{Set}(1,F(X))\cong\widehat{\mathcal C}(P,X).
\]
したがって \(F\) は \(P\) により表現される．さらに \(F\) は全余極限を保つので \(P\) は tiny projective である．
標準的な category-of-elements 表示
\[
P\cong\operatorname*{colim}_{(c,x)\in\int P}y(c)
\]
へ \(\widehat{\mathcal C}(P,-)\) を適用する．この関手は上の余極限を保つため，\(\operatorname{id}_P\) はある一つの成分から来る．従って，ある \(c\) と射
\[
P\xrightarrow{r}y(c)\xrightarrow{i}P,
\qquad ir=\operatorname{id}_P
\]
が存在し，\(P\) は representable の retract である．Cauchy completeness によりこの retract は representable \(y(d)\) である．Yoneda lemma から
\[
F(X)\cong\widehat{\mathcal C}(y(d),X)\cong X(d).
\]
## Interpretation
十分な exactness を持つ「全体から値を取り出す操作」は，generalized point ではなく一つの Cauchy point に硬化する．したがって
\[
\text{双連続 observer}=\text{representing point}
\]
である．Arrow 型の独裁を直接証明する定理ではないが，「独裁者＝合意形成作用を表現する一点」という物語の厳密な圏論的原型を与える．
## Status
証明は自己完結しているが，文献上の既知性・priority は未監査である．