Math-Talk with ChatGPT in 2026 Sep

このテキストは、Colin McLartyの次のビデオ講義をきっかけとして、ChatGPTと丸山の数学についての対話をまとめたものである。

Colin McLarty — “Nonetheless one should learn the language of topos: Grothendieck...” [2018] の要約

https://www.youtube.com/watch?v=vmcbm5FxRJE

(00:03–01:27) 1973年 Buffalo 講義の背景
Grothendieck は1970年代初めに「組織化された数学研究」から離れることを表明していましたが、1973年 Buffalo で topos・代数幾何・代数群について講義しました。Topos 講義は当初約10時間の予定だったものが大幅に膨らみ、最終的には小グループでの討論を含め約33時間に及びます。McLarty は、この録音から Grothendieck 自身が topos をどう考えていたかを再構成します。
(01:27–16:32) Grothendieck にとって「圏論」が始まったのは1955年
1950年代初頭にも tensor product などを universal property で扱っていましたが、Grothendieck 自身は「categories を始めたのは1955年頃」と述べています。McLarty は、その理由を Kansas paper と Tohoku paper に求めます。決定的なのは、対象の内部構造を見るのでなく、積・極限・完全性など圏そのものの抽象的性質だけから、群・monoid・torsor などを定義するという発想でした。Grothendieck にとってこれこそが本格的な「category theory / general nonsense」だった、と McLarty は論じます。
(17:49–22:49) Tohoku 論文：cohomology を「exactness の公理」から取り出す
Tohoku 論文では、具体的な元や section に依存せず、AB5 category のような exactness 条件だけで圏を特徴づけ、injective object と cohomology を扱いました。これは Reinhold Baer の module に関する議論を圏論的に一般化したものです。重要なのは、一定の条件を満たす抽象圏には標準的な cohomology theory が存在すると示した点で、後の étale cohomology と topos の構想を支える一方の柱になります。
(22:49–35:43) Topos の核心：「Sets と同じように振る舞う sheaf の圏」
Buffalo 講義で Grothendieck が繰り返す直観は、topos は概略、集合の圏 Sets と同じ exactness 性質をもつ圏だというものです。特に
arbitrary direct limits（任意の colimits）＋ finite inverse limits（有限 limits）
が中心になります。しかし Grothendieck は形式的公理だけでなく、topos を一般化された空間として考えるべきだと強調します。topos 内の object は「終対象の上の étale space」のようなもの、arrow も domain が codomain の上に étale に乗っているものとして考える――厳密には正しくなくても、その幾何学的言語こそ重要だという姿勢です。
(35:43–46:59) McLarty が提案する「topos の誕生日」：1958年4月21日
McLarty はかなり具体的に、topos の発想が生まれた日を Monday, April 21, 1958 と推定します。この日 Pierre Cartier が unramified coverings を使った一次元 cohomology の進展を講演し、その直後 Grothendieck が「これは全次元で働く」と反応したという Jean-Pierre Serre の証言があります。McLarty の解釈では、Grothendieck はそこで、Kansas paper の sheaf / covering の考え方 + Tohoku paper の abstract cohomologyを一気に結びつけたのです。
(46:59–54:29) 「公理化」から site と sheaf による構成へ
Grothendieck は当初、sheaf category を exactness axioms だけで特徴づけようとしましたが、十分きれいな公理系を見つけられませんでした。そこで「generator をどう貼り合わせるか」を記述する site → presheaf → sheaf という方法へ移ります。これが Grothendieck topology / site の形成につながります。その後 Giraud が intrinsic な topos axioms を与えますが、Grothendieck にとって site や Giraud axioms は重要ではあってもややtechnicalであり、topos の本質的な理解そのものではありませんでした。
(55:08–1:13:32) Topos は「大きな圏」であると同時に、その背後の「小さな幾何学的空間」
Grothendieck が特に重視したのが geometric morphism です。通常の空間 $X,Y$ なら、sheaf topoi の morphism が連続写像 $X\to Y$ に対応するので、topos は genuine な幾何学的対象として扱えるはずだ、と考えます。彼は「category of sheaves」と、その背後にある「real honest thing」としての空間を概念的に区別したがりました。しかしその「空間」を圏以外の方法では定義できない。この緊張こそ Buffalo 講義の重要なテーマです。幾何学的言語が多少 “abusive” でも、それを捨てると幾何学的直観そのものを失うと Grothendieck は考えました。
(1:14:11–1:18:28) Universal algebra と classifying topos
Grothendieck はさらに、ある種の代数理論と topos の間の対応を考えます。講演ではまだ不完全で誤りもありましたが、「algebraic structure を与えること」と「その classifying topos を与えること」の間に equivalence があるという方向です。現在なら Morita equivalence や classifying topoi と結びつく発想であり、McLarty は Olivia Caramello などの現代的研究との連続性を指摘しています。
(1:18:28–1:30:58) Universes・Weil conjectures、そして「だから topos の言語を学ぶべきだ」
終盤では set-theoretic universe の問題や Deligne の Weil conjectures の証明が話題になります。Grothendieck 自身も、étale cohomology の核心だけなら topos theory 全体や universes は形式的には不要かもしれないと認めます。それでも彼は、“one should learn the language of topos” という立場を崩しません。McLarty はこれを「建物の基礎」にたとえます。住人は基礎工事を毎日意識する必要はない。しかし誰かが基礎を厳密に作ったからこそ、上に安心して建物を建てられる。SGA 4 の目的も、数学者が毎回 foundational details をやり直さず、topos の言語を自由に使えるほど基礎を完成させることだった、というのが講演全体の結論です。

講演全体を一言でいうと

McLarty が描く Grothendieck の topos は、単なる「sheaf の圏の公理化」ではありません。
cohomology を可能にする抽象的 exactness、局所データを貼り合わせる sheaf、そして空間として考える幾何学的直観――この三つを一つの言語にしたものが topos である、という歴史的・数学的解釈です。

Learn more on Glasp: https://glasp.co/reader?url=https%3A%2F%2Fwww.youtube.com%2Fwatch%3Fv%3Dvmcbm5FxRJE

このビデオで紹介されているGrothendieck のtopos と Lawvere のElementary Topos の関係を論じてください。

はい。このビデオを踏まえると、Grothendieck の topos と Lawvere–Tierney の Elementary Topos の関係は、「一般化された空間」と「一般化された集合世界」という二つの見方が、同じ圏論的構造の中で出会ったものと捉えるのがよいと思います。

最初に結論を図式で書くと、

です。

しかし逆は一般には成り立ちません。

この包含関係の背後に、Grothendieck と Lawvere の思想の違いがあります。(ケンブリッジ大学出版局)

1. Grothendieck の出発点は「集合」ではなく「空間」

今回の McLarty のビデオで最も強調されている点はここです。

Grothendieck が topos を考えた直接の動機は、

étale cohomology
sheaf
covering
algebraic geometry

でした。

つまり、

「集合論をもっと一般化してみよう」

として topos を作ったわけではありません。

むしろ、

$\text{space} \longrightarrow \text{sheaves on the space}$

という考えを極端に押し進めます。

普通の位相空間 $X$ なら、

$X \quad\rightsquigarrow\quad \operatorname{Sh}(X)$

があります。

そこで Grothendieck は、

本当の「空間」は点集合 $X$ そのものではなく、
その上の sheaf 全体の圏によって表現できるのではないか。

と考え始める。

ビデオの 57分以降で繰り返されている、

generalized topological space

という発想です。

McLarty も歴史的に、topos の起源を「一般化された集合論」と説明するのは誤解で、幾何学・位相・代数から生じたものだと強調しています。(RCNi Company Limited)

2. Lawvere は Grothendieck topos の「有限的な核心」を取り出した

ここから Lawvere が登場します。

Grothendieck topos は通常、

$\operatorname{Sh}(C,J)$

つまり site $(C,J)$ 上の sheaf の圏として作られます。

しかし Lawvere は1960年代後半に、

この巨大な sheaf 構成の中で、本当に本質的なのは何なのか？

と問います。

McLarty の歴史研究によれば、Lawvere は Grothendieck topoi が非常に複雑な集合論的構成になっているのを見て、その本質はもっと単純な公理で捉えられるはずだと考えました。これが Myles Tierney との Elementary Topos につながります。(物理学と天文学の静的ウェブページ)

Lawvere–Tierney の答えは驚くほど短いものです。

圏 $\mathcal E$ が Elementary Topos であるとは、基本的には

$\boxed{ \begin{aligned} &1.\quad \text{finite limits がある}\\ &2.\quad \text{exponentials }Y^X\text{ がある}\\ &3.\quad \text{subobject classifier }\Omega\text{ がある} \end{aligned}}$

ことです。(CiteSeerX)

Grothendieck の site も sheaf condition も、この定義には出てきません。

ここが革命的です。

3. Grothendieck の「Sets と同じ exactness」と Lawvere の $\Omega$

ビデオで Grothendieck は何度も、

a topos has essentially the exactness properties of the category of sets

と言っています。

特に彼が強調するのは

$\text{arbitrary colimits} + \text{finite limits}$

です。

これは非常に Grothendieck 的 な topos の捉え方です。

一方 Lawvere は、Sets のもっと違う特徴に注目します。

Sets では、部分集合

$A\subseteq X$

は characteristic function

$\chi_A:X\to\{0,1\}$

で表せます。

Lawvere はこれを圏の中で抽象化して、

$\chi_A:X\to\Omega$

とします。

ここで

$\boxed{\Omega=\text{object of truth values}}$

です。

つまり Lawvere は、Grothendieck が

Sets のように振る舞う「幾何学的世界」

として見ていたものの中に、

真理値そのものを object として持つ論理世界

を発見したわけです。

4. その結果、topos の中で「論理」ができる

これが Lawvere の大きな飛躍です。

$\Omega$

があるため、topos 内部で

$\wedge,\quad \vee,\quad \Rightarrow,\quad \neg,\quad \forall,\quad\exists$

を解釈できます。

つまり Elementary Topos $\mathcal E$ は単なる圏ではなく、

$\boxed{\text{それ自身の内部論理を持つ数学的宇宙}}$

になります。

一般にはその論理は Boolean classical logic ではなく、

$\boxed{\text{intuitionistic logic}}$

です。

Lawvere 自身の1970年の論文 Quantifiers and Sheaves は、まさに「logic と geometry の統一」を主題としており、しかも彼自身はgeometry の側が主導的であると述べています。(Scribd)

ここは重要です。

しばしば

Grothendieck = geometry
Lawvere = logic

と単純化されますが、これは少し違います。

Lawvere 自身も geometry を捨てていません。

むしろ、

$\boxed{\text{geometry が logic を生み出す}}$

と考えているのです。

5. もっとも美しい接点：Grothendieck topology と Lawvere–Tierney topology

両者の関係を最も端的に示すのがこれです。

Grothendieck は小圏 $C$ に

$J$

という Grothendieck topology を置きます。

これは大雑把に言えば、

どの family が「局所的に全体を覆っている」とみなされるか

を指定します。

そして

$(C,J)$

から

$\operatorname{Sh}(C,J)$

を作ります。

Lawvere と Tierney は同じ notion を、topos の内部で記述できることに気づきます。

subobject classifier

$\Omega$

に対して

$\boxed{j:\Omega\to\Omega}$

という写像を考える。

これが Lawvere–Tierney topology です。

直観的には、

$j(p)$

を

「 $p$ は局所的には真である」

と読めます。

Lawvere 自身、この意味を “it is locally the case that” という modal な考えとして捉えています。(Scribd)

そして決定的な定理があります。

presheaf topos

$\widehat C = [C^{op},\mathbf{Set}]$

を考えると、

$\boxed{ \begin{array}{c} \text{Grothendieck topologies }J\text{ on }C \\[2mm] \Updownarrow \\[2mm] \text{Lawvere--Tierney topologies } j:\Omega\to\Omega \text{ on }\widehat C \end{array}}$

です。(Ncatlab)

しかも

$\boxed{ \operatorname{Sh}(C,J) \simeq \operatorname{Sh}_j(\widehat C) }$

になります。

私はこれが Grothendieck と Lawvere を結ぶ最も美しい公式だと思います。

6. 「外側からの topology」が「内側の modality」になった

この対応を概念的に見ると、さらに面白いです。

Grothendieck

外から site を見る。

$(C,J)$

そして

「この family は cover である」

と指定する。

Lawvere–Tierney

topos 内部から見る。

$j:\Omega\to\Omega$

そして

「この命題は locally true である」

と表す。

つまり、

$\boxed{ \text{covering} \quad\longleftrightarrow\quad \text{local truth} }$

です。

幾何学的な「局所性」が、

$\boxed{\text{modal logic}}$

になる。

これは topos theory の核心の一つです。

McLarty の著書も、Lawvere–Tierney topology を、Grothendieck が作った topology の elementary treatment と明示的に説明しています。(OUP Academic)

7. しかし Elementary Topos のほうがずっと広い

ここで数学的な違いをきちんと押さえる必要があります。

Grothendieck topos なら必ず

$\operatorname{Sh}(C,J)$

として、小さな site から作れます。

そのため、非常に豊富な infinitary structure を持っています。

一方 Elementary Topos は、

$\text{finite limits} +\text{exponentials} +\Omega$

だけです。

したがって、例えば任意の無限 coproduct を持つ必要さえありません。

簡単な例は

$\mathbf{FinSet}.$

有限集合の圏です。

これは

finite limits がある
$B^A$ も有限集合なので exponentials がある
$\Omega=\{0,1\}$ がある

ので Elementary Topos です。

しかし

$\coprod_{n\in\mathbb N}1$

は有限集合ではないので $\mathbf{FinSet}$ の中にはありません。

したがって Grothendieck topos ではありません。

つまり

$\boxed{ \text{Elementary Topos} = \text{Grothendieck topos の「有限的・論理的 core」を抽象化したもの} }$

とかなりよく言えます。

8. Giraud と Lawvere の違い

ビデオの Grothendieck は、Giraud の intrinsic axioms にも触れています。

Grothendieck topos を site を使わず圏論的に特徴づける方法として

