正本：FormalLab/LogicAndComputation/ToposesAndCategoricalLogic.lean

第80章：トポスと部分対象分類子——真理値で部分対象を分類する#

集合 A の部分集合は述語 P:A→Prop で表せます。要素 a:A が部分集合に属するかは、真理値 P(a) を調べれば分かります。逆に述語から部分型 {a // P a} を作れます。この対応では、一つの対象 Prop が全ての集合上の部分対象を分類しています。

圏論では、部分集合をモノ射 m:U↪X、真理値の対象を Ω、真を選ぶ射を true:1→Ω へ置き換えます。モノ射ごとに特性射

\chi_m:X\longrightarrow\Omega

が一意に存在し、m は true を χ_m に沿って引き戻した射になります。この Ω を部分対象分類子と呼びます。

有限極限、デカルト閉構造、部分対象分類子を持つ圏が初等トポス（topos）です。一方、サイト上の集合値層の圏と圏同値な圏をGrothendieckトポスと呼びます。本章では両概念を区別します。Type の述語から一般の分類正方形、部分対象関手の表現可能性へ進み、前層の篩と層の閉篩を一つの流れで結びます。分類子がどの部分対象を、どの意味で一意に回収するかを中心問題とします。

`Type` では述語が部分対象を分類する#

型 A 上の述語 P:A→Prop から部分型 Subtype P が得られます。特性関数は述語自身であり、真となるファイバーを取れば元の部分型へ戻ります。

Leankernel-checked counterpartL34–63

namespace FormalLab.LogicAndComputation.ToposesAndCategoricalLogic

universe u v

noncomputable section

abbrev TruthValue := Prop

def truth : Unit → TruthValue := fun _ => True

def characteristic {A : Type u} (P : A → Prop) : A → TruthValue := P

def trueFiber {A : Type u} (χ : A → TruthValue) := {a : A // χ a}

def classifiedSubtypeEquiv {A : Type u} (P : A → Prop) :
    trueFiber (characteristic P) ≃ Subtype P :=
  Equiv.refl _

theorem characteristic_unique {A : Type u} (P : A → Prop) (χ : A → Prop)
    (sameFiber : ∀ a, χ a ↔ P a) : χ = characteristic P := by
  funext a
  exact propext (sameFiber a)

example : characteristic (fun n : Nat => n < 3) 2 := by
  change 2 < 3
  omega

example : ¬characteristic (fun n : Nat => n < 3) 4 := by
  change ¬4 < 3
  omega

Prop は二要素型 Bool ではありません。命題を対象として持ち、その証明はLeanの Prop に属します。 propext は論理的同値な命題を等しい真理値として扱い、証明無関連性は同じ命題の証明を区別しません。これはLeanのメタ理論で Type の例を実装した結果です。一般のトポスの内部真理値をLeanの Prop と同一視はできません。

また一般の部分対象は、最初から部分型の包含という形で与えられるとは限りません。Type の単射 m:U→X は、像の述語 ∃u,m(u)=x が定める部分型と同型になります。部分対象はモノ射そのものではなく、終域を固定したモノ射を同型で同一視した類です。

一般圏では真の引戻しとして部分対象を回収する#

圏 E の部分対象分類子は、対象 Ω₀,Ω、モノ射 truth:Ω₀→Ω、各モノ射 m:U→X に対する特性射 χ_m:X→Ω を持ちます。公理から Ω₀ は終対象になります。通常は最初から Ω₀=1 と書きます。

分類条件は次の正方形が引戻しであることです。

\begin{array}{ccc} U&\longrightarrow&\Omega_0\\ \downarrow m&&\downarrow\mathsf{true}\\ X&\xrightarrow{\chi_m}&\Omega \end{array} \qquad\text{is a pullback.}

さらに、この引戻し正方形を作る X→Ω は χ_m に限られます。

Leankernel-checked counterpartL93–113

open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.MonoidalClosed
open scoped MonoidalCategory

universe uE vE

variable {E : Type uE} [Category.{vE} E]
variable (𝒞 : Subobject.Classifier E)
variable {U X : E} (m : U ⟶ X) [Mono m]

def abstractCharacteristic : X ⟶ 𝒞.Ω := 𝒞.χ m

example : IsPullback m (𝒞.χ₀ U) (abstractCharacteristic 𝒞 m) 𝒞.truth :=
  𝒞.isPullback m

theorem abstract_characteristic_unique (χ' : X ⟶ 𝒞.Ω)
    (square : IsPullback m (𝒞.χ₀ U) χ' 𝒞.truth) :
    χ' = abstractCharacteristic 𝒞 m :=
  𝒞.uniq m square

可換性だけでは分類になりません。正方形が引戻しであるため、χ_m が真になる部分を任意の試験対象から一意に持ち上げられます。また各 m に特性射が一つ存在するだけでも不十分で、同じ部分対象を分類する射の一意性が必要です。

特性射は部分対象の外側で必ず「偽」を返す二値関数だ、と考えるのも一般には正しくありません。Ω は二点だけを持つ必要がなく、段階や局所性を記録する多くの真理値を持ち得ます。分類公理が決めるのは、真のファイバーが指定した部分対象であることです。

部分対象分類子は部分対象関手を表現する#

引戻しを持つ圏では、射 f:Y→X に沿って X の部分対象を Y へ引き戻せます。従って

\operatorname{Sub}(-):\mathcal E^{\mathrm{op}}\longrightarrow\mathsf{Type}

は前層になります。分類子 Ω の公理は、自然な同値

\operatorname{Sub}(X)\cong\operatorname{Hom}_{\mathcal E}(X,\Omega).

を与えます。すなわち部分対象前層は Ω によって表現可能です。

Leankernel-checked counterpartL140–147

section Representability

variable [HasPullbacks E]

example : (Subobject.presheaf E).RepresentableBy 𝒞.Ω :=
  𝒞.representableBy

end Representability

この同値の右から左は、射 φ:X→Ω に沿って truth を引き戻します。左から右は部分対象の代表モノ射へ特性射を割り当てます。二操作が逆になることが、分類正方形の普遍性と特性射の一意性です。部分対象分類子は、真理値を格納する対象という直観に加えて、反変な部分対象関手の表現対象という普遍的特徴づけを持ちます。

初等トポスの三つの成分#

本書では初等トポス（elementary topos）を、次の構造を持つ圏として扱います。

有限極限
デカルト閉構造
部分対象分類子

有限極限は終対象、積、等化子、引戻しを与えます。デカルト閉性は指数対象 B^A と高階関数を与えます。部分対象分類子は述語と部分対象を内部化します。この三成分により有限文脈と高階関数を圏内で解釈できます。さらに、等式、論理結合子、量化も解釈できます。

定義には小完備性、小余完備性、生成対象、自然数対象、選択公理を含めません。これらを備える初等トポスはありますが、初等トポスの公理だけから全ては従いません。文献では「有限極限と冪対象」など同値な公理系も使われるため、定義の形だけで別概念と判断せず、サイズ仮定を含む同値定理を確認します。

Leankernel-checked counterpartL171–182

section ElementaryToposSignature

variable [HasFiniteLimits E]
variable [CartesianMonoidalCategory E] [MonoidalClosed E]
variable [HasSubobjectClassifier E]

example : E := HasSubobjectClassifier.Ω E

example {U X : E} (m : U ⟶ X) [Mono m] : X ⟶ HasSubobjectClassifier.Ω E :=
  HasSubobjectClassifier.χ m

end ElementaryToposSignature

現行mathlibには、これら三条件を一語で束ねる中心的な ElementaryTopos 型クラスを使う代わりに、 HasFiniteLimits, CartesianMonoidalCategory, MonoidalClosed, HasSubobjectClassifier を個別に組み合わせるAPIがあります。この実装上の分解は数学的定義を変更しません。定理が実際に必要とする構造だけを型クラス引数へ出せます。

前層トポスの真理値は篩である#

小圏 C 上の集合値前層圏 Cᵒᵖ→Type を考えます。段階 X:C における分類子の値は、X 上の篩全体です。

\Omega(X)=\{\text{$X$ 上の篩}\}.

射 f:Y→X に沿う制限は、篩を f に沿って引き戻します。真 true_X は全ての射を含む最大篩です。

Leankernel-checked counterpartL203–235

section PresheafClassifier

universe uC vC

variable {C : Type uC} [Category.{vC} C]

example (X : C) :
    (Functor.sieves C).obj (Opposite.op X) = Sieve X := rfl

def presheafTruth :
    (Functor.const Cᵒᵖ).obj PUnit ⟶ Functor.sieves C :=
  Presheaf.truth C

def presheafClassifier :
    Subobject.Classifier (Cᵒᵖ ⥤ Type (max uC vC)) :=
  Presheaf.classifier C

variable {F G : Cᵒᵖ ⥤ Type (max uC vC)}

def presheafCharacteristic (m : F ⟶ G) : G ⟶ Functor.sieves C :=
  Presheaf.χ m

example (m : F ⟶ G) [Mono m] :
    IsPullback m ((Functor.isTerminalConst _ Types.isTerminalPUnit).from F)
      (presheafCharacteristic m) (presheafTruth (C := C)) :=
  Presheaf.isPullback_χ_truth m

example (m : F ⟶ G) (X : Cᵒᵖ) (x : G.obj X) (Y : C) (f : Y ⟶ X.unop) :
    ((presheafCharacteristic m).app X x).arrows f ↔
      ∃ a, G.map f.op x = m.app (Opposite.op Y) a :=
  Iff.rfl

end PresheafClassifier

最後の式が篩の意味を示します。要素 x∈G(X) に対する χ_m(x) は、制限 x|_f が段階 Y で部分前層 F に入るような射 f:Y→X 全体です。一度局所的に入れば、さらに制限しても入るので下方閉です。従って単なる Prop 一つではなく、射に沿う持続性を記録した篩になります。

最大篩は「現在の段階でも全ての将来の制限でも真」であることを表します。空篩以外にも中間的な篩が多数あり得るため、前層トポスの内部論理は一般に二値でも古典的でもありません。

層トポスでは閉篩だけが真理値になる#

サイト (C,J) 上の層では、前層分類子の全篩をそのまま使うのではなく、Grothendieck位相 J に関して閉じた篩を使います。局所的に被覆されて真なら真とみなす閉包条件が、層の貼り合わせと整合します。

Leankernel-checked counterpartL251–267

section SheafClassifier

universe uC vC

variable {C : Type uC} [Category.{vC} C]
variable (J : GrothendieckTopology C)

def sheafTruthValues : Sheaf J (Type (max uC vC)) :=
  Sheaf.Ω J

def sheafClassifier :
    Subobject.Classifier (Sheaf J (Type (max uC vC))) :=
  Sheaf.classifier J

example : (sheafClassifier J).Ω = sheafTruthValues J := rfl

end SheafClassifier

Sheaf.Ω J の段階 X の要素は J-閉篩です。特性篩は、ある被覆上で部分層へ局所的に入るなら閉包によってその射自身も含みます。前章までの「篩」「層条件」「層化」が、ここで内部真理値の構成へ合流します。

サイト上の集合値層の圏はGrothendieckトポスです。mathlibは、適切な本質的小ささの仮定の下で前層圏と層圏に HasSubobjectClassifier インスタンスを与えます。有限極限とデカルト閉性も備わるので、Grothendieckトポスは初等トポスになります。

逆は成り立ちません。たとえば有限集合の圏は初等トポスですが、任意の小余極限を持たないためGrothendieckトポスではありません。初等トポスは有限個の構造による公理的概念、Grothendieckトポスはサイト上の層としての表示を持つ概念です。

要点#

部分対象分類子は、各モノ射 m:U→X を真の引戻しとして回収する一意な特性射 χ_m:X→Ω を与える。
分類子 Ω は部分対象前層 Sub(-) の表現対象であり、Sub(X)≃Hom(X,Ω) が自然に成り立つ。
初等トポスは有限極限、デカルト閉構造、部分対象分類子を持つ圏である。
前層トポスの真理値は篩、層トポスの真理値はGrothendieck位相に関する閉篩である。
Grothendieckトポスは層として表示される初等トポスだが、全ての初等トポスがGrothendieckトポスではない。

研究史と文献案内#

GrothendieckらのSGA 4 [SGA4] は、サイト上の層の圏を幾何学とコホモロジーの基礎として体系的に展開した一次資料です。複数巻・複数著者のseminarであり、トポス、サイト、幾何学的射、内部論理の全成果を一人の単著へ帰属させません。初等トポスと部分対象分類子の標準的な扱いには [MM92]、現行Lean APIには [MATHLIB] を参照してください。

問題#

`Type` の単射から特性述語を構成する#

単射 m:U→X に対して χ_m(x):=∃u,m(u)=x と定義し、Subtype χ_m から U への関数を構成してください。逆向きの関数と二つの逆法則を単射性から証明し、包含 Subtype χ_m→X と m が X 上の部分対象として同型であることを示します。さらに同じ真のファイバーを持つ任意の述語が χ_m と命題外延性で等しいことまで示せば完了です。

分類子と表現可能性の二方向を再構成する#

引戻しを持つ圏と分類子 𝒞 を固定します。射 φ:X→Ω から truth の引戻し部分対象を作る写像と、部分対象から特性射を作る写像を書いてください。𝒞.isPullback と 𝒞.uniq を使って二つの合成が恒等になることを証明し、射 f:Y→X に沿う前合成と部分対象の引戻しについて自然性正方形を完成できれば完了です。

前層の特性篩を要素ごとに計算する#

部分前層のモノ射 m:F→G、段階 X、要素 x∈G(X) を固定し、Presheaf.χ m が割り当てる射の集合を定義から書き下してください。後合成で閉じて篩になることを自然性から証明します。x が F(X) から来ることと特性篩が最大篩であることの同値を示し、これが Presheaf.isPullback_χ_truth の要素表示になることを説明してください。

Leankernel-checked counterpartL318–318

end