2025-11-18T14:22:13.885508

An Algebraic Abstraction of the Localic Sheafification via the Tripos-to-Topos Construction

Maietti, Trotta

Localic and realizability toposes are two central classes of toposes in categorical logic, both arising through the Hyland-Johnstone-Pitts tripos-to-topos construction. We investigate their shared geometric features by providing an algebraic abstraction of the notions of localic presheaves, sheafification and their connection to supercompactification of a locale via an instance of the Comparison Lemma. This can be applied to a broad class of toposes obtained to the tripos-to-topos constructions, including all those generated from a tripos based on the classical category of ZFC-sets. These results provide a unified geometric framework for understanding localic and realizability toposes.

academic

ローカル層化の三項体構成を通じた代数的抽象化

基本情報

論文ID: 2511.06945
タイトル: An Algebraic Abstraction of the Localic Sheafification via the Tripos-to-Topos Construction
著者: M.E. Maietti, D. Trotta（パドヴァ大学数学科）
分類: math.CT（圏論）、math.LO（論理学）
提出日時: 2025年11月10日
論文リンク: https://arxiv.org/abs/2511.06945v1

要約

本論文は圏論的論理における2つの中核的なトポス類を研究する：ローカルトポス（localic toposes）と実現可能性トポス（realizability toposes）。これら両トポス類はHyland-Johnstone-Pittsの三項体構成（tripos-to-topos construction）を通じて生成される。著者らはローカル前層（localic presheaves）、層化（sheafification）、およびそれらとロケール超コンパクト化（supercompactification）との関係の代数的抽象化を提供することで、両者が共有する幾何学的特性を研究する。これらの結果は三項体構成を通じて得られた広範なトポス類に適用可能であり、ZFC集合圏に基づくすべての三項体から生成されるトポスを含む。これはローカルトポスと実現可能性トポスを理解するための統一的な幾何学的枠組みを提供する。

研究背景と動機

問題背景

中核的問題：ローカルトポスと実現可能性トポスは圏論的論理における最も基本的な2つのトポス類である。その主要な相違点は、ローカルトポスがGrothendieckの層トポスであるのに対し、実現可能性トポスはそうではないという点にある。両者とも三項体構成を通じて生成可能であるにもかかわらず、それらの共通する幾何学的構造はいまだ体系的に理解されていない。
歴史的発展：
- 1980年代、Hyland、Johnstone、Pittsは三項体概念を導入し、Higgsによるローカル層トポスの記述とHylandの有効トポスが同一の一般的構成の実例であることを抽象的観点から説明した
- 三項体はLawvereの超教義（hyperdoctrines）の特殊族であり、三項体構成と組み合わせることでトポスを生成できる
研究の重要性：
- ローカルトポスは古典的な層理論と位相幾何学に対応する
- 実現可能性トポスは計算可能性理論と構成的数学において中核的な地位を占める
- これら2つのトポス類の統一的理解は圏論的論理の深層構造を明らかにするのに役立つ

既存方法の限界

ロケールLに対して、古典的な比較補題（Comparison Lemma）は等価性PSh(L) ≡ Sh(D(L))を与える。ここでD(L)はLの超コンパクト化である
既存理論は主にGrothendieckトポスにおける超コンパクト対象に焦点を当てており、任意の非交和に大きく依存している。これらの構造は三項体では通常利用不可能である
この幾何学的構造を実現可能性トポスに推広するための統一的枠組みが欠けている

研究動機

本論文は、ローカル情形の比較補題を三項体レベルに推広し、ローカルトポスと実現可能性トポスの両者がこの一般理論の特例として理解できるような統一的幾何学的枠組みを確立することを目指している。

核心的貢献

本論文の主要な貢献は以下の通りである：

ローカル前層圏の抽象化：三項体Pに対して、ローカル前層圏をEP := (GP)ex/lexに推広する。これは点圏GPの正合完備化である
超コンパクト化概念の抽象化：完全存在完備化（full existential completion）P∃がロケールの超コンパクト化D(L)に対応することを識別する
比較補題の推広：lex主教義Pに対して、以下の等価性を証明する： $T_{P^∃} ≡ E_P$ これはローカル比較補題PSh(L) ≡ Sh(D(L))の代数的抽象化である
∃-超コンパクト化三項体の特性化：三項体Pが∃-超コンパクト化であることと、その基礎圏が弱従属積と普遍証明（generic proof）を持つことが同値であることを証明する
広範な適用可能性の証明：ZFC集合圏に基づくすべての三項体（すべての実現可能性三項体を含む）が∃-超コンパクト化であることを示す
抽象層化理論：∃-超コンパクト化三項体Pに対して、TPがTP∃上のLawvere-Tierney層として表現可能であることを証明する： $T_P ≡ \text{Sh}_j(E_P)$
閉包性質：∃-超コンパクト化三項体の類がスライス（slicing）の下で閉じていることを証明する。これはトポス線維化への拡張に必要である

