\def\pgfsysdriver{pgfsys-dvipdfmx.def} % ★PGFドライバを強制
\documentclass{amsart}
\usepackage[left=2cm, right=2cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{amsfonts, amsthm, amssymb, mathtools,etoolbox}
\usepackage{blindtext}
\usepackage[colorlinks=true, urlcolor=blue, linkcolor=blue, citecolor=blue]{hyperref}
\usepackage{tikz,tikz-cd}
\usepackage{cleveref}
\usepackage{array}
\usepackage[style=alphabetic,sorting=nyt]{biblatex}
\renewbibmacro{in:}{}
% \addbibresource{biblio.bib}
\addbibresource{CommonBiblio20240922.bib}
\tikzset{pullback/.style={minimum size=1.2ex,path picture={
\draw[opacity=1,black,-,#1] (-0.5ex,-0.5ex) -- (0.5ex,-0.5ex) -- (0.5ex,0.5ex);%
}}}
\usetikzlibrary{calc}
\usepackage{epigraph}


\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{todo}[theorem]{Todo}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{fact}[theorem]{Fact}

\theoremstyle{definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{question}[theorem]{Question}
\newtheorem{answer}[theorem]{Answer}
\newtheorem{problem}[theorem]{Problem}
\newtheorem{slogan}[theorem]{Slogan}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\dq}[1]{``#1"}
\newcommand{\memo}[1]{\textcolor{red}{memo: #1}}
\newcommand{\invmemo}[1]{\textcolor{blue}{本当は話したいこと: #1}}
\newcommand{\summary}[1]{\textcolor{green!70!black}{\textbf{summary: #1}}}
\newcommand{\para}[1]{\paragraph{\textbf{#1}}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\ob}{\mathrm{ob}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\Top}{\mathbf{Top}}
\newcommand{\Group}{\mathbf{Group}}
\newcommand{\fg}{\mathrm{f.g.}}
\newcommand{\fgf}{\mathrm{f.g.f.}}
\newcommand{\Topprof}{\mathbf{Top}_{\textrm{prof.}}}
\newcommand{\BoolAlg}{\mathbf{BoolAlg}}
\newcommand{\Topoi}{\mathbf{Topoi}}
\newcommand{\FinSet}{\mathbf{FinSet}}
\newcommand{\PSh}{\mathbf{PSh}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Cont}{\mathbf{Cont}}
\newcommand{\Func}[2]{\mathbf{Func}(#1,#2)}
\newcommand{\Funcpd}[2]{\mathbf{Func}^{\mathrm{fin.prd.}}(#1,#2)}
\newcommand{\T}{\mathbb{T}}
\newcommand{\abs}[1]{\left|#1\right|}
\newcommand{\demph}[1]{\textbf{#1}}
\font\maljapanese=dmjhira at 2.5ex
\newcommand{\yo}{\textrm{\!\maljapanese\char"48}}
\newcommand{\Pow}{\mathcal{P}}
\newcommand{\Open}{\mathcal{O}}
\newcommand{\Int}{\mathrm{Int}}
\newcommand{\ignore}[1]{{\color{red!70!black} #1}}

\title{トポス理論と博論の概略}
\author{Ryuya Hora}
\thanks{Graduate School of Mathematical Sciences, University of Tokyo. \url{hora@ms.u-tokyo.ac.jp}}
% % \date{\today}
% \subjclass[2020]{MSC}
% \keywords{Keywords}


\begin{document}
\begin{abstract}
このノートは，池先生に洞の博士論文の内容を説明するセミナーの参考資料である．
最初の$3$パートで，「幾何学と論理学をつなぐ理論」としてのトポス理論を幾何学者向けに話す．
最後の$1$パートで，博士論文の$3$つの主定理について概説する．
\end{abstract}
\maketitle


\ignore{無視すると幾らかの正確さが失われるが，}赤い文字は無視して良い．
\tableofcontents
目的
\begin{itemize}
    \item \Cref{part:Geometry} トポスが位相空間の一般化であることを説明し，トポスと幾何学的射の定義を復習する．
    \item \Cref{part:Logic} 論理学におけるトポスの役割を概観する．特に，「意味 vs 構文」という論理学における二項対立がトポスへ統一される歴史をたどる．
    \item \Cref{part:Bridge} 幾何学と論理学の双方にトポスが現れる理由について，「ベン図$\to$ストーン双対$\to$トポス」の順番で歴史的に説明する．
    \item \Cref{part:PhDthesis}: 博士論文の内容である，トポスに関する$3$つの定理を概説する．
\end{itemize}




% \part{トポス入門}
% \section{幾何学におけるトポス (15分)}
% \section{論理学におけるトポス (15分)}
% \section{なぜ繋がるのか？(30分)}
% \part{トポス理論入門}\label{sec:ToposTheory}
% \ignore{トポスが幾何と論理の双方に本質的に現れるということを説明する．全体に共通する思想は，\demph{操作論的}であるということで，超越的な仮定を置かず，「実際に我々に操作可能なもの」に徹底的に還元する立場である．}



\part{幾何学におけるトポス (Grothendieck のトポス)(15 min)}\label{part:Geometry}

\section{位相空間の一般化としてのトポス}

位相空間$X$に対して，その上の(集合値)層の圏を$\Sh(X)$と書く．このとき，位相空間$X$が最悪でなければ\footnote{Soberであれば，の意味．例えば，Hausdorff空間や多様体やschemeはsober．}，$X$は圏$\Sh(X)$から復元できる．この意味で，位相空間上の層の圏は位相空間の情報を十分に持っていると言える．\memo{微分構造や構造層などの付加構造も，$\Sh(X)$への付加構造だと思える．}

Grothendieckは，幾何学的道具(コホモロジーや基本群など)を数論へ応用できるようにするため，空間概念を拡張しようと試みた．そして，彼は
\[
\begin{tikzcd}
\text{空間}
  \arrow[r]
&
\text{空間上の層(=\dq{計測\footnote{arpentage\cite{grothendieck1992recoltes}}})}%
\end{tikzcd}
\]

というこれまでの枠組みを反転させ，
\[
\begin{tikzcd}
\text{空間}
&
\text{空間上の層(=\dq{計測})}\arrow[l]
\end{tikzcd}
\]
という\dq{操作論的な}立場に立った．
そして，位相空間上の層の圏を公理化したものを「空間にとって最も本質的なものの受肉\cite{grothendieck1992recoltes}」であるとし，\demph{トポス}と名付けた．

\begin{definition}[\cite{grothendieck1972SGA4}]
    圏$\E$がGrothendieck トポス\footnote{トポスと呼ばれる概念は二つある．Grothendieck トポスは，\cite{grothendieck1972SGA4}でtoposと呼ばれている概念である．Lawvereらによって導入された初等トポスは，Grothendieck トポスを含むより大きな圏のクラスである．See also \cite{johnstone2002sketchesv1, johnstone2002sketchesv2, maclane1994sheaves, caramello2018theories}.}であるとは，以下の同値な条件のいずれか，従って全てを満たすことをいう．
    \begin{itemize}
        \item ある小さい景$(\C,J)$が存在し，$\E\simeq \Sh(\C,J)$となる．
        \item $\E$は以下の圏論的条件を満たす．
        \begin{itemize}
        \item ある小圏$\C$が存在し，
            \item $\C$の前層圏$\PSh(\C)\coloneqq \Func{\C^{\op}}{\Set}$に$\E$は忠実充満に埋め込め$i\colon \E \hookrightarrow \PSh(\C)$,
            \item さらに埋め込み$i$は左随伴$L\dashv i$を持ち，
            \item さらに$L$は有限極限を保つ.
    \end{itemize}
        \item \ignore{$\E$はlocally presentableな初等トポスである．}
    \end{itemize}
\end{definition}


\section{連続写像の一般化としての幾何学的射}
さらに，トポス理論は連続写像の概念も一般化する．
\begin{fact}
    任意の連続写像$f\colon X\to Y$は，層の圏の間の随伴
\[
\begin{tikzcd}
\Sh(X)
  \arrow[r, shift right=1.4ex, "f_*"']
  \arrow[r, phantom, "\rotatebox{270}{$\dashv$}" description]
&
\Sh(Y)
  \arrow[l, shift right=1.4ex, "f^*"']
\end{tikzcd}
\]
を誘導し，さらに引き戻し関手$f^*$は有限極限を保つ．
\end{fact}

% 連続写像の概念の一般化も同様に存在する．
\begin{definition}[幾何学的射]
    トポス$\E$からトポス$\F$への\demph{幾何学的射}$f\colon \E \to \F$とは，随伴
    \[
\begin{tikzcd}
\E
  \arrow[r, shift right=1.4ex, "f_*"']
  \arrow[r, phantom, "\rotatebox{270}{$\dashv$}" description]
&
\F
  \arrow[l, shift right=1.4ex, "f^*"']
\end{tikzcd}
\]であって，左随伴部分$f^*$が有限極限を保つもののことをいう．
\end{definition}

引き戻し関手$f^*\colon \Sh(Y)\to \Sh(X)$を$X$は幾何学的射である．さらに，連続写像$f$は，「$X,Y$がsoberである」という非常にマイルドな条件を満たすとき，幾何学的射$f^*\colon \Sh(Y)\to \Sh(X)$から復元される．





\begin{fact}[トポスは位相空間の一般化]
    層の圏をとる操作$\Sh:\Top \to \Topoi$は，位相空間の圏$\Top$をだいたい\footnote{厳密には，$\Top$をsoberな位相空間の圏 (もしくは，より自然にはLocaleの圏)に取り替える必要がある．さらに，$\Topoi$は本来$2$圏なので，$2$圏的な構造も考慮する必要がある．この$2$点を訂正すれば厳密な主張になる．}忠実充満にトポスと幾何学的射の圏$\Topoi$に埋め込む.
\end{fact}

\begin{remark}\label{トポスの点}
    トポス$\E$の点とは，$1$点上の層のトポス$\Sh(1)$，つまり$\Set$からの幾何学的射のことを言う．
\end{remark}


% \section{思想と広がり}

\memo{その思想: 群論的操作を空間とみなす．}

\part{論理学におけるトポス  (Lawvere のトポス) (25 min)}\label{part:Logic}

{論理学とトポスは密接に結びついているという事実}
\begin{itemize}
    \item \demph{連続体仮説の$ZFC$からの独立性}の Cohen トポスによる証明 (cf. \cite{maclane1994sheaves})
    \item \demph{選択公理の$ZF$からの独立性}のFreyd toposによる証明 \cite{freyd1980axiom}
    \item 様相論理の可能世界意味論と，トポスの内部言語 (cf. \cite{maclane1994sheaves})
    \item 時間軸\footnote{$+$ 付加構造}上の層のトポスを用いた，時制論理とシステムの\demph{安全性検証}\cite{schultz2019temporal}
    \item ボーアトポスを用いた，\demph{量子基礎論}\cite{landsman2017foundations}
    \item Lawvere-Tierney位相を用いた\demph{計算可能性理論} \cite{kihara2023lawvere}
    \item Schanuel toposを用いた\demph{選択公理}の(より繊細な)破壊 (\cite{fourman1980sheaf}+ongoing)
    \item Classifying topos of geometric theory
    \item Deligne's theorem (ある種の景に関する，stalk functorの存在定理)を用いた，ゲーデルの完全性定理の証明
\end{itemize}


\subsection{「意味 vs 構文」からトポスへの歴史 (1/3) Signifi\'e \texorpdfstring{$\leftarrow$}{leftarrow} Signifiant}
論理学では，「意味 vs 構文」という二項対立を理解することが重要である．この二項対立は，言語学における「Signifi\'e (指し示されるもの) vs Signifiant (指し示すもの)」という二項対立とパラレルである．

\[
\begin{tikzcd}[column sep = 80 pt]
    \text{Signifi\'e} & \text{Signifiant}\ar[l, "\text{指し示す}"']
\end{tikzcd}
\]

\[
\begin{tikzcd}[column sep = 80 pt]
    \text{意味} & \text{構文}\ar[l, "\text{}"']
\end{tikzcd}
\]

% \[
% \begin{tikzcd}[column sep = 80 pt]
%     {\color{blue} \bullet} & \text{`青'}\ar[l, ""']
% \end{tikzcd}
% \]

\[
\begin{tikzcd}[column sep = 80 pt]
    {\tikz[baseline=-0.6ex]\node[fill=blue, circle, minimum size=20pt, inner sep=0pt]{};}
      & \text{`青'} \ar[l, ""']
\end{tikzcd}
\]




\subsection{「意味 vs 構文」からトポスへの歴史 (2/3) 意味の圏 \texorpdfstring{$\leftarrow$}{leftarrow} 構文の圏}
Lawvereの博士論文\cite{lawvere1963functorial}は，上記の矢印を本当に関手にするものだった．
最初の\footnote{歴史的に最初，という意味ではない．}考察は，以下の命題である．
\begin{fact}
    有限生成自由群の圏を$\Group_{\fgf}$とし，有限直積を保つ関手圏を$\Funcpd{-}{-}$で書くことにすると，以下の圏同値が成立する．
    \begin{itemize}
        \item $\Funcpd{\Group_{\fgf}^\op}{\Set} \simeq \Group$
        \item $\Funcpd{\Group_{\fgf}^\op}{\Top} \simeq \text{位相群の圏}$
         \item $\Funcpd{\Group_{\fgf}^\op}{\mathbf{Manifolds}} \simeq \text{リー群の圏}$
    \end{itemize}
\end{fact}

{
\centering
\begin{description}
    \item[群] 
    \begin{tikzcd}[column sep = 80 pt]
    \Set & \Group_{\fgf}^\op\ar[l, "\mathrm{fin.prd.}"']
    \end{tikzcd}
    \item[位相群] 
    \begin{tikzcd}[column sep = 80 pt]
    \Top & \Group_{\fgf}^\op\ar[l, "\mathrm{fin.prd.}"']
    \end{tikzcd}
    \item[リー群] 
    \begin{tikzcd}[column sep = 80 pt]
    \mathbf{Manifolds} & \Group_{\fgf}^\op\ar[l, "\mathrm{fin.prd.}"']
    \end{tikzcd}
\end{description}
}

「群論」を記述する記号的方法はいろいろある\footnote{例えば左単位性は無駄とか}が，そのどれを用いても$\Group_{\fgf}^\op$は圏同値になる．Lawvereは，$\Group_{\fgf}^\op$という\demph{圏こそが「群論」であると考えた．}

彼はより一般に，任意の代数理論\footnote{等式だけで定義される理論．例えば群論や環論など．体論は$x\neq 0 \implies \exists y, x\cdot y=1$という公理で$\neq$とか$\exists$を使っているのでダメ．}$\T$に対して，その\demph{構文圏}$\C_{\T}$を有限生成自由$\T$代数の圏のoppositeとして定義し\footnote{これは実際に構文的に, つまり記号列の組合せ論を用いて，定義できる．}，これが理論である，考えた．

そして，一般に
\[
\Funcpd{\C_\T}{\E}\simeq \text{($\E$における理論$\T$のモデルの圏)}
\]
を証明した．

このような，
\begin{itemize}
    \item 理論 $=$ 圏
    \item 意味(モデル) $=$ 構造を保つ関手
\end{itemize}
という枠組みを\demph{関手的意味論}という．
\[
\begin{tikzcd}[column sep = 80 pt]
    \text{意味の圏}\E & \text{構文の圏}\C_\T\ar[l, "\text{構造を保つ関手}"']
\end{tikzcd}
\]

\subsection{「意味 vs 構文」からトポスへの歴史 (3/3) トポス \texorpdfstring{$\to$}{to} トポス}
Lawvereの博士論文の段階では，圏論的意味論は代数理論に限られていた．しかし，その範囲は拡大に拡大を続け，現代では一階述語論理(我々が普段数学をやっているZFCはこれ)を含む\footnote{適切な変換のもとで}範囲を扱えるようになっている．そのために必要な道具がトポスである．

理論\footnote{扱える理論のクラスは，現代ではgeometric theoryという名前が付けられている．ここでは，代数理論はもちろん，体論，局所環論，圏論，順序集合論，集合論など，普段の数学を大抵扱える．}$\T$に対して，その\demph{分類トポス} $\E_\T$ ($=$ 構文トポス)を考えることができる．そして，任意のトポス$\F$について，
\[
\Topoi(\F, \E_\T) \simeq \text{(トポス$\F$における理論$\T$のモデルの圏)}
\]
が成立する．

\begin{itemize}
    \item 「意味の圏」も「構文の圏」もトポスである
    \item 扱える理論$\T$の範囲が(ほとんど無制限に)広がっている．
    % \item 射の向きが逆転している．
\end{itemize}


ここで，射の向きが逆転していることに注意．関手的意味論のこれまでの文脈合わせるなら，一義的には
    \begin{tikzcd}[column sep = 80 pt]
    \F& \E_\T\ar[l, "\mathrm{fin.prd.}+ \mathrm{sml.colim.}"']
\end{tikzcd}
を考えることになるのだが，この関手は右随伴を持ち，ちょうど逆向きの幾何学的射の概念と一致している\footnote{これはいわゆる「代数と幾何の双対性」の一種である．}．
\[
\begin{tikzcd}[column sep = 150pt]
    \F & \C_\T\text{: 構文圏}\ar[l, "\text{関手的意味論}"'{name=A}]\\
    \F\ar[r, "\text{幾何学的射}"'{name=B}] & \E_\T\text{: 分類トポス$=$moduli}\ar[from = A, to = B, phantom , "\rotatebox{90}{$=$}"]
\end{tikzcd}
\]

分類トポス$\E_\T$は，moduli spaceのようなものである．実際，$\E_\T$の点$\Set= \Sh(1) \to \E_\T$は$\T$の$\Set$でのモデルと対応する．
\begin{figure}[ht]
    \centering

% \begin{tikzcd}[column sep = 200 pt]
%     {\tikz[baseline=-0.6ex]\node[fill=blue, circle, minimum size=20pt, inner sep=0pt]{};}
%       & \text{`青'} \ar[l, "\text{一つのモデルを選ぶ}"']
% \end{tikzcd}

    \begin{tikzpicture}[scale= 0.06]

    \node (B) at (25,100) {\huge `青'};
    % 0～1 の範囲で R,G,B を定義（常に「青寄り」になるように調整）
        \pgfmathsetmacro{\R}{0.10 + 0.40*(10/50)}  % 左→右で赤みが増える
        \pgfmathsetmacro{\G}{0.15 + 0.55*(40/50)}  % 下→上で緑が増える
        \pgfmathsetmacro{\B}{1}                 % 青は常に強め

        % 毎回その座標用の色を定義
        \definecolor{myblue}{rgb}{\R,\G,\B}
    \node[fill=myblue, circle, minimum size=30pt, inner sep=0pt] (C) at (-100, 100) {};
    \draw[thick, black, ->] (B) -- (C);
    \node[anchor=south] at (-37.5, 100) {モデルを一つ選ぶ};


    \node (A) at (-100,25) [circle, fill=black, inner sep=0.5pt] {};
    
    % x, y によって RGB が連続的に変わるような色場
    % x, y は 0,...,50 の格子点
    \foreach \x in {0,...,50}{
      \foreach \y in {0,...,50}{
        % 0～1 の範囲で R,G,B を定義（常に「青寄り」になるように調整）
        \pgfmathsetmacro{\R}{0.10 + 0.40*(\x/50)}  % 左→右で赤みが増える
        \pgfmathsetmacro{\G}{0.15 + 0.55*(\y/50)}  % 下→上で緑が増える
        \pgfmathsetmacro{\B}{1}                 % 青は常に強め

        % 毎回その座標用の色を定義
        \definecolor{myblue}{rgb}{\R,\G,\B}

        % 小さな矩形を塗ることで，連続的なグラデーションっぽく見せる
        \fill[myblue, draw=none] (\x,\y) rectangle ++(1.1,1.1);
      }
    }
    \draw[->, thick, black] (A) --(10,40);
    \node[anchor=south] at (-37.5, 20) {点を一つ選ぶ};
    \node at (-37.5, 70) {\huge\rotatebox{90}{$=$}};
    \node[anchor=north] at (25, 0) {青のmoduli space};
\end{tikzpicture}
    \caption{moduliを考えると射の向きが反転する}
    \label{fig:ModuliConverting}
\end{figure}




\begin{example}
以下のような例がある
    \begin{itemize}
        \item $\Topoi(\Set, \E_{\text{群論}}) \cong \Group$
        \item $\Topoi(\Set, \E_{\text{$\mathbb{C}$-線型空間}}) \cong \mathbf{Vect}_{\mathbb{C}}$
        \item $\Topoi(\Sh(X), \E_{\text{$\mathbb{C}$-線型空間}}) \cong \text{$X$上の$\mathbb{C}$-線型空間の層の圏}$
        \item $\Topoi(\PSh(G), \E_{\text{$\mathbb{C}$-線型空間}}) \cong \text{群$G$の表現の圏}$
        \item $\Topoi(\Cont(\widehat{G}), \E_{\text{$\mathbb{C}$-線型空間}}) \cong \text{profinite群$\widehat{G}$のsmooth表現の圏}$
    \end{itemize}
\end{example}

% \begin{remark}
%     ゲーデルの完全性定理は，coherentトポスにおける点の存在定理 ($=$ Deligneの定理)から従う(というか\dq{同一}になる)．
% \end{remark}

\begin{fact}[Topos theory = theory of theories]
    任意のgeometric theoryは分類トポスを持つ．さらに，任意のGrothendieck トポスは，あるgeometric theoryの分類トポスと同値である．
\end{fact}


\begin{table}[ht]
    \centering
    \begin{tabular}{|c|c|}\hline
         理論 $\T$& 分類トポス$\E_\T$\\\hline
         モデル& 点 \\\hline
         公理の追加& 部分空間\\\hline
         コンパクト性& コンパクト性\\\hline
         ゲーデルの完全性定理& (Deligne's)点の存在定理\\\hline
         理論の等価性& 同相 (=圏同値)\\\hline
         定数記号の追加& \'{e}tale cover\\ \hline
    \end{tabular}
\end{table}


\part{論理学と幾何学をつなぐトポス理論 (35 min)}\label{part:Bridge}

\begin{itemize}
    \item トポスは「操作の圏」であり，トポスによる架橋は\demph{空間への操作と論理的操作の対応}によって実現している．
    \item 「空間への操作と論理的操作の対応」という原理の原型は，ベン図(より正確にはオイラー図)まで遡ることができる．
    \item 
\end{itemize}
\subsection{「論理 vs 幾何」からトポスへの歴史(1/4) 命題 vs ベン図}

\begin{quote}Leonhard Euler \cite{Euler1761LettreCIII}:
    これらの丸い図形，いやむしろ(どのような形を与えようともかまわないのですから)\textbf{空間}は，この主題についての考察を容易にするのに非常に適しており，\textbf{論理学}の中で自慢げに語られ，多大な苦労をして証明される神秘の全てを，私たちに明らかにしてくれるのです\footnote{著者訳, 強調も著者による．原文: Ces figures rondes, ou plutôt ces espaces (car il n'importe quelle figure nous leur donnions) sont très propres à faciliter nos réflexions sur cette matière, \& à nous découvrir tous les mystères dont on se vante dans la Logique, \& qu'on y démontre avec bien de la peine, ...
% pendant que par le moyen de ces signes tout saute d'abord aux yeux.
}．
\end{quote}

\subsection{「論理 vs 幾何」からトポスへの歴史(2/4) ブール代数 vs profinite space}

\begin{definition}[ブール代数(雑)]
    ブール代数とは，集合$B$とその上の$0$項演算($=$元)$\top, \bot\in A$と$2$項演算$\land, \lor \to\colon B^2\to B$の組であって，普通の論理学における等式
    \begin{itemize}
        \item $p\land p = p$
        \item $p\lor (p\to\bot) = \top$ (排中律)
    \end{itemize}
    を全て満たすものをいう．ブール代数とブール代数準同型\footnote{普通の定義}の圏を，$\BoolAlg$と書く．
\end{definition}

\begin{lemma}
    任意の位相空間$X$について，そのclopen set全体$B(X)$は(普通の集合演算で)ブール代数になる．
\end{lemma}
この構成$B$は，反変関手
\[
B \colon \Top^\op \to \BoolAlg
\]
を定める．この関手は，定義域を制限することで，profinite space\footnote{位相空間がprofiniteであるとは，totally disconnected compact Hausdorffであることをいう．}と連続写像の圏$\Topprof$との圏同値を誘導する．これが\demph{ストーン双対}である．
\begin{fact}[ストーン双対{\cite{stone1936theory, stone1937applications, doctor1964categories}}]
    $\BoolAlg^{\op} \simeq \Topprof$
\end{fact}
See also \cite{johnstone1982stone}.

この圏同値は，「論理学的操作とトポロジカルな操作の等価性」というスローガンに合致するものではあるが，
\begin{itemize}
    \item 対応する空間のクラスが狭すぎる (Clopenで復元できるような空間しか扱えない．)
    \item 扱える論理のクラスが狭すぎる (量化子$\exists, \forall$を扱えない)
\end{itemize}
という欠点がある．

\subsection{「論理 vs 幾何」からトポスへの歴史 (3/4) 直観主義論理 vs 位相空間}
ストーン双対では，Clopenで復元できるような空間しか扱えなかった．一般のsoberな位相空間($=$開集合から復元できる位相空間)を扱うには，どうすればいいだろうか？

\begin{definition}[frame]
    \demph{Frame}とは，任意サイズのinfとsupを持つ順序集合$F$であって，さらに以下の同値な\footnote{同値性は随伴関手定理から従う．}条件を満たすものをいう．
    \begin{itemize}
        \item 任意の$x\in F$と$\{y_i\}_{i\in I}$について，
        \[
        x\land\left(\bigvee_{i\in I} y_i\right) = \bigvee_{i\in I} (x\land y_i).
        \]
        \item 任意の$x\in F$について，$x\land -\colon F \to F$は右随伴$x\to -\colon F \to F$を持つ．
        \[
        (x\land y \leq z) \text{ if and only if } y\leq x\to z
        \]
    \end{itemize}
\end{definition}
See \cite{maclane1994sheaves} for now.


\begin{example}
    任意の位相空間$X$について，そのopen subset全体のなす順序集合$\Open(X)$はframeである．$X$がsoberなら，位相空間$X$はframe$\Open(X)$から復元できる．
\end{example}

\begin{remark}
    Frameの圏のoppositeとして，\demph{locale}の圏が定義される．このlocaleという概念は，いわゆるpoint-less topologyの研究対象である．定義から自明な反変圏同値
    \[
    \mathbf{Frame}^{\op} \simeq \mathbf{Locale}
    \]
    はストーン双対の一般化\footnote{Profinite spaceはsoberなので，$\Topprof$はfully faithfulに$\mathbf{Locale}$へ埋め込める．一方，一般のブール代数は決してframeではないが，(一見非自明だがよく考えると当たり前な方法で)ブール代数からframeを構成できて，この構成によって$\mathbf{Frame}$へ埋め込める}と見做せる．
\end{remark}

Frameの概念は，直観主義命題論理($=$ 排中律を仮定しない命題論理)と密接に関係している．デモンストレーションとして，\demph{直観主義命題論理では二重否定除去が証明不可能であることの証明}をしよう．

証明とは，有限な文字列を有限的な操作用いて，特定の文字列に変形できるか？という類のパズルであるので，良い不変量を持ってくれば不可能性を証明できそうである．実際，frameは直観主義論理の証明に関する良い\footnote{完全な}不変量\footnote{この文章では，「不変量」と「意味論」は類義語だと思って良い．}になっている．

    命題記号の集合$V$(例えば$V=\{p,q\}$)とframe $F$を任意にとる．$V$の元$p$について，$F$の元$U_p\in F$を(なんでもいいので)とる．このとき，$V$から$\top, \bot, \land \lor,\to$を用いて帰納的に作られる命題$\phi$ ($\phi$は例えば$p\lor q$や$p \to \bot$など)に対して，$U_{\phi}\in F$を以下で帰納的に定義する．
\begin{itemize}
    \item $U_\top \coloneqq (F\text{の最大元})$, 
    \item $U_\bot \coloneqq (F\text{の最小元})$,
    \item $U_{\phi\land \psi} \coloneqq U_{\phi}\land U_{\psi}$,
    \item $U_{\phi\lor \psi} \coloneqq U_{\phi}\lor U_{\psi}$,
    \item $U_{\phi\to \psi} \coloneqq U_{\phi}\to U_{\psi}$.
\end{itemize}
と定める．すると，以下が成り立つ．
\begin{fact}
    命題$\phi$から命題$\psi$を導く証明が存在するとき，(frame $F$や$U_p,U_q$の選択に依存せずに) \[U_\phi \leq U_\psi\]が成立する．
\end{fact}
\begin{proof}[Sketch of proof]
    証明で許された有限個の導出規則に関して，帰納法を用いる．例えば，$\phi\land (\phi\to \psi)$から$\psi$を導いて良いという規則(モーダス・ポーネンス)に関する帰納法のステップでは，
    \[
    U_{\phi \land(\phi \to \psi)} \leq U_\psi
    \]
    を示す必要がある．これは，
    随伴
    \[
\begin{tikzcd}[column sep = 50 pt]
F
  \arrow[r, shift right=1.4ex, "U_\phi \to {-}"']
  \arrow[r, phantom, "\rotatebox{270}{$\dashv$}" description]
&
F
  \arrow[l, shift right=1.4ex, "U_\phi \land {-}"']
\end{tikzcd}
\]
の$U_\psi \in F$におけるcounit
\[
U_\phi \land(U_\phi \to U_\psi) \leq U_\psi
\]
の左辺を$U_\phi \land(U_\phi \to U_\psi) = U_{\phi \land(\phi \to \psi)}$と書き換えることで証明できる．
\end{proof}

\begin{proposition}
    直観主義命題論理では，$(p\to \bot)\to \bot$から$p$は証明できない．
\end{proposition}
\begin{proof}
% $\top$\footnote{仮定なしであることと，$\top$を仮定することは同じことである．$0=0$}から$p\lor (p\to\bot)$が証明できないことを，上のFactを用いて示そう．

任意の位相空間$X$とその任意の開集合$U\in \Open(X)$について，$U$の\dq{否定}$U\to \emptyset$は$U$と交わらない最大の開集合，つまり補集合の内部$\Int(U^c)$である．よって，$\Int(\Int(U^c)^c) \not\subset U$となる例を一つ見つけてくれば良い．
    例えば，frame $F$として，$F=\Open(\R)$をとり，$U_p=\R\backslash\{0\}$と定める．このとき，$U_{p\to \bot} = \Int(U_p^c) = \emptyset$となり，$U_{(p\to \bot)\to \bot} = \Int(\emptyset^c) = \R$となる．
    \[
    U_{(p\to \bot)\to \bot} = \R \not \subset \R\backslash\{0\} = U_p
    \]
    なので，もし$(p\to \bot)\to \bot$から$p$が証明できたら上記のFactに矛盾する．
\end{proof}



\subsection{「論理 vs 幾何」からトポスへの歴史 (4/4) 量化子 vs 層}
これまでは，量化子のない論理を，空間の開集合で考えてきた．しかし，我々の論理には量化子$\exists, \forall$は必須であるから，幾何学側にも対応物が欲しい．実は，量化子を扱う方法こそが，\demph{層}である\cite{lawvere1970quantifiers}．


\[
\begin{tikzcd}[column sep= 80pt]
    \text{命題論理} \ar[r, dashed, "+\text{量化子$\exists, \forall$}"]\ar[d,"\text{\dq{不変量}}"]& \text{述語論理}\ar[d,"\text{\dq{不変量}}"]\\
    \text{開集合のなす順序集合} \ar[r, dashed, "+\text{fiberの豊かさ}"]& \text{層のなす圏=\demph{トポス}}
\end{tikzcd}
\]

量化子を扱えるということは，ほとんどの数学を扱えるということである\footnote{集合論を扱えるという意味では，正当化できるだろう．}

\begin{example}
    Cohen toposは，排中律や選択公理を満たすが，連続体仮説を満たさない．これは，Cohen強制法によるZFCからの連続体仮説の独立性証明と同じものである．
\end{example}

位相空間の開集合が命題論理の不変量理論なのであれば，大袈裟に言えば，トポスは「数学そのもの」の不変量理論であると言える．



\section{Lawvereの7つの未解決問題}
残念ながらLawvereは2023年に亡くなった．しかし2009年，既に70歳を超えていたLawvereは，集会でトポスの7つの未解決問題を提示し，次のように述べた．
\begin{quote}
    F. William Lawvere \cite{lawvere2025opennLab}: ここに挙げる七つの問題は，私がまだ解くことができていないものである．
これらが明確になれば，トポス理論やその熱力学，代数幾何学，論理学への応用の研究は，さらに前進するだろう\footnote{著者訳.原文: Here are seven problems that I have not yet been able to solve. Clarification on them would further advance work on topos theory and its applications to thermomechanics, to algebraic geometry, and to logic.}.
\end{quote}

\begin{enumerate}
    \item Quotient Toposes
    \item Subquotients and Idempotents
\item Boundaries of classes of models
\item The jump operator on levels within a topos
\item Coverings that admit averaging and microlinearity
\item How strong is the adjointness of fractional exponents?
\item The algebra of time
\end{enumerate}
進捗状況は\url{https://ncatlab.org/nlab/show/Open+problems+in+topos+theory}で
見ることができる．

\newpage
\part{博士論文概説(45 min)}\label{part:PhDthesis}
\section{toposの完全連結性 (15 min)}\cite{hora2025grothendieck}\\

トポス$\E$の持つ様々な幾何学的な性質は，$\E$から$\Set$への唯一の幾何学的射
\[
f\colon \E\leftarrow \Set
\]
の性質で表現される．
例えば，
\begin{description}
    \item[連結性] トポス$\E$が\demph{連結}であるのは，\underline{$f^*$が忠実充満}であるとき．
    % これは位相空間の連結性と整合的である．
    任意の位相空間$X$について，$X$が位相空間として連結なこととトポス$\Sh(X)$が連結なことは同値である．
    \item[局所連結性] トポス$\E$が\demph{局所連結}であるのは，\underline{$f^*$が左随伴を持つ}とき．
    % これは位相空間の局所連結性と整合的である．
    任意の位相空間$X$について，$X$が位相空間として局所連結なこととトポス$\Sh(X)$が局所連結なことは同値である．
    \item[局所性]  トポス$\E$が\demph{局所}であるのは，\underline{$f^*$が右随伴の右随伴を持つ}とき．
    任意の可換環$A$について，$A$が局所環なこととトポス$\Sh(\mathrm{Spec}A)$が局所なことは同値である．
\end{description}


\cite{hora2025grothendieck}を元にした博論の第一部では，まず$f^*$の左右に続く随伴列を分類することで，「随伴の存在」として語ることができるトポスの性質が$5$つであることを示した．さらに，その中で極端に研究が少ない\footnote{ないわけではない．\cite{hemelaer2021monoid}}ものを「完全連結性」と呼ぶことにした\footnote{本当のモチベーションはこのような技術的なものではなくて別にあるのだが...}．
\begin{definition}
    トポス$\E$が\demph{完全連結}であるとは，$f^*$が左随伴の左随伴を持つことをいう．
\end{definition}

完全連結性は，これまで調べられてきたトポスの連結性概念\ignore{(連結性，局所連結性，安定局所連結性\cite{johnstone2011remarks}強連結性，トータル連結性\cite{bunge1996spreads})}のどれよりも強い，非常に極端な連結性概念である．それにもかかわらず，次が成立する．
\begin{proposition}[完全連結トポスは少なすぎない{\cite{hora2025grothendieck}}]
    \ignore{任意のトポスはある完全連結トポスの閉部分トポスである．}
\end{proposition}

完全連結性の定義は，\ignore{局所トポスの定義の「右随伴」を「左随伴」に形式的に変更したものになっており，}一見双対概念のように見える．しかし，\ignore{そもそもトポスの双対圏がトポスになることはほとんどなく\footnote{$\E$も$\E^\op$もトポスであれば，どちらも$1$点圏になる．}，}この双対性を数学的に記述するのは難しそうに見える．しかし，\cite{hora2025grothendieck}では，完全連結性が局所性と\dq{双対な\ignore{景による}特徴づけ}を持つことを示した．\ignore{この定理は，論文中の用語を用いて次のように述べられている．
\begin{theorem}\cite{hora2025grothendieck}
    トポスが完全連結であることと，ある完全連結景上の層の圏であることとは同値である．
\end{theorem}}

\invmemo{次の予想を示したい．良いトポスには，その双対トポスが存在する．互いに双対であるトポスについては，それらの次元の完備束が同型になる．}
\section{toposの商に関するLawvereの問題 (15 min)}\cite{kamio2024solution}\\

トポスにも，商の概念がある．
\begin{definition}[商トポス]
    \ignore{トポス$\E$の(連結)\demph{商トポス}とは，$\E$からの幾何学的射$f\colon \E \leftarrow \F$であって$f^+\colon \F \to \E$が忠実充満なものをいう．}
\end{definition}
商の概念は，トポスの論理学でも自然に現れる．例えば，(内部)選択公理を満たさないようなトポスの最も簡単な構成\footnote{基礎の公理を満たさないので独立性証明には使えないらしい．}は，Freydの論文「選択公理\cite{freyd1980axiom}」の導入部にも書かれている通り，\ignore{群$\Z$作用のトポス$\PSh(\Z)$の}商をとることである．
\invmemo{Grothendieck-Galois / Permutation modelとの関係}

しかし，\ignore{「部分トポスと様相演算子の対応定理」と対照的に，}商トポスの振る舞いに関する理論的成果はあまり知られていなかった．商トポスは本当に統制できないほどめちゃくちゃに氾濫しているのだろうか?それとも実は\ignore{部分トポスのように，商トポスにも}「商トポスと??の対応定理」が存在しているのだろうか?この問いこそがLawvereの未解決問題の第一問であった．

\begin{quote}\cite{lawvere2025opennLab}
    Is there a Grothendieck topos for which the number of these quotients is not small? At the other extreme, could they be parameterized internally, as subtoposes are?
\end{quote}

未解決問題は二つの部分に分かれている．後半は，「商トポスと??の対応定理」が存在するかを聞いていて，これは著者の修論の一部\cite{hora2024internal}で部分的に\footnote{部分的と言ったものの，\cite{johnstone2025remarks}でJohnstoneが言ったように，これこそがLawvereが\dq{本来問うべきだった問い}の答えであったと思う．}肯定した．博論第二部の元になった\cite{kamio2024solution}では，前半の問いにYesと回答している．つまり，あるトポスが真クラス個の商を持つことを示した．
\begin{theorem}\cite{kamio2024solution}
    \ignore{可算無限生成自由モノイド作用の}トポス\ignore{$\PSh(M_\omega)$}は真クラス個の商トポスをもつ．
\end{theorem}
\ignore{そこでは，任意の集合上にリジッドな二項関係が入るというVopenka, Pultr, Hedrlinの結果\cite{vopvenka1965rigid}を用いている．}


\section{toposの次元に関するLawvereの問題 (15 min)}\cite{hora2025lawvere}\\

Lawvereは，彼の物理学的および関数解析的バックグラウンドから，特定のトポスに強い興味(執着?)を抱いていた．その一つが，\demph{ブール代数の分類トポス}\ignore{$\PSh(\FinSet_{>0})$}である．例えば，彼の論文「組合せトポロジーと関数解析における，余離散的対象で生成されたトポス
\cite{lawvere1988toposesGenerated}」の中で彼は，次のことを考えている．
\begin{question}[真と偽を幾何的に同一視するブール代数]
    Hausdorffな位相ブール代数\footnote{位相空間上のブール代数構造であって，全てのブール演算が連続になるようなもの．}であって，$\bot \neq \top$だが可縮なものはあるか？
\end{question}
\begin{answer}
    (weak)無限次元球面$S^\infty$ \cite{lawvere1988toposesGenerated}.
\end{answer}
彼はこのことを，まず$S^\infty$を関数空間$L^2([0,1])$に埋め込むことで実現し，さらにブール代数の分類トポス$\PSh(F)$の言葉で記述した．

この問題は，おそらく彼のヘーゲル哲学への情熱と関連している．(絵を書いて説明する) 実際，彼はトポスにおける\demph{アウフヘーベン}の概念を定義し\cite{lawvere1989display, lawvere1991more}，それを用いてトポスにおける次元論を展開した\cite{lawvere2006some}．Lawvereの未解決問題の4番は，ブール代数の分類トポスのアウフヘーベンを計算することである．
\begin{quote}\cite{lawvere2025opennLab}
    ... What is, in combinatorial or number theoretic terms, the way below relation for this basic topos?
\end{quote}

博論の第三部の元になった\cite{hora2025lawvere}では，\ignore{simplicial setに対する\cite{kennett2011levels}の手法を利用して，}この問題を解いた．その解答は，諸々の定義を省略して，以下の通りである．
\begin{theorem}\cite{hora2025lawvere}
    ブール代数の分類トポスのアウフヘーベンは，$l\geq 3$に対して$2l-1$である．
\end{theorem}





\appendix

\section{証明不可能性を証明して何が嬉しいのか}
論理学者(resp. 理論計算機学者)は，証明不可能性の証明 (resp. 計算不可能性の証明)をしたがる．


証明不可能性の証明の意義は，単なる好奇心や無駄な努力の排除，というだけではなく，より根源的な目的がある．
論理学者であるあなたは，新しい論理体系\footnote{例えば，排中律をなくしたシステムに別の公理を入れるとか，$\mathrm{ZFC}+\lnot \textrm{連続体仮説}$とか，
$\mathrm{ZF}+\lnot \textrm{選択公理}$とか，
もっとradicalなシステムなど}を提案する．
あなたの次の仕事は，
\[
\begin{tikzcd}[column sep = 50pt]
    \text{この論理体系が破綻していないこと}\ar[r, "\text{だいたい}", Leftrightarrow] &\demph{矛盾を証明できてしまわないこと}
\end{tikzcd}
\]
の証明である．

あなたが理論計算機科学者なら，新たなプログラミング言語や制御のためのシステムを考え，それが致命的な破綻をしないように保証する必要がある．その仕事は，実質的に証明不可能性の証明と同じものになる\footnote{cf. Curry-Howard(-Lambek) 対応, プログラム論理，モデル検査}．
\[
\begin{tikzcd}[column sep = 50pt]
    \text{計算システムの振る舞い}\ar[r, "\text{だいたい}", leftrightarrow] &\demph{対応する証明体系の振る舞い}
\end{tikzcd}
\]


\section{部分トポスの分類定理} 
Lawvereは，彼の論文「量化子と層」(Quantifiers and Sheaves \cite{lawvere1970quantifiers})の中で，Grothendieckの理論と論理の関係を明らかにした．トポスに対する理論は幾何学的解釈と論理学的解釈の二面性を持つとがわかった．数あるそのような「架橋の定理」の中でも，\cite{lawvere1970quantifiers}に現れる最も古典的な例が次である．
% 本来ならその主題である量化子の解釈について述べるべきだが(その時間はないので)，ここでは次の言葉を引用する．
\begin{quote} F. William Lawvere \cite{lawvere1970quantifiers}:
Grothendieck「位相」は様相演算子という形で最も自然に現れる．
\footnote{著者訳．原文:
    ... a Grothendieck \dq{topology} appears most naturally
as a modal operator ...}
% , of the nature \dq{it is locally the case that}, 
\end{quote}

この言葉は，通常次の定理の形で述べられる．

\begin{fact}
    任意のトポス$\E$について，以下の$2$つのデータには一対一対応が存在する．
    \begin{description}
        \item[部分空間] \ignore{$\E$の部分トポス, つまり$\E$への幾何学的射$\E \leftarrow \F \colon f^*$であって，忠実充満な右随伴を持つもの．}
        \item[様相演算子] \ignore{$\E$の部分対象分類子$\Omega$上の自己射$j\colon \Omega \to \Omega$ であって，
        \begin{enumerate}
            \item $j(\top )=\top$
            \item $j(j(p))=j(p)$
            \item $j(p\land q)=j(p)\land j(q)$
        \end{enumerate}
        を満たすもの．}
    \end{description}
\end{fact}
% \subsection*{Acknowledgment}
% ロジックが専門ではない友人として，事前に発表練習に付き合ってくれた高梨さんに感謝する．

\printbibliography

\end{document}