import Mathlib.CategoryTheory.Topos.Sheaf
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
import FormalLab.CategoryTheory.YonedaLemma
import FormalLab.CategoryTheory.Sheaves
import FormalLab.Bridges.CartesianClosedCategories

/-!
# 第78章：トポスと圏論的論理——部分対象を真理値で分類する

集合 `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` に沿って引き戻した射になります。この `Ω` を部分対象分類子と呼びます。

有限極限、デカルト閉構造、部分対象分類子を持つ圏が初等トポスです。一方、サイト上の集合値層の圏と圏同値な圏を
Grothendieckトポスと呼びます。本章では両概念を区別し、`Type` の述語、一般の分類正方形、前層における篩、層に
おける閉篩を一つの流れで結びます。その後、部分対象がHeyting論理を持つ理由、量化が随伴になる仕組み、内部論理と
外部のメタ理論の差を扱います。

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

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

namespace FormalLab.Bridges.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` に限られます。
-/

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).
$$

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

section Representability

variable [HasPullbacks E]

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

end Representability

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

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

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

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

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

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

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が
あります。この実装上の分解は数学的定義を変更しません。定理が実際に必要とする構造だけを型クラス引数へ出せます。

## 冪対象は部分対象を族として分類する

初等トポスで対象 `A` を固定すると、指数対象

$$
P(A):=\Omega^A.
$$

を冪対象（power object）と呼びます。カリー化と部分対象分類を続けると

$$
\operatorname{Hom}(X,\Omega^A)
\cong\operatorname{Hom}(A\times X,\Omega)
\cong\operatorname{Sub}(A\times X).
$$

を得ます。従って射 `X→P(A)` は、`X` によって添字付けられた `A` の部分対象族を分類します。
-/

section PowerObjects

variable [CartesianMonoidalCategory E] [MonoidalClosed E]

def powerObject (A : E) : E := (ihom A).obj 𝒞.Ω

example {A X : E} :
    (A ⊗ X ⟶ 𝒞.Ω) ≃ (X ⟶ powerObject 𝒞 A) :=
  (ihom.adjunction A).homEquiv X 𝒞.Ω

def membershipCharacteristic (A : E) : A ⊗ powerObject 𝒞 A ⟶ 𝒞.Ω :=
  (ihom.ev A).app 𝒞.Ω

end PowerObjects

/-!
`membershipCharacteristic` の真の引戻しが、内部の所属関係 `∈_A↪A×P(A)` です。集合論の冪集合を要素の集まりとして
先に作るのではなく、全ての部分対象族を自然に分類する対象として特徴づけています。

`P(A)` をLeanの型 `Set A = A→Prop` と同一視できるのは `Type` の具体例です。一般のトポスでは冪対象も圏内の
対象であり、その外部の大域要素だけで全ての内部部分対象族を観測できるとは限りません。

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

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

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

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

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` に関して閉じた篩を
使います。局所的に被覆されて真なら真とみなす閉包条件が、層の貼り合わせと整合します。
-/

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トポスはサイト上の層としての表示を
持つ概念です。

## 部分対象は内部のHeyting論理をなす

対象 `Γ` を文脈と読むと、その部分対象 `P↪Γ` は自由変数 `Γ` を持つ述語です。有限極限により、部分対象の共通部分
が連言、最大部分対象が真になります。部分対象分類子とデカルト閉性を用いると、含意と否定を含むHeyting代数構造が
得られます。

$$
P\land Q=\text{引戻しによる共通部分},
\quad P\Rightarrow Q=\max\{R\mid R\land P\le Q\},
\quad\neg P=P\Rightarrow\bot.
$$

Heyting代数では `P∨¬P=⊤` は一般には成立しません。全ての部分対象について排中律が成り立つトポスをBooleanトポスと
呼びます。Boolean性は初等トポスの公理ではなく追加条件です。外部のLeanで古典論理を使って証明を行っても、対象と
しているトポスの内部論理が自動的にBooleanになるわけではありません。

## 量化は再添字付けの随伴である

射 `f:Δ→Γ` に沿う述語の代入は、部分対象の引戻し

$$
f^*:\operatorname{Sub}(\Gamma)\longrightarrow\operatorname{Sub}(\Delta)
$$

です。適切な像と依存積を使うと、左随伴と右随伴

$$
\exists_f\dashv f^*\dashv\forall_f.
$$

を得ます。射影 `π:Γ×A→Γ` の場合、これらが変数 `a:A` に関する存在量化と全称量化です。第73章の型族における
`Σ_f⊣f⁎⊣Π_f` と同じ随伴形が、ここでは部分対象上の論理演算として現れます。

等式述語は対角射 `A→A×A` が表す部分対象です。項の代入は射の合成、述語の代入は引戻し、量化はその左右の随伴に
なります。圏論的論理では、推論規則を対象と射の普遍性として読み替えます。

## 高階性は冪対象と指数対象から生じる

`P(A)=Ω^A` があるため、述語そのものを変数として量化できます。関数対象 `B^A` も圏内にあるので、高階関数と
高階述語を内部言語で扱えます。このため初等トポスは直観主義高階論理のモデルになります。

ただし「集合論の全公理が自動的に成り立つ」という意味ではありません。自然数対象がなければ内部自然数論を標準的な
形で解釈できず、選択公理や排中律も一般には成立しません。サイズを越えて「全ての対象の対象」を作る操作も
トポス公理にはありません。どの内部理論を解釈するかに応じて追加構造を明示します。

## Kripke–Joyal意味論は局所的な真理を読む

層トポスの内部式を外部から読む方法がKripke–Joyal意味論です。対象 `U` を段階または局所的文脈とし、
`U ⊩ φ` を「`U` 上で `φ` が成り立つ」と読みます。射 `V→U` に沿って真理は制限されます。