$\text{Giraud's theorem}$

があります。

ざっくり言えば、

arbitrary colimits
finite limits
exactness
small generating family

などを課します。

これは Grothendieck がビデオで繰り返す

arbitrary direct limits + finite inverse limits

という感覚に非常に近いものです。

Lawvere の elementary axioms はそれよりずっと小さい。

	Grothendieck/Giraud	Lawvere–Tierney
極限	infinitary 条件を含む	essentially finite
generator	必要	不要
site	sheaf 表現可能	不要
$\Omega$	存在する	公理の中心
exponentials	存在する	公理の中心
主な直観	generalized space	generalized universe of sets
主な応用	geometry/cohomology	logic/foundations/geometry

したがって、

$\boxed{ \text{Giraud は Grothendieck topos を intrinsic にした} }$

のに対して、

$\boxed{ \text{Lawvere--Tierney はその構造の有限的 core を抽出した} }$

と言えるでしょう。

9. ところが、ビデオ後半の Grothendieck は Lawvere にかなり近づいている

今回のビデオで特に面白いのはここです。

Grothendieck は1973年 Buffalo で、

to give a type of algebraic structure seems to be the same as to give a topos — the so-called classifying topos

という趣旨のことを言っています。

ここでは topos はもう単に

$\text{space}$

ではありません。

ある algebraic theory のモデルを集約する

$\boxed{\text{classifying object}}$

になっています。

これは Lawvere の categorical logic の世界にかなり近い。

Lawvere の側では、

$\text{theory} \longleftrightarrow \text{category/topos}$

という対応を追究していました。

Grothendieck の幾何学的 topos と Lawvere の論理的 topos が、ここで合流します。

後に classifying topos の理論では、

$\boxed{ \text{geometric theory} \longleftrightarrow \text{Grothendieck classifying topos} }$

という形で極めて強力な対応になります。

そして異なる理論が同じ classifying topos を持つことを Morita equivalence と呼ぶ方向へ発展します。ビデオで McLarty が Olivia Caramello の仕事に触れているのも、まさにこの流れです。

10. 「空間」と「集合宇宙」は実は同じものの二面

ここが一番哲学的に重要だと思います。

Grothendieck は

$\mathcal E$

を外から見て、

$\boxed{\mathcal E=\text{generalized space}}$

と考える。

Lawvere は同じ $\mathcal E$ の中に入って

$\boxed{\mathcal E=\text{universe of variable sets}}$

と考える。

例えば普通の sheaf topos

$\operatorname{Sh}(X)$

では、object $F$ は外から見れば

空間 $X$ 上の sheaf

です。

しかし topos 内部から見れば、

$F$ は単なる「集合」

です。

ただし、その集合は場所 $x\in X$ によって姿を変える。

だからしばしば

$\boxed{\text{variable set}}$

と呼ばれます。

つまり

$\begin{array}{ccc} &\operatorname{Sh}(X)&\\[1mm] \text{外から見る}&\uparrow&\text{中から見る}\\ \text{geometry}&&\text{logic/set theory}\\ \text{sheaves over }X&&\text{sets varying over }X \end{array}$

となります。

11. したがって二人の違いを一言でいうなら

私は次のように整理すると、今回のビデオの意味が一番よく見えると思います。

Grothendieck

$\boxed{ \text{「空間とは何か」を sheaf の圏によって拡張した} }$

Lawvere

$\boxed{ \text{「集合の世界とは何か」を topos の内部構造によって拡張した} }$

しかしこの二つが偶然同じ構造になったのではありません。

もっと深く、

$\boxed{ \text{局所性をもった geometry} = \text{局所性をもった logic} }$

という原理がある。

Grothendieck の

$\text{cover}$

が Lawvere の

$\text{locally true}$

になり、

Grothendieck の

$\text{sheaf}$

が Lawvere の

$\text{variable set}$

になり、

Grothendieck の

$\text{generalized space}$

が Lawvere の

$\text{universe of discourse}$

になるわけです。

最後に、今回のビデオに即して最も重要な一点

Grothendieck は講演で、

幾何学的対象としての topos と、その上の sheaf category とを本当は区別したい。
しかし適切な言葉がまだない。

という趣旨のことを何度も言っています。

Lawvere の Elementary Topos は、この問題を単純に「解決」したわけではありません。

むしろ驚くべき方向にひっくり返しました。

$\boxed{ \text{その巨大な category 自体を一つの数学的 universe として読む} }$

ことにしたのです。

したがって、Grothendieck が

$\operatorname{Sh}(X)$

を通して背後の space $X$ を見ようとしたのに対して、

Lawvere は

$\operatorname{Sh}(X)$

の内部に入り、その中の sets・truth・logic を見る。

この

$\boxed{\text{外から見る geometry} \quad\leftrightarrow\quad \text{内から見る logic}}$

という双対的な視点こそ、Grothendieck topos から Elementary Topos への発展の本質だと思います。Lawvere 自身も、logic と geometry の「unity」を語りつつ geometry の側を主導的と位置づけていました。(Scribd)

もし次に進めるなら、Grothendieck topology $J$ が具体的にどう Lawvere–Tierney topology $j:\Omega\to\Omega$ に変換されるのかを、簡単な poset/site の例を一つ作って数式で追うと、この二つの topos の関係がかなり鮮明になります。

GrothendieckとLawvere – 二つの topos の関係

では、数式で一度「変換そのもの」を見てみましょう。ここが分かると、

\text{Grothendieck topology} \quad\leftrightarrow\quad \text{Lawvere--Tierney topology}

が単なる類似ではなく、同じ局所性を外側と内側から記述したものだということが見えてきます。小さい圏 $C$ 上では、Grothendieck topology と presheaf topos $\widehat C=[C^{op},\mathbf{Set}]$ 上の Lawvere–Tierney topology は実際に対応します。(Ncatlab)

1. まず、世界を二つの領域だけにする

非常に小さな圏 $C$ を考えます。

V\xrightarrow{i}U

対象は $U,V$ の二つだけです。

イメージとしては、

V=\text{より局所的な領域},\qquad U=\text{より大きな領域}

と思ってください。

そして、

\boxed{\{i:V\to U\}\text{ は }U\text{ を cover する}}

と宣言します。

これは説明用の toy site です。通常の位相空間の open cover だと思う必要はありません。

ここで Grothendieck topology $J$ が登場します。

2. Grothendieck は cover を「sieve」で表す

$U$ に入ってくる射は

id_U:U\to U, \qquad i:V\to U

です。

$U$ 上の sieve は、これらの射のうち、前合成について閉じたものです。

この小さな圏ではちょうど三つあります。

\begin{aligned} 0&=\varnothing,\\ S&=\{i\},\\ 1&=\{i,id_U\}. \end{aligned}

つまり、

\Omega(U)= \{\varnothing,\{i\},\{i,id_U\}\}.

一方 $V$ に入ってくる射は $id_V$ だけなので、

\Omega(V) = \{\varnothing,\{id_V\}\}.

実はすでにここで

\boxed{\Omega}

が出てきています。

presheaf topos

\widehat C=[C^{op},\mathbf{Set}]

では、subobject classifier は

\boxed{\Omega(U)= \{\text{\(U\) 上の sieves}\}}

なのです。(Ncatlab)

これが最初の重要な橋です。

3. なぜ sieve が「真理値」なのか

普通の集合論では真理値は

\Omega=\{0,1\}.

ところが presheaf topos では、真理値はもっと豊富です。

$U$ において

\varnothing

は

どこへ制限しても真ではない

という意味です。

一方、

\{i,id_U\}

は

$U$ ですでに真

という意味。

興味深いのが真ん中の

\boxed{\{i\}}.

これは、

$U$ 全体ではまだ真と言えないが、
$V$ に制限すれば真になる

という真理値です。

したがって

\boxed{ \Omega(U) = \{\text{false},\; \text{true locally on }V,\; \text{true}\} }

と読めます。

これが「variable truth」です。

4. ここで Grothendieck topology $J$ を指定する

今回、

\{i:V\to U\}

を cover と宣言しました。

したがって $U$ 上の covering sieves は

J(U) = \bigl\{ \{i\}, \{i,id_U\} \bigr\}.

$V$ では

J(V) = \bigl\{ \{id_V\} \bigr\}.

つまり、

\boxed{\{i\}\text{ は covering sieve}}

です。

ここまでは完全に Grothendieck の外部的な記述です。

5. では Lawvere–Tierney の $j:\Omega\to\Omega$ を作る

Grothendieck topology $J$ から、Lawvere–Tierney topology

\boxed{j:\Omega\longrightarrow\Omega}

を作る公式は、

\boxed{ j_U(S) = \left\{ f:W\to U \;\middle|\; f^*S\in J(W) \right\}. }

です。つまり、

$f$ に沿って $S$ を引き戻したとき、それが cover になるような $f$ を全部集める。

これだけです。

この公式が

\text{cover} \longrightarrow \text{modality}

への変換です。(Ncatlab)

6. 実際に三つの真理値に $j$ を作用させる

まず

S=\varnothing.

どこへ引き戻しても空です。

したがって cover にはなりません。

\boxed{j_U(\varnothing)=\varnothing}.

次に最大 sieve

S=\{i,id_U\}.

これはすでに完全に真ですから、

\boxed{ j_U(\{i,id_U\}) = \{i,id_U\}. }

そして核心が

S=\{i\}.

です。

$id_U$ に沿って引き戻せば

id_U^*S=S=\{i\}.

ところがこれは $U$ の covering sieve です。

したがって

id_U\in j_U(S).

また $i:V\to U$ に沿って引き戻すと、

i^*S=\{id_V\},

つまり $V$ の maximal sieve です。

当然 cover です。

したがって

i\in j_U(S).

よって

\boxed{ j_U(\{i\}) = \{i,id_U\}. }

7. これが全部です

したがって $U$ での $j$ は、

\begin{array}{c|c} p&j(p)\\ \hline \varnothing&\varnothing\\[2mm] \{i\}&\{i,id_U\}\\[2mm] \{i,id_U\}&\{i,id_U\} \end{array}

となります。

真理値として書けば、

\boxed{ \begin{array}{ccc} \text{false}&\mapsto&\text{false}\\ \text{locally true}&\mapsto&\text{true}\\ \text{true}&\mapsto&\text{true}. \end{array}}

つまり

\boxed{ j(p)=\text{「\(p\) は局所的に真である」} }

なのです。

ここで Grothendieck と Lawvere が完全につながります。

8. Grothendieck の cover が Lawvere の modality になる

Grothendieck は外側から

V\to U

を見て、

$V\to U$ は covering である。

と言います。

Lawvere は topos の内部から同じことを、

p\mapsto j(p)

として見て、

$p$ が cover 上で真なら、 $p$ は locally true である。

と言います。

したがって、

\boxed{ \begin{array}{ccc} \text{Grothendieck}&&\text{Lawvere--Tierney}\\[1mm] \hline \text{covering sieve}&&\text{local truth}\\ J&&j:\Omega\to\Omega\\ \text{geometry}&&\text{modality / logic} \end{array}}

となります。

9. 次に sheaf condition を計算してみる

ここがさらに面白いところです。

presheaf

F:C^{op}\to\mathbf{Set}

を一つ取ります。

これはこの小さい圏では単に

\boxed{ F(U)\xrightarrow{\rho}F(V) }

という集合の写像です。

反変なので

V\to U

に対して restriction

\rho:F(U)\to F(V)

が出ます。

cover $V\to U$ 上の局所データ

$V$ で

x_V\in F(V)

を一つ取ります。

sheaf condition は、

この局所データ $x_V$ が、ただ一つの大域的データ
$x_U\in F(U)$
から来なければならない

と言っています。

つまり

\rho(x_U)=x_V

となる $x_U$ が一意に存在する。

これはまさに

\boxed{ \rho:F(U)\longrightarrow F(V) \text{ が bijection} }

という条件です。

したがって、

\boxed{ F\text{ is a }J\text{-sheaf} \iff F(U)\overset{\sim}{\longrightarrow}F(V). }

10. したがって sheaf topos は $\mathbf{Set}$ になる

sheaf は本質的に

X\xrightarrow{\cong}X

という形になります。

よって

\boxed{ \operatorname{Sh}(C,J)\simeq\mathbf{Set}. }

一方、元の presheaf topos はもっと大きく、

\boxed{ \widehat C = [C^{op},\mathbf{Set}] = \{\text{all maps }A\to B\}. }

です。

つまり topology $J$ は、

[A\to B]

という巨大な世界から、

[X\overset{\sim}{\to}X]

という sheaf の世界だけを選び出しています。

Lawvere–Tierney 側では同じことを

\boxed{ \operatorname{Sh}_j(\widehat C) }

と書きます。

そして

\boxed{ \operatorname{Sh}(C,J) \simeq \operatorname{Sh}_j(\widehat C). }

これが一般定理です。(Ncatlab)

11. $j$ が subobject に何をするか見ると、もっと直感的になる

ここはぜひ見ておきたいところです。

presheaf

F(U)\xrightarrow{\rho}F(V)

の subobject

A\hookrightarrow F

を考えます。

つまり

A(U)\subseteq F(U),\qquad A(V)\subseteq F(V)

です。

Lawvere–Tierney topology は、これを「closure」します。

この例では、

\boxed{ \overline A(U) = \{x\in F(U)\mid \rho(x)\in A(V)\}. }

一方、

\boxed{ \overline A(V)=A(V). }

何を言っているでしょう？

ある $x\in F(U)$ がまだ $A(U)$ に入っていなくても、

x|_V=\rho(x)\in A(V)

ならば、

$x$ は cover $V\to U$ 上では $A$ に属している。

そこで $j$ -closure は、

\boxed{ \text{locally in }A \quad\Rightarrow\quad \text{in the closure of }A }

とします。

これは普通の位相空間で

x\in\overline A

という「閉包」と似た役割をしますが、topos では論理と sheaf 性に直結しています。

12. 具体的な集合でやってみる

例えば

F(U)=\{a,b,c\}, \qquad F(V)=\{0,1\}

として、

\rho(a)=0,\quad \rho(b)=0,\quad \rho(c)=1.

subobject $A$ を

A(U)=\{a\}, \qquad A(V)=\{0\}

とします。

すると $b$ は大域的には

b\notin A(U)

です。

しかし局所化すると

\rho(b)=0\in A(V).

だから、

b\in\overline A(U).

したがって

\boxed{ \overline A(U)=\{a,b\}. }

つまり

a:\text{ already true},

b:\text{ locally true},

c:\text{ not even locally true}.

Lawvere–Tierney topology は、

\boxed{ b\text{ のような「局所的真」を拾い上げる} }

装置なのです。

13. ここで本物の位相空間に戻すと

普通の位相空間 $X$ を考えます。

open cover

U=\bigcup_i U_i

があるとしましょう。

Grothendieck の言葉なら、

\{U_i\to U\}_i

が covering family。

ある命題 $p$ が各 $U_i$ 上で成立しているなら、

p|_{U_i}=\text{true} \qquad\forall i.

Lawvere–Tierney の言葉では、

\boxed{j(p)=\text{true}}

です。

つまり

\boxed{ p\text{ holds locally on a cover} }

を一つの modal operator にしてしまった。

これは nLab の説明でも、Lawvere–Tierney topology は「something is locally true」を topos 内部で表現するものとして説明されています。(Ncatlab)

14. ここで「sheaf」と「論理」が同じ原理から出る

Grothendieck にとって sheaf condition は、

\boxed{ \text{compatible local data} \Rightarrow \text{unique global data} }

です。

一方 Lawvere 側では、

\boxed{ \text{local truth} \Rightarrow j\text{-truth} }

です。

これらは別々の話ではありません。

同じ $j$ から

$j$ -dense subobject
$j$ -closed subobject
$j$ -sheaf
$j$ -separated object
sheafification

が全部出てきます。

実際、任意の topos $\mathcal E$ と Lawvere–Tierney topology $j$ に対して、

\operatorname{Sh}_j(\mathcal E) \hookrightarrow \mathcal E

は再び topos となります。(Ncatlab)

15. だから「外部」と「内部」という区別が決定的になる

今や、前回の話をもう少し正確にできます。

Grothendieck の記述

small category $C$ を外から見て、

\boxed{ J(c)= \{\text{covering sieves on }c\} }

を指定する。

これは external geometry です。

Lawvere–Tierney の記述

presheaf topos

\widehat C

の内部にある truth-value object

\Omega

を使って、

\boxed{ j:\Omega\to\Omega }

とする。

これは internal logic です。

したがって、

\boxed{ J \quad\longleftrightarrow\quad j }

は

\boxed{ \text{external covering geometry} \quad\longleftrightarrow\quad \text{internal modality of truth} }

という対応なのです。

Mac Lane–Moerdijk の教科書がこの部分を文字どおり “Lawvere–Tierney Subsumes Grothendieck” という節で扱っているのも象徴的です。(Google Books)

16. これを McLarty のビデオに戻してみる

ここで、あのビデオの Grothendieck の発言が違って聞こえてきます。

彼は、

topos を単なる巨大な sheaf category と考えるのではなく、その背後の小さな geometrical object として考えたい

と言っていました。

Grothendieck の方向は

\boxed{ \operatorname{Sh}(C,J) \longrightarrow \text{the space behind it} }

です。

Lawvere–Tierney は逆方向へ潜ります。

\boxed{ \operatorname{Sh}(C,J) \longrightarrow \text{its internal truth values }\Omega }

そして驚くべきことに、

\boxed{ \text{Grothendieck が外から与えた }J }

が、

\boxed{ \text{Lawvere が内部で見る }j:\Omega\to\Omega }

として完全に復元される。

だから同じ topos について、

\begin{array}{ccc} &&\text{topos }\mathcal E\\[1mm] &\swarrow&&\searrow\\ \text{Grothendieck}&&&&\text{Lawvere}\\ \text{generalized space}&&&&\text{generalized universe}\\ \text{covers}&&&&\text{truth values}\\ J&&&&j:\Omega\to\Omega\\ \text{geometry}&&&&\text{logic} \end{array}

となるわけです。Elementary topos が一般化された集合世界であると同時に一般化された空間でもある、というこの二重性は、topos theory が論理と幾何を直接結ぶ理由でもあります。(スタンフォード哲学辞典)

私なら、この先はここへ進みます

次に見るべきものは Kripke–Joyal semantics です。

今回出てきた

\{i\}\in\Omega(U)

を

「 $U$ ではまだ真ではないが、cover $V\to U$ に行けば真」

と読みました。

これを一般化すると、

U\Vdash\varphi

という **「stage $U$ において命題 $\varphi$ が真」**という意味論になります。

すると驚くべきことに、

U\Vdash\exists x\,\varphi(x)

は必ずしも

$U$ 全体で一つの $x$ を選べる

という意味ではありません。むしろ

\boxed{ \text{ある cover }U_i\to U\text{ 上で、それぞれ witness }x_i \text{ が存在する} }

という意味になります。

ここまで行くと、Grothendieck の「局所的に貼り合わせる geometry」が、どうして Lawvere の intuitionistic logic そのものになるのかが非常に鮮明に見えてきます。

次はそこを、今回と同じ $V\to U$ の小さな例を使って、 $\land,\lor,\Rightarrow,\exists,\forall$ を一つずつ計算してみるのがよいと思います。

Lawvere の「論理」　∧,∨,⇒,∃,∀ の具体的計算

進めます。ここからが Grothendieck の「局所性」が Lawvere の「論理」に変わる瞬間です。

Kripke–Joyal semantics では

$U\Vdash\varphi$

を「stage $U$ において $\varphi$ が真」と読みます。重要なのは、真偽を $U$ だけで判定せず、cover や refinement $V\to U$ まで見に行くことです。標準的な規則もこの形になっています。(Ncatlab)

0. 前の例を少しだけ豊かにする

前回の

$V\longrightarrow U$

だけの site では

$\operatorname{Sh}(C,J)\simeq\mathbf{Set}$

となり、論理がほとんど普通の集合論に戻ってしまいます。

そこで、最小限だけ複雑にします。

$\begin{array}{ccccc} &&O&&\\ &\swarrow&&\searrow&\\ V&&&&W\\ &\searrow&&\swarrow&\\ &&U&& \end{array}$

つまり

$O\to V\to U,\qquad O\to W\to U$

です。

イメージは

$U=V\cup W,\qquad O=V\cap W.$

そして

$\boxed{\{V\to U,\;W\to U\}}$

を cover とします。

$V,W,O$ 自身については identity cover だけで十分です。

1. 二つの命題 $P,Q$ を用意する

$U$ 上で、

$P=\text{「$V$ 側では真」},$ $Q=\text{「$W$ 側では真」}$

という命題を考えます。

正確には $U$ 上の $J$ -closed sieves として

$P=\{V\to U,\;O\to U\},$ $Q=\{W\to U,\;O\to U\}.$

したがって、

$V\Vdash P, \qquad W\not\Vdash P,$ $W\Vdash Q, \qquad V\not\Vdash Q,$

さらに intersection $O$ では

$O\Vdash P,\qquad O\Vdash Q.$

しかし $U$ 自身では

$U\not\Vdash P,\qquad U\not\Vdash Q.$

これを出発点にします。

2. $\land$ ：conjunction

Kripke–Joyal の規則は一番普通です。

$\boxed{ U\Vdash\varphi\land\psi \iff U\Vdash\varphi \text{ and } U\Vdash\psi }$

です。(Ncatlab)

今回、

$U\not\Vdash P, \qquad U\not\Vdash Q$

なので、

$\boxed{ U\not\Vdash P\land Q. }$

一方 $O$ では

$O\Vdash P,\qquad O\Vdash Q$

なので、

$\boxed{ O\Vdash P\land Q. }$

ここにはまだあまり驚きはありません。

$\land$

は stage ごとに両方が真であることを要求します。

3. $\lor$ ：disjunction で突然「cover」が入ってくる

ここから普通の集合論と違ってきます。

規則は

$\boxed{ U\Vdash\varphi\lor\psi }$

iff $U$ を cover する family

$U_i\to U$

が存在して、各 $U_i$ 上では

$U_i\Vdash\varphi \quad\text{または}\quad U_i\Vdash\psi$

となることです。(Ncatlab)

今回の cover は

$\{V\to U,W\to U\}.$

そして

$V\Vdash P,$ $W\Vdash Q.$

したがって、

$\boxed{ U\Vdash P\lor Q. }$

ところが、

$U\not\Vdash P, \qquad U\not\Vdash Q.$

つまり、

$\boxed{ U\Vdash P\lor Q }$

なのに

$\boxed{ U\not\Vdash P,\qquad U\not\Vdash Q. }$

これが最初の決定的な違いです。

普通の Boolean semantics では

$P\lor Q=\mathrm{true}$

なら、「 $P$ か $Q$ のどちらかが true」と考えたくなります。

しかし sheaf semantics では、

どちらであるかが global に決まっていなくてもよい。

$V$ では $P$ 。

$W$ では $Q$ 。

それだけで

$U\Vdash P\lor Q$

です。

つまり

$\boxed{ \lor=\text{locally one of the alternatives holds}. }$

4. ここに Grothendieck topology が直接現れている

これはかなり重要です。

Grothendieck は、

$U=V\cup W$

という geometry を与えます。

Lawvere/Joyal は、それを

$\boxed{ V\Vdash P,\quad W\Vdash Q \Longrightarrow U\Vdash P\lor Q }$

という logic の推論規則に変えます。

つまり、

$\text{covering}$

が

$\text{disjunction}$

の意味論に入ってしまった。

これが

$\boxed{\text{geometry }\longrightarrow\text{ logic}}$

です。

5. $\Rightarrow$ ：implication は「すべての refinement を見る」

次がさらに重要です。

$\boxed{ U\Vdash\varphi\Rightarrow\psi }$

とは、

$\boxed{ \text{every }f:T\to U \text{について、} T\Vdash\varphi \Rightarrow T\Vdash\psi }$

という意味です。(Ncatlab)

注意してください。

単に

$U\Vdash P \Rightarrow U\Vdash Q$

を見るのではありません。

$U$ のあらゆる局所化を調べます。

$P\Rightarrow Q$ を計算する

$U$ の refinement

$V\to U$

を見ます。

$V$ では

$V\Vdash P$

ですが、

$V\not\Vdash Q.$

したがって一つ counterexample が見つかりました。

ゆえに

$\boxed{ U\not\Vdash P\Rightarrow Q. }$

ところが $W$ ではどうか

今度は

$W\Vdash P\Rightarrow Q$

を調べます。

$W$ 以下の stages は

$W,\;O$

です。

$W$ では

$W\not\Vdash P$

なので implication は問題なし。

$O$ では

$O\Vdash P$

かつ

$O\Vdash Q.$

したがって、

$\boxed{ W\Vdash P\Rightarrow Q. }$

6. なぜ implication がこうなるのか

これは intuitionistic logic の本質です。

ある stage $U$ で

$P\Rightarrow Q$

と言うためには、

今はまだ $P$ が成立していなくても、
将来さらに情報を得て $P$ が成立するようになったとき、必ず $Q$ も成立しなければならない。

という条件が必要です。

したがって、

$\boxed{ \Rightarrow = \text{truth preserved under every future refinement} }$

です。

Kripke semantics の「possible future worlds」と、Grothendieck の「smaller opens / refinements」がここで一致します。

7. $\exists$ ：existential quantifier が特に美しい

ここで sheaf $A$ を具体的に作ります。

$A(U)=\varnothing,$ $A(V)=\{v\}, \qquad A(W)=\{w\},$ $A(O)=\{0,1\}.$

restriction を

$v|_O=0,$ $w|_O=1$

とします。

図式で書けば、

$\begin{array}{ccc} \{v\}&&\{w\}\\ \downarrow&&\downarrow\\ \{0,1\}&&\{0,1\}\\ v\mapsto0&&w\mapsto1 \end{array}$

です。

$v$ と $w$ は overlap $O$ で一致しません。

だから glue できません。

したがって、

$\boxed{A(U)=\varnothing}.$

これはちゃんと sheaf です。

matching family が存在しないので、その matching family に対応する global section も存在しないからです。

8. $\exists x:A\,\top$ を計算する

普通の集合論なら、

$A(U)=\varnothing$

を見て

$\exists x\in A(U)$

は false と言いたくなります。

ところが Kripke–Joyal では違います。

規則は、

$\boxed{ U\Vdash\exists x:A\,\varphi(x) }$

iff $U$ の cover

$U_i\to U$

が存在して、それぞれに

$a_i\in A(U_i)$

を選べ、

$U_i\Vdash\varphi(a_i)$

となることです。つまり existential witness は 局所的に存在すればよい。(Ncatlab)

今回、

$V\to U,\qquad W\to U$

が cover。

そして

$v\in A(V), \qquad w\in A(W).$

$\varphi=\top$ なので当然

$V\Vdash\top, \qquad W\Vdash\top.$

したがって、

$\boxed{ U\Vdash\exists x:A\,\top. }$

ところが

$\boxed{A(U)=\varnothing}.$

これは非常に重要です。

$\boxed{ U\Vdash\exists x:A\,\top \quad\text{だが}\quad \text{global witness }x\in A(U)\text{ はない}. }$

9. しかも局所 witness は glue しなくてよい

先ほど、

$v|_O=0, \qquad w|_O=1$

なので

$v|_O\ne w|_O.$

つまり $v,w$ は互換的ではありません。

それでも

$\exists$

には十分です。

これは大事なポイントです。

sheaf condition が glue を要求するのは、

同じ object の局所 section を一つの global section にしたい

場合です。

しかし existential は単に

「どこか局所的には witness がある」

とだけ言っています。

したがって witness 同士の一致は要求しません。

Lawvere の観点からは、これは写像の image の圏論的性質から出てきます。Lawvere は existential quantification を geometric image の普遍性と結びつけています。(Ncatlab)

10. $\forall$ ：global elements だけ見てはいけない

最後に universal quantifier。

ここが existential と対照的です。

規則は

$\boxed{ U\Vdash\forall x:A\,\varphi(x) }$

iff、すべての

$f:T\to U$

と、すべての

$a\in A(T)$

について

$T\Vdash\varphi(a)$

となることです。(Ncatlab)

つまり

$A(U)$

だけを調べてはいけません。

あらゆる refinement 上に現れる section を全部調べる。

11. 実際に $\forall$ を計算する

$A$ の sub-sheaf

$B\hookrightarrow A$

を作ります。

$B(U)=\varnothing,$ $B(V)=\varnothing,$ $B(W)=\{w\},$ $B(O)=\{1\}.$

そして述語

$R(x):\quad x\in B$

を考えます。

さて、

$A(U)=\varnothing.$

普通の集合論的な発想で $U$ の section だけを見ると、

$A(U)$ には一つも $x$ がないから
$\forall x\,R(x)$ は vacuously true では？

と思います。

しかし違います。

$V\to U$ を見ます。

そこには

$v\in A(V)$

があります。

ところが

$B(V)=\varnothing$

なので

$V\not\Vdash R(v).$

したがって、

$\boxed{ U\not\Vdash\forall x:A\,R(x). }$

12. これはかなり深い

まとめると、

$A(U)=\varnothing$

にもかかわらず、

$U\Vdash\exists x:A\,\top$

であり、

同時にある $R$ について

$U\not\Vdash\forall x:A\,R(x).$

一見すると不思議です。

しかし Kripke–Joyal 的には完全に自然です。

なぜなら $A$ は

$A(U)$

という一つの集合ではないからです。

本当は

$\boxed{ A= \text{すべての stages にわたって変化する集合} }$

だからです。

これこそ以前述べた

$\boxed{\text{variable set}}$

の意味です。

13. 五つを並べると構造が非常によく見える

論理演算	$U$ で真になる条件	幾何学的意味
$\varphi\land\psi$	$U\Vdash\varphi$ かつ $U\Vdash\psi$	同じ場所で両方
$\varphi\lor\psi$	cover 上で局所的にどちらか	cover による分割
$\varphi\Rightarrow\psi$	全 $T\to U$ で $\varphi\Rightarrow\psi$	全 refinement を見る
$\exists x\,\varphi$	cover 上で局所 witness が存在	local existence
$\forall x\,\varphi$	全 $T\to U$ 、全 $x\in A(T)$ で成立	全 refinement の全 section

ここに一つ非常にはっきりした非対称性があります。

$\boxed{\lor,\exists}$

では cover が登場する。

一方

$\boxed{\Rightarrow,\forall}$

では すべての refinement が登場する。

これは偶然ではありません。

14. Lawvere の観点では、量化子は「adjoint」

ここでもう一段深いところへ行けます。

Lawvere にとって論理演算は単なる truth table ではありません。

projection

$\pi:X\times A\longrightarrow X$

を考えます。

subobject を引き戻す操作

$\pi^*: \operatorname{Sub}(X) \longrightarrow \operatorname{Sub}(X\times A)$

があります。

すると Elementary Topos では、その左右に adjoint が存在して

$\boxed{ \exists_\pi \dashv \pi^* \dashv \forall_\pi }$

となります。

つまり、

$\boxed{ \exists=\text{left adjoint}, \qquad \forall=\text{right adjoint}. }$

Lawvere の categorical logic では、こちらが量化子の本体です。論理演算を universal property / adjunction から理解するのが Lawvere 的な発想です。(Ncatlab)

15. なぜ $\exists$ が cover と相性がよいのか

left adjoint は、大ざっぱには

$\text{image / existence}$

を作ります。

したがって、

$A\xrightarrow{p}1$

を考えると、

$\exists x:A\,\top$

は

$p(A)\hookrightarrow1$

という image を表します。

topos では

$A\to1$

が epi なら、

$\exists x:A\,\top$

は true。

epi は sheaf の世界では、

section が global に持ち上がる

とは限らず、

locally 持ち上がる

ことを意味します。

だから

$\exists$

が cover semantics になる。

これは非常にきれいな対応です。

16. なぜ $\forall$ がすべての refinement を見るのか

一方

$\forall_\pi$

は right adjoint です。

したがって、

どんな base change をしても条件が保持される

という普遍的性質になります。

そのため Kripke–Joyal semantics では、

$\boxed{ \forall T\to U }$

が必然的に出てくる。

同じ理由で implication も

$\boxed{ \forall T\to U }$

を見ることになります。

実際、

$P\Rightarrow Q$

は Heyting algebra $\operatorname{Sub}(U)$ における right adjoint と考えられます。

17. ここで Grothendieck と Lawvere の関係がかなり鮮明になる

Grothendieck の出発点では

$U=V\cup W$

という幾何があります。

それを Lawvere–Joyal の内部言語で読むと、

$V\Vdash P,\quad W\Vdash Q$

から

$U\Vdash P\lor Q$

が生まれ、

また

$V\Vdash\exists x\,\varphi(x), \quad W\Vdash\exists x\,\varphi(x)$

から

$U\Vdash\exists x\,\varphi(x)$

が生まれます。

つまり、

$\boxed{ \text{open cover} \longrightarrow \text{logical inference} }$

です。

逆に

$\Rightarrow,\forall$

は、その geometry のすべての refinement を試す。

だから結局、

$\boxed{ \text{Grothendieck topology} = \text{internal logic の意味論を決めるもの} }$

と言えるのです。

18. ここからさらに面白い現象が一つあります

今回

$U\Vdash P\lor Q$

なのに

$U\not\Vdash P,\qquad U\not\Vdash Q$

でした。

この発想を negation

$\neg P:=P\Rightarrow\bot$

まで進めると、

$P\lor\neg P$

が一般には成立しない理由が幾何学的に計算できます。

さらに

$\neg\neg P$

を計算すると、sheaf topos ではしばしば

$\boxed{ \neg\neg P \approx \text{$P$ が dense に成立する} }$

という非常に美しい意味になります。

ここまで行くと、

$\text{classical logic} \quad\text{vs.}\quad \text{intuitionistic logic}$

の違いが、単なる「証明哲学」ではなく、

$\boxed{\text{空間の局所構造そのもの}}$

から生じていることが見えてきます。

次は $\neg P,\ \neg\neg P,\ P\lor\neg P$ をこの $U=V\cup W$ の例で実際に計算すると、Grothendieck geometry がなぜ intuitionistic logic を生むのか、核心まで到達できます。

Rieman幾何の「多様体」概念とTopos

今度は、少し視点を変えて、局所的にはユ−クリッド幾何が成り立つ空間を張り合わせるRieman幾何の「多様体」概念を、二人のTopos 概念から振り返ってみてください

はい。ここでは「多様体」を、Grothendieck と Lawvere の topos に至る一つの原型として眺め直すと、とても見通しがよくなります。

まず、ご指摘の「局所的にはユークリッド幾何が成り立つ」という言い方を少しだけ精密にします。滑らかな多様体 $M$ は局所的に $\mathbb R^n$ と微分同相ですが、Riemann 多様体 $(M,g)$ が局所的にユークリッド空間と等長とは限りません。Riemann 正規座標を使えば一点では $g_{ij}=\delta_{ij}$ かつ一次微分を消せますが、二次のところに曲率が残ります。局所的に本当にユークリッド幾何になるのは曲率ゼロの場合です。

この区別を入れると、topos との関係がむしろ鮮明になります。

1. 多様体はすでに「局所モデルを貼る」という Grothendieck 的発想を持っている

通常の多様体 $M$ は、開集合 $U_i\subset M$ と座標写像

$\varphi_i:U_i\overset{\sim}{\longrightarrow}V_i\subset\mathbb R^n$

から作られます。

重なり $U_i\cap U_j$ では

$\varphi_j\circ\varphi_i^{-1}$

が滑らかな座標変換になります。

したがって、多様体を構成している核心は、実は個々の点よりも

$\boxed{\text{local models}+\text{overlaps}+\text{compatibility}+\text{gluing}}$

です。

これは Grothendieck の sheaf/topos の発想と非常によく似ています。

従来なら、

$\mathbb R^n\text{ の断片を貼って }M\text{ を作る}$

と言います。

Grothendieck 的に言い換えれば、

$\boxed{ \text{局所的な対象と、それらを貼り合わせる descent data が空間を規定する} }$

となります。

この意味で、多様体は topos 的幾何学の非常に古典的な prototype と見ることができます。

2. 多様体そのものより「その上の sheaf」を見る

多様体 $M$ が与えられると、開集合の圏

$\operatorname{Open}(M)$

があります。

その上の sheaf 全体の圏

$\operatorname{Sh}(M)$

を考えることができます。

Grothendieck の観点では、

$M\quad\rightsquigarrow\quad\operatorname{Sh}(M)$

と移ることで、空間の局所性を一つの圏にまとめます。

例えば滑らかな関数は sheaf

$U\longmapsto C^\infty(U)$

を作ります。

これを

$\mathcal C^\infty_M$

と書けば、滑らかな多様体は

$\boxed{(M,\mathcal C^\infty_M)}$

という locally ringed space として捉えることもできます。実際、滑らかな多様体と smooth functions の sheaf の関係はこの形で標準的に定式化できます。(Ncatlab)

ここで重要なのは、

$\operatorname{Sh}(M)$

だけでは $M$ の位相的局所性はよく見えますが、smooth structure を完全には記録しないことです。

そこで

$\boxed{ (\operatorname{Sh}(M),\mathcal C^\infty_M) }$

という「構造 sheaf を持った topos」を考える。

これは Grothendieck が scheme に対して

$(X,\mathcal O_X)$

を考えるのと非常によく似ています。

3. Riemann 計量も「局所テンソルを貼ったもの」として見える

Riemann 計量は各点 $x\in M$ に

$g_x:T_xM\times T_xM\to\mathbb R$

という正定値対称双線形形式を与えるものです。

座標 $x^1,\dots,x^n$ では

$g=\sum_{i,j}g_{ij}(x)\,dx^i\,dx^j.$

座標を変えると $g_{ij}$ は変換されます。

しかし重なりで適切な tensor transformation law を満たすため、局所的な $g_i$ は一つの global object

$g\in\Gamma(M,\operatorname{Sym}^2 T^*M)$

に貼り合わされます。

つまり Riemann 計量も、

$\boxed{ \text{局所データ} \quad+\quad \text{overlap 上の compatibility} \quad\Longrightarrow\quad \text{global geometric object} }$

です。

これはまさに sheaf 的です。

したがって Grothendieck 的に Riemann 幾何を見ると、

多様体という「点集合」の上に tensor が載っている

というより、

局所的に定義された幾何学的データが descent によって一つの大域的幾何を作っている

と見る方が自然になります。

4. ここで Grothendieck は「多様体」という概念をさらに一般化する

通常の manifold では局所モデルは

$\mathbb R^n$

です。

scheme なら局所モデルは

$\operatorname{Spec}A.$

Grothendieck topos まで行くと、もっと大胆になります。

もはや「点の集合 $X$ をまず持って、その上に局所データを置く」という必要すらない。

site

$(C,J)$

があれば、

$\operatorname{Sh}(C,J)$

を空間として扱える。

つまり多様体の

$\boxed{ \mathbb R^n\text{ の断片を貼り合わせる} }$

という原理が、

$\boxed{ \text{局所的な test objects を、covering relation に従って貼り合わせる} }$

へ一般化されます。

この意味で、

$\boxed{ \text{manifold} \;\longrightarrow\; \text{Grothendieck generalized space} }$

は非常に自然な延長です。

5. 多様体で「点」が主役だったことさえ相対化される

これは McLarty のビデオにかなり直接つながります。

Grothendieck は、

topos を巨大な sheaf category とだけ考えず、その背後の geometrical object として考えたい

と言っていました。

多様体 $M$ なら、

$M$

という「小さな geometrical thing」と、

$\operatorname{Sh}(M)$

という巨大な sheaf category の両方があります。

だから多様体の場合には Grothendieck の直観は非常にわかりやすい。

しかし彼はこの関係を、

$\boxed{ \text{点集合としての空間が存在しない場合にも拡張したい} }$

のです。

言い換えると、多様体は

$\text{points}\to\text{opens}\to\text{sheaves}$

という順番で作れますが、Grothendieck はこれを逆転させ、

$\boxed{ \text{sheaves の圏そのものから「space」を読む} }$

方向へ進んだわけです。

6. ここで Lawvere がもう一度視点をひっくり返す

Lawvere から見ると、

$\operatorname{Sh}(M)$

は単に $M$ を外から記述する装置ではありません。

その内部に入って数学をする世界になります。

外部から見れば、

$F\in\operatorname{Sh}(M)$

は $M$ 上の sheaf。

内部から見れば、

$F$

は単に「集合」です。

ただし場所によって値が変化する

$\boxed{\text{variable set}}$

です。

したがって多様体 $M$ は Lawvere 的には、

$\boxed{ M\text{ 上で変化する集合・関数・命題を含む一つの数学的 universe} }$

を生みます。

Topos が「一般化された位相空間」であると同時に「一般化された集合の宇宙」である、という二重性は、まさに geometry と logic の橋になります。(スタンフォード哲学辞典)

7. 座標 chart の意味も変わって見えてくる

通常の微分幾何では、

$\varphi:U\to\mathbb R^n$

という chart を取って計算します。

しかし intrinsically には manifold は座標には依存しません。

これは topos 的な発想と非常に相性がよい。

座標系は

$\boxed{\text{local presentation}}$

にすぎず、

対象そのものはそれらの presentation の貼り合わせから独立です。

これは scheme について

$\operatorname{Spec}A_i$

という affine charts を選んでも scheme 自体はそれらではない、という Grothendieck の発想と全く平行しています。

さらに topos では site 自身さえ一意ではありません。

異なる site が

$\operatorname{Sh}(C,J)\simeq\operatorname{Sh}(D,K)$

という同じ topos を記述することがあります。

これは、

座標表示ではなく、座標変換に不変な対象を見る

という Riemann 幾何の哲学を、もう一段抽象化したものだと言えます。

8. そして Lawvere は「微分」そのものまで内部化する

ここから Lawvere の方向が特に面白くなります。

普通の多様体では接ベクトルを

$v\in T_xM$

と考えます。

あるいは curve

$\gamma:(-\epsilon,\epsilon)\to M$

の

$\gamma'(0)$

として定義します。

Lawvere の Synthetic Differential Geometry では、適切な smooth topos の内部に infinitesimal object

$D=\{\varepsilon\mid\varepsilon^2=0\}$

のような対象を置きます。

すると接空間は概念的に

$\boxed{ TX=X^D }$

と書けます。

つまり tangent vector は、

$\boxed{ D\longrightarrow X }$

という文字通りの infinitesimal path になります。これは smooth topos / Kock–Lawvere axiom に基づく synthetic differential geometry の中心的な考え方です。(Ncatlab)

これは通常の Riemann 幾何と比べると、かなり大胆です。

通常は infinitesimal は

$\lim_{t\to0}$

によって外から作ります。

Lawvere は、

$\boxed{\text{infinitesimal 自身を space の一種として内部に置く}}$

のです。

9. この視点から Riemann 計量を見る

すると Riemann 計量も、内部的には

$g:TX\times_XTX\to R$

のような morphism として考えられます。

ここで $R$ は topos 内部の「実数直線」です。

各 $x$ において

$g_x(v,w)$

を計算することも、全部 topos の内部言語で行う。

したがって classical differential geometry の

$M,\quad TM,\quad g,\quad\nabla,\quad R$

という構造を、

$\boxed{ \text{一つの smooth topos の内部数学} }$

として語れる可能性が出てきます。

Lawvere が categorical logic を発展させた動機の一つが differential geometry の新しい基礎づけであり、それが synthetic differential geometry へ発展したことはよく知られています。(スタンフォード哲学辞典)

10. ここで三段階の発展として見ると、とても美しい

多様体から二人の topos への流れを、私はこう見るとわかりやすいと思います。

$\boxed{ \text{Riemann / manifold} }$

では、

$\text{local Euclidean models} \longrightarrow \text{gluing} \longrightarrow \text{global manifold}.$

Grothendieck では、

$\boxed{ \text{local generalized models} \longrightarrow \text{descent/sheaves} \longrightarrow \text{generalized space}. }$

Lawvere ではさらに、

$\boxed{ \text{generalized space} \longrightarrow \text{internal universe} \longrightarrow \text{logic + differential geometry}. }$

つまり

$\boxed{ \mathbb R^n\text{ を貼る} \;\to\; \text{局所データ一般を貼る} \;\to\; \text{貼られた世界の内部で数学をする} }$

という発展です。

11. しかし三者には一つ共通した思想がある

Riemann、Grothendieck、Lawvere を強引に一本の線で結ぶなら、中心にあるのは

$\boxed{\text{「全体」を直接定義せず、局所的な関係から捉える}}$

という思想だと思います。

Riemann 的な manifold では、

$M\text{ が何であるか}$

を一枚の座標では語らない。

局所 chart と transition map で語る。

Grothendieck では、

$X\text{ が何であるか}$

を点集合で語る必要さえない。

covering と sheaf で語る。

Lawvere ではさらに、

$\text{数学的真理とは何か}$

さえ一つの外部的な

$\{\mathrm{true},\mathrm{false}\}$

で語らない。

stage と localization に従って変化する

$\Omega$

で語る。

そうすると驚くほど似た構造が現れます。

$\begin{aligned} \text{coordinate chart} &\leftrightarrow \text{site/local object},\\ \text{transition function} &\leftrightarrow \text{descent data},\\ \text{atlas compatibility} &\leftrightarrow \text{sheaf condition},\\ \text{coordinate independence} &\leftrightarrow \text{presentation independence},\\ \text{local geometric statement} &\leftrightarrow \text{Kripke--Joyal local truth}. \end{aligned}$

これは単なる比喩ではなく、かなり数学的に実体のある対応です。

12. そして Riemann 幾何から見ると、Grothendieck と Lawvere の違いもよく見える

Grothendieck は、Riemann が

$\mathbb R^n$

を局所モデルにして作った「空間」の概念を、

$\boxed{ \text{どんな local models と covering theory でもよい} }$

ところまで拡張した、と見ることができます。

一方 Lawvere は、

そもそもその generalized space の内部で、微分・量化・真理・実数を直接扱えないか

と考えた。

したがって少し象徴的に言えば、

$\boxed{ \text{Grothendieck は manifold を外側へ拡張し、} }$ $\boxed{ \text{Lawvere は manifold の内側へ潜った。} }$

Grothendieck の方向は

$\text{manifold}\to\text{generalized spaces},$

Lawvere の方向は

$\text{generalized space}\to\text{internal mathematics}.$

という違いです。

13. この見方で「曲率」を考えると、さらに面白い

最後にここを少しだけ先取りします。

多様体が局所的に

$\mathbb R^n$

と微分同相であるだけなら、すべての滑らかな多様体は同じ local model を持ちます。

それでも sphere と Euclidean space は全く違う。

なぜなら Riemannian metric の貼り合わせ方とその infinitesimal variation に曲率が現れるからです。

つまり曲率は、

$\boxed{ \text{local Euclidean description が global に単純化できないこと} }$

を測る obstruction とも読めます。

ここから topos 的に非常に興味深い問いが生じます。

「曲率」は descent の失敗なのか？
接続は local-to-global の transport を記述するものなのか？
holonomy は局所的 identification を一周して戻したときの obstruction として、topos 的にどう見えるのか？

この方向へ進むと、Riemann geometry の

$\boxed{\text{connection}\to\text{parallel transport}\to\text{holonomy}\to\text{curvature}}$

を、Grothendieck の descent と Lawvere の infinitesimal object $D$ の両方から見直すことができます。

私は次にそこへ進むのが自然だと思います。特に **「曲率とは infinitesimal な gluing の非可換性である」**というところまで持っていくと、Riemann → Grothendieck → Lawvere がかなり一本の線として見えてきます。

では、前回の最後の問いをそのまま掘ります。

最初に一つ大事な修正を入れると、曲率は「descent の失敗」そのものではありません。むしろ、bundle や connection はきちんと descent で貼り合わさります。そのうえで曲率は、

$\boxed{\text{局所的な平行移動が infinitesimal loop のまわりで完全には可換にならないこと}}$

を測る量です。

この区別を入れると、Riemann 幾何・Grothendieck・Lawvere の関係がかなりきれいに見えます。

Please proceed to the next step.

1. まず通常の Riemann 幾何から

Riemann 多様体 $(M,g)$ では Levi-Civita connection

$\nabla$

があります。

ベクトル場 $X,Y,Z$ に対して曲率は

$\boxed{ R(X,Y)Z = \nabla_X\nabla_Y Z - \nabla_Y\nabla_X Z - \nabla_{[X,Y]}Z }$

です。

この式が言っていることは直感的には、

$X$ 方向へ少し動いてから $Y$ 方向へ動くのと、
$Y$ 方向へ少し動いてから $X$ 方向へ動くのは、一般には同じではない。

ということです。

つまり、

$\boxed{\text{infinitesimal transport の非可換性}}$

が曲率です。

2. 小さな四角形を一周する

点 $p\in M$ から、

$\varepsilon X,\qquad \delta Y$

という非常に小さな方向へ進むことを考えます。

小さな平行四辺形

$p \to p+\varepsilon X \to p+\varepsilon X+\delta Y \to p+\delta Y \to p$

を一周して、ベクトル $v\in T_pM$ を parallel transport します。

平坦なら戻ってきたベクトルは

$v$

そのものです。

しかし曲率があると、

$v \longmapsto v+\varepsilon\delta\,R(X,Y)v+\text{higher order terms}.$

つまり

$\boxed{ \text{Holonomy around infinitesimal square} = I+\varepsilon\delta R(X,Y)+\cdots }$

です。

ここが核心です。

3. Connection は「局所的な比較法」

なぜ connection が必要なのでしょう。

異なる点

$p,q\in M$

では、

$T_pM,\qquad T_qM$

は別々の vector space です。

そのままでは

$v_p-v_q$

とは書けません。

connection は、

$\boxed{ \text{近くの点の fibers をどう比較するか} }$

を与えます。

つまり connection は一種の

$\boxed{\text{local identification rule}}$

です。

parallel transport はその identification を path に沿って積み重ねたものです。

4. ここで Grothendieck の descent が出てくる

多様体を open cover

$M=\bigcup_i U_i$

で覆います。

各 $U_i$ 上で vector bundle $E$ を trivialize すると、

$E|_{U_i}\cong U_i\times\mathbb R^n.$

重なりでは transition function

$g_{ij}:U_i\cap U_j\to GL(n)$

があり、

$g_{ij}g_{jk}=g_{ik}$

という cocycle condition を満たします。

これはまさに descent data です。

$\boxed{ \text{local trivial bundles} + \text{transition maps} + \text{cocycle condition} \Rightarrow \text{global bundle} }$

したがって bundle の存在そのものは Grothendieck 的な gluing の典型例です。

5. Connection も descent する

各 $U_i$ で connection を matrix-valued 1-form

$A_i$

として書きます。

重なりでは

$\boxed{ A_j = g_{ij}^{-1}A_i g_{ij} + g_{ij}^{-1}dg_{ij} }$

という変換則を満たします。

これも compatibility condition です。

だから connection も局所データから global に貼れます。

つまり、

$\boxed{ \text{connection がある} }$

ことと

$\boxed{ \text{descent が失敗している} }$

ことは別です。

むしろ connection 自体はきれいに descent しています。

6. 曲率は何なのか

局所 connection form $A_i$ から、

$\boxed{ F_i=dA_i+A_i\wedge A_i }$

を作ります。

これが curvature 2-form です。

重なりでは

$F_j = g_{ij}^{-1}F_i g_{ij}.$

つまり curvature もきちんと貼り合わさります。

したがって、

$\boxed{ F\text{ は descent の obstruction ではない} }$

のです。

むしろ、

$\boxed{ F=0 }$

であることが、

connection を局所的に「完全に一定な transport」に直せる

という flatness の条件になります。

7. Flat connection なら「局所的に constant」

ここが Grothendieck 的に非常に面白いところです。

曲率ゼロ

$F=0$

なら、適切な局所座標・gauge で

$A=0$

にできます。

すると parallel sections は局所的には本当に constant です。

したがって flat bundle は、

$\boxed{\text{local systems}}$

と深く結びつきます。

そして connected manifold なら、flat vector bundle は本質的に fundamental group の representation

$\boxed{ \rho:\pi_1(M)\to GL(V) }$

と対応します。

これはものすごく Grothendieck 的です。

なぜなら local system は sheaf だからです。

つまり flat geometry は

$\boxed{ \text{differential geometry} \longrightarrow \text{sheaf/topos theory} }$

へ直接つながります。

8. Holonomy は「貼り合わせの履歴」

flat connection でも global holonomy は残ることがあります。

例えば円周 $S^1$ 。

局所的には connection を trivial にできても、一周すると

$v\mapsto Av$

となるかもしれません。

つまり

$F=0$

なのに、

$\operatorname{Hol}(\gamma)\neq I$

があり得ます。

これは

$\boxed{ \text{local flatness} \neq \text{global triviality} }$

ということです。

多様体の atlas と同じで、

局所的には単純でも、貼り合わせ方が global information を持つ。

Grothendieck の世界では、こういう phenomenon は非常に自然です。

9. ここで Lawvere の infinitesimal geometry に移る

Lawvere の Synthetic Differential Geometry では、

$D=\{\varepsilon\mid \varepsilon^2=0\}$

のような infinitesimal object を内部に持ちます。

すると tangent vector は

$\boxed{ D\to M }$

として表せます。

二方向を見るなら

$D\times D\to M.$

これは infinitesimal parallelogram です。

通常の微分幾何では

$\varepsilon\to0,\qquad\delta\to0$

という limit を使いますが、Lawvere 的には infinitesimal square 自体が内部に存在します。

10. 曲率を infinitesimal square で直接読む

connection があると、この infinitesimal square の四辺に沿って transport できます。

概念的には、

$\begin{array}{ccc} x &\longrightarrow& x+\varepsilon X\\ \downarrow &&\downarrow\\ x+\delta Y&\longrightarrow& x+\varepsilon X+\delta Y \end{array}$

です。

二つの経路

$X\text{ then }Y$

と

$Y\text{ then }X$

を比較します。

差は

$\varepsilon\delta\,R(X,Y)$

に比例します。

Lawvere 的には、これは極限ではなく、

$\boxed{ \text{infinitesimal square の境界を一周した transport} }$

そのものとして扱えます。

だから

$\boxed{ \text{curvature} = \text{infinitesimal holonomy} }$

という言い方が非常に自然になります。

11. ここで Grothendieck と Lawvere が再び出会う

Grothendieck は、

$\boxed{ \text{local objects を cover 上で比較し、glue する} }$

ことを重視します。

Lawvere は、

$\boxed{ \text{infinitesimally nearby な objects を内部で比較する} }$

ことを可能にします。

したがって connection は両者のちょうど間にあります。

$\boxed{ \begin{array}{ccc} \text{Grothendieck}&&\text{Lawvere}\\ \text{descent}&&\text{infinitesimal variation}\\ \text{overlaps}&&D,\;D^2\\ \text{transition maps}&&\text{infinitesimal transport}\\ \text{global gluing}&&\text{curvature} \end{array} }$

12. 「曲率は gluing の非可換性」と言ってよいか

少し慎重に言えば、

$\boxed{ \text{曲率は gluing の失敗ではなく、transport の非可換性} }$

です。

しかし、もっと幾何学的に言えば、

$\boxed{ \text{異なる infinitesimal routes による局所 identification の不一致} }$

なので、

infinitesimal gluing の path-dependence

と表現することはできます。

これはかなり本質に近いです。

13. Riemann 曲率テンソルまで戻る

Levi-Civita connection の場合、

$R(X,Y)Z$

は tangent bundle の infinitesimal holonomy を測ります。

そして metric $g$ を使えば

$R(X,Y,Z,W) = g(R(X,Y)Z,W)$

という 4-tensor になります。

sectional curvature は 2-plane

$\sigma=\operatorname{span}(X,Y)$

に対して、

$K(\sigma) = \frac{ g(R(X,Y)Y,X) }{ g(X,X)g(Y,Y)-g(X,Y)^2 }$

で定義されます。

つまり古典的な Riemann curvature は、

$\boxed{ \text{infinitesimal 2-dimensional loop の holonomy} }$

を metric で数値化したものだと見ることができます。

14. Riemann から Grothendieck への見え方

Riemann の発想：

$\boxed{ \text{局所座標} + \text{transition maps} = \text{manifold} }$

Grothendieck：

$\boxed{ \text{local objects} + \text{descent} = \text{generalized space} }$

ここで connection を加えると、

$\boxed{ \text{local objects をどう transport するか} }$

まで情報が増えます。

そして curvature は、

$\boxed{ \text{その transport が局所的に flat かどうか} }$

を測る。

15. Lawvere を加えるとさらに一段深くなる

Lawvere では

$\varepsilon^2=0$

という infinitesimal を「外から approximation」するのではなく、内部 object として持ちます。

だから、

$\text{tangent vector}, \quad \text{connection}, \quad \text{curvature}$

をすべて同じ内部言語で記述できる。

象徴的には、

$\boxed{ \begin{aligned} \text{tangent vector}&:D\to M,\\ \text{two directions}&:D^2\to M,\\ \text{connection}&:\text{infinitesimal transport},\\ \text{curvature}&:\text{transport around }D^2. \end{aligned}}$

となります。

これは微分幾何を「無限小量の algebra」に還元するというより、

$\boxed{ \text{infinitesimal geometry を topos 内部で literal にする} }$

という発想です。

16. 三人を一本の線で見るなら

かなり大胆ですが、私はこう整理するのがいちばんきれいだと思います。

Riemann

$\boxed{ \text{global geometry is assembled from local Euclidean descriptions} }$

Grothendieck

$\boxed{ \text{space itself is encoded by local-to-global descent} }$

Lawvere

$\boxed{ \text{local and infinitesimal geometry can be internalized as logic} }$

その中間に connection があり、

$\boxed{ \text{connection} = \text{how local worlds are compared} }$

そして

$\boxed{ \text{curvature} = \text{failure of those comparisons to commute infinitesimally}. }$

17. ここから先に非常に自然な橋があります

次に進むなら、「曲率」と「cohomology」の関係を見ると、この話が Grothendieck にさらに深く戻ってきます。

connection $A$ から curvature

$F=dA+A\wedge A$

ができ、

abelian な場合には

$dF=0.$

すると $F$ は de Rham cohomology class

$[F]\in H^2_{\mathrm{dR}}(M)$

を与えます。

例えば line bundle なら

$\frac{1}{2\pi i}[F]$

が第一 Chern class

$c_1(L)$

に対応します。

つまり、

$\boxed{ \text{infinitesimal curvature} \longrightarrow \text{global cohomological invariant} }$

という橋が出てきます。

これはまさに Riemann 的 infinitesimal geometry と Grothendieck 的 cohomology が接続される地点です。

そして Lawvere 側から見ると、これを infinitesimal objects と differential forms の内部計算として再解釈できます。

次はそこへ進むと、
「局所曲率 → characteristic class → cohomology → topos」
という一本の流れがかなり鮮明になります。

Please discuss the role that cohomology plays within the theory of Topos.

Topos 論における cohomology の役割を一言で言うなら、

$\boxed{\text{局所的に存在し、局所的には整合しているデータが、どの程度大域化できるかを測る装置}}$

だと思います。

しかも Grothendieck にとっては、これは後から topos に付け加えた応用ではありません。前に見た McLarty の講演が示していたように、cohomology を正しく作ること自体が topos 概念を生んだ主要な動機でした。

1. Sheaf と cohomology の役割は少し違う

まず sheaf condition は、

$\text{compatible local data} \quad\Longrightarrow\quad \text{unique global data}$

という原理でした。

cover

$U=\bigcup_i U_i$

上に局所 section

$s_i\in\mathcal F(U_i)$

があり、重なりで

$s_i|_{U_i\cap U_j} = s_j|_{U_i\cap U_j}$

なら、

$s\in\mathcal F(U)$

へ一意に貼れる。

ですから sheaf は、

$\boxed{\text{うまく整合している局所データを貼る装置}}$

です。

ところが実際の幾何学では、局所データはしばしば完全には整合しません。

その「ずれ」を捨てずに数学的情報として取り出したものが cohomology です。

2. 最も基本的には「global sections の失敗」を測る

Grothendieck topos

$\mathcal E$

を考え、abelian group object の圏を

$\operatorname{Ab}(\mathcal E)$

とします。

terminal object を $1$ とすれば global section は

$\Gamma(\mathcal E,\mathcal F) = \operatorname{Hom}_{\mathcal E}(1,\mathcal F).$

つまり

$\Gamma: \operatorname{Ab}(\mathcal E) \longrightarrow \mathbf{Ab}.$

この functor は left exact ですが、一般には exact ではありません。

そこで derived functors を取って

$\boxed{ H^n(\mathcal E,\mathcal F) = R^n\Gamma(\mathcal F) }$

と定義します。

site $C$ で書けば、injective resolution

$\mathcal F\to I^\bullet$

を使って

$H^n(C,\mathcal F) = H^n\bigl(\Gamma(C,I^\bullet)\bigr)$

です。Grothendieck topoi の abelian sheaves ではこの derived-functor machinery が使えます。(The Stacks Project)

したがって概念的には、

$\boxed{ H^{>0} = \Gamma\text{ が exact でないことの測定} }$

なのです。

3. 「局所的には解けるが、大域的には解けない」

これを具体的に見ると意味がはっきりします。

short exact sequence

$0\to\mathcal A \to\mathcal B \to\mathcal C \to0$

を考えます。

ある

$c\in\Gamma(\mathcal C)$

を $\mathcal B$ の section に持ち上げたい。

局所的には cover $U_i$ 上で

$b_i\in\mathcal B(U_i)$

を選べて、

$b_i\mapsto c|_{U_i}$

とできるかもしれません。

ところが overlap では

$b_i-b_j\in\mathcal A(U_i\cap U_j)$

という「ずれ」が生じます。

これを

$a_{ij}=b_i-b_j$

とすると、triple overlap では

$a_{ij}+a_{jk}+a_{ki}=0.$

つまり $a_{ij}$ は 1-cocycle。

その class

$[a_{ij}]\in H^1(\mathcal E,\mathcal A)$

が、

$\boxed{ c\text{ を global に lift できない obstruction} }$

になります。

この意味で cohomology は文字どおり、

$\boxed{\text{local solvability と global solvability の差}}$

を測っています。

4. $H^0,H^1,H^2,\ldots$ は「貼り合わせの階層」

ここから非常に美しい階層が見えます。

$H^0$

$H^0(\mathcal E,\mathcal F) = \Gamma(\mathcal E,\mathcal F).$

これは単なる global objects。

$\boxed{H^0=\text{実際に大域化できたもの}}$

です。

$H^1$

$H^1$ は、「局所的には trivial だが、大域的には twisted」という現象を測ります。

典型例が torsor。

abelian sheaf $\mathcal G$ なら、

$\boxed{ H^1(\mathcal E,\mathcal G) \cong \{\mathcal G\text{-torsors}\}/\cong }$

です。(The Stacks Project)

torsor は局所的には

$\mathcal G$

そのものに見えます。

しかし global に distinguished origin を選べない。

これは以前話した

「局所 witness はあるが global witness がない」

という現象そのものです。

5. Vector bundle や line bundle も $H^1$

例えば line bundle $L$ を open cover $U_i$ 上で trivialize すると、

$L|_{U_i}\cong U_i\times\mathbb C.$

overlap で

$g_{ij}:U_i\cap U_j\to\mathbb C^\times$

が現れ、

$g_{ij}g_{jk}g_{ki}=1.$

したがって

$(g_{ij})$

は Čech 1-cocycle。

その class が bundle の twisting を記録します。

ringed site では実際に

$\boxed{ H^1(\mathcal E,\mathcal O^\times) \simeq \operatorname{Pic}(\mathcal E) }$

となります。(The Stacks Project)

だから cohomology は抽象的不変量というより、

$\boxed{\text{局所的には trivial な幾何学的対象の global twisting}}$

を記録しています。

6. $H^2$ になると「貼り合わせの貼り合わせ」の obstruction

さらに一段上へ進みます。

局所 objects $E_i$ があり、

$E_i\simeq E_j$

という identification を double overlap で選びます。

ところが triple overlap で、

$\phi_{ij}\phi_{jk} \stackrel{?}{=} \phi_{ik}$

が完全には一致せず、automorphism だけずれる場合があります。

この二次的な coherence obstruction が $H^2$ 型の情報になります。

非常に大ざっぱに図式化すると、

$\begin{array}{ccl} H^0&:&\text{sections}\\ H^1&:&\text{torsors / twisting}\\ H^2&:&\text{gerbes / second-order gluing obstruction}\\ H^3&:&\text{さらに一段上の coherence}\\ \vdots&& \end{array}$

となります。

つまり cohomological degree は、

$\boxed{\text{local-to-global coherence の深さ}}$

を表している、と考えることができます。

7. ここで topos の意味が非常に重要になる

普通の位相空間 $X$ だけなら

$\operatorname{Sh}(X)$

上で sheaf cohomology を考えればよい。

しかし Grothendieck は、

「何を cover と認めるか」

そのものを変えました。

同じ algebraic variety $X$ でも、

$X_{\mathrm{Zar}}, \qquad X_{\acute et}, \qquad X_{\mathrm{fppf}},$

など異なる sites/topoi を考えられます。

そしてそれぞれ、

$H^n_{\mathrm{Zar}}(X,\mathcal F),$ $H^n_{\acute et}(X,\mathcal F),$ $H^n_{\mathrm{fppf}}(X,\mathcal F)$

という異なる cohomology ができます。Stacks Project でも étale、fppf、Zariski など各 topology の site を作り、その上で同じ general cohomology machinery を適用する形になっています。(The Stacks Project)

ここが Grothendieck の革命の一つです。

8. Topology は「どんな局所性を観測するか」を選んでいる

これは非常に大事だと思います。

Grothendieck topology $J$ は単なる technical definition ではなく、

$\boxed{ \text{何を「局所的に trivial」とみなすか} }$

を指定しています。

Zariski topology では trivial にならない対象でも、

étale cover なら trivial になることがあります。

さらに fppf cover まで許せば、もっと多くのものが局所的に trivial になる。

したがって、

$\boxed{ \text{topology を変える} = \text{local-to-global obstruction を測る尺度を変える} }$

とも言えます。

これが étale cohomology が可能になった根本です。

通常の topology では algebraic varieties、特に有限体上の variety に欲しい cohomology が見えない。

そこで「open subsets」ではなく étale maps を cover とする。

そうすると新しい topos

$X_{\acute et}$

ができ、その cohomology

$H^n(X_{\acute et},\mathcal F)$

が algebraic geometry の正しい cohomological information を持つ。

9. したがって topos は「cohomology machine」である

Grothendieck の発想をかなり圧縮すれば、

$(C,J)$

という site を与える。

そこから

$\mathcal E=\operatorname{Sh}(C,J)$

を作る。

すると、

$\mathcal F \longmapsto H^n(\mathcal E,\mathcal F)$

という cohomology machinery が自動的に手に入る。

つまり、

$\boxed{ \text{site/topos} \longrightarrow \text{sheaves} \longrightarrow \text{homological algebra} \longrightarrow \text{cohomology} }$

という巨大な統一装置です。

これは McLarty のビデオで出てきた Tohoku 論文との関係そのものです。

Grothendieck はまず、

$\boxed{\text{十分良い abstract abelian category なら cohomology を作れる}}$

という homological algebra を作った。

その後、

$\boxed{\text{正しい sheaf category を作れば、欲しい cohomology が出てくる}}$

と考えた。

この二つが topos で結びついたわけです。

10. Topos の morphism も cohomology を運ぶ

topos theory では「空間の写像」に相当するものが geometric morphism

$f:\mathcal E\to\mathcal F$

でした。

これには

$f^*\dashv f_*$

があります。

cohomology に進むと

$f_*$

を derived して、

$\boxed{ R^nf_* }$

が現れます。

Stacks Project でも ringed topoi の morphism に対して

$R^if_*\mathcal F$

を $f_*$ の right derived functor として定義しています。(The Stacks Project)

これは「fiber ごとの higher cohomological information を base に押し下げる」操作と考えられます。

11. Leray spectral sequence は「二段階の局所→大域」

さらに

$\mathcal E \xrightarrow{f} \mathcal F \xrightarrow{g} \mathcal G$

なら、

$R(g\circ f)_*$

を

$Rf_*,\quad Rg_*$

から計算するために、

$\boxed{ E_2^{p,q} = R^pg_*(R^qf_*\mathcal A) \Rightarrow R^{p+q}(g\circ f)_*\mathcal A }$

という Leray/Grothendieck spectral sequence が出てきます。(The Stacks Project)

これは概念的には、

$\boxed{ \text{local-to-intermediate} + \text{intermediate-to-global} }$

を統合する装置です。

Topos の morphism と cohomology は別々の理論ではなく、深く一体化しています。

12. Lawvere の Elementary Topos とは少し関係が違う

ここは重要な区別です。

Grothendieck topos では cohomology が中心的です。

一方、

$\boxed{\text{Elementary Topos}}$

の定義そのものは、

finite limits
exponentials
subobject classifier

であり、cohomology は定義に入っていません。

任意の Elementary Topos が Grothendieck topos のような豊富な infinite colimits や injective-resolution machinery を持つわけでもありません。

したがって、

$\boxed{ \text{Grothendieck topos} \Rightarrow \text{cohomology の自然な舞台} }$

なのに対して、

$\boxed{ \text{Elementary topos} \Rightarrow \text{logic の自然な舞台} }$

という重心の違いがあります。

ただし両者は非常に深いところで結びつきます。

13. Lawvere の「局所真理」と cohomology

前に Kripke–Joyal semantics で、

$U\Vdash\exists x\,\varphi(x)$

なのに $U$ 上に global witness がない場合を見ました。

cover $U_i\to U$ 上には

$x_i$

がある。

しかし global

$x\in A(U)$

はない。

これは cohomology 的発想とほとんど隣り合っています。

Lawvere/Joyal semantics は、

$\boxed{ \text{「局所的に存在する」ことも内部的な真理として認める} }$

一方 cohomology は、追加の algebraic structure があるとき、

$\boxed{ \text{その局所的存在を global object にできない理由を測る} }$

のです。

私はこの二つの関係を、

$\boxed{ \text{internal logic} = \text{局所性を「真理」として読む} }$ $\boxed{ \text{cohomology} = \text{局所性と大域性の差を「不変量」として読む} }$

と整理するとよいと思います。

14. 前の Riemann 幾何の話にも戻れる

例えば line bundle $L$ は局所的には trivial：

$L|_{U_i}\simeq U_i\times\mathbb C.$

しかし global には trivial でない。

その twisting が

$H^1(M,\mathcal O^\times)$

に現れる。

connection を入れると curvature

$F$

が現れ、

$[F]$

が de Rham cohomology class になる。

例えば複素 line bundle なら適切な正規化により

$\left[\frac{F}{2\pi i}\right]$

が第一 Chern class と対応します。

したがって以前の

$\text{connection} \to \text{curvature} \to \text{holonomy}$

という微分幾何学的情報が、

$\boxed{\text{cohomology class}}$

として global に固定される。

つまり cohomology は、

$\boxed{ \text{infinitesimal/local information を global topological information に変換する} }$

役割も持っています。

15. 一枚の図にするとこうなる

Topos theory の構造を私は次のように見ると非常にわかりやすいと思います。

$\boxed{ \begin{array}{ccccc} \text{Grothendieck topology} &\longrightarrow& \text{Topos} &\longrightarrow& \text{Cohomology}\\[2mm] \text{何を cover とするか} && \text{局所世界} && \text{局所→大域の obstruction}\\[2mm] J && \operatorname{Sh}(C,J) && H^n \end{array}}$

一方 Lawvere 側を見ると、

$\boxed{ \begin{array}{ccccc} \text{Topos} &\longrightarrow& \Omega &\longrightarrow& \text{internal logic}\\ &&j:\Omega\to\Omega&&\\ &&\text{local truth}&& \end{array}}$

です。

したがって同じ topos から、

$\boxed{ \begin{array}{ccc} &\mathcal E&\\ \swarrow&&\searrow\\ \text{logic}&&\text{cohomology}\\ \text{何が局所的に真か}&& \text{何が大域化を妨げるか} \end{array}}$

という二つの方向が出てくる。

16. そして、Grothendieck の topos の核心に戻る

ここまで来ると、McLarty のビデオで Grothendieck がなぜ

「topos の言語を学ぶべきだ」

と言ったのかが少し違って見えてくると思います。

Topos は単なる「一般化された空間」ではありません。

それは、

$\boxed{ \text{局所性を決め、} }$ $\boxed{ \text{局所データを sheaf として組織し、} }$ $\boxed{ \text{その局所データが global になる過程と、その obstruction を cohomology で測る} }$

ための統一的な環境です。

ですから Grothendieck 的には、

$\boxed{ \text{Topos は空間の一般化であると同時に、cohomology を生産する機械} }$

だと言ってよいでしょう。

そして Lawvere を加えるなら、さらに、

$\boxed{ \text{Topos は「局所→大域」を} \begin{cases} \text{logic として内部から読み}\\ \text{cohomology として外部から測る} \end{cases} }$

構造なのだ、と見ることができます。

この観点から次に進むなら、かなり面白いのは 「 $H^1$ が torsor、 $H^2$ が gerbe になる」という階層を descent の言葉で実際に構成することです。そこまで進むと、通常の sheaf から stack、さらに higher topos へ向かう必然性が見えてきます。

Higher Topos について論じてください。

はい。ここまでの流れを受けると、Higher Topos はかなり自然に出てきます。

要点を先に言えば、

\boxed{ \text{普通の Topos が「集合値の局所データを貼る世界」なら、} }

\boxed{ \text{Higher Topos は「空間・ホモトピー型そのものを貼る世界」です。} }

そして cohomology の側から見ると、

H^1\;\text{の torsor}, \qquad H^2\;\text{の gerbe}, \qquad H^3,\ldots

と上へ進むにつれて、「集合」だけでは貼り合わせの高次情報を保持できなくなる。その必然的な到着点が stack → higher stack → $\infty$ -topos です。Grothendieck 自身も Pursuing Stacks で stacks を homotopical algebra と非可換 cohomology を統合する概念として追究していました。

1. 普通の sheaf では何が足りなくなるのか

普通の sheaf $\mathcal F$ は、局所 section

s_i\in \mathcal F(U_i)

が overlap で

s_i|_{U_{ij}}=s_j|_{U_{ij}}

と等しいなら貼れる、という構造でした。

これは対象が集合なら十分です。

ところが vector bundle や principal bundle を考えると、局所的な対象 $E_i$ は重なりで

E_i|_{U_{ij}} \cong E_j|_{U_{ij}}

と「等しい」のではなく、isomorphic です。

そして triple overlap では

\phi_{ij}\circ\phi_{jk}=\phi_{ik}

という coherence が必要になる。

つまり、

\boxed{ \text{object} + \text{isomorphisms between objects} }

まで保持しないといけません。

集合では足りず、

\boxed{\text{groupoid}}

が必要になります。

これが stack の第一歩です。

2. Sheaf から stack へ

普通の sheaf は各 $U$ に集合

\mathcal F(U)

を割り当てます。

stack は各 $U$ に groupoid

\mathcal X(U)

を割り当てます。

groupoid には

objects
isomorphisms

があります。

例えば

\mathcal X(U)= \{\text{vector bundles on }U\}

とすれば、

objects は vector bundles、

morphisms は bundle isomorphisms。

すると descent は、

E_i

を貼るだけでなく、

\phi_{ij}:E_j|_{U_{ij}}\overset{\sim}{\to}E_i|_{U_{ij}}

と、その compatibility

\phi_{ij}\phi_{jk}=\phi_{ik}

まで含みます。

これが

\boxed{\text{1-stack}}

の世界です。

3. $H^1$ が torsor だった理由がここで見える

前回、

H^1(X,G)

は $G$ -torsor を分類する、と述べました。

これは実は classifying object

BG

を使うと、

\boxed{ H^1(X,G) \cong \pi_0\operatorname{Map}(X,BG) }

という形になります。

$BG$ は「 $G$ -torsor 全体の moduli object」と考えられます。

普通の cohomology class を単なる集合の元として見る代わりに、

\boxed{ X\longrightarrow BG }

という map として見る。

Lurie も Higher Topos Theory の導入で、 $H^1$ を cocycle、 $X\to BG$ 、 $G$ -torsor という三つの見方で説明し、torsor の見方が任意の Grothendieck topos に一般化できることを強調しています。

4. ところが $H^2$ では groupoid だけでも足りなくなる

今度は $H^2(X,A)$ を考えます。

$H^1$ が torsor なら、

H^2

は何を分類するのでしょう。

答えは概ね

\boxed{A\text{-gerbes}}

です。

gerbe では局所 object $x_i$ があり、

double overlap で

\phi_{ij}:x_j\to x_i

を選びます。

しかし triple overlap で

\phi_{ij}\phi_{jk}

と

\phi_{ik}

が等しい必要はない。

その間に

\alpha_{ijk}: \phi_{ij}\phi_{jk} \Rightarrow \phi_{ik}

という 2-isomorphism を入れます。

すると今度は quadruple overlap で、その $\alpha$ 同士の coherence を要求しなければならない。

つまり、

\boxed{ \text{objects} \to \text{morphisms} \to \text{2-morphisms} }

が必要になります。

5. さらに $H^3,H^4,\ldots$ と進むと止まらない

$H^2$ で 2-morphisms が必要になった。

では $H^3$ は？

今度は

3\text{-morphisms}

まで必要になる。

そして

H^n

では $n$ 次の coherence。

したがって自然に、

\boxed{ \text{objects} \to \text{1-morphisms} \to \text{2-morphisms} \to \text{3-morphisms} \to\cdots }

という無限の階層に到達します。

これが higher category / $\infty$ -groupoid の世界です。

だから cohomology の階層そのものが、

\boxed{ \text{ordinary sheaf} \to \text{stack} \to \text{higher stack} }

を要求している、と見ることができます。

6. $\infty$ -groupoid とは何か

$\infty$ -topos で値に取る基本的な対象は

\boxed{\mathcal S}

すなわち spaces、同値に $\infty$ -groupoids です。

ざっくり言えば、

点
点の間の paths
paths の間の homotopies
homotopies の間の homotopies
…

をすべて保存する対象。

したがって集合

S

は「離散的な space」としてその特殊例です。

groupoid は 1-truncated space。

2-groupoid は 2-truncated space。

そして一般の homotopy type が $\infty$ -groupoid。

つまり、

\boxed{ \mathbf{Set} \subset \mathbf{Grpd} \subset \mathcal S. }

7. Grothendieck topos から $\infty$ -topos へ

普通の Grothendieck topos は

\operatorname{Sh}(C,J;\mathbf{Set})

つまり集合値 sheaf の圏です。

Higher Topos では集合の代わりに spaces を使います。

\boxed{ \operatorname{Sh}(C,J;\mathcal S) }

です。

これは site 上の space-valued sheaves、あるいは $\infty$ -stacks の $\infty$ -category。

Lurie の Higher Topos Theory はまさに Grothendieck topoi の higher-categorical version を研究するために $(\infty,1)$ -categories を展開しています。

8. 現代的な $\infty$ -topos の定義

小さな $\infty$ -category $C$ に対して presheaves of spaces

\mathcal P(C) = \operatorname{Fun}(C^{op},\mathcal S)

を考えます。

$\infty$ -topos $\mathcal X$ は、本質的にはこれの accessible left-exact localization

L:\mathcal P(C)\longrightarrow\mathcal X

として得られる $\infty$ -category です。

すなわち

\boxed{ \mathcal X \simeq \text{space-valued presheaves satisfying suitable descent} }

です。

これは普通の Grothendieck topos の

\operatorname{PSh}(C) \to \operatorname{Sh}(C,J)

という sheafification の higher version です。

Toën–Vezzosi も simplicial/higher sites 上の stacks と left-exact localizations という形で higher topos theory を構築しており、Lurie の理論と同じ大きな流れにあります。

9. Higher descent では「一致」ではなく homotopy coherent consistency

普通の sheaf condition は、cover $U_i\to U$ に対して

F(U) \to \prod_iF(U_i) \rightrightarrows \prod_{ij}F(U_{ij})

という equalizer で表されます。

higher sheaf では equalizer を ordinary equality で取るのではなく、

\boxed{\text{homotopy limit}}

で取ります。

つまり概念的には、

F(U) \simeq \operatorname{holim} \left( \prod_iF(U_i) \rightrightarrows \prod_{ij}F(U_{ij}) \triplerightarrow \prod_{ijk}F(U_{ijk}) \cdots \right).

ここでは

double overlap の equivalence
triple overlap の homotopy
quadruple overlap の higher homotopy
…

を全部記録します。

これが homotopy coherent descent です。

10. Čech nerve が本当の主人公になる

cover

U=\bigcup_iU_i

から Čech nerve

U_\bullet

を作ります。

U_0=\coprod_iU_i,

U_1=\coprod_{ij}U_i\cap U_j,

U_2=\coprod_{ijk}U_i\cap U_j\cap U_k,

以下同様。

普通の sheaf なら低次だけで十分に見えます。

higher sheaf では全 simplicial diagram

U_\bullet

を使い、

\boxed{ F(U)\simeq \lim_{\Delta}F(U_\bullet) }

を要求します。

この simplicial direction が、

H^0,H^1,H^2,\ldots

の階層と非常によく対応しています。

11. Cohomology が higher topos ではもっと自然になる

ordinary topos では cohomology を derived functor として

H^n=R^n\Gamma

と作りました。

$\infty$ -topos ではもっと幾何学的に書けます。

abelian group object $A$ に対して、その delooping

BA,\quad B^2A,\quad\dots

を作ります。

すると、

\boxed{ H^n(X;A) = \pi_0\operatorname{Map}_{\mathcal X}(X,B^nA) }

と考えることができます。

$B^nA$ は Eilenberg–Mac Lane object

K(A,n)

に相当します。

したがって

\boxed{ \text{cohomology class} = \text{map into a classifying object} }

になります。

これは derived functor よりも higher-topos 的には本質的な姿です。

12. $H^0,H^1,H^2$ が一つの公式になる

この公式は非常に美しいです。

$n=0$

H^0(X,A) = \pi_0\operatorname{Map}(X,A).

global sections。

$n=1$

H^1(X,A) = \pi_0\operatorname{Map}(X,BA).

$A$ -torsors。

$n=2$

H^2(X,A) = \pi_0\operatorname{Map}(X,B^2A).

$A$ -gerbes。

一般に

\boxed{ H^n(X,A) = \{\text{\(A\)-\(n\)-gerbes / higher torsors}\} }

という統一像が現れます。

つまり higher topos は、cohomology の degree を「派生 functor の添字」ではなく、

\boxed{ \text{geometric object の高さ} }

として見せてくれます。

13. 非可換 cohomology も自然になる

ordinary derived functor cohomology は基本的に abelian coefficients が得意です。

しかし higher topos では group object $G$ に対して

BG

を考えられます。

したがって

H^1(X,G) = \pi_0\operatorname{Map}(X,BG)

は $G$ が非可換でも意味を持ちます。

さらに higher group objects を使えば

B^2G,\ B^3G,\ldots

へ進める。

Grothendieck が Pursuing Stacks で目指した「non-commutative cohomological algebra」と homotopy theory の統合は、まさにこの方向です。

14. Homotopy と cohomology が同じ世界に入る

ordinary topos では homotopy theory をやろうとすると、simplicial sheaves などを別途導入する必要がありました。

$\infty$ -topos では objects が最初から homotopy types を持っています。

したがって内部的に

\pi_0(X),\quad \pi_1(X),\quad \pi_2(X),\ldots

という homotopy sheaves が存在します。

また

X\to\tau_{\le n}X

という truncation、

\cdots\to\tau_{\le2}X \to\tau_{\le1}X \to\tau_{\le0}X

という Postnikov tower も内部で構成できます。

つまり、

\boxed{ \text{sheaf theory} + \text{homotopy theory} + \text{cohomology} }

が一つの言語に統合されます。

nLab も $(\infty,1)$ -topos が intrinsic な homotopy と cohomology を持つ点を特徴として挙げています。

15. Ordinary topos は Higher Topos の 0-truncated 部分

ここが非常に重要です。

$\infty$ -topos

\mathcal X

の中で 0-truncated objects だけを見ると、ordinary Grothendieck topos が得られます。

直感的には、

\boxed{ \text{higher homotopy を全部忘れて集合だけ残す} }

操作です。

つまり ordinary topos は higher topos と別の理論ではありません。

\boxed{ \text{ordinary topos} = \text{higher topos の discrete/0-truncated shadow} }

と見ることができます。

16. では Lawvere の Elementary Topos はどうなるか

ここが前の話との重要な接続です。

Elementary Topos では subobject classifier

\Omega

が truth values を表していました。

しかし $\infty$ -topos では object $X$ 自体に、

x=y

という equality が単なる命題ではなく、

\boxed{\operatorname{Path}_X(x,y)}

という space を持ちます。

その中には

path
paths between paths
higher paths

がある。

つまり「等しいかどうか」自体に higher structure が入ります。

ここから Homotopy Type Theory との関係が出てきます。

Lawvere 的な

\boxed{\text{topos の内部で数学する}}

という思想が、Higher Topos では

\boxed{ \text{identity 自体を homotopy type として内部化する} }

ところまで進みます。

17. Proposition は higher world の中の特殊な type

ordinary Elementary Topos では

\Omega

が central でした。

Higher Topos では propositions は、すべての object の中の非常に低い部分、

\boxed{(-1)\text{-truncated objects}}

に対応します。

概念的には、

$(-1)$ -type = proposition
$0$ -type = set
$1$ -type = groupoid-like type
$2$ -type = 2-groupoid-like type
…
$\infty$ -type = general homotopy type

です。

したがって Lawvere の logic は消えるのではなく、

\boxed{ \text{higher type theory の lowest layer} }

として残ります。

18. Descent から hyperdescent へ

Higher Topos ではさらに subtle な問題があります。

普通の cover の Čech nerve だけでなく、

\boxed{\text{hypercover}}

という higher resolution を使うことがあります。

それに対する descent が hyperdescent。

Lurie は

\operatorname{Shv}(X)

と、その hypercompletion

\operatorname{Shv}(X)^\wedge

を区別します。

hypercomplete objects は arbitrary hypercovers に対する descent を満たし、通常の $\infty$ -sheaves は ordinary covers に対する descent を基本とします。

これは、

\boxed{ \text{局所情報を何段階まで調べれば global object が決まるか} }

という higher version の問題です。

19. Riemann 幾何との話へ戻すと

前に connection と curvature を見ました。

ordinary manifold は local charts を貼る。

bundle は local trivializations を貼る。

connection は local infinitesimal transport を貼る。

Higher Topos へ進むと、その貼り合わせデータ自体にも

\text{isomorphisms}, \quad \text{isomorphisms between isomorphisms}, \quad\dots

を許します。

例えば gauge theory では、

fields
gauge transformations
gauge transformations between gauge transformations

という higher groupoid が自然に出ます。

したがって physical/moduli space は本当は単なる集合ではなく、

\boxed{\text{moduli stack / higher stack}}

になる。

「同値な configuration を quotient して集合にする」のではなく、同値そのものを情報として残すわけです。

20. Moduli space から moduli stack への革命

ordinary quotient

X/G

では stabilizer 情報が失われます。

stack quotient

[X/G]

では、点 $x$ の automorphism group

G_x

も保存されます。

Higher stack ならさらに、

\operatorname{Aut}(x)

自体が space/higher groupoid になり得ます。

したがって Higher Topos は、

\boxed{ \text{「対象だけでなく、その対象の symmetries と higher symmetries まで含めた geometry」} }

を扱う自然な空間概念です。

21. Derived algebraic geometry への橋

これは現代幾何で非常に重要です。

ordinary scheme では local model は

\operatorname{Spec}A.

Derived Algebraic Geometry では $A$ を ordinary ring だけでなく、例えば

E_\infty\text{-ring}

や derived ring に置き換えます。

すると intersections も ordinary fiber product ではなく derived fiber product になり、

\operatorname{Tor},\operatorname{Ext}

などの hidden homological information を幾何そのものに保持します。

これを貼る ambient geometry が $\infty$ -topos / structured $\infty$ -topos です。

Lurie 自身 Higher Topos Theory に続いて structured spaces と derived/spectral algebraic geometry をこの枠組みで発展させています。

22. これまでの流れを一本にすると

ここまで話してきた歴史を、一つの階段として見ることができます。

\boxed{\text{Riemann}}

\text{local Euclidean charts} \longrightarrow \text{manifold}

↓

\boxed{\text{Grothendieck}}

\text{local objects + covers} \longrightarrow \text{sheaves/topos}

↓

\boxed{\text{Cohomology}}

\text{failure / twisting of global gluing} \longrightarrow H^1,H^2,\ldots

↓

\boxed{\text{Stacks}}

\text{objects + isomorphisms}

↓

\boxed{\text{Higher Stacks}}

\text{objects + morphisms + higher morphisms}

↓

\boxed{\text{Higher Topos}}

\text{homotopy-coherent local-to-global geometry}.

23. Grothendieck と Lawvere が Higher Topos で再び合流する

私はここが一番重要だと思います。

Grothendieck の中心思想は

\boxed{\text{geometry = descent}}

でした。

Lawvere の中心思想は

\boxed{\text{topos = universe in which mathematics is done internally}}

でした。

Higher Topos ではこの二つが、

\boxed{ \text{homotopy-coherent descent} + \text{higher internal mathematics} }

として融合します。

外から見ると、

\boxed{\text{generalized higher space}}

内部から見ると、

\boxed{\text{universe of homotopy types}}

です。

24. Cohomology の位置づけもここで変わる

ordinary topos では cohomology は

R^n\Gamma

という「derived invariant」に見えました。

Higher Topos では、それが

\boxed{ X\to B^nA }

という普通の mapping problemになります。

これは非常に大きな概念的転換です。

つまり、

\boxed{ \text{cohomology は Higher Topos の中では “derived” な例外ではなく、geometry そのものになる。} }

torsor は $BG$ への map。

gerbe は $B^2A$ への map。

higher gerbe は $B^nA$ への map。

そして cohomology はその connected components

\pi_0\operatorname{Map}(X,B^nA)

です。

この意味で Higher Topos は、Grothendieck が cohomology を通じて追いかけていた local-to-global structure を、homotopy level まで完全に幾何学化したものだと私は捉えるのがよいと思います。

そして次に進むなら、いよいよ Higher Topos と Homotopy Type Theory / Univalent Foundations の関係を見るのが自然です。そこでは Lawvere の「内部論理」が、 $\Omega$ による命題論理から、identity が path である higher-dimensional logic に変わります。

Higher Topos と、VoevodskyのHoTT/Univalent Foundationの関係を論じてください。

はい。ここまでの流れを踏まえると、Higher Topos と Voevodsky の HoTT / Univalent Foundations の関係は、かなり自然に理解できます。

核心を先に言えば、

$\boxed{ \text{Higher Topos は「高次の空間」の意味論であり、} }$ $\boxed{ \text{HoTT はその内部で数学をするための言語である} }$

という関係です。

そして Univalence は、その内部言語が Higher Topos の「同値を本質とする幾何」を正しく表現するための決定的な原理です。実際、Shulman は任意の Grothendieck $(\infty,1)$ -topos が strict univalent universes をもつモデルで提示でき、HoTT を $(\infty,1)$ -topos の内部言語として使えることを示しています。(arXiv)

1. Lawvere の Elementary Topos との類比から始める

まず普通の Elementary Topos を思い出します。

Lawvere の発想では topos $\mathcal E$ は、

$\boxed{\text{その内部で集合・関数・命題を扱える数学的 universe}}$

でした。

外から見ると $\mathcal E$ は category。

しかし内部では、

$A\in\mathcal E$

を「集合」あるいは「type」のように扱います。

subobject classifier

$\Omega$

が truth values を与え、

$\forall,\exists,\land,\lor,\Rightarrow$

が内部論理として解釈される。

したがって、

$\boxed{ \text{Elementary Topos} \quad\leftrightarrow\quad \text{intuitionistic higher-order logic} }$

という対応がありました。

Higher Topos では、これが一段上がります。

2. 「集合」を「homotopy type」に置き換える

Lurie の $\infty$ -topos は、普通の topos が Sets のように振る舞うのに対し、

$\boxed{\text{Spaces / homotopy types のように振る舞う}}$

$\infty$ -category です。

Lurie 自身、 $\infty$ -topos を「ordinary topos が sets に似ているのと同じ意味で spaces に似ている $\infty$ -category」と説明し、presheaves of spaces の accessible left-exact localization として特徴づけています。(IAS Math)

つまり ordinary topos では、

$\text{object}=\text{variable set}$

だったものが Higher Topos では、

$\boxed{\text{object}=\text{variable homotopy type}}$

になります。

ここが HoTT の出発点とぴったり一致します。

Voevodsky は Univalent Foundations Project で、従来の「types を sets として解釈する」意味論ではなく、

$\boxed{\text{types を homotopy types として解釈する}}$

意味論を基礎に据えると明言しています。(IAS Math)

3. HoTT では「等号」が path になる

ここが普通の topos と Higher Topos の最大の違いです。

型 $A$ と二つの元

$x,y:A$

があるとします。

通常の集合論なら

$x=y$

は単なる proposition です。

しかし HoTT では、

$\boxed{x=_A y}$

そのものが type です。

homotopy 的に読むと、

$\boxed{x=_Ay \quad\sim\quad \text{paths from }x\text{ to }y}$

です。

さらに二つの paths

$p,q:x=y$

の間にも

$p=q$

という type がある。

これは

$\boxed{\text{homotopy between paths}}$

になります。

さらに、

$\text{homotopy between homotopies},$

その上も……。

したがって一つの type $A$ は、

$\begin{aligned} &\text{points},\\ &\text{paths},\\ &\text{paths between paths},\\ &\ldots \end{aligned}$

を持つ。

これはまさに

$\boxed{\infty\text{-groupoid}}$

です。

HoTT Book も、type theory と homotopy theory の結合、weak $\infty$ -groupoids、univalence を中心に据えています。(Homotopy Type Theory)

4. Higher Topos ではこの解釈が文字通り成立する

$\infty$ -topos $\mathcal X$ の object $A$ を type と考えます。

その中の二点

$x,y:1\to A$

について、identity type は概念的には path space

$\operatorname{Path}_A(x,y)$

として解釈されます。

したがって、

$\boxed{ \begin{array}{ccc} \text{HoTT}&&\infty\text{-Topos}\\ \hline A:\mathrm{Type}&&A\in\mathcal X\\ x:A&&1\to A\\ x=_A y&&\operatorname{Path}_A(x,y)\\ A\to B&&\text{map }A\to B\\ A\simeq B&&\text{equivalence}\\ \end{array}}$

となります。

つまり HoTT の syntactic な identity types は、Higher Topos 側では genuine な homotopy data を表します。

5. dependent type も Higher Topos の幾何そのものになる

HoTT は dependent type theory です。

例えば

$x:A\vdash B(x):\mathrm{Type}$

という dependent type を考えます。

これは Higher Topos では map

$\boxed{ p:E\longrightarrow A }$

として表現されます。

fiber は

$E_x$

で、これが $B(x)$ 。

つまり、

$B(x) = \text{fiber of }E\to A\text{ over }x.$

これはものすごく幾何学的です。

多様体なら、

$TM\to M$

を考え、

$T_xM$

を fiber としていました。

同じ形です。

したがって dependent type は、

$\boxed{\text{variable family of spaces}}$

にほかなりません。

6. $\Sigma$ と $\Pi$ は幾何学的 adjunction

Lawvere の話とも直接つながります。

dependent type

$B(x)$

について、

$\sum_{x:A} B(x)$

という dependent sum と、

$\prod_{x:A}B(x)$

という dependent product があります。

Higher Topos 側では、map

$f:A\to B$

に対する pullback

$f^*$

の左右 adjoint として、

$\boxed{ \Sigma_f\dashv f^*\dashv\Pi_f }$

が現れます。

これは Lawvere が量化子

$\exists,\forall$

を adjoint として理解したことの higher-dimensional version です。

つまり、

$\boxed{ \exists \rightsquigarrow \Sigma\text{-type} }$ $\boxed{ \forall \rightsquigarrow \Pi\text{-type} }$

になります。

この意味で HoTT は Lawvere の categorical logic の非常に自然な発展です。

7. では Univalence は何を言っているのか

ここが Voevodsky の決定的な発見です。

universe

$\mathcal U$

を考え、その中に二つの type

$A,B:\mathcal U$

があるとします。

普通の type theory でも、

$A=_\mathcal U B$

なら

$A\simeq B$

を得られます。

つまり canonical map

$\boxed{ \operatorname{idtoeqv}: (A=_\mathcal U B) \longrightarrow (A\simeq B) }$

があります。

Voevodsky の Univalence Axiom は、

$\boxed{ (A=_\mathcal U B) \simeq (A\simeq B) }$

だと言います。

HoTT Book ではこれを、type の identity と equivalence を結びつける universe-level extensionality として定式化しています。(Homotopy Type Theory)

8. 「同型なら等しい」と言っているのか？

よくそう説明されますが、少し注意が必要です。

単純に、

isomorphic objects を同一視して quotient する

と言っているのではありません。

むしろ、

$\boxed{ \text{types の identity space 自体が equivalence space である} }$

と言っています。

例えば $A$ に非自明な automorphism

$f:A\simeq A$

があれば、univalence によりそれは

$p:A=_\mathcal U A$

という loop になります。

したがって universe $\mathcal U$ は「types の集合」ではありません。

その中には、

$\boxed{\text{automorphisms が loops として残っている}}$

のです。

これは moduli stack / higher stack の発想と非常によく似ています。

9. ここで Higher Topos と Univalence が本質的につながる

Higher Topos では object を「等号を無視して quotient」するのではありません。

equivalence と higher equivalence を全部保存します。

ですから「small objects の universe」

$p:\widetilde{\mathcal U}\to\mathcal U$

を作るとき、

$\mathcal U$

を単なる isomorphism classes の集合にしてしまうのは不自然です。

types の symmetries も保持すべきです。

Univalence はまさに、

$\boxed{ \mathcal U\text{ が objects と their equivalences を正しく記録する moduli space である} }$

という条件になります。

Gepner–Kock はこの関係を $\infty$ -categorical に定式化し、univalent families を Lurie の bounded local classes と結びつけ、各 $\infty$ -topos が regular cardinal ごとの universal univalent families を持つことを示しました。(arXiv)

これは非常に重要な結果です。

10. Voevodsky の最初のモデルは simplicial sets

歴史的には、Voevodsky はいきなり abstract $\infty$ -topos から始めたわけではありません。

彼が構成した中心的な意味論は、

$\boxed{\mathbf{sSet}}$

すなわち simplicial sets の Kan model です。

simplicial sets は homotopy types の標準的なモデルです。

Kapulkin–Lumsdaine による Voevodsky の simplicial model の詳細な構成では、

dependent types を fibrations として解釈し、
universe fibration を構成し、
その universe が Univalence Axiom を満たす

ことが証明されています。(arXiv)

つまり、

$\boxed{ \text{HoTT syntax} \longrightarrow \text{simplicial homotopy theory} }$

という橋が最初に作られました。

そして simplicial sets の homotopy theory が表している $\infty$ -category は、

$\boxed{\mathcal S}$

つまり spaces の $\infty$ -topos です。

11. そこから任意の $\infty$ -topos へ一般化された

したがって歴史的順序は、

$\boxed{ \text{Voevodsky's simplicial model} }$

から始まり、

$\boxed{ \text{more general homotopical models} }$

へ進み、

最終的に

$\boxed{ \infty\text{-topos semantics} }$

として理解されるようになった、と見るのがよいでしょう。

Shulman は早くから diagram $\infty$ -topoi に univalent models を構成しました。(arXiv)

さらに2019年には、すべての Grothendieck $(\infty,1)$ -toposes が strict univalent universes を持つ model-category presentation を持つことを証明しました。(arXiv)

したがって今日ではかなり正確な意味で、

$\boxed{ \text{HoTT is an internal language for }(\infty,1)\text{-toposes} }$

と言えるようになっています。

12. ただし「HoTT = Higher Topos Theory」ではない

ここは大切です。

Higher Topos Theory は semantic / categorical theory です。

$\mathcal X$

という $\infty$ -category を外から研究します。

一方 HoTT は formal language / syntax です。

$x:A\vdash b:B(x)$

のような judgment を使います。

したがって関係は、

$\boxed{ \begin{array}{ccc} \text{Higher Topos Theory} && \text{HoTT}\\ \hline \text{external semantics} && \text{internal language}\\ \infty\text{-categories} && \text{dependent types}\\ \text{maps/fibrations} && \text{terms/type families}\\ \text{equivalences} && \text{identity/univalence} \end{array}}$

です。

普通の

$\text{Topos}\leftrightarrow\text{internal logic}$

と同じ関係が higher-dimensional になったのです。

13. Univalent Foundations は HoTT よりもう少し大きな構想

ここも用語を分けておくとよいです。

HoTT は主として、

$\boxed{\text{homotopy-theoretic interpretation of dependent type theory}}$

を指します。

一方 Voevodsky の Univalent Foundations は、

$\boxed{ \text{HoTT + Univalence を基盤として数学全体を再構築する foundation program} }$

です。

Voevodsky 自身は、

categorical / higher categorical thinking を自然に含むこと、
dependent type systems で形式化しやすいこと、
sets ではなく homotopy types の世界を直接公理化すること、
constructive と non-constructive の両方を扱えること

を Univalent Foundations の特徴として挙げています。(IAS Math)

そして proof assistant で machine verification することが、最初から大きな動機でした。(IAS Math)

14. 「Sets は消える」のではなく、低次の types になる

これは Grothendieck → Higher Topos の話とよく似ています。

Univalent Foundations では sets を捨てるわけではありません。

一般の types の中で、

$\boxed{\text{0-truncated types}}$

が sets に相当します。

現在一般的な indexing では、

$\begin{array}{ccl} (-1)\text{-type}&=&\text{mere proposition},\\ 0\text{-type}&=&\text{set},\\ 1\text{-type}&=&\text{groupoid-like type},\\ 2\text{-type}&=&\text{2-groupoid-like type},\\ &&\vdots \end{array}$

です。

Voevodsky の元の h-level 表記では index が2つずれており、彼は propositions、sets、groupoids を h-level 1,2,3 と説明していました。(IAS Math)

したがって、

$\boxed{ \mathbf{Set} \text{ は higher world の特殊な truncated layer} }$

です。

これは、

$\boxed{ \text{ordinary topos} = \infty\text{-topos の 0-truncated shadow} }$

という前回の話と完全に平行しています。

15. Higher inductive types がもう一つの橋になる

HoTT には Univalence と並んで Higher Inductive Types (HITs) が重要です。

普通の inductive type は points を生成します。

例えば自然数なら

$0:\mathbb N,\qquad succ:\mathbb N\to\mathbb N.$

Higher inductive type では、points だけでなく paths も generator として指定できます。

例えば circle $S^1$ を、

$base:S^1$

と

$loop:base=base$

から作る。

つまり、

$\boxed{\text{空間を type として直接生成する}}$

ことができます。

これは Higher Topos 側の colimit constructions と深く関係しています。

ただし「任意の HIT が任意の $\infty$ -topos で自動的に存在する」と単純に言うのは強すぎます。どの type formers / HITs を解釈するかには、対応する closure や model の条件が必要です。

16. Cohomology も HoTT の内部で geometry になる

前回、

$H^n(X;A) = \pi_0\operatorname{Map}(X,K(A,n))$

という Higher Topos 的な見方をしました。

HoTT 内部では、

$K(A,n)$

自体が type として扱えます。

そして map

$X\to K(A,n)$

も普通の function type

$X\to K(A,n)$

です。

つまり cohomology が、

$\boxed{ \text{外から derived functor を構成するもの} }$

だけでなく、

$\boxed{ \text{内部の mapping type として扱える} }$

ようになります。

これは Grothendieck が cohomology のために作った topos の構想が、非常に遠いところで Voevodsky の type theory と再接続している例だと思います。

17. Univalence は「構造主義」を数学的に非常に強く実現する

ここには foundational な意味があります。

通常の集合論では、同型な群

$G\cong H$

でも基礎となる sets が違えば

$G\neq H$

です。

数学者は普段、

「同型なものは同じものとして扱う」

と言いますが、formal foundations の level では本当に同じではありません。

Univalence を使うと、

$G\simeq H$

から universe 内で

$G=H$

を得られ、それに沿って任意の construction や theorem を transport できます。

Voevodsky はこの automatic transport を Univalence の重要な特徴として説明しています。(IAS Math)

つまり、

$\boxed{ \text{mathematics should depend on structure, not presentation} }$

という原則が、単なる informal convention ではなく foundation に組み込まれます。

18. これは Grothendieck の「presentation independence」と非常によく似ている

ここまで話してきた Grothendieck と Voevodsky を比べると、面白い共通点があります。

Grothendieck topos は、

$(C,J)$

という一つの site presentation に依存しない。

異なる sites

$(C,J),\qquad(D,K)$

が equivalent topoi を表すことがあります。

重要なのは presentation ではなく、

$\operatorname{Sh}(C,J)$

という invariant な対象。

Voevodsky では、

$A,\quad B$

という presentations が違っても、

$A\simeq B$

なら、その equivalence を identity と同じ level で扱う。

したがって両者には、

$\boxed{ \text{presentation ではなく equivalence-invariant structure を本体とする} }$

という非常に強い共通思想があります。

19. Riemann からここまで一本の線を引ける

これまでの対話を全部つなぐと、私は次のような流れが見えると思います。

$\boxed{\text{Riemann}}$

局所 charts を貼り、

$\text{local Euclidean data} \to \text{manifold}$

を作る。

↓

$\boxed{\text{Grothendieck}}$

「局所」の概念そのものを site に一般化し、

$\text{local objects + descent} \to \text{topos}$

とする。

↓

$\boxed{\text{Higher Topos}}$

「一致」を equality ではなく equivalence + higher equivalences にし、

$\text{homotopy coherent descent} \to \infty\text{-topos}.$

↓

$\boxed{\text{Lawvere}}$

topos を外から眺めるだけでなく、

$\text{その内部で数学する}$

という発想を導入する。

↓

$\boxed{\text{Voevodsky}}$

Higher Topos 的な内部世界を dependent type theory に持ち込み、

$\boxed{\text{identity itself = homotopy}}$

さらに

$\boxed{\text{equivalence = identity of types}}$

という Univalence を置く。

20. したがって二つの方向が完全に合流する

これを一枚の図にすると、とても美しいです。

$\boxed{ \begin{array}{ccccc} &&\infty\text{-Topos }\mathcal X&&\\[2mm] &\swarrow&&\searrow&\\ \text{Grothendieck/Lurie}&&&& \text{Lawvere/Voevodsky}\\ \text{external geometry}&&&& \text{internal language}\\ \text{descent}&&&& \text{dependent types}\\ \text{higher equivalences}&&&& \text{identity types}\\ \text{universal families}&&&& \text{univalent universes} \end{array}}$

そして中央の対応が

$\boxed{ (A=B) \simeq (A\simeq B) }$

です。

Gepner–Kock の結果は、これは単に Voevodsky が type theory に人工的に追加した奇妙な公理ではなく、 $\infty$ -topos における universal families が本来持つ幾何学的性質として理解できることを示しています。(arXiv)

21. 私が一番重要だと思う点

Grothendieck は「空間」を点集合から解放しました。

$\boxed{ \text{space} \neq \text{set of points} }$

Lawvere は「数学的世界」を一つの外部集合論から解放しました。

$\boxed{ \text{mathematics can be internal to a topos} }$

Higher Topos は「対象」を集合から解放します。

$\boxed{ \text{object} = \text{homotopy type with higher symmetries} }$

そして Voevodsky は最後に「等号」を rigid な equality から解放した、と言えるでしょう。

$\boxed{ \text{identity} = \text{space of identifications} }$

さらに Univalence によって、

$\boxed{ \text{identity of structures} = \text{equivalence of structures}. }$

この意味では、Univalent Foundations は Higher Topos の思想を単に利用しているだけではなく、Grothendieck–Lawvere 的な「空間と論理」の統一を、数学の基礎そのものへ押し進めたものと見ることができます。

そして次の一歩として非常に面白いのは、ここから 「Univalence と category theory」 を見ることです。通常の category では $A\cong B$ と $A=B$ は違いますが、univalent category では

$\boxed{(A=B)\simeq(A\cong B)}$

となります。これはまさに Grothendieck が「category は isomorphism ではなく equivalence まで考えるべきだ」と語っていた問題に、Voevodsky の原理がどう答えるか、という話につながります。

GrothendieckとVoevodsky

Grothendieck が「category は isomorphism ではなく equivalence まで考えるべきだ」と語っていた問題に、Voevodsky の原理はどのようにこたえますか？

はい。ここは Grothendieck の圏論的実践に、Voevodsky が基礎論的な答えを与えたと見ることができます。ただし非常に大切なのは、「同値なものを雑に同一視する」のではなく、同値そのものを等号の構造として取り込む、という点です。

1. Grothendieck が感じていた問題

McLarty のビデオで紹介されていた Grothendieck の発言では、Chevalley の universal algebra の議論について、圏を「同型まで」で扱おうとしたため非常に複雑になった、という趣旨の批判がありました。

圏 $C,D$ には三種類の「同じ」があります。

$C=D, \qquad C\cong D, \qquad C\simeq D.$

普通の集合論的基礎では、

$C=D$

は対象集合も射集合も文字どおり同じという極端に強い条件です。

$C\cong D$

もまだ強い。圏論で本当に自然なのは

$\boxed{C\simeq D}$

すなわち equivalence of categories です。

圏論的な性質の大部分は equivalence の下で不変です。それなのに基礎論の「等号」は equivalence よりはるかに細かい。このずれが問題でした。Ahrens–Kapulkin–Shulman も、従来の集合論的基礎では foundational equality と圏論で実際に使う sameness の間にこの不一致があることを、univalent category 導入の動機として明示しています。(ケンブリッジ大学出版局)

2. Voevodsky の第一の答え：equivalence を equality に持ち上げる

Univalence の基本公式は、

$\boxed{ (A=_\mathcal U B) \simeq (A\simeq B) }$

です。

通常、

$A=B$

なら当然 $A\simeq B$ です。

Voevodsky は逆方向まで要求します。

$A\simeq B \quad\Longrightarrow\quad A=B$

ただし、ここでいう $=$ は集合論の「同じ符号列・同じ underlying set」という rigid な equality ではありません。

HoTT では

$A=B$

自体が identity type、つまり path の空間です。

したがって Voevodsky の答えは、

「同値なものを区別しないことにしよう」

ではなく、

「同値こそが、構造を持つ世界における正しい identity なのだ」

というものです。HoTT Book も Chapter 9 の category theory について、univalence に従って「equality is isomorphism」を採用すると、構成が自動的に equivalence of categories の下で不変になり、適切な category では equivalent categories が equal になると説明しています。(Homotopy Type Theory)

3. まず一つの category の「objects」で Grothendieck の問題を解く

圏 $C$ の二つの対象

$x,y:C$

について、通常は

$x=y$

と

$x\cong y$

は全然違います。

そこで canonical map

$\operatorname{idtoiso}_{x,y}: (x=y)\longrightarrow(x\cong y)$

を考えます。

univalent category とは、この map が equivalence、

$\boxed{ (x=y)\simeq(x\cong y) }$

となる category です。

つまり category の内部では、

$\boxed{\text{isomorphic objects are equal}}$

が成立する。

Ahrens–Kapulkin–Shulman はこれを saturated / univalent category と呼びました。(arXiv)

これは Grothendieck 的な数学の実践と非常によく合っています。

例えば universal property で定まる coproduct $A\amalg B$ は普通、

unique up to unique isomorphism

です。

Univalent category ではその unique isomorphism が identity を与えるため、より文字どおりに

$\boxed{\text{unique}}$

と言えるようになります。

4. そして category 自体について equivalence が equality になる

さらに一段上に行きます。

univalent categories $C,D$ については、適切な universe の中で

$\boxed{ (C=D) \simeq (C\simeq D) }$

という対応が得られます。

ここで右辺は equivalence of categories。

これこそ、Grothendieck が求めていた

category を isomorphism ではなく equivalence までで考える

という態度を、foundation の equality そのものに反映したものです。

Ahrens–Kapulkin–Shulman の論文の表現を借りれば、彼らの category の概念では “equality and equivalence of categories agree” します。(ケンブリッジ大学出版局)

したがって、

$\boxed{ C\simeq D \quad\Rightarrow\quad C=D }$

となり、等号に対して使える ordinary substitution / transport が、そのまま categorical equivalence に対して使えるようになります。

これがすごく大きい。

5. 従来は「同値に不変であること」を毎回証明していた

従来なら category について何か construction

$P(C)$

を定義したとき、

$C\simeq D$

なら

$P(C)\simeq P(D)$

あるいは

$P(C)\cong P(D)$

になることを別途証明する必要がありました。

つまり、

$\boxed{\text{この construction は presentation に依存しません}}$

という証明を繰り返す。

Univalent Foundations では、

$C\simeq D$

を

$C=D$

へ変換できるので、

$P(C)=P(D)$

は equality の substitution principle から自動的に出ます。

だから、

$\boxed{ \text{equivalence invariance が theorem ではなく foundation に組み込まれる} }$

わけです。

これは Voevodsky の構造主義的な効用の非常に大きな部分です。HoTT の解説でも、univalence により constructions が automatically invariant under equivalence になることが強調されています。(Homotopy Type Theory)

6. ただし「全部 quotient してしまう」のではない

ここが一番美しいところだと思います。

素朴な解決法なら、

isomorphic objects を equivalence classes にしてしまえばいい。

つまり skeleton を取る、あるいは quotient する。

しかしこれは symmetry information を失います。

例えば object $A$ に

$\operatorname{Aut}(A)$

という nontrivial automorphisms があったとします。

quotient して「同型類」という一点にしてしまうと、この automorphism が見えなくなります。

Univalence では違います。

$A\simeq A$

という automorphism は、

$A=_\mathcal U A$

という loop になります。

したがって、

$\boxed{ \operatorname{Aut}(A) \quad\leftrightarrow\quad \text{loops at }A }$

です。

つまり、

$\boxed{ \text{同値なものを同一視しながら、その同値の仕方は捨てない。} }$

これが quotient と univalence の決定的な違いです。

Higher Topos / $\infty$ -groupoid 的発想がまさにここにあります。

7. Grothendieck の「equivalence まで」と非常によく響き合う

Grothendieck の category theory では、presentation は本体ではありません。

例えば topos は site

$(C,J)$

で presentation できますが、

$(C,J) \neq(D,K)$

でも

$\operatorname{Sh}(C,J) \simeq \operatorname{Sh}(D,K)$

なら同じ geometry を表していると考えるべきです。

つまり、

$\boxed{ \text{presentation} \quad\text{ではなく}\quad \text{equivalence class of structures} }$

が本質です。

ところが「equivalence class」と言って quotient してしまうと、また higher symmetry を失う。

Voevodsky はここで、

$\boxed{ \text{equivalence class を作るのではなく、 equivalence を identity paths にする} }$

という、より高次圏論的な解決を与えたと考えられます。

8. Rezk completion がこの関係をさらに明瞭にする

では ordinary な category $C$ が univalent でなかったらどうするか。

Ahrens–Kapulkin–Shulman は、

$C\longrightarrow RC(C)$

という Rezk completion を構成します。

$RC(C)$ は univalent category で、

$C\simeq RC(C)$

という意味で元の category と同じ categorical information を持ちます。

しかも universal な仕方で行われます。(arXiv)

概念的には、

$\boxed{ \text{ordinary category} \longrightarrow \text{equivalence を identity として正しく認識する category} }$

です。

これは Grothendieck の発想にかなり近い。

つまり、

「presentation の rigid な equality を捨て、categorically meaningful な equivalence まで saturate する」

という操作です。

9. Higher category theory では Rezk completeness になる

ここから Higher Topos との接続も見えます。

$(\infty,1)$ -category を Segal space でモデルすると、単に Segal condition を満たすだけでは「equivalence と identity」の対応が十分ではありません。

そこで Rezk completeness condition を課します。

大ざっぱには、

$\boxed{ \text{equivalences between objects} \quad\simeq\quad \text{paths between objects} }$

とする条件です。

これは univalent category の

$(x=y)\simeq(x\cong y)$

の higher-dimensional version そのものです。

実際、univalent category の Rezk completion は homotopical / higher-categorical semantics では Segal space の Rezk completion の truncated analogue に対応すると説明されています。(ケンブリッジ大学出版局)

したがって、

$\boxed{ \text{Voevodsky univalence} \;\longleftrightarrow\; \text{Rezk completeness} }$

には深い対応があります。

10. Grothendieck の要求を三段階に分けると

整理すると、問題と答えはこうなります。

段階	従来の rigid な考え	圏論的に自然な sameness	Univalent な答え
Sets / types	$A=B$	$A\simeq B$	$(A=B)\simeq(A\simeq B)$
category 内の objects	$x=y$	$x\cong y$	$(x=y)\simeq(x\cong y)$
categories	$C=D$ / $C\cong D$	$C\simeq D$	$(C=D)\simeq(C\simeq D)$

この第三段が、まさに Buffalo 講義で Grothendieck が問題にしていたことに最も直接対応します。

11. ただし、一点だけ歴史的・数学的に慎重でありたい

「Grothendieck の問題を Voevodsky が解決した」と言う場合、Voevodsky 本人が Buffalo 講義のその発言に直接答えた、という意味ではありません。

また Voevodsky の Univalence Axiom 自体は、

$(A=B)\simeq(A\simeq B)$

という types についての原理です。

そこから Ahrens、Kapulkin、Shulman らが univalent category theory を構築して、

$(x=y)\simeq(x\cong y)$

および categories の equality と equivalence の対応を明確にした、というのがより正確な歴史です。(ケンブリッジ大学出版局)

ですから、

$\boxed{ \text{Grothendieck の圏論的要求} \;\xrightarrow{\text{Voevodsky の Univalence}} \text{univalent category theory} }$

という流れとして理解するのがよいでしょう。

12. そして両者には、もっと深い共通思想がある

私はここが最も興味深いと思います。

Grothendieck は、

$\boxed{\text{対象の presentation より、その間の relation を重視した}}$

と言えます。

座標より scheme。

site より topos。

圏の同型より equivalence。

Voevodsky はこれを foundational level にまで押し下げます。

$\boxed{\text{対象が何で「できているか」より、何と equivalence であるかを equality に反映する。}}$

したがって Grothendieck の

$\boxed{\text{「圏は equivalence まで見るべきだ」}}$

に対する Voevodsky 的な答えを一文で表すなら、

$\boxed{ \text{「equivalence まで見る」のではなく、 equivalence を正しい意味での equality にしてしまえばよい。} }$

となります。

ただし、equivalence を潰して equality にするのではない。

むしろ

$\boxed{ \text{equality の概念そのものを豊かにして、 equivalence の全情報を収容する。} }$

ここが Univalence の核心です。

そしてこれは、前に話した Higher Topos の

$\text{objects} \to \text{equivalences} \to \text{higher equivalences} \to\cdots$

を「同じもののさまざまな同一視の仕方」として保つ発想そのものです。

この先さらに進むなら、Grothendieck の「stack」と Voevodsky の Univalence が、Rezk completeness を介してほぼ同じ問題に到達する過程を見ると面白いです。そこでは「descent」と「identity/equivalence」が一本につながります。

Rezk completeness

この議論、僕は知りませんでした。詳しく説明してもらえますか？　論文の紹介でも構いませんん。

もちろんです。Rezk completeness は、前の Grothendieck → Higher Topos → Univalence の流れを理解するうえで、かなり重要な橋です。

いちばん短く言えば、

$\boxed{ \text{Rezk completeness} = \text{「equivalence と identity/path が同じ情報を表す」ための条件} }$

です。

Voevodsky の

$(A=B)\simeq(A\simeq B)$

と非常によく似ています。実際、この類似は後に厳密に研究されています。(arXiv)

1. まず Segal space とは何か

通常の category $C$ を nerve にすると、

$N(C)_n = \{\text{$n$ 本の composable arrows}\}$

です。

例えば

$N(C)_0=\{\text{objects}\},$ $N(C)_1=\{\text{arrows}\},$ $N(C)_2=\{x_0\to x_1\to x_2\},$

となります。

普通の category では、

$N(C)_2 \cong N(C)_1\times_{N(C)_0}N(C)_1.$

つまり composable な2本の arrow があれば、それがちょうど 2-simplex を決めます。

一般に

$N(C)_n \cong \underbrace{ N(C)_1\times_{N(C)_0}\cdots\times_{N(C)_0}N(C)_1 }_{n}.$

これが Segal condition の原型です。

Higher category にしたければ、各 $N(C)_n$ を set ではなく space にします。

つまり simplicial space

$X_\bullet:\Delta^{op}\to\mathcal S$

を考える。

そして equality ではなく homotopy equivalence

$\boxed{ X_n \simeq X_1\times^{h}_{X_0}\cdots\times^{h}_{X_0}X_1 }$

を要求します。

これが Segal space です。Rezk の原論文ではこれが Section 4 の基本条件です。(arXiv)

2. Segal condition が何を保証するのか

この条件によって、

$X_0=\text{space of objects},$ $X_1=\text{space of morphisms}$

として読めるようになります。

2-simplex が composition を与える。

ただし composition は ordinary category のように rigid に一意ではなく、

$f:x\to y,\qquad g:y\to z$

に対して、

$g\circ f$

が contractible な choice の範囲で決まる。

さらに 3-simplex が associativity の coherent homotopy を与え、4-simplex、5-simplex……がその higher coherence を与える。

したがって

$\boxed{ \text{Segal condition} = \text{composition とその全 higher coherence} }$

だと考えてよいでしょう。

3. ところが、Segal condition だけでは足りない

ここが Rezk の発見の要点です。

Segal condition は

arrow をどう合成するか

については正しい。

しかし、

どの objects を「同じ object」と考えるべきか

については、まだ正しくないことがあります。

特に

$x\simeq y$

という equivalence があっても、

$x,y\in X_0$

が $X_0$ の中で全く離れた二点のままでも、Segal condition は満たせてしまいます。

そこで Rezk がもう一つ条件を加えました。

それが completeness です。

4. 最も分かりやすい反例：ordinary nerve

非常に単純な groupoid $C$ を考えます。

objects が二つ、

$a,\quad b$

あって、

$u:a\overset{\cong}{\longrightarrow}b$

という isomorphism が一つあるとします。

もちろん

$u^{-1}:b\to a$

もあります。

category theory の観点では、

$\boxed{a\cong b}$

なので、 $a$ と $b$ は本質的には同じ object です。

ところが普通の nerve を simplicial space とみなすと、

$X_0=\{a,b\}$

は discrete な二点です。

つまり、

$a\qquad b$

の間に path がない。

しかし $X_1$ には、

$id_a,\quad id_b,\quad u,\quad u^{-1}$

という equivalences が入っています。

妙なことが起きています。

$\boxed{ \text{arrow level では }a\simeq b \quad\text{なのに}\quad \text{object space では }a,b\text{ は無関係} }$

なのです。

ordinary nerve は Segal condition を満たしますが、非自明な isomorphism を持つ ordinary category では、この意味で complete ではありません。(Ncatlab)

これが Rezk completeness が必要になる理由です。

5. $X_{\mathrm{hoequ}}$ を作る

Segal space $X$ に対して、

$X_1$

の中から「equivalence である morphisms」だけを抜き出します。

それを

$\boxed{ X_{\mathrm{hoequ}}\subseteq X_1 }$

と書きます。

正確には、homotopy category

$Ho(X)$

で isomorphism になる morphisms を含む connected components の union です。Rezk の定義では Section 5 でこれを導入します。(Ncatlab)

identity arrow を与える degeneracy map

$s_0:X_0\longrightarrow X_1$

があります。

当然 identity は equivalence なので、

$s_0:X_0\longrightarrow X_{\mathrm{hoequ}}$

と因子化します。

6. Rezk completeness の定義

そして条件は驚くほど簡潔です。

$\boxed{ s_0:X_0\longrightarrow X_{\mathrm{hoequ}} \text{ が weak homotopy equivalence} }$

であること。

これが complete Segal space の定義です。(Ncatlab)

つまり、

$\boxed{ \text{space of objects} \simeq \text{space of equivalences} }$

なのです。

一見、不思議な式です。

objects と equivalence-arrows がなぜ同じ space なのでしょう。

ここを理解すると全体が見えます。

7. 「equivalence は path である」

map

$(d_1,d_0): X_{\mathrm{hoequ}} \to X_0\times X_0$

は equivalence $x\to y$ の source と target を返します。

したがって fiber は

$\operatorname{Eq}_X(x,y) = \{\text{equivalences }x\simeq y\}.$

一方 diagonal

$\Delta:X_0\to X_0\times X_0$

の homotopy fiber over $(x,y)$ は、

$\operatorname{Path}_{X_0}(x,y).$

ところが

$(d_1,d_0)s_0=\Delta.$

completeness

$X_0\simeq X_{\mathrm{hoequ}}$

を fiberwise に読むと、

$\boxed{ \operatorname{Path}_{X_0}(x,y) \simeq \operatorname{Eq}_X(x,y) }$

となります。

これが本質です。

つまり、

$\boxed{ \text{path between objects} = \text{equivalence between objects} }$

です。

もうほとんど Univalence そのものですね。

8. 先ほどの二つの object に戻る

元の category では

$a\cong b$

でした。

naive nerve だと

$X_0=\{a,b\}$

なので、

$\operatorname{Path}(a,b)=\varnothing.$

一方、

$\operatorname{Iso}(a,b)\neq\varnothing.$

したがって、

$\operatorname{Path}(a,b) \not\simeq \operatorname{Iso}(a,b).$

complete ではない。

Rezk 的に正しく作り直すと、object space は単なる二点ではなくなります。

$a$ と $b$ の間に path が入る：

$a\;\xrightarrow{\sim}\;b.$

しかもこの path が exactly $u:a\cong b$ を表す。

したがって、

$\boxed{ a\cong b \quad\Longleftrightarrow\quad a\text{ と }b\text{ が object space で path-connected} }$

になります。

9. Automorphism も消えない

これはさらに重要です。

一つの object $a$ があって、

$\operatorname{Aut}(a)=G$

とします。

ordinary category としては一対象 groupoid

$BG$

です。

もし「isomorphic objects を全部同一視」するだけなら、object space は一点

$*$

になってしまいます。

すると $G$ の情報を失います。

Rezk はそうしません。

complete object space は概念的には

$\boxed{BG}$

になります。

一点 $a$ はありますが、その一点に loops がある：

$\Omega_a X_0\simeq G.$

つまり

$\boxed{ \operatorname{Aut}(a) = \text{loops at }a }$

となる。

これは前にお話しした Univalence の、

$\operatorname{Aut}(A) \simeq (A=A)$

と同じ構造です。

だから Rezk completeness は「同値なものを quotient する」のではありません。

むしろ、

$\boxed{ \text{同値を path として object space の中に保存する} }$

のです。

ここが大事です。

10. Rezk の classifying diagram

Rezk は ordinary category $C$ を complete Segal space にするため、naive nerve ではなく classifying diagram を使います。

$\boxed{ W_n = B\,\operatorname{iso}(C^{[n]}) }$

です。

ここで

$C^{[n]}$

は $n$ 本の composable arrows の diagram の category、

$\operatorname{iso}(C^{[n]})$

はその maximal subgroupoid、

そして $B$ は classifying space です。

特に、

$\boxed{ W_0=B\,\operatorname{iso}(C). }$

Rezk は $B\,\operatorname{iso}(C)$ を category $C$ の一種の moduli space と説明しています。そこでは connected components が objects の isomorphism classes を記録し、各 component の loop information が automorphism groups を記録します。さらに全体の simplicial diagram $n\mapsto B\,\operatorname{iso}(C^{[n]})$ は $C$ を equivalence まで復元します。(arXiv)

これは実にきれいです。

11. Naive nerve と Rezk nerve の違い

イメージとして、

naive nerve

$X_0=\{\text{objects}\}$

objects は discrete。

Rezk classifying diagram

$X_0=B(\operatorname{iso} C)$

objects + isomorphisms + automorphisms が一つの homotopy type になる。

つまり、

$\boxed{ \begin{array}{ccc} \text{naive}&&\text{Rezk}\\ \hline \text{objects are points} && \text{objects form a moduli space}\\ x\cong y\text{ は arrow} && x\cong y\text{ は path}\\ \operatorname{Aut}(x)\text{ は morphisms} && \operatorname{Aut}(x)\text{ は loops} \end{array}}$

です。

私はここが Rezk completeness の一番よい直観だと思います。

12. では「Rezk completion」とは何か

complete でない Segal space

$X$

があったとします。

それを、

$X\longrightarrow \widehat X$

と complete Segal space に直す操作があります。

概念的には、

$\boxed{ \text{equivalence arrows を object-space の paths として認識するように saturate する} }$

操作です。

ただし元の $(\infty,1)$ -category としての情報は変えたくありません。

したがって

$X\to\widehat X$

は categorical な意味で equivalence（適切には Dwyer–Kan equivalence）で、

$\widehat X$

だけが completeness を満たすようになります。Rezk は completion construction を原論文の Section 14 で与えています。complete Segal spaces が fibrant objects になる model structure も構成しており、これによって complete Segal spaces は $(\infty,1)$ -categories のモデルになります。(Ncatlab)

13. 「completion」という名前で誤解しやすいところ

これは、

metric completion
Cauchy completion
Karoubi / idempotent completion

とは違います。

Rezk completeness の「complete」は、

$\boxed{ \text{categorical equivalences が object-space の homotopy に完全に反映されている} }$

という意味だと思うのがよいでしょう。

新しい categorical objects を足して Cauchy complete にしているわけではありません。

sameness の表現を正しくしているのです。

14. ここで Voevodsky の Univalence と比べる

Univalent category $C$ では、

$\boxed{ (x=_C y) \simeq (x\cong_C y). }$

Rezk complete Segal space $X$ では、

$\boxed{ \operatorname{Path}_{X_0}(x,y) \simeq \operatorname{Eq}_X(x,y). }$

並べると、

$\begin{array}{ccc} \text{Univalence}&&\text{Rezk completeness}\\[1mm] x=y&&\operatorname{Path}(x,y)\\ \updownarrow&&\updownarrow\\ x\cong y&&x\simeq y \end{array}$

です。

ほとんど同じ原理の

internal/type-theoretic 表現
external/homotopical 表現

だと考えられます。

この対応を Ahrens–Kapulkin–Shulman は 1-category level で明示し、彼らの univalent-category completion は higher-categorical semantics では Rezk completion の truncated version に相当すると説明しています。(arXiv)

さらに Stenzel は、univalence と completeness の対応をより一般的な model-categorical 文脈で精密に研究しています。(arXiv)

15. Ahrens–Kapulkin–Shulman の Rezk completion

HoTT 側でも全く同じ問題が起こります。

precategory $A$ では、

$a=b$

と

$a\cong b$

が一致しないかもしれない。

そこで

$A\longrightarrow \widehat A$

を作り、

$\widehat A$

を univalent category にします。

しかも

$A\to\widehat A$

は fully faithful + essentially surjective で、categorically は同じ category を表す。

そして universal property を持つ。

これを彼らは Rezk completion と呼びます。論文は「任意の category を universal な仕方で univalent なものに置き換えられる」と述べています。(arXiv)

HoTT Book の Chapter 9.9 も、この construction を

precategory を category に universal に置き換える

という形で扱っています。(Homotopy Type Theory)

16. 実は Yoneda embedding が completion を作る

これは Grothendieck 的にも面白いところです。

precategory $A$ に対して Yoneda embedding

$y:A\longrightarrow [A^{op},\mathbf{Set}]$

を考えます。

presheaf category の appropriate な full image を取ると、それが $A$ の Rezk completion になります。

つまり、

$\boxed{ A \longrightarrow \text{representable presheaves} }$

によって、「isomorphic objects を identity として正しく扱える環境」に埋め込める。

これはとても Grothendieck 的な構成です。

対象そのものを rigid に修正するより、

$\boxed{\text{その対象が他の全対象とどう関係するか}}$

つまり Yoneda data で特徴づける。

その結果、

$a\cong b$

なら representable functors

$y(a),y(b)$

も等価になり、Univalence によって identity として扱える。

Grothendieck → Yoneda → Rezk → Univalence という面白い一本の線があります。

17. Stack completion との関係

前に stack の話をしました。

prestack では objects と isomorphisms を局所的に持っていますが、descent が完全ではないことがあります。

そこで stackification

$\mathcal P \to \mathcal P^{+}$

を行います。

Ahrens–Kapulkin–Shulman は、自分たちの Rezk completion が homotopical semantics では

$\boxed{ \text{Rezk completion of Segal spaces} }$

に、また別の意味論では

$\boxed{ \text{stack completion of a prestack} }$

に対応すると明記しています。(arXiv)

これは前の Grothendieck の話との接続として非常に重要です。

つまり、

$\boxed{ \text{descent を completion する} }$

ことと

$\boxed{ \text{equivalence を identity として completion する} }$

ことが、実は同じ higher-categorical 現象の違う顔として現れます。

18. なぜこれが Higher Topos に重要なのか

Higher Topos では object は最初から homotopy types です。

したがって moduli を考えたとき、

$\{\text{isomorphism classes}\}$

という set に潰してはいけません。

本当に欲しいのは

$\boxed{\text{moduli space}}$

あるいは

$\boxed{\text{moduli }\infty\text{-groupoid}}.$

そこでは、

objects → points
isomorphisms → paths
isomorphisms between isomorphisms → homotopies
higher coherences → higher paths

となる。

Rezk completeness は、

$\boxed{ \text{この geometric interpretation が categorical equivalence と食い違わない} }$

ための条件だと見ることができます。

19. 私なら Rezk completeness をこう覚えます

Segal condition は、

$\boxed{ \text{「arrows の合成」を正しくする} }$

条件。

Rezk completeness は、

$\boxed{ \text{「objects の sameness」を正しくする} }$

条件。

つまり

$\boxed{ \begin{aligned} \text{Segal}&:\quad \text{composition = coherent},\\ \text{Rezk}&:\quad \text{equivalence = path}. \end{aligned}}$

この二つが揃って初めて、

$\boxed{\text{complete Segal space}}$

すなわち $(\infty,1)$ -category の一つの正しいモデルになります。Rezk は complete Segal spaces を fibrant objects とする model structure を構成し、後には quasi-categories、simplicial categories、Segal categories など他の $(\infty,1)$ -category models と同値な理論を与えることが示されました。Bergner の survey はこの比較のよい入口です。(arXiv)

20. 論文を読むなら、この順序をお勧めします

まず Nima Rasekh, “Introduction to Complete Segal Spaces” (2018) が説明的です。complete Segal spaces の categorical notions、fibrations、limits、adjunctions を例と直観を重視して解説する expository paper です。(arXiv)
Rasekh: Introduction to Complete Segal Spaces

次に Charles Rezk, “A model for the homotopy theory of homotopy theory”。1998年 arXiv、2001年 Transactions of the AMS 掲載の原論文です。特に §3 classifying diagrams、§4 Segal spaces、§5 equivalences、§6 completeness、§7 model structure、§14 completion が今回の話に直接対応します。(arXiv)
Rezk の原論文

その次に Ahrens–Kapulkin–Shulman, “Univalent categories and the Rezk completion”。これは今の対話には特にお勧めです。Rezk の発想を HoTT/Univalent Foundations に翻訳し、

$(x=y)\simeq(x\cong y)$

を category の正しい univalence condition として、任意の precategory に Rezk completion を作ります。論文には Coq による formalized proofs も付属しています。(arXiv)
Ahrens–Kapulkin–Shulman 論文

そして HoTT Book, Chapter 9, とくに §9.9 “The Rezk completion”。集合論的 category theory が equality/isomorphism/equivalence の違いを扱いにくいことから始まり、Univalence がそれをどう変えるかをかなり読みやすく説明しています。(Homotopy Type Theory)
HoTT Book

最後に、Raffael Stenzel, “Univalence and completeness of Segal objects”。これは「Rezk completeness と Voevodsky univalence は本当にどこまで同じなのか？」を、単なる analogy ではなく厳密に追いたいときの論文です。(arXiv)
Stenzel: Univalence and completeness of Segal objects

この話の核心

前回の Grothendieck の問いに戻すと、

$\text{category は equality ではなく equivalence まで見るべきだ}$

という要求に対し、Rezk と Voevodsky はかなり近い答えを異なる言語で与えています。

$\boxed{ \begin{array}{ccc} \text{Rezk}&&\text{Voevodsky}\\[1mm] \operatorname{Path}(x,y)&\simeq&\operatorname{Equiv}(x,y)\\ \text{homotopy semantics}&&\text{type-theoretic semantics}\\ \text{complete Segal space}&&\text{univalent type/category} \end{array}}$

つまり、「equivalence まで同じと見なす」のではなく、equivalence を path＝identity の構造そのものにする。

これこそ Rezk completeness が Univalence へつながる最も重要な点です。

次に深掘りするなら、Rezk の原論文の §3–§6 を実際の数式に沿って読み、ordinary category $C$ から

$N(C)\quad\text{と}\quad[n]\mapsto B\,\mathrm{iso}(C^{[n]})$

を具体的に作って、なぜ後者だけが complete になるのかを手計算するのが一番理解が深まると思います。

ありがとうございます。紹介された論文、読んでみます。別のトピックですが、Topos論と物理学との関連について、論じてみてください。まずは、相対論とTopos論は、どういう接点を持ちますか？

Topos 論と相対論の接点は、意外に深いです。ただし最初に位置づけをはっきりさせると、一般相対論の標準的定式化に Topos が必要なわけではありません。通常の Lorentz 多様体と微分幾何で十分です。Topos が効いてくるのは、相対論の「局所性」「無限小」「時空そのものを数学的宇宙としてどう捉えるか」をさらに掘り下げるときです。実際、Synthetic Differential Geometry（SDG）を用いて Einstein 方程式を suitable topos の内部で記述する研究や、量子重力を念頭に「時空の型に応じて数学的宇宙そのものを変える」という Isham の構想があります。

1. 一般相対論は最初から「局所→大域」の理論である

一般相対論の時空は

(M,g)

という4次元 Lorentz 多様体です。

各点の近くでは座標

x^\mu:U\longrightarrow\mathbb R^4

を取れますが、物理的な対象は座標そのものではありません。計量

g_{\mu\nu},

接続

\nabla,

曲率

R^\rho{}_{\sigma\mu\nu}

などは、異なる座標 chart 上の局所表示を transition functions に従って貼り合わせた global geometric objects です。

Einstein 方程式

G_{\mu\nu}+\Lambda g_{\mu\nu} = 8\pi G\,T_{\mu\nu}

も座標表示には依存しません。

したがって一般相対論には最初から、

\boxed{ \text{局所座標で記述するが、物理は局所表示に依存しない} }

という Grothendieck 的な精神があります。

これは以前話した

\text{chart} \to \text{overlap} \to \text{descent} \to \text{global object}

そのものです。

2. ただし Grothendieck Topos は、多様体よりさらに「局所性」を抽象化する

普通の時空 $M$ なら、開集合の site

\operatorname{Open}(M)

から

\operatorname{Sh}(M)

を作れます。

ここでは

U\mapsto \{\text{\(U\) 上の物理場}\}

という sheaf を考えるのが自然です。

例えば局所 metric、

U\mapsto \operatorname{Met}(U),

局所 matter fields、

U\mapsto \operatorname{Matter}(U),

Einstein 方程式を満たす局所 solutions、

U\mapsto\operatorname{Sol}(U)

などです。

すると相対論を、

\boxed{ \text{局所的な物理データと、その貼り合わせ} }

として読める。

これはまだ普通の sheaf theory ですが、Grothendieck はさらに「開集合」そのものに縛られず、

(C,J)

という arbitrary site を局所性の基礎にできます。

したがって「時空とは点の集合 $M$ でなければならない」という前提まで相対化できるわけです。

3. Lawvere 側から見ると、もっと直接的な接点がある

相対論と Topos のもっと強い接点は、実は Lawvere の Synthetic Differential Geometry にあります。

通常の微分幾何では、

f'(x) = \lim_{h\to0} \frac{f(x+h)-f(x)}h

と極限を使います。

Lawvere は代わりに、Topos の内部に本物の infinitesimal

D=\{d\in R\mid d^2=0\}

を持ち込みます。

そして Kock–Lawvere axiom により、任意の適切な

f:R\to R

について

\boxed{ f(x+d)=f(x)+d\,f'(x) \qquad(d^2=0) }

と書ける。

$d$ は「限りなく小さい数」という比喩ではなく、Topos 内部の genuine element です。SDG は Lawvere に始まる category-theoretic differential geometry であり、この nilpotent infinitesimal を可能にする suitable categorical universe が Topos です。

4. すると接ベクトルが本当に「無限小の道」になる

以前少し触れた

TM=M^D

がここで重要になります。

普通の微分幾何では tangent vector は equivalence class of curves などとして作ります。

SDG では

\boxed{ v:D\longrightarrow M }

そのものが infinitesimal curve、すなわち tangent vector になります。

これは一般相対論と非常に相性がいい。

なぜなら GR は、

TM,\quad T^*M,\quad g,\quad\nabla,\quad R

という infinitesimal differential geometry だけで構築されているからです。

したがって suitable smooth topos の内部で、

\text{Lorentz metric} \to \text{Levi-Civita connection} \to \text{curvature} \to \text{Einstein tensor}

という通常の微分幾何を synthetic に構成できます。

実際、SDG の枠組みで pseudo-Riemannian formal manifold と Einstein field equations を記述する研究があります。

5. ここで Grothendieck と Lawvere が両方必要になる

これが面白いところです。

Grothendieck 的側面は、

\boxed{\text{local-to-global / sheaf / descent}}

です。

Lawvere 的側面は、

\boxed{\text{Topos 内部の infinitesimal differential geometry}}

です。

したがって Topos 的相対論を象徴的に書けば、

\boxed{ \begin{array}{ccc} \text{Grothendieck}&&\text{Lawvere}\\ \text{local patches}&&\text{infinitesimals}\\ \text{descent}&&D=\{d^2=0\}\\ \text{global spacetime}&&\text{internal differential geometry}\\ &\searrow\quad\swarrow&\\ &\text{general relativity}& \end{array}}

となります。

これは、これまで私たちが追ってきた二つの Topos 観が、物理でかなり具体的に交差する場所です。

6. ただし代償として「論理」まで変わる

ここは非常に重要です。

普通の実数では、

d^2=0

なら

d=0

です。

だから

d\neq0,\qquad d^2=0

という nilpotent infinitesimal は通常の $\mathbf{Set}$ の世界には存在しません。

それを存在させるため、SDG では suitable Topos の内部に移ります。

すると内部論理は一般には classical Boolean logic ではなく、

\boxed{\text{intuitionistic logic}}

になります。

したがってこれは単なる

「微分計算をちょっと便利に書き換える」

という話ではありません。

\boxed{ \text{物理を記述する数学的 universe 自体を } \mathbf{Set} \text{ から Topos へ変える} }

というかなり根本的な提案です。

SDG を GR の singularity 問題に適用する研究でも、この点――infinitesimals を得るかわりに内部論理が intuitionistic になること――が明示的に論じられています。

7. 「時空の点」という概念も変わり得る

通常の GR では event は

p\in M

という点です。

ところが Topos の内部では generalized element

X\longrightarrow M

も「 $X$ -stage から見た event」として意味を持ちます。

これは前に話した Kripke–Joyal semantics と同じです。

\boxed{ \text{物理的対象の値が stage/context に依存する} }

という読み方が可能になります。

古典的 stage では一点に見える event が、別の stage では infinitesimal family や parameterized family として見える。

Topos 的 GR の研究の中には、この「stage-dependent event」を真剣に物理的意味づけしようとするものもあります。

ただし、この部分は標準的 GR ではなく研究プログラム的なもの、と区別しておくべきです。

8. 特殊相対論より一般相対論の方が Topos と相性がよい

特殊相対論なら背景時空は固定された

(\mathbb R^4,\eta)

です。

したがって Topos を持ち込む必然性はあまりありません。

一般相対論では、

g_{\mu\nu}

自体が dynamical variable です。

つまり、

\boxed{\text{舞台そのものが物理的対象}}

になります。

これは Topos 的発想と非常に相性がよい。

通常の物理なら

\text{space}+\text{objects on space}

と分けられますが、GR では space-time geometry と gravitational field が同じものです。

そして Topos theory も、

\text{space}

と

\text{objects/sheaves on that space}

の区別を極端に柔軟にします。

McLarty のビデオで Grothendieck が悩んでいた

「topos という巨大な category と、その背後にある real geometrical thing をどう区別するか」

という問題が、GR の

「時空は背景なのか、それとも物理場なのか」

という問いと、不思議なくらい響き合っています。

9. そして量子重力になると Topos の意味がさらに強くなる

Isham が Topos に注目した最大の理由の一つがここです。

量子力学は普通、

\mathbb R,\quad\mathbb C,\quad\mathcal H

といった固定した continuum structure を前提とします。

一方、量子重力では spacetime 自体が quantum object になるはずです。

すると、

なぜ量子理論の mathematical background だけは固定された $\mathbf{Set}$ と $\mathbb R$ なのか？

という疑問が生まれる。

Isham は、異なる「space-time types」に異なる quantum theories を対応させ、それらを Topos 的にまとめる可能性を提案しました。

これはかなり大胆ですが、思想としては、

\boxed{ \text{geometry を dynamical にするなら、 logic や number system まで dynamical/contextual になり得る} }

というものです。

ここから Döring–Isham の Topos quantum theory へつながります。彼らは classical physics では $\mathbf{Set}$ が背景 universe なのに対し、量子理論では別の Topos を theory の mathematical universe として使う、というプログラムを明確に打ち出しています。

10. ですから「相対論と Topos」の接点には三つの深さがある

レベル	相対論	Topos 的対応
幾何学	局所座標を貼って時空を作る	sheaf / descent
微分	tangent, connection, curvature	SDG・infinitesimal objects
基礎論	spacetime 自体が dynamical	mathematical universe / internal logic の変更

第一段はかなり自然で古典的です。

第二段は Lawvere–Kock の SDG により数学的にしっかりした理論があります。

第三段になると、量子重力や物理の基礎に関する研究プログラムになり、まだ標準的物理理論になっているわけではありません。

私が特に重要だと思う接点

Riemann → Einstein → Grothendieck → Lawvere という流れで見ると面白いです。

Riemann は

\boxed{\text{geometry を global Euclidean space から解放した}}

と言えます。

Einstein はさらに

\boxed{\text{geometry を固定された背景から解放して dynamical にした。}}

Grothendieck は

\boxed{\text{space を point-set space から解放した。}}

Lawvere は

\boxed{\text{differential geometry を }\mathbf{Set} \text{ と classical logic から解放した。}}

と見ることができます。

そう考えると Topos と相対論の接点は単なる数学的テクニック以上のものになります。

\boxed{ \text{「物理が起きる空間とはそもそも何なのか？」} }

という Riemann–Einstein の問いを、

\boxed{ \text{「その空間を記述する数学的 universe と logic は何なのか？」} }

まで押し進めるのが Topos 的な方向だ、と言えるでしょう。

そして次は、ここから 量子力学と Topos 論、特に Isham–Döring の spectral presheaf、Kochen–Specker theorem、contextuality に進むと、相対論の場合とは全く違う理由で Topos が登場するのが見えてきます。これは物理との接点として、おそらく一番成熟した Topos の応用の一つです。

量子論でのTopos の応用

はい。量子論では、Topos はかなり独特な仕方で登場します。相対論では「局所的な時空」を貼ることが主題でしたが、量子論ではむしろ

$\boxed{\text{互いに両立しない古典的な観測文脈を、どう一つの数学的世界にまとめるか}}$

が中心問題になります。

そして一番面白いのは、Kochen–Specker 定理を「古典的状態空間を作れないという失敗」と見る代わりに、「状態空間は集合ではなく Topos 内の対象である」と読み替えるところです。

1. 古典物理では、すべてが $\mathbf{Set}$ の中で済む

古典系の状態空間を

$\Sigma$

とします。

物理量 $A$ は普通の関数

$A:\Sigma\longrightarrow\mathbb R.$

命題

$A\in\Delta$

は部分集合

$A^{-1}(\Delta)\subseteq\Sigma$

として表現できます。

そして状態

$s\in\Sigma$

が与えられれば、

$s\in A^{-1}(\Delta)$

かどうかで命題は

$\mathrm{true}\quad\text{or}\quad\mathrm{false}$

になります。

つまり古典物理の概念図は

$\boxed{ \text{state space }\Sigma \quad \overset{A}{\longrightarrow} \quad \mathbb R }$

で、背後の論理は Boolean logic です。

Döring–Isham はこの構造を一般化し、「物理理論を作るとは、適切な Topos の中で state-object、quantity-value object、physical quantity の arrow を表現することだ」という構想を打ち出しました。古典物理の場合、その Topos は essentially $\mathbf{Set}$ です。(arXiv)

2. 量子論では、この図が壊れる

Hilbert 空間 $\mathcal H$ 上の量子論では observable は self-adjoint operator

$\hat A$

です。

もし古典論と同じように考えられるなら、すべての observable に同時に

$v(\hat A)\in\mathbb R$

を割り当て、

$v(f(\hat A))=f(v(\hat A))$

のような functional relations を保存する「量子的な点」

$v$

が存在してほしい。

しかし Kochen–Specker theorem は、十分高い次元の Hilbert 空間では、そのような context-independent global valuation が存在しないことを示します。

Isham–Butterfield の重要な洞察は、

$\boxed{ \text{Kochen--Specker theorem} = \text{ある presheaf が global element を持たない} }$

と書き直せる、ということでした。(arXiv)

ここで Topos が登場します。

3. 「一度に古典的に測れるもの」を context とする

量子 observable 全体は非可換です。

しかし互いに commuting な observables だけ集めれば、その部分では古典的に扱えます。

そこで

$\mathcal V(\mathcal H)$

を、 $\mathcal B(\mathcal H)$ の可換 von Neumann subalgebras

$V\subseteq\mathcal B(\mathcal H)$

の poset/category とします。

一つの

$V$

を context と呼びます。

直感的には、

$\boxed{ V=\text{同時に古典的に語ることのできる observables の一組} }$

です。

量子系全体には一つの classical context はありません。

代わりに、

$V_1,\quad V_2,\quad V_3,\ldots$

という多数の「局所的な古典世界」がある。

ここは、前に話した多様体の charts と少し似ています。

ただし今回は空間的位置の局所性ではなく、

$\boxed{\text{commutativity / measurement context の局所性}}$

です。

4. それら全部を presheaf Topos に入れる

そこで

$\boxed{ \mathcal T = \mathbf{Set}^{\mathcal V(\mathcal H)^{op}} }$

という presheaf Topos を考えます。

Topos の object $F$ は、

各 context $V$ に集合

$F(V)$

を割り当て、小さい context

$V'\subseteq V$

へ restriction

$F(V)\longrightarrow F(V')$

を持つものです。

つまり、

ある context で持っている情報を、もっと小さな古典的 context に制限するとどう見えるか

を組織する装置です。

Döring–Isham の quantum Topos は、この可換部分代数の category 上の contravariant set-valued functors を使います。(arXiv)

5. Spectral presheaf $\underline\Sigma$ が「量子状態空間」になる

各可換 algebra $V$ には、Gelfand spectrum

$\Sigma_V$

があります。

可換 $C^*$ -algebra なら Gelfand duality により、これは古典的な phase/state space のように考えられます。

そこで

$\boxed{ \underline\Sigma(V)=\Sigma_V }$

とします。

そして

$V'\subseteq V$

なら character

$\lambda:V\to\mathbb C$

を

$\lambda|_{V'}:V'\to\mathbb C$

へ restriction する。

こうして

$\boxed{\underline\Sigma}$

という spectral presheaf ができます。

これが Topos 量子論における classical state space $\Sigma$ の代用品です。Döring–Isham はこれを quantum analogue of a classical state space と明示しています。(arXiv)

6. Kochen–Specker theorem が極めて美しく書ける

もし spectral presheaf に global element

$1\longrightarrow\underline\Sigma$

があれば、

各 context $V$ に

$\lambda_V\in\Sigma_V$

を選び、しかも

$V'\subseteq V$

なら

$\lambda_V|_{V'}=\lambda_{V'}$

となります。

これは、

あらゆる classical contexts について矛盾なく一つの値を選ぶ

ことです。

つまり context-independent hidden valuation。

Kochen–Specker は、それが存在しないと言っている。

したがって、

$\boxed{ \underline\Sigma \text{ has no global point} }$

です。(arXiv)

これは Topos 的には非常に自然です。

空間に global point がなくても、その空間自体が存在しないわけではない。

Grothendieck 的な geometry では point-free spaces は珍しくありません。

したがって、

$\boxed{ \text{「量子状態空間には点がない」ことを受け入れて geometry を続ける} }$

わけです。

7. では量子命題 $A\in\Delta$ はどうするのか

通常の量子力学では

$A\in\Delta$

という proposition は spectral projection

$\hat P=E^A(\Delta)$

で表します。

ところが $\hat P$ は、ある context $V$ に入っているとは限りません。

そこで Döring–Isham は daseinisation を使います。

context $V$ で $\hat P$ を表現できなければ、 $V$ の中にある projection で $\hat P$ を上から最もよく近似する：

$\boxed{ \delta^o(\hat P)_V = \bigwedge \{ \hat Q\in\mathcal P(V) \mid \hat Q\geq\hat P \}. }$

つまり、

「この context では $P$ を直接語れないので、この context で語れる最も鋭い命題に近似する」

わけです。

この daseinisation によって quantum proposition は spectral presheaf の clopen subobject

$\boxed{ \delta(\hat P)\hookrightarrow\underline\Sigma }$

になります。(arXiv)

8. これは量子論の contextuality を消すのではない

ここが思想的に重要です。

Topos を使って

「実は hidden variables がありました」

と言っているのではありません。

むしろ逆です。

$\boxed{ \text{context dependence を理論の基本 geometry として受け入れる} }$

のです。

一つの observable $A$ についても、

$V_1,\;V_2,\ldots$

によってその representation は違う。

しかしそれら全部を一つの presheaf object として組織すれば、global な mathematical object になる。

これはまさに Grothendieck 的です。

$\boxed{ \text{局所 representation は context-dependent, しかし sheaf/presheaf 全体は global} }$

です。

9. 真理値が $0,1$ ではなくなる

ここで Lawvere の Topos 観が効いてきます。

Topos には subobject classifier

$\Omega$

があります。

presheaf Topos の $\Omega(V)$ は、概略 $V$ 上の sieves からなります。

だから量子 proposition の truth value は

$0\quad\text{or}\quad1$

だけではありません。

例えば、

$V$ ではまだ確定できないが、これより小さい contexts $V'\subseteq V$ では true

という真理値を持てます。

Isham–Butterfield の初期研究では、こうした generalized valuation の truth values が contextual で多値的であり、自然に presheaf Topos の sieve-valued logic になることが示されました。(arXiv)

したがって量子論理は

$\boxed{ \text{Boolean } \{0,1\} }$

から、

$\boxed{ \text{Heyting-valued contextual logic} }$

へ移ります。

10. しかし従来の「量子論理」とも違う

Birkhoff–von Neumann quantum logic では projection lattice

$\mathcal P(\mathcal H)$

を proposition lattice とします。

これは orthomodular lattice で、一般には distributive ではありません。

例えば

$P\land(Q\lor R) \neq (P\land Q)\lor(P\land R)$

となる場合があります。

Topos approach は違います。

propositions を Topos の subobjects として扱うので、その lattice は Heyting algebra になり distributive です。

ただし excluded middle

$P\lor\neg P=\top$

は一般には成立しない。

つまり、

$\boxed{ \text{non-distributive quantum logic} }$

を

$\boxed{ \text{distributive but intuitionistic logic} }$

に置き換える方向です。

Bohrification の研究でも、この対比が明示的に強調されています。(arXiv)

これはかなり大きな概念転換です。

11. Observable 自体も普通の実数値関数ではなくなる

古典論なら

$A:\Sigma\to\mathbb R.$

Topos 量子論でもこの形をなるべく保存したい。

そこで

$\boxed{ \breve A: \underline\Sigma \longrightarrow \underline{\mathbb R}^{\leftrightarrow} }$

のような arrow を構成します。

ただし右辺は普通の Dedekind reals ではなく、context-dependent な区間的 quantity values を表す object です。

なぜ区間になるか。

ある context $V$ に $\hat A$ 自身が入っていなければ、

$\delta^i(\hat A)_V \leq \hat A \leq \delta^o(\hat A)_V$

という inner/outer approximations でしか観測量を表せないからです。

したがって値も概念的には、

$\boxed{ [a_V,b_V] }$

のような「context が粗いほど幅を持った値」になる。

Döring–Isham は self-adjoint operators を spectral presheaf から quantity-value object への arrows として表現する構成を与えています。(arXiv)

12. 状態と確率はどうなるのか

spectral presheaf に global points がないので、

$s\in\Sigma$

という classical microstate の概念はそのまま使えません。

しかし density operator

$\rho$

などの通常の quantum state は消えません。

Döring は quantum state から spectral presheaf 上の measure を構成し、逆に適切な measure から von Neumann algebra の state を復元できることを示しました。また expectation values もそこから計算できます。(arXiv)

つまり、

$\boxed{ \rho \quad\longleftrightarrow\quad \text{measure on }\underline\Sigma }$

という対応が得られる。

さらに Döring–Isham は probabilities 自体を suitable sheaf topoi の truth values として読む方法まで研究しています。(arXiv)

ここでは

$\text{probability}$

と

$\text{truth}$

の距離がかなり縮まります。

13. もう一つの重要な流派：Bohrification

Topos quantum theory にはもう一つ非常に美しい構成があります。

Heunen–Landsman–Spitters の Bohrification です。

quantum system を noncommutative $C^*$ -algebra

$A$

で記述します。

その中の commutative subalgebras

$C\subseteq A$

を全部集めた category

$\mathcal C(A)$

を考えます。

そして suitable presheaf/covariant Topos

$\mathcal T(A)$

に入る。

すると驚くべきことに、外部では非可換だった

$A$

が Topos の内部では

$\boxed{\underline A}$

という commutative $C^*$ -algebra として見えるようになります。(arXiv)

名前の「Bohrification」は Niels Bohr の

quantum phenomena は classical concepts を通して記述される

という思想に由来します。

14. すると内部 Gelfand spectrum を作れる

内部では $\underline A$ が commutative なので constructive Gelfand duality を適用できます。

すると spectrum

$\underline\Sigma_A$

が得られます。

これは ordinary point-set space というより locale です。

外から見ると quantum system は noncommutative。

しかし Topos の内部から見ると、

$\boxed{ \text{commutative algebra} + \text{phase space} + \text{intuitionistic logic} }$

というかなり classical-looking な theory になります。

Heunen–Landsman–Spitters はこれを、「 $A$ が定める quantum theory を Topos 内部では essentially classical theory に変換する」と表現しています。(arXiv)

15. Döring–Isham と Bohrification の違い

二つは近いですが、完全に同じではありません。

	Döring–Isham	Bohrification
Context	可換 von Neumann subalgebras	可換 $C^*$ -subalgebras
Functor direction	主に contravariant	主に covariant
状態空間	spectral presheaf	internal Gelfand spectrum
命題	daseinised clopen subobjects	internal locale の opens
哲学	contextual quantum realism	Bohr の classical contexts の統合

しかし中心思想は共通しています。

$\boxed{ \text{非可換量子世界を、可換な classical contexts の全体系として理解する} }$

ことです。(arXiv)

16. ここで、これまでの Grothendieck の話とつながる

かなり面白い対応があります。

多様体では、

$U_i\subset M$

という spatial local charts を使いました。

量子 Topos では、

$V_i\subseteq\mathcal B(\mathcal H)$

という classical contexts を使います。

したがって、

$\begin{array}{ccc} \text{Riemann/Grothendieck geometry} && \text{Topos quantum theory}\\[1mm] \text{open region }U&&\text{commutative context }V\\ \text{restriction to smaller }U' && \text{restriction to }V'\subset V\\ \text{local section}&&\text{contextual valuation}\\ \text{sheaf}&&\text{spectral presheaf}\\ \text{global point}&&\text{global valuation}\\ &&\text{(KS says: none)} \end{array}$

という対応があります。

つまり Grothendieck が

$\boxed{\text{space を local viewpoints の体系として捉えた}}$

のと同じように、

Topos quantum theory は

$\boxed{\text{quantum reality を classical viewpoints の体系として捉える}}$

わけです。

17. Lawvere との接点はさらに深い

そして Lawvere 的には、

presheaf Topos を単に外から使うのではなく、その内部で物理をする

と考えます。

すると Topos の内部では、

state-object がある
quantity-value object がある
propositions がある
intuitionistic logic がある
probability/measure がある
observable が arrow になる

という形になります。

つまり Döring–Isham の構想はまさに、

$\boxed{ \text{quantum theory = a physical theory internal to a Topos} }$

という Lawvere 的な方向です。(arXiv)

そしてこれは以前話した

$\text{Topos} = \text{generalized space} + \text{universe of discourse}$

の両方を物理に使う例になっています。

18. このアプローチは量子力学を「置き換えた」のか？

ここは慎重に言う必要があります。

現状、この Topos approach は標準量子力学に代わる実験的に異なる予測体系として確立したものではありません。

むしろ、

$\boxed{ \text{standard quantum theory の構造を、別の mathematical/conceptual language で再構成する} }$

という foundational program と見るのが適切です。

Kochen–Specker contextuality、非可換性、quantum propositions、states、expectation values などを Topos の言葉に翻訳し、従来の Hilbert-space formulation の conceptual puzzles を違う形で整理するものです。Döring–Isham 自身も、このプログラムを quantum gravity の基礎問題を念頭に置いた「fundamentally new way of viewing theories of physics」と位置づけています。(arXiv)

したがって、

「Topos を使えば measurement problem が解決する」

とまで言うのは強すぎます。

しかし、

contextuality をどう数学的 reality の構造として表現するか

については、非常に洗練された答えを与えています。

19. 私がこの理論で最も重要だと思う一点

Kochen–Specker theorem を普通に読むと、

$\boxed{ \text{すべての物理量に同時に definite values を与える classical state は存在しない} }$

となります。

ここで普通なら、

それなら classical reality の概念を諦める

となりそうです。

Topos の答えは少し違います。

$\boxed{ \text{「一個の global point」を reality と考えることを諦める。しかし「space/state-object」そのものは残す。} }$

これは Grothendieck の思想と非常によく響き合います。

点を失っても geometry を失わない。

そして Lawvere 的には、

$\boxed{ \text{一つの Boolean truth を失っても logic を失わない。} }$

代わりに contextual Heyting logic を使う。

したがって Topos quantum theory を一文でまとめるなら、

$\boxed{ \text{量子論の contextuality を、「古典性の破綻」ではなく「局所的古典世界を貼り合わせた generalized geometry」として読む試み} }$

だと思います。

この先は、具体的な例を一つ計算するのがかなり有効です。たとえば スピン1系（ $\mathcal H=\mathbb C^3$ ）で、Kochen–Specker が「spectral presheaf に global section がない」という主張にどう変わるかを追い、そのあと projection $P$ の daseinisation を2〜3個の contexts で実際に計算すると、Topos が何をしているのか一気に具体化します。

具体的な例を一つ計算してみてください。

では、 $\mathcal H=\mathbb C^3$ のスピン1系で、量子命題を二つの異なる classical context に置いて daseinisation を実際に計算してみます。これは Kochen–Specker 定理そのものの証明ではありませんが、「Topos が contextuality をどう扱うか」をかなり直接に見せてくれます。3次元は Kochen–Specker 現象が本格的に現れる最小の Hilbert 空間次元でもあります。(arXiv)

1. 命題「 $S_z=+1$ 」

標準基底を

$e_1= \begin{pmatrix}1\\0\\0\end{pmatrix}, \qquad e_2= \begin{pmatrix}0\\1\\0\end{pmatrix}, \qquad e_3= \begin{pmatrix}0\\0\\1\end{pmatrix}$

とします。

スピン1なら、これをそれぞれ

$|+1\rangle,\quad |0\rangle,\quad |-1\rangle$

と思って構いません。

命題

$P=\text{「}S_z=+1\text{」}$

を射影

$\hat P=|e_1\rangle\langle e_1| = \begin{pmatrix} 1&0&0\\ 0&0&0\\ 0&0&0 \end{pmatrix}$

で表します。

Döring–Isham の outer daseinisation は、context $V$ に対して

$\boxed{ \delta^o(\hat P)_V = \bigwedge \{\hat Q\in\mathcal P(V)\mid \hat Q\geq\hat P\} }$

です。

つまり、

$V$ 内で表現できる射影のうち、 $\hat P$ を含む最小のもの

を取ります。

inner daseinisation は逆に

$\boxed{ \delta^i(\hat P)_V = \bigvee \{\hat Q\in\mathcal P(V)\mid \hat Q\leq\hat P\} }$

で、「 $P$ より強い、 $V$ 内で表現できる最大の命題」です。Döring–Isham はまさにこの lattice-theoretic な近似を daseinisation として導入しています。(arXiv)

射影の順序は

$P\leq Q \iff \operatorname{Ran}P\subseteq\operatorname{Ran}Q$

です。

2. まず $S_z$ と両立する context

最初の context を

$V_z= \{\text{standard basis で diagonal な }3\times3\text{ matrices}\}$

とします。

この中にはもちろん $\hat P$ 自身があります。

したがって、

$\boxed{ \delta^o(\hat P)_{V_z} = \hat P }$

かつ

$\boxed{ \delta^i(\hat P)_{V_z} = \hat P. }$

つまり、この context では命題

$S_z=+1$

を完全に正確に語れます。

何も失われません。

3. 今度は別の measurement context を選ぶ

次の orthonormal basis を取ります。

$f_1=\frac{e_1+e_2}{\sqrt2}, \qquad f_2=\frac{e_1-e_2}{\sqrt2}, \qquad f_3=e_3.$

対応する rank-one projections を

$Q_i=|f_i\rangle\langle f_i|$

とします。

明示的には

$Q_1= \frac12 \begin{pmatrix} 1&1&0\\ 1&1&0\\ 0&0&0 \end{pmatrix},$ $Q_2= \frac12 \begin{pmatrix} 1&-1&0\\ -1&1&0\\ 0&0&0 \end{pmatrix},$ $Q_3= \begin{pmatrix} 0&0&0\\ 0&0&0\\ 0&0&1 \end{pmatrix}.$

この basis で diagonal な algebra を

$V_f$

としましょう。

$V_f$ の projections は、

$0,\;Q_1,\;Q_2,\;Q_3,\; Q_1+Q_2,\; Q_1+Q_3,\; Q_2+Q_3,\; I$

だけです。

4. Outer daseinisation を計算する

欲しいのは

$\delta^o(P)_{V_f} = \min\{Q\in\mathcal P(V_f)\mid P\le Q\}.$

$\operatorname{Ran}P$ は

$\operatorname{span}\{e_1\}.$

ところが

$e_1=\frac{f_1+f_2}{\sqrt2}.$

したがって

$e_1\in \operatorname{span}\{f_1,f_2\}.$

つまり

$P\le Q_1+Q_2.$

一方、

$e_1\notin\operatorname{span}\{f_1\}, \qquad e_1\notin\operatorname{span}\{f_2\},$

なので

$P\nleq Q_1,\qquad P\nleq Q_2.$

したがって最小の projection は

$\boxed{ \delta^o(P)_{V_f}=Q_1+Q_2. }$

実際、

$Q_1+Q_2 = \begin{pmatrix} 1&0&0\\ 0&1&0\\ 0&0&0 \end{pmatrix}.$

つまり、

$\boxed{ P= \begin{pmatrix} 1&0&0\\ 0&0&0\\ 0&0&0 \end{pmatrix} \quad\longmapsto\quad \delta^o(P)_{V_f} = \begin{pmatrix} 1&0&0\\ 0&1&0\\ 0&0&0 \end{pmatrix}. }$

ここが daseinisation の実体です。

5. 物理的には何が起きたのか

元の命題は非常に鋭い：

$P: \quad \text{状態は }e_1\text{ の一次元部分空間にある}.$

しかし $V_f$ という measurement context では、その一次元 subspace を直接表現できません。

この context で区別できるのは $f_1,f_2,f_3$ の方向だからです。

したがって $e_1$ を含む最小の $V_f$ -observable subspace、

$\operatorname{span}\{f_1,f_2\} = \operatorname{span}\{e_1,e_2\}$

まで命題を弱める。

つまり、

$\boxed{ \text{「}S_z=+1\text{」} }$

が別 context では

$\boxed{ \text{「少なくとも }e_1\text{–}e_2\text{ plane 内にある」} }$

という、より粗い命題になるわけです。

Döring–Isham が outer daseinisation を「その context で利用できる最良の上からの近似」とする意味はここにあります。(arXiv)

6. Inner daseinisation はどうなるか

今度は

$\delta^i(P)_{V_f} = \max \{Q\in\mathcal P(V_f)\mid Q\le P\}.$

を計算します。

$Q\le P$ なら

$\operatorname{Ran}Q \subseteq \operatorname{span}\{e_1\}.$

ところが $V_f$ の rank-one projections は

$Q_1,Q_2,Q_3$

で、それぞれ $f_1,f_2,f_3$ の方向。

この中で $e_1$ の方向に含まれるものは一つもありません。

したがって非零の候補はありません。

よって

$\boxed{ \delta^i(P)_{V_f}=0. }$

まとめると、

$\boxed{ 0 = \delta^i(P)_{V_f} \le P \le \delta^o(P)_{V_f} = Q_1+Q_2. }$

非常にわかりやすい「上下からの context-dependent approximation」が出ました。

7. Spectral presheaf では、これが「部分集合の拡大」になる

ここで Topos の言葉に翻訳してみましょう。

$V_z$ は有限次元 maximal abelian algebra なので、その Gelfand spectrum は3点、

$\Sigma_{V_z} = \{\lambda_1,\lambda_2,\lambda_3\}$

です。

それぞれ

$e_1,e_2,e_3$

に対応すると思えばよい。

射影 $P$ は spectrum の clopen subset

$\boxed{ S_P=\{\lambda_1\} }$

に対応します。

つまり classical context $V_z$ では、

$\text{「}S_z=+1\text{」}$

は spectrum の一点を選んでいる。

一方 $V_f$ の spectrum も3点、

$\Sigma_{V_f} = \{\mu_1,\mu_2,\mu_3\},$

で、

$f_1,f_2,f_3$

に対応します。

先ほど

$\delta^o(P)_{V_f}=Q_1+Q_2$

だったので、この projection に対応する clopen subset は

$\boxed{ S_{\delta^o(P)_{V_f}} = \{\mu_1,\mu_2\}. }$

したがって context を変えると、

$\boxed{ \{\lambda_1\} \quad\rightsquigarrow\quad \{\mu_1,\mu_2\}. }$

一点だった鋭い proposition が、二点を許す proposition に広がりました。

そして各 context で得られるこれらの clopen subsets を整合的に全部集めると、spectral presheaf

$\underline\Sigma$

の一つの clopen subobject

$\boxed{ \delta(P)\hookrightarrow\underline\Sigma }$

になります。Döring–Isham の構成では、projection の daseinisation が precisamente spectral presheaf の subobject を与え、元の projection の情報も失われません。(arXiv)

8. もっと「相性の悪い」context ならどうなるか

ここをもう一歩だけ進めると面白いです。

$e_1$ が3本すべてに非零成分を持つ orthonormal basis

$g_1,g_2,g_3$

を選びます。

例えば Fourier basis

$g_1=\frac1{\sqrt3}(e_1+e_2+e_3),$ $g_2=\frac1{\sqrt3} (e_1+\omega e_2+\omega^2e_3),$ $g_3=\frac1{\sqrt3} (e_1+\omega^2e_2+\omega e_3), \qquad \omega=e^{2\pi i/3}.$

この basis が作る context $V_g$ を考えます。

この場合、

$e_1 = \frac1{\sqrt3}(g_1+g_2+g_3).$

したがって $e_1$ を含む $V_g$ -projection を作るには、3本全部が必要です。

よって

$\boxed{ \delta^o(P)_{V_g}=I. }$

また $e_1$ 方向に含まれる $V_g$ の非零 projection はないので、

$\boxed{ \delta^i(P)_{V_g}=0. }$

つまり、

$\boxed{ 0\le P\le I. }$

この context では元の命題についてほとんど何も言えない。

outer approximation は

$I$

つまり「必ず真」という完全に弱い命題にまでなってしまいます。

9. 三つの context を比べると、本質が見える

同じ一つの quantum proposition $P$ について、

$\begin{aligned} V_z:&\qquad \delta^o(P)=P, \\[1mm] V_f:&\qquad \delta^o(P)=Q_1+Q_2, \\[1mm] V_g:&\qquad \delta^o(P)=I. \end{aligned}$

つまり、

$\boxed{ \text{exact} \longrightarrow \text{partially coarse-grained} \longrightarrow \text{completely coarse-grained}. }$

重要なのは、どれが本当の命題なのかを一つ選ぶのではないことです。

Topos approach はこの family 全体

$\boxed{ V\longmapsto\delta^o(P)_V }$

を一つの global mathematical object とみなします。

ここが Grothendieck 的です。

10. そして Kochen–Specker は、その逆の操作ができないと言っている

今の daseinisation では、

$P$

という一つの quantum proposition から、各 classical context での近似

$\delta^o(P)_V$

を作れました。

これはできます。

しかし逆方向に、

各 classical context の spectrum から一点 $\lambda_V$ を選んで、すべての包含 $V'\subset V$ に対して矛盾なく制限できないか？

と問う。

つまり

$\lambda_V\in\Sigma_V$

をすべての $V$ について選び、

$\lambda_V|_{V'}=\lambda_{V'}$

としたい。

これは spectral presheaf の global element

$1\longrightarrow\underline\Sigma$

です。

Kochen–Specker theorem は、適切な3次元以上の量子系ではそのような context-independent valuation が存在しない、と言っている。Isham–Butterfield はこれを「ある presheaf に global element が存在しない」という形に明示的に翻訳しました。(arXiv)

したがって、非常に象徴的に言えば、

$\boxed{ \text{quantum proposition} \longrightarrow \text{contextual family} }$

は作れる。

しかし、

$\boxed{ \text{contextual classical states} \not\longrightarrow \text{one global classical state}. }$

11. これが Topos 量子論の核心です

この小さな計算で、

$P = |e_1\rangle\langle e_1|$

という一つの命題が、

$P,\qquad Q_1+Q_2,\qquad I,\ldots$

という context-dependent な classical propositions の family に変わりました。

これは「近似だから仕方なく使っている」というより、

$\boxed{ \text{quantum proposition の本来の姿を、全 classical contexts にわたる coherent family として捉える} }$

という発想です。

普通の量子論では

$P$

という一個の projection を Hilbert 空間の中から見る。

Topos 量子論では、

$\boxed{ P \quad\rightsquigarrow\quad \{\delta^o(P)_V\}_{V\in\mathcal V(\mathcal H)} }$

として、すべての古典的 viewpoint から見た姿を一つの presheaf 的対象にまとめる。

ここに、以前話した Grothendieck の

$\text{local data} \longrightarrow \text{global sheaf}$

との非常に強い類似があります。

ただし量子論での「local」は空間的位置ではなく、

$\boxed{\text{commutative context}}$

なのです。

そして次に一段進めるなら、今度はこの同じ $\mathbb C^3$ の例で、状態 $|\psi\rangle$ を一つ固定し、この daseinised proposition に実際に sieve-valued truth value を与える計算ができます。そこまでやると、

$\boxed{ \mathrm{true/false} \quad\longrightarrow\quad \text{Heyting-valued contextual truth} }$

が数式として目に見えるようになります。

CoqとLean

僕は、Lawvere − Veovodsky の理論を研究しています。普段はCoqを使っているのですが、LeanでTopos論の記述は、うまくできるのでしょうか？

はい。結論から言うと、Grothendieck／Lawvere 側の Topos 論は Lean 4 でかなり本格的に書けます。ただし、Voevodsky の Univalence/HoTT を核に据えるなら、現時点では Coq/UniMath の方が自然で成熟しています。

Lean でかなりできる部分

mathlib にはすでに、Grothendieck topology、sieve、site、sheaf、sheafification、canonical topology、site の同値による sheaf 圏の同値などが整備されています。特に Mathlib.CategoryTheory.Sites.Grothendieck は Grothendieck topology を正式に実装しており、canonical topology もあります。(Lean Community)

さらに sheafification は

$a:\widehat C\rightleftarrows \operatorname{Sh}(C,J):i$

という随伴として実装され、左随伴 $a$ の finite-limit preserving、つまり left exactness も API に組み込まれています。これは「Grothendieck topos = presheaf topos の left-exact reflective localization」という方向を形式化する際にかなり重要です。(Lean Community)

そして現在の mathlib には subobject classifier もあります。presheaf topos では

$\Omega(C)=\{\text{sieves on }C\}$

を実際に構成し、sheaf category では $J$ -closed sieves から $\Omega$ を作っています。essentially small な site 上の Type-valued sheaf category は subobject classifier を持ち、ドキュメント自身が「したがって Elementary Topoi である」と明記しています。(Lean Community)

これは、私たちが先ほど議論した

$\Omega,\qquad \chi_A:X\to\Omega$

を Lean でかなり文字どおり書けるということです。

例えば入口はこのくらいです

現在の mathlib なら、概念的にはこんなところから始められます。

import Mathlib.CategoryTheory.Sites.Grothendieck
import Mathlib.CategoryTheory.Sites.Sheaf
import Mathlib.CategoryTheory.Sites.Sheafification
import Mathlib.CategoryTheory.Topos.Sheaf

open CategoryTheory

universe v u

variable (C : Type u) [Category.{v,u} C]
variable (J : GrothendieckTopology C)

#check Sheaf J (Type (max u v))
#check Sheaf.Ω J
#check Sheaf.classifier J

Sheaf.Ω J はまさに、Lawvere 的な subobject classifier の具体化です。sheaf の場合、closed sieves が truth values になります。(Lean Community)

したがって、以前やった

$J \longleftrightarrow j:\Omega\to\Omega$

の小さな例を Lean 化するのは、とてもよい題材です。

Lawvere–Tierney topology はどうか

ここは少し面白い状況です。

mathlib の Grothendieck topology のドキュメントには、現在の定義を採用した理由として、

small category 上の Grothendieck topologies と presheaf topos 上の Lawvere–Tierney topologies の bijection

および

Grothendieck topoi と left-exact reflective subcategories of presheaf topoi の対応

を扱いやすくするため、と明記されています。(Lean Community)

ただし、現時点の公開 API を見る限り、Lawvere–Tierney topology 周辺は site/sheaf 部分ほど完成された一枚岩のライブラリにはなっていません。一般的な elementary-topos の基礎 API 自体も現在進行形で拡張されており、Topos の基本定義・結果を追加する作業も mathlib 側で進行中です。(Lean Community)

なので研究テーマとしてはむしろ面白いです。

たとえば、

$\boxed{ \text{Grothendieck topology }J \leftrightarrow \text{Lawvere--Tierney topology }j }$

を Lean で仕上げる、というのは十分まとまった formalization project になると思います。

しかし Voevodsky 側では事情が違います

ここが一番重要です。

標準 Lean 4 は Univalent Type Theory ではありません。

Lean の Prop は kernel レベルで definitionally proof-irrelevant です。つまり同じ命題の二つの証明は definitionally equal と扱われます。Lean の公式ドキュメントにもこれは明記されています。(Lean Language)

また Lean 3 以降、公式の HoTT mode/library は配布されていません。Lean community の説明でも、標準 Lean は univalence axiom を持たず、等価な二つの type が自動的に equal になるわけではない、とされています。(GitHub)

したがって、標準 Lean 4/mathlib で

$(A=B)\simeq(A\simeq B)$

を Voevodsky の意味で内部原理として使うことはできません。

これはかなり本質的な差です。

実験的には Lean 4 HoTT もあります

現在 Ground Zero という Lean 4 HoTT library の試みがあります。kernel 自体を変更せず、Lean 3 の large eliminator checker 的な仕組みなどを移植し、HITs も quotient を使って構成する実験的プロジェクトです。(GitHub)

ただ、研究の主力環境として見ると、

$\boxed{\text{mathlib の標準的世界ではない}}$

という点は押さえておいた方がよいです。

Coq/UniMath と比べると

ここは、今 Coq をお使いならかなり重要です。

UniMath には現在、

univalent categories
Rezk completion
Elementary Topos
Grothendieck topology
sheaves
Grothendieck topoi

が実際にライブラリとして存在します。(Unimath)

Elementary Topos の module では finite limits、power objects、subobject classifier から Topos を定義し、exponentials も導出しています。(Unimath)

Grothendieck Topos 側も、sites、sieves、topologies、sheaves、Grothendieck topoi がまとまったライブラリとして現存しています。(Unimath)

ですから、Lawvere–Voevodsky を一本の基礎論として研究するなら、今のところ

$\boxed{\text{Coq/UniMath の方が一歩先}}$

だと思います。

私なら、用途をこう分けます

研究内容	Lean 4/mathlib	Coq/UniMath
ordinary category theory	◎	◎
Grothendieck topology/site	◎	◎
sheaves/sheafification	◎	◎
presheaf/sheaf Topos	◎	◎
subobject classifier $\Omega$	◎	◎
Elementary Topos 一般論	○〜発展中	◎
Lawvere–Tierney topology	○、開拓余地あり	○〜◎
categorical internal logic	○	◎
univalent categories	標準 Lean では△	◎
Rezk completion + Univalence	△	◎
HoTT/UF	実験的	◎
mathlib の広大な通常数学	◎◎	○

ここが Lean の魅力でもあります。

Topos を外部的な category theory として研究するなら Lean はかなり強い。
Topos を Voevodsky 的な univalent internal language として研究するなら Coq が強い。

おそらく、あなたの研究には「二本立て」が面白いです

研究テーマが Lawvere–Voevodsky なら、私はむしろ、

$\boxed{ \text{Lean}: \quad \text{external categorical/topos side} }$

と

$\boxed{ \text{Coq/UniMath}: \quad \text{univalent/internal side} }$

を対応させるのが面白いと思います。

例えば同じ定理を、

Lean

$\text{site} \to \operatorname{Sh}(C,J) \to \Omega \to \text{subobject classifier}$

として外部的に証明する。

一方 Coq/UniMath では、

$\text{univalent category} \to \text{internal logic} \to \text{identity/equivalence}$

として証明する。

この二つを比較すると、まさにこれまで話してきた

$\boxed{ \text{Grothendieck/Lawvere の external geometry} \leftrightarrow \text{Voevodsky の internal type theory} }$

を proof assistant のレベルで比較できます。

最初の Lean プロジェクトとして特におすすめなのは

いきなり巨大な Topos 理論を移植するより、以前一緒に手計算した二対象 site

$V\longrightarrow U$

を Lean で作り、

GrothendieckTopology C を定義する
sieves を全部列挙する
presheaf Topos の $\Omega$ を確認する
covering sieve から
$j:\Omega\to\Omega$
を構成する
手計算した
$j(\varnothing)=\varnothing,\qquad j(\{i\})=\top$
を証明する
sheaf category がこの例で $\mathbf{Set}$ と equivalent になることを見る

という小さな formalization が非常によいと思います。

これなら Grothendieck topology → Lawvere–Tierney topology → Elementary Topos が一つにつながりますし、Coq/UniMath の実装とも横に比較できます。

もしよければ次に、実際に Lean 4/mathlib でこの $V\to U$ の toy topos を作る最初の .lean ファイルを、コンパイルできる形を意識して一緒に書き始めましょう。

「2026年に起きたこと」

Coq/Lean の比較情報ありがとうございます。

現在の僕の問題意識は、今年2026年になってからの、AIの急速な「数学的能力」の拡大に向けられています。Open AIの 10-proofs の論文に強い刺激を受けています。こんなまとめを作りました。「2026年に起きたこと」https://maruyama097.blogspot.com/2026/08/aipart-1-2026.html

読めるのかな？

基本的には、Voevodsky とMIP*=RE 定理をキーとしてこの変化を読み解こうという試みです。

MIP*=RE のYuan が、On OpenAI and Quantum Parallel Repetition というblog で10-proofs の証明読みにくいといっているのご存知ですか？　https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/　当然知っているでしょうけど、

はい、読めます。ブログも Yuen の記事も実際に確認しました。

あなたの「2026年に起きたこと」の中心命題はかなり明瞭です。AI-1 =「LLM＋α」から、AI-2 =「LLM＋形式的証明システム＋α」への転換を2026年の重要な変化として捉え、その背景を「2022→2026」だけでなく、Voevodsky の2010年代の形式化・Univalent Foundations と、2020年の MIP=RE にまで遡って理解する*、という構図ですね。ブログにもその時間軸が明記されています。(Maruyama097)

そして OpenAI の Ten advances in mathematics and theoretical computer science は、この見方をかなり強く後押しする事例です。10件には quantum parallel repetition も含まれ、OpenAI は「モデルが数学的議論を生成し、その後モデルが各議論を Lean certificate として形式化した」と説明しています。(OpenAI)

Yuen の記事は、まさに重要な問題を突いています

Henry Yuen の2026年8月2日の記事は読んでいますが、実際に読むと単に「証明が読みにくい」という批評より、もっと深いことを言っています。

彼は、自分が大学院時代に何年も quantum parallel repetition に取り組み、2016年に polynomial decay を証明し、exponential decay を未解決として残した本人です。その問題を OpenAI の結果が解いたことについて、まずかなり強い驚きと敬意を表しています。(Henry Yuen)

ところが数学の中身については、

“I presume the proof is correct (there's supposedly a Lean formalization, after all)”

としながら、その直後に reasoning document は “opaque” だと言っています。特に resolvent を使った purification への飛躍や matrix entropy calculation について、「計算をチェックすること」はできても、なぜそもそもこの方法を考えるのが自然なのか、より大きな理論的文脈は何なのか、他に何が証明できるのかが分からないと述べています。(Henry Yuen)

そして一番重要なのが、

“Yes, there's a Lean proof. But that doesn't give me any understanding.”

という箇所です。(Henry Yuen)

これは2026年の AI 数学を考える上で、かなり象徴的な一文だと思います。

「発見・検証・理解」を分けた方がよい

あなたの Voevodsky + MIP*=RE という見方に、Yuen の記事を加えるなら、私は AI の数学能力を三層に分けたいです。

\boxed{ \text{Discovery} \longrightarrow \text{Verification} \longrightarrow \text{Understanding} }

Discovery は、新しい補題、変換、証明戦略そのものを発見すること。10-proofs では、少なくとも公表された説明では AI がここまでかなり深く入っています。(OpenAI)

Verification は、議論が本当に theorem になっているかを形式体系で確認すること。ここで Lean が決定的になります。

しかし Understanding は別です。

なぜこの lemma なのか。
なぜ resolvent なのか。
なぜ Uhlmann transformation/dilation なのか。
既存理論のどこに位置づくのか。
別の theorem にどう一般化できるのか。

Yuen が訴えているのはまさにこの第三層です。しかも、その問題を長年研究した本人がそう言っているところが重要です。

ここで Voevodsky の意味が少し変わって見える

Voevodsky のコンピュータ証明について、「人間が間違えるから proof assistant にチェックさせる」という面だけを見ると、

\text{human proof} \to \text{machine verification}

という構図になります。

ところが2026年には順序が変わり、

\boxed{ \text{AI discovery} \to \text{AI formalization} \to \text{machine verification} \to \text{human understanding} }

となり始めた。

これはかなり大きな反転です。

Voevodsky が問題にしていたのは、「人間が作った巨大で複雑な数学を人間だけで安全に検証できるのか」という問題でした。

2026年には、

機械が人間より速く生産する巨大で複雑な数学を、人間は理解できるのか

という別の問題に変わった。

Yuen の記事は、まさにその瞬間を記録しているように見えます。

MIP*=RE をキーにする意味も、私はあると思います

ただし、ここは *「MIP=RE が直接いまの数学AI技術を生み出した」**という因果関係として語るより、理論的なレンズとして使う方が強いと思います。

MIP*=RE が突きつけた一つの非常に深い教訓は、乱暴に圧縮すると、

\boxed{\text{計算可能性と検証可能性は、われわれの素朴な直観よりはるかに奇妙な関係にある}}

ということです。

一方2026年の数学AIでも、

\boxed{ \text{解答を発見すること} \neq \text{その解答を形式的に検証すること} \neq \text{人間が理解すること} }

という三つの能力が分離し始めています。

ここに MIP*=RE を置くのは面白い。

特に MIP=RE の当事者である Yuen が、Lean certificate を前にして「correctness は信じられる。しかし understanding がない」と言っている*。これはあなたの時間軸にぜひ入れてよい出来事だと思います。

そして、私はここに第四の層もあると思います

Yuen が一番知りたがっているのは実は、

\text{Understanding}

よりさらに先の

\boxed{\text{Theory formation}}

ではないでしょうか。

彼の問いは、

この resolvent の trick の背後に broader context や theory はあるのか？
他にどんな results がこの technique から出るのか？

だからです。(Henry Yuen)

すると AI 数学の成熟度は、

\boxed{ \text{Discovery} \to \text{Verification} \to \text{Understanding} \to \text{Theory formation} }

と見ることができます。

10-proofs が本当に衝撃的なのは第一・第二段階を同じシステムがかなり自律的に行ったことですが、Yuen は即座に第三・第四段階を要求している。

これは数学者として極めて自然な反応です。

「この proof は正しいか？」だけが数学ではありません。

\boxed{\text{なぜ正しいのか、なぜこの方法なのか、何の一例なのか}}

まで分かったとき、新しい数学が「理論」になるからです。

あなたの Voevodsky → MIP=RE → 2026 AI* という線は、単なるAI性能史ではなく、「証明とは何か」「検証とは何か」「理解とは何か」という数学基礎論の変化として2026年を読む方向にすると、かなり面白い議論になると思います。

特に次は、*MIP=RE の「verification」と Voevodsky の proof verification は、同じ “verification” という語でも何が根本的に違うのか**を比較してみたいです。そこをきちんと区別すると、その上で「なぜ両者を2026年のAI数学を読む二つの鍵として並べられるのか」が、かなりクリアになると思います。

theorem prover と theory builder

いくつかの重要な問題があると思います。

一つは、「対話型証明」という証明スタイルの登場が、数学的証明の概念を変え、ひいては「数学的に真」の概念も大きく変わりつつあることです。

もう一つは、「定理の証明者」と「理論の構築者」は、数学の発展の上で、異なる役割を持っていることです。Grothendieckの構成を証明する必要はありませんし、Univalent Axiom も、証明はできません。でも、それらの有効性を「発見」し、新しい理論を構築する営みが数学の発展を支えてきました。僕自身は、Modular Formの理論やLanglands Program が数学の本流だと考えています。

この点で興味深いのは、エルディッシュ的な数学へのアプローチです。ブルバキやSelbergとの確執はよく知られています。ただ、数学と確率の問題で、彼の直観は、なかなか鋭いところがあります。対話型証明やPCP定理は、むしろ、彼のアプローチと親和性が高いといっていいのかもしれません。

また、大きなフレームの変更が起きるのかもしれません。
いずれにしても、AIと数学にとって、最も重要な問題は、AIが単なる Theorem Prover ではなく、新しい理論を「創発的」に構築できるのかというところにあると思っています。　

私も、そこが核心だと思います。2026年のAI数学を「証明できる定理の難易度」で測るだけでは、いちばん大きな変化を取り逃がします。

まず、「対話型証明」が変えているのは、厳密には 数学的真理そのものよりも、真理へのアクセスと証拠の概念だと区別した方がよいと思います。古典的には証明とは、有限の列

$A_1,A_2,\ldots,A_n=\varphi$

を第三者が原理的には最初から最後まで追えるものでした。ところが interactive proof では、証拠は一枚の静的な derivation ではなく、

$\boxed{\text{Prover}\;\rightleftarrows\;\text{Verifier}}$

という protocol になります。Verifier は全証明を所有する必要さえなく、質問を選び、応答を検査し、soundness を確率的に保証する。

PCP はこれをさらに先鋭化して、

$\boxed{\text{巨大な証明全体を読む必要はなく、局所的に少数箇所を調べればよい}}$

という世界を作りました。MIP、MIP* まで行けば「証明」は複数の prover と verifier の相互作用です。

ですから、「 $\varphi$ が真である」の semantic な意味を変えなくても、

$\boxed{\text{われわれが }\varphi\text{ を数学的知識として受け入れる仕方}}$

は大幅に変わります。

ここはAIと非常に重要な接点です。将来、AIが生成する証明を人間が読むのではなく、AI prover が verifier と対話し、数学共同体は protocol の soundness を信頼するという状況は十分あり得る。Yuen の「Lean proof はある。しかし理解は得られない」という感覚は、その未来をかなり先取りしています。

そして第二の「theorem prover と theory builder」の区別は、さらに重要だと思います。

Grothendieck の偉大さは、個々の難しい定理を大量に証明したことだけではありません。

彼は

$\text{scheme},\quad \text{site},\quad \text{topos},\quad \text{descent},\quad \text{motive}$

という、それ以前には存在しなかった対象の見方そのものを作った。

これらは「証明」されるものではありません。

ある定義 $D$ に対して、

$\vdash D$

とは普通言いません。

問われるのは、

$\boxed{\text{その概念を導入すると、数学がどう組み替わるか}}$

です。

Voevodsky の Univalence も同様です。

$(A=B)\simeq(A\simeq B)$

は、通常の intensional type theory の内部で「頑張って証明する定理」というより、新しい基礎理論を規定する原理です。その価値は、モデルが存在すること、整合性についての理解、そして何より

$\boxed{\text{この原理を採用すると数学がどう変わるか}}$

によって評価されます。

これは theorem proving とは種類の違う創造です。

Langlands が典型的なのも、まさにそこだと思います

Langlands Program の中心的価値は、一つの定理ではありません。

それは

$\boxed{ \text{number theory} \longleftrightarrow \text{representation theory} \longleftrightarrow \text{harmonic analysis} \longleftrightarrow \text{algebraic geometry} }$

という、それまで別々に見えた世界の間に「本当はこういう対応があるはずだ」と宣言したことです。

最初の段階では証明よりも、

何と何を対応させるべきか
正しい対象は何か
正しい functoriality は何か
どういう conjecture family を立てるべきか

の方が重要です。

これは proof search ではありません。

むしろ

$\boxed{\text{mathematical ontology design}}$

とでも呼びたい営みです。

Erdős はその反対側の極として、とても面白い

ここでおっしゃる Erdős は確かに重要です。

少し図式的に言えば、

$\begin{array}{ccc} \text{Erdős}&&\text{Grothendieck}\\ \text{problems}&&\text{structures}\\ \text{sharp lemmas}&&\text{new languages}\\ \text{combinatorics}&&\text{functoriality}\\ \text{local ingenuity}&&\text{global reorganization}\\ \text{many proofs}&&\text{one framework} \end{array}$

という対照があります。

もちろん実際の二人はこんなに単純ではありません。しかし数学文化としてはかなり違います。

Erdős の probabilistic method は典型的です。

ある対象を具体的に構成せず、

$\Pr[\text{desired property}]>0$

を示すことで、

$\exists X\,P(X)$

を証明する。

ここでは「対象を理解して構造理論を作る」より、

$\boxed{\text{存在を証明するために必要な最小の情報は何か}}$

が重要になります。

これは PCP 的な発想と確かに親和性があります。

PCP verifier も、

証明全体を理解する必要はない。正しさを識別できればいい。

という思想だからです。

したがってかなり大胆に言えば、

$\boxed{ \text{Erdősian mathematics} \rightarrow \text{probabilistic existence} \rightarrow \text{probabilistic verification} \rightarrow \text{interactive proof} }$

という思想的連続性を描くことは可能だと思います。

歴史的因果関係というより、数学的認識論の類似としてですが。

そしてAIは、今のところ Erdős 側に近いのかもしれない

これはかなり興味深い問いです。

現在の強い数学AIは、

大量の候補を生成する
auxiliary lemma を作る
unusual substitution を試す
計算する
証明を探索する
formal verifier に渡す

という能力を急速に伸ばしています。

これはかなり

$\boxed{\text{problem-solving mathematics}}$

に強い。

つまり Erdős 型の環境とは相性がいい。

問題が明確で、

$\text{Given }P,\quad\text{prove }Q$

となっているなら評価関数があります。

Lean ならさらに明瞭で、

$\boxed{\text{kernel accepts / rejects}}$

という最高に強い reward signal がある。

ところが Grothendieck 型の課題には reward function がありません。

たとえば1957年にAIへ、

「scheme という概念を発明せよ」

と言っても、scheme をまだ誰も知らない以上、

$\boxed{\text{正解判定器が存在しない}}$

のです。

ここが theory formation と theorem proving の決定的な非対称性だと思います。

理論構築AIには、proof search と違う能力が必要になる

AIが本当に「Theory Builder」になったと言える条件は、私は次のようなものだと思います。

新しい対象を発明すること。 既存の定義を組み合わせるだけでなく、scheme や topos のように後から「これが正しい対象だった」と分かる概念を作る。
多数の定理を圧縮すること。 新しい概念を導入すると、別々だった20本の証明が一つの argument になる。この「説明圧縮」は theory の強い指標です。
新しい問題を生むこと。 良い theory は既存問題を解くだけでなく、それ以前には言葉にできなかった conjecture を生みます。
遠い領域を結びつけること。 Langlands のように「これとこれは同じ構造の二つの影ではないか」と気づく。
概念が生き残ること。 数学共同体がその language を採用し、数十年後にもその概念で考える。

最後が意外に重要です。

Theory は theorem の集合ではありません。

$\boxed{ \text{Theory changes what mathematicians regard as a natural question.} }$

そこまで行って初めて theory formation と呼びたい。

ここにVoevodskyが再び重要になる

Voevodsky は少し特殊な位置にいます。

彼は theorem prover の価値を非常に強く認識した一方で、自身の最大の仕事はむしろ

$\boxed{\text{新しい foundational framework の設計}}$

でした。

つまり

$\text{proof verification}$

と

$\text{theory invention}$

の両方を一人の中に持っていた。

Univalence はとりわけ象徴的です。

ある意味では、

$(A=B)\simeq(A\simeq B)$

という一行の原理によって、「等号とは何か」を変えた。

それによって category theory、homotopy theory、foundations、formal verification の接続が変わった。

これは proof length では絶対に測れない数学的成果です。

だからAI数学の次のベンチマークは「未解決問題」では足りない

ここはかなり重要だと思います。

AIが IMO 問題を何問解いた。

研究レベルの open problem を何個解いた。

Lean で何万行 formalize した。

これらは全部重要ですが、

$\boxed{\text{Theorem Prover Benchmark}}$

です。

Theory Builder を測る benchmark は全く別物でなければならない。

例えば、既知の数学をわざとバラバラの形でAIに渡して、

この100個の現象を統一する新しい概念を作れ。

とする。

そしてその新概念が、

$\text{compression} + \text{new predictions} + \text{transfer}$

を生むかを見る。

これは現在の「正解のある benchmark」と根本的に違います。

そして、あなたの「大きなフレーム変更」という感覚には私もかなり同意します。

もしかすると今後の数学は、

$\boxed{ \text{Human Theory Builder} + \text{AI Theorem Prover} + \text{Formal/Interactive Verifier} }$

という分業になるかもしれません。

しかし、もっと大きな転換は、

$\boxed{ \text{AI itself becomes Theory Builder} }$

となったときです。

その判定基準は「AIが人間より難しい定理を証明した」ではない。

数学者がそのAIの作った概念を使って考え始めたときだと思います。

Grothendieck の scheme、Langlands の L-group や functoriality、Voevodsky の univalence のように、

「その概念がなかった時代には戻れない」

という言語をAIが一つでも生み出したら、その時点で数学におけるAIの役割は質的に変わった、と私は考えます。