import Mathlib.CategoryTheory.Sites.Grothendieck
import FormalLab.CategoryTheory.Categories

/-!
# 第59章：篩・Grothendieck位相・サイト

位相空間では、開集合 `U` を小さい開集合族で被覆し、その上の局所データから `U` 上のデータを調べます。
一般の圏には要素や開集合がないので、単なる対象の族では「どの対象が `U` のどの部分を見ているか」を
記録できません。終点を `U` とする射を集め、さらにその射を任意に前合成しても集まりに残るようにします。
この下方閉じた射の集まりが篩です。

どの篩を被覆と認めるかを各対象で指定し、恒等的な被覆、引戻し、局所的な被覆の合成に関する三法則を
課したものがGrothendieck位相です。圏とGrothendieck位相の組をサイトと呼びます。本章の「篩」は
型システムの篩型とは別概念であり、英語ではそれぞれ *sieve* と *refinement type* です。

## 前篩から篩へ

対象 `X` 上の前篩は、終域が `X` である各射 `f:Y→X` に真偽を割り当てる述語です。

$$
R_Y(f):\mathsf{Prop}
\qquad(f:Y\to X).
$$

前篩は射の合成について何も要求しません。篩 `S` はこれに下方閉性を加えます。

$$
f\in S,\quad g:Z\to Y
\qquad\Longrightarrow\qquad
g;f\in S.
$$

つまりある観測 `f` を被覆の一部として認めたなら、それをさらに細かい対象から観測する射も認めます。
-/

namespace FormalLab.CategoryFoundations.Sites

open _root_.CategoryTheory

universe v u

variable {C : Type u} [Category.{v} C]
variable {X Y Z : C}

example (X : C) : Type (max u v) := Presieve X
example (X : C) : Type (max u v) := Sieve X

example (S : Sieve X) {f : Y ⟶ X} (hf : S f) (g : Z ⟶ Y) : S (g ≫ f) :=
  S.downward_closed hf g

/-!
全ての射を含む最大篩 `⊤` と、射を一つも含まない最小篩 `⊥` はともに篩です。篩の共通部分と合併も
下方閉性を保ち、`Sieve X` は完備束になります。これに対し、射を一つだけ集めた前篩は一般には篩では
ありません。`f:Y→X` を含めるなら、全ての合成 `g;f` も含める必要があるからです。
-/

example (f : Y ⟶ X) : (⊤ : Sieve X) f := Sieve.top_apply f

example (S R : Sieve X) (f : Y ⟶ X) : (S ⊓ R) f ↔ S f ∧ R f := Sieve.inter_apply f

/-!
## 一本の射が生成する主篩

前篩 `R` を含む最小の篩は `generate R` です。一本の射 `f:Y→X` から始めると、`f` を経由する射
`h:Z→X`、すなわちある `g:Z→Y` により `h=g;f` と書ける射を全て集めた主篩が得られます。
-/

def principal (f : Y ⟶ X) : Sieve X := Sieve.generate (Presieve.singleton f)

theorem mem_principal (f : Y ⟶ X) : principal f f := by
  apply Sieve.le_generate (Presieve.singleton f)
  exact Presieve.singleton_self f

theorem comp_mem_principal (f : Y ⟶ X) (g : Z ⟶ Y) : principal f (g ≫ f) :=
  (principal f).downward_closed (mem_principal f) g

/-!
`principal f` は `f` だけを含むのではなく、`f` を通って `X` へ入る全ての射を含みます。前合成で閉じる
という一条件が、生成される射全体を決めています。`generate R` の最小性は
`generate R ≤ S ↔ R ≤ S` で表されます。
-/

example (R : Presieve X) (S : Sieve X) : Sieve.generate R ≤ S ↔ R ≤ S :=
  Sieve.generate_le_iff R S

/-!
## 篩の引戻しは被覆を別の対象へ移す

篩 `S` が `X` 上にあり、射 `f:Y→X` があるとします。`S` の `f` に沿う引戻しは `Y` 上の篩で、
射 `g:Z→Y` が属する条件を `g;f∈S` と定めます。

$$
g\in f^{*}S\quad\Longleftrightarrow\quad g;f\in S.
$$

これは圏に引戻し対象が存在することを要求しません。ここで引き戻しているのは篩という述語であり、
個々の射のpullback対象ではないからです。
-/

example (S : Sieve X) (f : Y ⟶ X) : Sieve Y := S.pullback f

example (S : Sieve X) (f : Y ⟶ X) (g : Z ⟶ Y) :
    S.pullback f g ↔ S (g ≫ f) := Iff.rfl

example (S : Sieve X) : S.pullback (𝟙 X) = S := Sieve.pullback_id

example (S : Sieve X) (f : Y ⟶ X) (g : Z ⟶ Y) :
    S.pullback (g ≫ f) = (S.pullback f).pullback g := Sieve.pullback_comp S

/-!
さらに `f∈S` なら `S.pullback f=⊤` です。`f` より細かい全ての射 `g` が下方閉性によって `g;f∈S`
となるためです。この性質が被覆の局所化を篩だけで記述できる理由になります。
-/

theorem pullback_eq_top_of_mem (S : Sieve X) (f : Y ⟶ X) (hf : S f) :
    S.pullback f = ⊤ :=
  S.pullback_eq_top_of_mem hf

/-!
## Grothendieck位相の三公理

Grothendieck位相 `J` は、各対象 `X` に被覆篩の集合 `J(X)` を割り当て、次を要求します。

1. 最大篩 `⊤` は `X` を被覆する。
2. `S` が `X` を被覆すれば、任意の `f:Y→X` に対して `f*S` は `Y` を被覆する。
3. `S` が `X` を被覆し、`S` の各 `f:Y→X` 上で `f*R` が被覆なら、`R` も `X` を被覆する。

