import Mathlib.CategoryTheory.Topos.Sheaf
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
import FormalLab.CategoricalConstructions.YonedaLemma
import FormalLab.CategoricalExtensions.Sheaves
import FormalLab.CategoricalTypeTheory.CartesianClosedCategories

/-!
# 第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` が得られます。特性関数は述語自身であり、真となるファイバーを
取れば元の部分型へ戻ります。
-/

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

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

-/

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

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


## 要点

* 部分対象分類子は、各モノ射 `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` の要素表示になることを説明してください。
-/

end

end FormalLab.LogicAndComputation.ToposesAndCategoricalLogic