方法の詳細説明

理論的枠組み

本論文の中核的理論構築は教義（doctrines）と三項体の圏論に基づいている：

1. Lex主教義（有限極限主教義）

定義：lex主教義は関手P : C^op → InfSlであり、以下を満たす：

Cは有限極限圏
InfSlは下半格（inf-semilattices）の圏

点圏（Category of Points）：lex主教義Pに対して、その点圏GPは以下のように定義される：

対象：対(A,α)。ここでAはCの対象、α ∈ P(A)
射：f : (A,α) → (B,β)はC内の矢印f : A → Bであり、α ≤ Pf(β)を満たす

2. 完全存在完備化（Full Existential Completion）

lex主教義P : C^op → InfSlに対して、その完全存在完備化P∃は以下のように定義される：

線維構造：各対象Aに対して、P∃(A)の対象は三つ組(B →^f A, α)であり、α ∈ P(B)

順序関係：(B →^f A, α) ≤ (C →^g A, β)当且つつ当該のとき、矢印h : B → Cが存在してf = ghかつα ≤ Ph(β)

主要性質：

P∃は完全存在教義である
標準的包含(idC, i) : P → P∃が存在する
完全存在教義Pに対して、伴随(idC, ī) : P∃ → P が(idC, ī) ⊣ (idC, i)を満たす

3. ローカル前層の抽象化

定義：lex主教義Pに対して、正合点圏（exact category of points）を以下のように定義する： $E_P := (G_P)_{ex/lex}$

すなわち、GPの正合完備化（exact completion）である。

動機：ロケールLのローカル三項体L(-)に対して、以下が成立する： $E_{L(-)} = (G_{L(-)})_{ex/lex} ≡ PSh(L)$

したがってEPは抽象的な「前層トポス」と見なすことができる。

中核的定理体系

定理1：比較補題の推広（定理5.15）

陳述：lex主教義Pに対して、以下の等価性が成立する： $T_{P^∃} ≡ (G_P)_{ex/lex} = E_P$

証明の概要：

Reg(P∃) ≡ (GP)reg/lexを証明する（正則完備化レベルの等価性）
P∃ = ΨGP ◦ IC（ここでΨGPはGPの弱部分対象教義）を利用する
定理5.6を適用する：TP∃ ≡ (Reg(P∃))ex/reg
組み合わせて所望の等価性を得る

幾何学的図景：

P -----> T_P
|         |
|         | (層化)
v         v
P^∃ ----> T_{P^∃} ≡ E_P

定理2：∃-超コンパクト化の特性化（定理6.2）

陳述：lex主教義Pに対して、以下は同値である：

Pは∃-超コンパクト化教義である（GPは弱従属積と普遍証明を持つ）
ΨGP : GP^op → InfSlは完全三項体である
P∃ : C^op → InfSlは完全三項体である
EPはトポスである

証明の中核：

(1 ⇒ 2)：系5.8を適用する
(2 ⇒ 3)：P∃ = ΨGP ◦ ICとMenni定理を利用する
(3 ⇒ 4)：定理5.15と系4.12から導く
(4 ⇒ 1)：定理5.7（Menni特性化）から導く

定理3：弱従属積の保存（定理7.2）

陳述：Pが含意的かつ全称的なlex主教義であり、Cが弱従属積を持つならば、GPは弱従属積を持つ。

構成：Cの弱従属積に対して：

X ---e---> E ---h---> Z
|          |          |
f          |          |
v          v          v
J --------g--------> I

GPにおいて以下を構成する：

(X,α) --e--> (E, Pg*h(β) ∧ Ph*g(σ)) --h--> (Z,σ)
  |                                           |
  f                                           |
  v                                           v
(J,β) -----------------g-----------------> (I,γ)

ここでσ := ∀hg(Pgh(β) → Pe(α)) ∧ Ph(γ)

定理4：抽象層化（系8.2）

陳述：Pが∃-超コンパクト化三項体ならば、TP∃上のLawvere-Tierney位相jが存在して以下が成立する： $T_P ≡ \text{Sh}_j(T_{P^∃})$

証明：

定理4.2からP ↪→ P∃の幾何学的埋め込みを得る
定理2.36からTP ↪→ TP∃の幾何学的埋め込みを得る
幾何学的埋め込みはLawvere-Tierney位相に対応する

技術的革新点

概念レベルの革新：
- ロケールの超コンパクト化を完全存在完備化として識別する
- 任意和（三項体では必ずしも利用可能でない）を存在量化で置き換える
- 教義完備化とトポス完備化の対応を確立する
証明技法：
- ΨGPとP∃の関係を巧妙に利用する（補題5.9）
- Menni特性化定理を通じて圏的性質と教義的性質を結びつける
- 正則完備化と正合完備化の分解を使用する
統一的枠組み：
- 任意和積に依存しない（Grothendieckトポス方法の中核）
- 有限極限、存在量化、含意に純粋に基づく
- Set基盤でない三項体に適用可能