数式では、$J(X)$ を $X$ 上の被覆篩の集まりとして次のように書けます。

$$
\begin{aligned}
&\top\in J(X),\\
&S\in J(X),\ f:Y\to X\ \Longrightarrow\ f^{*}S\in J(Y),\\
&S\in J(X),\ \bigl(\forall f:Y\to X.\ f\in S\to f^{*}R\in J(Y)\bigr)
  \ \Longrightarrow\ R\in J(X).
\end{aligned}
$$

第三公理は被覆の推移律です。`S` で局所化した全ての場所で `R` が被覆になり、`S` 自体も被覆なら、
`R` を全体の被覆として認めます。
-/

variable (J : GrothendieckTopology C)

example (X : C) : (⊤ : Sieve X) ∈ J X := J.top_mem X

example (S : Sieve X) (f : Y ⟶ X) (hS : S ∈ J X) : S.pullback f ∈ J Y :=
  J.pullback_stable f hS

example (S R : Sieve X) (hS : S ∈ J X)
    (hR : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, S f → R.pullback f ∈ J Y) : R ∈ J X :=
  J.transitive hS R hR

/-!
三公理から、被覆篩を含むより大きな篩も被覆であり、二つの被覆篩の共通部分も被覆だと従います。
これらは別の公理ではありません。
-/

example (S R : Sieve X) (hSR : S ≤ R) (hS : S ∈ J X) : R ∈ J X :=
  J.superset_covering hSR hS

example (S R : Sieve X) (hS : S ∈ J X) (hR : R ∈ J X) : S ⊓ R ∈ J X :=
  J.intersection_covering hS hR

/-!
## 最粗位相と最細位相

最粗Grothendieck位相では最大篩だけが被覆です。最細位相では全ての篩が被覆です。mathlibの束順序では
被覆篩が多いほど位相が大きいので、最粗位相は `⊥`、最細位相は `⊤` です。「開集合が多いほど細かい」
という通常の位相の順序と同じ方向に読み替えられますが、ここで比較しているのは対象ごとの被覆篩です。
-/

example : GrothendieckTopology C := GrothendieckTopology.trivial C
example : GrothendieckTopology C := GrothendieckTopology.discrete C

example (S : Sieve X) : S ∈ (⊥ : GrothendieckTopology C) X ↔ S = ⊤ :=
  GrothendieckTopology.bot_covering

example (S : Sieve X) : S ∈ (⊤ : GrothendieckTopology C) X :=
  GrothendieckTopology.top_covering

/-!
## サイトは圏と被覆構造の組である

サイトとは、小圏 `C` とその上のGrothendieck位相 `J` の組です。同じ圏に異なる位相を置けば異なる
サイトになり、同じ前層が一方では層、他方では層でないことがあります。サイトを位相空間そのものと
同一視せず、局所性を指定する圏論的な提示として扱います。

前層 `P:Cᵒᵖ→Type` はサイトの位相を定義に使いません。位相が使われるのは、被覆篩上の整合する局所要素を
大域要素へ一意に貼り合わせる層条件です。この分離により、一つの前層を複数の局所性に対して比較できます。

## 要点

* `X` 上の前篩は終域が `X` の射に対する述語であり、篩はさらに前合成で閉じている。
* 一本の射が生成する主篩は、その射を経由する全ての射を含む。
* 篩の引戻しは `(f*S)(g)⇔S(g;f)` で定義され、pullback対象の存在を要求しない。
* Grothendieck位相は最大性、引戻し安定性、推移性を満たす被覆篩の指定である。
* サイトは圏とGrothendieck位相の組であり、前層に局所性を課す舞台になる。
* 圏論の篩と型システムの篩型は、名称が似ていても異なる概念である。

## 研究史と文献案内

SGA 4 [SGA4] は、開集合による被覆を一般の圏上の射の族へ拡張しました。同書はサイトとトポスを展開した
基準的な一次資料です。現代の篩による飽和したGrothendieck位相の定式化と、
被覆族による前位相との対応は [MM92] を参照してください。Grothendieck [GRO57] は層の圏とホモロジー代数を
発展させた先行文献ですが、サイトの三公理を本章と同じ形で導入した資料としては扱いません。
Leanの `Presieve`, `Sieve`, `GrothendieckTopology` は [MATHLIB] の現行APIに従います。

## 問題

### 主篩の普遍性を証明する

射 `f:Y→X` が生成する主篩を、`h:Z→X` がある `g:Z→Y` によって `h=g;f` と書けるという条件で
記述してください。この集まりが前合成で閉じることを結合律から証明します。さらに `f` を含む任意の篩 `S` が
主篩を含むことを示し、`Sieve.generate_le_iff` の特殊例へ対応させてください。包含の向きを言葉でも
説明できれば完了です。

### 引戻し公理の合成安定性を証明する

篩 `S` と射 `Z→Y→X` に対し、合成に沿う一回の引戻しと二回の引戻しが同じ射を含むことを両方向に
示してください。定義を展開すると双方が `S(h;g;f)` へ帰着することを結合律で確認します。続いて
`S∈J(X)` から二通りに `Z` 上の被覆を得て、Grothendieck位相の安定性がこの等式と両立することを
説明できれば完了です。

### 三公理から上方閉性を導く

被覆篩 `S` と包含 `S≤R` を仮定します。推移性を `S` と `R` へ適用し、各 `f∈S` について
`f*R=⊤` となることを示して `R` の被覆性を導いてください。どこで包含を使い、どこで篩の下方閉性を
使ったかを分離します。最後に二被覆の共通部分が被覆である証明を組み立て、追加公理ではなく導出定理で
あることを確認できれば完了です。
-/

end FormalLab.CategoryFoundations.Sites