← phd-thesis-overview-seminar

ロジックセミナー20251205__main.tex

\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{remark}[theorem]{Remark}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{question}[theorem]{Question}
\newtheorem{answer}[theorem]{Answer}
\newtheorem{problem}[theorem]{Problem}
\newtheorem{slogan}[theorem]{Slogan}

\newcommand{\dq}[1]{``#1"}
\newcommand{\memo}[1]{\textcolor{green!70!black}{memo: #1}}
\newcommand{\yodan}[1]{\textcolor{blue}{余談: #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{\Grp}{\mathbf{Grp}}
\newcommand{\FinSet}{\mathbf{FinSet}}
\newcommand{\PSh}{\mathbf{PSh}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Cont}{\mathbf{Cont}}
\newcommand{\Func}[2]{[#1,#2]}
\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{\Sub}{\mathrm{Sub}}
\newcommand{\Loops}{\mathbf{Loops}}
\newcommand{\ZSet}{\mathrm{\Z\text{-}\Set}}
\newcommand{\NSet}{\mathrm{\N\text{-}\Set}}
\newcommand{\ignore}[1]{{\color{red!70!black} #1}}
\newcommand{\mono}{\mathrm{mono}}
\newcommand{\GSet}{G\text{-}\Set}
\newcommand{\SymA}{\mathrm{Sym}(A)}
\newcommand{\supp}{\mathrm{supp}}
\newcommand{\Fix}{\mathrm{Fix}}

\title{選択公理とLocal state classifier(とpermutation model?)}
\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}

\end{abstract}
\maketitle

\tableofcontents


\ignore{無視すると幾らかの正確さが失われるが，}赤い文字は無視して良い．

\section{イントロ}

\ignore{トポス理論は論理学と幾何学の間に様々な橋を架けている．
\begin{itemize}
    \item Geometric theoryの関手的意味論
    \item Kripke-Joyal semantics
    \item Mitchell-Bénabou language
    \item G\"{o}del completeness and Deligne's existence theorem
    \item Cohen topos and forcing topoi.
    \item Brouwer's topos, in which every $f\colon \R \to \R$ is continuous.
    \item Semantics of modal logic/type theory?
    \item Effective topos and computability? 木原先生とか
\end{itemize}
全くestablishedではないが，個人的に興味がある話も複数ある．
\begin{itemize}
    \item Subtopoi of $\Sigma$-$\Set$ and Cicho\'{n}'s diagram? (j.w.w. Morgan Rogers)
    \item Internal choice of the condensed math (j.w.w. Ivan Tomasic)(+斎藤毅先生との研究室ローテーション)
    \item Topos of games and game semantics (Ivan di liberti)
    \item LSC and the axiom of choice (j.w.w. Matias Menni)
    \item Representation theories of quivers, groups, profinite groups, and monoids as internal linear algebras on the weaker foundations.
\end{itemize}}

\ignore{これら全てを概観するのは時間的にも私の基礎論の知識的にも難しいので，}
今日は\ignore{このうち}
\begin{itemize}
    \item LSC and the axiom of choice 
\end{itemize}
\ignore{のみ}について話す．
\ignore{特に，本来はなすべき思想の部分や，最も重要なアイデアであるトポスの内部言語について言及しないこととする．}

今日の発表の(ストーリー上の)目標は，次の予想の数学的内容を伝えることである．
\begin{conjecture}
    Grothendieck topos $\E$について，$\E$が選択公理を満たすこととと，以下の$2$条件を同時に満たすことは，同値である．
    \begin{itemize}
        \item $\E$は排中律を満たす．
        \item $\E$のLSC $\Xi$は最小元をもつ．
    \end{itemize}
\end{conjecture}
\ignore{いくつかの状況証拠から，これはかなりありうる話だし，もしこれが正しければ私の知る限り選択公理が成り立つか調べる最も単純な方法になる．}

私個人の目的は，トポスの選択公理の話と，林さんが話していたような有限選択公理やpermutation model?とかで現れる群論の話との類似/関連について指摘していただくこと．

\section{予備知識}
\subsection{圏}
\subsection{極限，余極限}
\subsection{カルテシアン閉圏}
\section{Topos}
\subsection{topos}
\begin{definition}
    Elementary toposとは，圏$\E$であって以下の条件を満たすもののことを言う．
    \begin{itemize}
        \item \ignore{$\E$は全ての有限極限を持つ．
        \item $\E$は部分対象分類子を持つ．}
        \item $\E$はカルテシアン閉である．
    \end{itemize}
\end{definition}
\section{Toposの排中律}

\begin{fact}
    任意のトポス$\E$とその対象$X$について，その部分対象全体のなす順序集合$\Sub_{\E}(X)$はHeyting algebraである．
\end{fact}

\ignore{
\begin{example}
    位相空間$X$について，その開集合のなすHeyting algebra $\mathcal{O}(X)$も，この形で現れる．実際，$X$上の層のなすtopos $\Sh(X)$において，そのterminal object $1$の部分対象束$\Sub_{\Sh(X)}(1)$が$\mathcal{O}(X)$と一致する．これがtopological semanticsとの関係の一つ...のはず
\end{example}}



\begin{definition}
    Topos $\E$が\demph{Boolean}である($=$排中律を満たす)とは，任意の対象$X\in \ob(\E)$について，その部分対象束$\Sub_{\E}(X)$がBool代数であることを言う．
\end{definition}

\ignore{
\begin{fact}[排中律との関係]
    トポス$\E$について，$\E$がBooleanであることと，$\E$の内部言語で
    \[
    1_{\E}\Vdash \forall p\in \Omega, p\lor{\lnot p}
    \]
    が成立することと等価である．
\end{fact}
}
\yodan{任意の部分トポスがclopenなこととも同値で，排中律の持つ幾何学的な"バラバラさ"の一つの現れである． (もう一つの現れはStone dual)}

Boolean toposが重要な集合論的な理由は，そこからZFのモデルができることらしい．
\begin{quote}
    \cite[Section VI. Topoi and Logic]{maclane1994sheaves} any Boolean Grothendieck topos $\F$ gives a model of Zermelo--Fraenkel set theory, constructed by mimicking within $\F$ the standard formulation of the cumulative hierarchy.
\end{quote}
\yodan{Boolean topos $\E$で基礎の公理が成り立つ理由はここにはなく，成り立たせるためにvon Neumann hierarchyの類似でwell-founded part $\E \supset\E_{\mathrm{w.f.}}$をとる．これは典型的なhyperconnected quotientである．}

\section{Toposの選択公理}

\subsection{排中律を満たすトポス}

\ignore{
「トポス$\E$が選択公理を満たす」という条件は，本来なら$\E$の\dq{内部言語}を用いて，
\[
1_{\E}\Vdash \forall f \in Y^X \left((\forall y\in Y, \exists x\in X,f(x)=y)\to (\exists s\in X^Y, \forall y \in Y, fs(y)=y)\right)
\]
と定義する．(cf. \cite[312]{maclane1994sheaves}) しかし，これと同値であることが知られている次の条件を今日は定義にする．
}

\begin{definition}
    Topos $\E$が\demph{選択公理\footnote{トポス理論に出てくる選択公理には外部選択公理と内部選択公理の$2$種類があり，今回は内部選択公理の方．内部が我々にとって嬉しい方で，実際，独立性証明で使われるのはこっちらしい．}を満たす}とは，任意の対象$X$についてその指数関手
    \[
    {-}^X\colon \E \to \E
    \]
    がepi射を保つことをいう．
\end{definition}

\begin{example}
    $\E=\Set$の場合を考える．集合$X$をとってきたとき，指数関手${-}^X\colon \Set \to \Set$は単にHom関手$\Set(X,-)$のこと．これがepi射=全射$f\colon Y \to Z$を保つというのは，
    \[
    \begin{tikzcd}
        &Y\ar[d,"f", twoheadrightarrow]\\
        X\ar[r, "h"]\ar[ru, dashed, "\exists ! \hat{h}"]&Z
    \end{tikzcd}
    \]
    と言う条件．これは選択公理．よって，(あなたが選択公理を認めれば)$\Set$は選択公理を満たす．
\end{example}

\ignore{
\begin{example}[Group(oid) action topos]
    $\Set^G$
\end{example}
\begin{example}[Cohen topos]
    
\end{example}
}

\subsection{排中律を満たさないトポス}

\begin{proposition}
    Grothendieck topos $\E$が選択公理を満たすとき，$\E$は排中律を満たす．
\end{proposition}

\begin{proposition}
    Grothendieck topos $\E$が選択公理を満たすとき，$\E$のinhabited objectsはsmall productをとる操作で閉じている．
\end{proposition}
\yodan{non-empty objects (=open dense support)は閉じていない．(Baire空間でやると...?)}
\memo{proof書く}





\section{LSC and normal filter}

$\ZSet$と$\Loops$の関係は，次の$2$つの方法で捉えられる:
\begin{itemize}
    \item $\Loops$は$\ZSet$のfull subcategoryであって，幾つもの操作で閉じている．
    \item $\Loops$は$\ZSet$のうち，$\Z$-actionのstabilizerに制約を設けたものである．
\end{itemize}

\subsection{商トポスと超連結商トポス}
\begin{definition}
    Grothendieck topos $\E$の\demph{商トポス}\footnote{これは普通の定義ではない．普通の定義との同値性は，Vopenka principleを仮定すると知られているが，仮定せずに示せるかは多分まだ未解決...?\memo{cite}}とは，$\E$のfull subcategory$\E\supset \F$であって以下の条件を満たすもの:
    \begin{itemize}
        \item $\F$は($\E$の)有限極限で閉じている．
        \item $\F$はsmall colimitで閉じている．
    \end{itemize}
    \demph{超連結商トポス} (hyperconnected quotient) とは，商トポス$\E\supset\F$であってさらに追加の条件
    \begin{itemize}
        \item $\F$は部分対象をとる操作で閉じている．
    \end{itemize}
    を満たすことをいう．
\end{definition}

\begin{proposition}
    Grothendieck topos $\E$が排中律を満たすなら，
    \begin{itemize}
        \item $\E$の商トポスも全て排中律を満たし，
        \item $\E$の商トポスは全て超連結である．
    \end{itemize}
\end{proposition}

\subsection{Local state classifier}
LSCについて\cite[Section 2]{hora2025normalizationv1}に基づいて簡単に説明する．
もう少し血の通った説明と，証明，例などは元論文\cite{hora2024internal}にある．

\subsubsection{定義}
\begin{definition}[{\cite[][Definition 3.4]{hora2024internal}}]
    圏 $\E$ の\demph{local state classifier} (以下，LSC) とは，$\E$ のすべてのmono射の余極限のことである．つまり，対象 $\Xi$ と射の族 $\{\xi_X \colon X \to \Xi\}_{X\in \ob(\E)}$であって，埋め込み関手 $\E_{\mono}\rightarrowtail \E$のcolimit coconeになるものである．
\end{definition}
このような大きなcolimitは大抵の場合存在しない\footnote{cf. \url{https://ncatlab.org/nlab/show/large\%2Bcocompleteness}}が，次を示せる．
\begin{proposition}[{\cite[][Section 3.16]{hora2024internal}}]\label{prop:ExistenceForGrothendieck}
    任意のGrothendieck topos $\E$ はLSCを持つ．
\end{proposition}

\begin{example}
    群$G$について，$\GSet$のLSCは，$G$の部分群全体からなる順序集合$\Sub_{\Grp}(G)$に，共役作用を入れたものである．$\xi_{X}\colon X \to \Xi$は，各元$x\in X$をそのstabilizerに送る．
\end{example}


\subsubsection{LSCのfilterが誘導する full subcategory}\label{sssec:InducedFullSub}
LSC $\Xi$ の任意の部分対象から $\E$ のfull subcategoryを構成できる．
圏$\E$ がLSC $\Xi$ をもつとして，
任意の部分対象 $\iota_F\colon F \rightarrowtail\Xi$
に対して，次の条件でfull subcategory $\E_F \hookrightarrow \E$ を定める．
\begin{equation}\label{eq:FullSubCondition}
    X\in \ob(\E_F)
\iff
\begin{tikzcd}
    & F\ar[d, rightarrowtail, "\iota_F"]\\
    X\ar[r,"\xi_X"']\ar[ru, dashed, "\exists"]&\Xi.
\end{tikzcd}
\end{equation}
つまり，full subcategory $\E_F$ を
\[
\ob(\E_F) \coloneqq \{X\in \ob(\E)\mid \text{射 $\xi_X$ が $F\rightarrowtail \Xi$ を経由する}\}
\]
で定める．

\subsubsection{LSCの半束構造}
LSCは，圏 $\E$ の直積構造を反映した半束構造を持つ．(ここが選択公理っぽさ！)
\begin{proposition}[{\cite[][Proposition 3.27]{hora2024internal}}]\label{prop:SemilatticeStructure}
    topos $\E$ のLSC $\{\xi_X\colon X\to \Xi\}_{X\in \ob (\E)}$ は，以下の条件を満たす内部 $\land$-半束構造をただ一つ持つ．
    \begin{itemize}
        \item 任意有限個の対象 $X_1, \dots, X_n \in \ob(\E),\; n\geq 0$ に対して
    \[
    \begin{tikzcd}[column sep =5pt]
        &X_1\times \dots \times X_n \ar[ld, "(\xi_{X_1}) \times \dots \times (\xi_{X_n})"']\ar[rd, "\xi_{(X_1 \times \dots \times X_n)}"]&\\
        \Xi^n\ar[rr,"\land"']&&\Xi
    \end{tikzcd}
    \]
    が可換になる．
    \end{itemize}
\end{proposition}
\begin{example}
    $\GSet$では，部分群のintersectionをとる操作になる．
\end{example}

% この内部半束構造は，各対象 $X\in \ob(\E)$ に対し，$\Xi$ へのホム集合 $\E(X,\Xi)$ の上に（通常の）半束構造を誘導する．したがって，各ホム集合 $\E(X, \Xi)$ には，$f\leq g \iff f\land g =f$ によって自然な半順序が入る．

\subsubsection{The classification theorem}
% 部分対象 $\iota_F \colon F \rightarrowtail \Xi$ が\demph{internal filter}であるとは，各包含写像 $\E(X,F) \rightarrowtail \E(X,\Xi)$ の像が通常の意味でfilter（すなわち，上に閉じていて，有限積 $\top, \land$ に関して閉じている部分集合）となることをいう．（\cite{hora2024internal} では，局所的大圏に対しても意味を持つように，著者はinternal filterの図式的な定義を採用している．）


\cite{hora2024internal} では，$\E$トポスで
部分対象 $F\rightarrowtail\Xi$ がinternal filterなら，
誘導されるfull subcategory $\E\supset \E_F$が超連結商トポスになることが示され，それが以下の一対一対応を与えることを示している．
\begin{theorem}[{\cite[][Theorem 4.1]{hora2024internal}}]
    任意のGrothendieck topos $\E$について，以下の$2$つのデータの間の一対一対応がある:
    \begin{itemize}
        \item $\E$ の超連結商トポス．
        \item LSC $\Xi$ のinternal filter．
    \end{itemize}
\end{theorem}

\begin{example}
    群$G$について，$\GSet$における$\Xi$のinternal filter$F\subset \Xi$は以下のように書き下される．$F\subset \Xi$は$\Xi=\Sub_{\Grp}(G)$の部分集合，つまり$G$の部分群からなる集合，であって以下を満たすもの．
    \begin{description}
        \item[nullary inf] $G\in F$
        \item[binary inf] 任意の$H, H'\in F$について $H\cap H'\in F$
        \item[upward closed] $(H\in F \land H\subset H') \implies H'\in F$
        \item[\dq{internal}] 任意の$H\in F$と$g\in G$について$gHg^{-1}\in F$
    \end{description}
\end{example}

\begin{example}[Schanuel topos(とpermutation model?)]\memo{知らないなりにNotationを寄せてみた}
$A$を可算無限集合とする．$A$上の置換(全単射自己写像の意味)全体からなる群を$\SymA$とかく．$\SymA\text{-}\Set$は排中律も選択公理も満たす．

一方，$\SymA$のinternal filter $F\subset \Sub_{\Grp}(\SymA)$を，任意の有限集合$S\subset A$について
\[
\Fix(S)\coloneqq \{\sigma \in \SymA\mid \sigma\restriction_{S} =\id_{S}\}
\]
が$F$に入るような最小のinternal filter $F$として定義する．すると，対応するトポス$\SymA\text{-}\Set_{F}$は\demph{Schanuel topos} \ignore{$\Sh(\FinSet^\op_{\mono}, \lnot \lnot)$}と一致し，排中律は満たすが選択公理は満たさない．nLab\footnote{cf. nLab \url{https://ncatlab.org/nlab/show/Schanuel+topos}}には
\begin{quote}
    It can be viewed as a category-theoretic variant of the Fraenkel-Mostowski model of set theory.
\end{quote}
と書いてある\footnote{LSCを使うところ以外は古典的な話のはずなので， \cite{fourman1980sheaf}とかを読むべき?}．
\end{example}



\subsection{LSCと選択公理}
\begin{conjecture}\label{conj:ac}
    Boolean Grothendieck topos $\E$について，以下は同値
    \begin{itemize}
        \item $\E$は選択公理を満たす．
        \item $\E$のLSCは最小元$\bot \colon 1_{\E} \to \Xi$を持つ．
    \end{itemize}
\end{conjecture}
\ignore{
この予想は，次のより広い予想の特別な場合である．
\begin{conjecture}\label{conj:etendue}
    Grothendieck topos $\E$について，以下は同値
    \begin{itemize}
        \item $\E$はétendue.
        \item $\E$のLSCは最小元$\bot \colon 1_{\E} \to \Xi$を持つ．
    \end{itemize}
\end{conjecture}
この予想の幾何学的文脈は\cite{menni2025nonsingular}で言及されていて，Menniもこの予想を支持すると言ってくれた．\Cref{conj:etendue} から \Cref{conj:ac}が従うことは，以下の定理からわかる．
\begin{fact}[Freyd-Scedrov ?]
    Grothendieck topos $\E$ について，$\E$が選択公理を満たすことと，$\E$がBoolean étendueであることは同値である．
\end{fact}
\yodan{étendueとロジックといえば，\dq{uniformly co-ordinatisable theory}とétendueの論文をJoshuaが出していた\cite{wrigley2025theories}}
}

\appendix
\section{多分読むべき文献}
\begin{itemize}
    \item \cite{freyd1980axiom}: The axiom of choice. 部分的に読んだ．ここでは(位相)群作用は基礎の公理満たしてないから役に立たない，みたいなことを言われている．
    \item \cite{fourman1980sheaf}: Sheaf models for set theory これのsection 3を読むべきそう．
    \item \cite{freyd1987all}: All topoi are localic or why permutation models prevail 名前からして関わりそう．
\end{itemize}

\printbibliography
\end{document}