実験/応用検証

本論文は純粋理論数学論文であり、従来的意味での実験を含まない。しかし、理論の適用可能性を検証するために多くの具体的例を提供している：

中核的例

1. ローカルトポス（例5.20）

設定：ロケールLのローカル教義L(-) : Set^op → InfSl

検証：

Lが超コンパクトのとき、L(-)は下半格S(-)の完全存在完備化である
等価性TL(-) ≡ Sh(L) ≡ (GS(-))ex/lexが成立する
古典的比較補題PSh(L) ≡ Sh(D(L))に合致する

2. 実現可能性トポス（例5.19, 8.7）

設定：部分組合代数（pca）Aの実現可能性教義P : Set^op → InfSl

検証：

PはA(-)の完全存在完備化である（定理4.5）
等価性TP ≡ (GA(-))ex/lex ≡ (PAsm(A))ex/lex ≡ RT(A)が成立する
ここでPAsm(A)は分割装備（partitioned assemblies）の圏
RT(A)はShj(EP)として表現可能である。ここでEPは「抽象前層トポス」

3. その他の重要な例

修正実現可能性トポス（Modified Realizability）：

HylandとOngによって導入された
∃-超コンパクト化三項体である
抽象層化として表現可能

拡張Weihrauch度トポス（例6.10, 8.9）：

分割装備圏に基づく（Set基盤でない）
Maschio と Trotta により最近導入された
∃-超コンパクト化であることを証明する
理論がSet基盤情形を超えた能力を示す

Dialectica トポス、Krivine トポス（例7.9）：

これらの古典的実現可能性トポスはすべて∃-超コンパクト化である
本論文の枠組みに統一的に組み込まれる

理論検証の完全性

Set基盤情形（系7.8）：
- すべてのSet基盤三項体が∃-超コンパクト化であることを証明する
- メタ理論における選択公理に依存する
- すべての古典的実現可能性トポスをカバーする
非Set基盤情形（例6.10）：
- 拡張Weihrauch度トポスが重要な反例を提供する
- 理論の広範な適用可能性を示す
反例（例7.12）：
- 基本トポス上の部分対象教義で普遍証明がない場合
- 非∃-超コンパクト化三項体の例を提供する
- 特性化定理の必要性を検証する

結論と議論

主要な結論

統一的幾何学的枠組み：
- ローカルトポスと実現可能性トポスは同じ幾何学的構造を共有する
- 両者ともTP ≡ Shj(EP)の形式で表現可能
- EPは「抽象前層トポス」の役割を果たす
主要な等価性： $T_{P^∃} ≡ E_P = (G_P)_{ex/lex}$ これはローカル比較補題の完全な抽象化である
特性化定理：三項体Pが∃-超コンパクト化である ⟺ Cが弱従属積と普遍証明を持つ
広範な適用可能性：
- すべてのSet基盤三項体（すべての古典的実現可能性トポスを含む）
- 拡張Weihrauch度トポスなどの非Set基盤例
- 閉包性質：∃-超コンパクト化三項体はスライスの下で閉じている

理論的意義

概念の明確化：
- 三項体レベルにおける「超コンパクト化」の意味を明確にする
- 存在量化と任意和の深層的関連を明らかにする
構造的洞察：
- 三項体構成を2つのステップに分解可能：
  - P → P∃（存在量化の追加）
  - P∃ → TP∃（三項体構成）
- Pが∃-超コンパクト化のとき、TPはTP∃の「層化」
圏論的論理の統一：
- 異なるトポス類を理解するための統一言語を提供する
- 論理（教義）と幾何学（トポス）を結びつける

限界

メタ理論への依存：
- Set基盤情形の証明はメタ理論における選択公理に依存する
- 構成的メタ理論への代替案は十分に探索されていない
非∃-超コンパクト化情形：
- 理論は主に∃-超コンパクト化三項体に焦点を当てている
- 一般的三項体に対して、EPはトポスでない可能性がある
- この情形の幾何学的意義についてさらなる研究が必要
計算的内容：
- 理論は高度に抽象的
- 具体的計算とアルゴリズム的側面の応用はいまだ十分に探索されていない
Grothendieckトポスとの関係：
- Grothendieckトポスにおける超コンパクト生成性
- 本論文の∃-超コンパクト化概念との正確な関係はいまだ明確でない

将来の方向

論文で明示的に提示されている研究方向：

線維化への拡張（Fibrations）：
- 枠組みをトポス線維化に推広する
- 予測的ローカルおよび実現可能性トポスを含む（例えば27）
- これは∃-超コンパクト化三項体がスライスの下で閉じていることを証明する動機
構成的メタ理論：
- 予測的または構成的メタ言語で理論を形式化する
- 選択公理への依存を回避する
計算応用：
- 計算可能性理論における理論の応用を探索する
- 特にWeihrauch度および関連構造