連言は同じ段階で両方が成り立つこと、含意は全ての制限段階で前件から後件が従うこととして読まれます。層の
Grothendieck位相では、選言や存在量化が被覆上で局所的に証明されれば全体で強制される場合があります。従って
`U⊩∃x,φ(x)` から、外部で一つの大域要素 `x` を選べるとは限りません。局所証人と大域証人を区別します。

この意味論は内部言語の定義そのものではなく、内部判断をサイト上の外部条件へ翻訳するforcing意味論です。同じ
トポスに異なるサイト表示があり得るので、内部真理を特定のサイトの構文へ同一視しません。

## 幾何学的射は論理の保存範囲を示す

トポス `E,F` の間の幾何学的射 `f:E→F` は、関手の随伴

$$
f^*:\mathcal F\rightleftarrows\mathcal E:f_*.
$$

で、逆像関手 `f⁎` が有限極限を保存するものです。空間の連続写像が層の逆像・直像を誘導する向きに合わせ、
幾何学的射の向きは右随伴 `f₊` の向きで記します。

有限連言、任意選言、存在量化から作る幾何学的論理は、逆像関手によって保存されます。全称量化や含意は一般の
幾何学的射で同じようには保存されません。この保存範囲は、どの公理がモデルの逆像に安定かを判定する基準になります。

トポスの点は `Type` または集合のトポスからそのトポスへの幾何学的射です。空間の点に対応する例がありますが、
全てのトポスが真理を判定するのに十分な点を持つとは限りません。点で全てを検査できるという集合論的直観を
無条件に持ち込みません。

## 現行mathlibが形式化する境界

mathlibの `Subobject.Classifier E` は分類子のデータ、`HasSubobjectClassifier E` はその存在を表します。
`Classifier.representableBy` は部分対象前層の表現可能性を与えます。`Presheaf.classifier C` は篩前層を分類子として
構成し、`Sheaf.classifier J` は `J`-閉篩の層を分類子として構成します。

本章で述べた論理の全体系を、これら数個の宣言だけで形式化したわけではありません。そこにはHeyting代数、
量化随伴、内部言語、Kripke–Joyal意味論、幾何学的射が含まれます。現行APIでは初等トポスの構成要素を
複数の型クラスとして扱います。Leanで
分類正方形が検査されたことと、特定の内部理論の健全性・完全性が全て証明されたことを区別します。

## 要点

* 部分対象分類子は、各モノ射 `m:U→X` を真の引戻しとして回収する一意な特性射 `χ_m:X→Ω` を与える。
* 分類子 `Ω` は部分対象前層 `Sub(-)` の表現対象であり、`Sub(X)≃Hom(X,Ω)` が自然に成り立つ。
* 初等トポスは有限極限、デカルト閉構造、部分対象分類子を持つ圏である。
* 冪対象 `Ω^A` は `A` の部分対象族を分類し、内部の高階述語を表す。
* 前層トポスの真理値は篩、層トポスの真理値はGrothendieck位相に関する閉篩である。
* 初等トポスの内部論理は一般に直観主義的で、排中律、選択公理、自然数対象は追加条件である。
* 述語の代入は引戻し、存在量化と全称量化はその左随伴と右随伴として解釈される。
* Grothendieckトポスは層として表示される初等トポスだが、全ての初等トポスがGrothendieckトポスではない。

## 研究史と文献案内

GrothendieckらのSGA 4 [SGA4] は、サイト上の層の圏を幾何学とコホモロジーの基礎として体系的に展開した一次資料です。
複数巻・複数著者のseminarであり、トポス、サイト、幾何学的射、内部論理の全成果を一人の単著へ帰属させません。

Lawvere [LAW70] は量化を随伴として扱い、層と論理の関係を明示した初等トポス形成期の一次資料です。講演は1970年、
会議録の刊行は1971年なので両年を区別します。Tierney [TIE72] は初等トポスと層意味論を集合論の独立性へ応用した
一次資料です。現在の標準的な定義とLawvere–Tierney位相については [MM92] を参照してください。同書は
Kripke–Joyal意味論、および初等トポスとGrothendieckトポスの比較も扱います。現行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` の要素表示になることを説明してください。

### 冪対象の所属関係から部分対象族を回収する

射 `p:X→Ω^A` を逆カリー化して `A×X→Ω` を作り、`truth` の引戻しとして部分対象 `R↪A×X` を構成してください。
逆に任意の `R↪A×X` の特性射をカリー化して `X→Ω^A` を得ます。二構成が互いに逆であることをβη則と分類子の
一意性へ分解し、`Hom(X,Ω^A)≃Sub(A×X)` の自然性まで示せば完了です。

### 排中律が失敗する局所的な真理値を調べる

位相空間の開集合の層トポスを一つ選び、真理値を開集合として読む具体例を構成してください。開集合 `U` のHeyting否定が
`int(X∖U)` になることを確認し、`U∪int(X∖U)` が全空間にならない例を与えます。外部の集合論では各点が `U` に
入るか否かを判定できても、内部の排中律が従わない理由を局所性と開性から説明できれば完了です。

### 二種類のトポスと保存される論理を比較する

有限集合の圏が有限極限、指数対象、部分対象分類子を持つことを示し、無限余積を持たないためGrothendieckトポスでは
ないことを証明してください。次に一つの前層トポスが任意の小極限・小余極限を対象ごとに持つことを確認します。
最後に幾何学的射の逆像が有限連言・任意選言・存在量化を保存する理由を、有限極限保存と左随伴性へ対応させれば
完了です。
-/

end

end FormalLab.Bridges.ToposesAndCategoricalLogic