import Mathlib.CategoryTheory.Sites.Sheafification
import FormalLab.CategoryTheory.Presheaves
import FormalLab.CategoryTheory.Sites

/-!
# 第60章：層条件・貼り合わせ・層化

局所的に定義した関数、解、切断を大きい領域へまとめたいとします。局所データが重なりで一致していても、
大域データが存在するとは限りません。存在しても、局所的には区別できない二つの大域データが残るかもしれません。
層条件は、この二つの障害をそれぞれ貼り合わせの存在と一意性によって排除します。

本章では、被覆篩上の整合族、貼り合わせ、分離前層、層を順に定義します。続いて層を前層圏の充満部分圏として
まとめ、任意の前層を最も普遍的な方法で層へ送る層化を随伴として記述します。Leanの定義が層条件を `Prop` に
置くため、存在証明と計算可能な貼り合わせアルゴリズムが同じでないことも明確にします。

## 被覆篩上の局所要素

集合値前層 `P:Cᵒᵖ→Type`、対象 `X`、`X` 上の篩 `S` を固定します。`S` 上の要素族とは、各
`f:Y→X` と証明 `f∈S` に対して要素

$$
x_f\in P(Y).
$$

を選ぶことです。添字は単なる対象 `Y` ではなく、`X` への射 `f` です。同じ `Y` から異なる二射があれば、
それぞれに別の局所要素を持ち得ます。
-/

namespace FormalLab.CategoryFoundations.Sheaves

open _root_.CategoryTheory

noncomputable section

universe w v u

variable {C : Type u} [Category.{v} C]
variable {X Y Z : C}
variable (P : Cᵒᵖ ⥤ Type w)
variable (S : Sieve X)

example : Type (max u v w) := Presieve.FamilyOfElements P S.arrows

/-!
数学的には要素族を従属積

$$
x:\prod_{\substack{f:Y\to X\\f\in S}}P(Y).
$$

と書けます。Leanの `FamilyOfElements` も同じ依存関数です。所属証明は `Prop` にあり証明無関連なので、
同じ射について所属証明の選び方だけで異なる局所要素を作ることはできません。

## 整合性は共通の細分上での一致である

二射 `f₁:Y₁→X`, `f₂:Y₂→X` に局所要素 `x_f₁`, `x_f₂` があるとします。射 `g₁:Z→Y₁`,
`g₂:Z→Y₂` が `g₁;f₁=g₂;f₂` を満たすなら、二つの局所要素を `Z` へ制限した結果が等しいことを
要求します。

$$
P(g_1)(x_{f_1})=P(g_2)(x_{f_2})
\qquad\text{whenever }g_1;f_1=g_2;f_2.
$$

この条件を整合性と呼びます。圏がpullbackを持つ場合は二射のpullback上での一致だけを調べる形へ
言い換えられますが、一般の定義はpullbackの存在を必要としません。
-/

variable {P S}
variable (x : Presieve.FamilyOfElements P S.arrows)

example : Prop := x.Compatible

example (hx : x.Compatible) {Y₁ Y₂ Z : C} (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂)
    {f₁ : Y₁ ⟶ X} {f₂ : Y₂ ⟶ X} (h₁ : S f₁) (h₂ : S f₂)
    (hcomm : g₁ ≫ f₁ = g₂ ≫ f₂) :
    P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂) :=
  hx g₁ g₂ h₁ h₂ hcomm

/-!
同じ対象上に局所要素が二つあるだけでは整合性を問えません。どの射に沿って同じ場所を見ているかを
合成等式で指定する必要があります。篩が射を添字に持つ利点がここに現れます。

## 貼り合わせは全ての局所要素を生む大域要素である

要素 `t∈P(X)` が族 `x` の貼り合わせであるとは、全ての `f:Y→X` in `S` について

$$
P(f)(t)=x_f
\qquad(f:Y\to X,\ f\in S).
$$

となることです。英語の *amalgamation* に対応してmathlibは `IsAmalgamation` と呼びます。
-/

example (t : P.obj (Opposite.op X)) : Prop := x.IsAmalgamation t

example (t : P.obj (Opposite.op X)) (ht : x.IsAmalgamation t)
    (f : Y ⟶ X) (hf : S f) : P.map f.op t = x f hf :=
  ht f hf

/-!
貼り合わせが存在すれば、その制限から作った族は自動的に整合します。これは前層の合成保存則と
`g₁;f₁=g₂;f₂` から従います。逆は一般には成り立たず、整合族に貼り合わせが存在するという追加条件が必要です。
-/

example (t : P.obj (Opposite.op X)) (ht : x.IsAmalgamation t) : x.Compatible :=
  Presieve.is_compatible_of_exists_amalgamation x ⟨t, ht⟩

/-!
## 分離性と層条件

前層 `P` が篩 `S` に関して分離的であるとは、各要素族の貼り合わせが高々一つであることです。`P` が
`S` に関する層であるとは、各整合族がちょうど一つの貼り合わせを持つことです。

$$
\begin{aligned}
\mathsf{IsSeparatedFor}(P,S)
  &:\quad\text{貼り合わせは高々一つ},\\
\mathsf{IsSheafFor}(P,S)
  &:\quad\text{各整合族に貼り合わせがちょうど一つ}.
\end{aligned}
$$

存在だけでは層になりません。一意性だけを持つ分離前層も、貼り合わせが欠ける可能性があります。
-/

example : Prop := Presieve.IsSeparatedFor P S.arrows
example : Prop := Presieve.IsSheafFor P S.arrows

example (h : Presieve.IsSheafFor P S.arrows) : Presieve.IsSeparatedFor P S.arrows :=
  h.isSeparatedFor

example (h : Presieve.IsSheafFor P S.arrows) (hx : x.Compatible) :
    ∃! t : P.obj (Opposite.op X), x.IsAmalgamation t :=
  h x hx

/-!
最大篩については全ての前層が層条件を満たします。整合族の `id_X` における要素が貼り合わせになり、
恒等射で制限すれば一意性も得られるからです。
-/

example : Presieve.IsSheafFor P (⊤ : Presieve X) :=
  Presieve.isSheafFor_top P

/-!
## サイト上の層

Grothendieck位相 `J` に関する層とは、`J` が被覆と指定する全ての篩について層条件を満たす前層です。

$$
\forall X\in\mathcal C\;\forall S\in J(X),
\quad\mathsf{IsSheafFor}(P,S).
$$

被覆でない篩について貼り合わせを要求しません。したがって位相を細かくして被覆篩を増やすほど、層となる
ための条件は強くなります。
-/

variable (J : GrothendieckTopology C)

example : Prop := Presieve.IsSheaf J P

example (hP : Presieve.IsSheaf J P) (hS : S ∈ J X) : Presieve.IsSheafFor P S.arrows :=
  hP S hS

example (hP : Presieve.IsSheaf J P) : Presieve.IsSeparated J P :=
  hP.isSeparated

/-!
最粗位相 `⊥` では最大篩だけが被覆なので、全ての前層が層です。最細位相 `⊤` では空篩さえ被覆になり、
層条件は非常に強くなります。位相の順序と層の包含は反変です。
-/

example : Presieve.IsSheaf (⊥ : GrothendieckTopology C) P :=
  Presieve.isSheaf_bot

example {J₁ J₂ : GrothendieckTopology C} (hJ : J₁ ≤ J₂)
    (hP : Presieve.IsSheaf J₂ P) : Presieve.IsSheaf J₁ P :=
  Presieve.isSheaf_of_le P hJ hP

/-!
## 層は前層圏の充満部分圏をなす

`A` 値層の圏 `Sheaf J A` の対象は、`A` 値前層と層条件の証明の組です。射には新しい局所条件を課さず、
基礎にある前層間の自然変換をそのまま使います。したがって層の圏は前層圏の充満部分圏です。
-/

example : Type _ := Sheaf J (Type w)

def asTrivialSheaf (P : Cᵒᵖ ⥤ Type w) : Sheaf (⊥ : GrothendieckTopology C) (Type w) :=
  ⟨P, _root_.CategoryTheory.Presheaf.isSheaf_bot P⟩

example : (sheafToPresheaf J (Type w)).FullyFaithful :=
  fullyFaithfulSheafToPresheaf J (Type w)

/-!
完全忠実性は、層間の射が前層間の自然変換と同じ情報を持つことを述べます。層条件は対象の性質であり、
射に追加データを持たせる構造ではありません。

## 層化は層への普遍射である

層化は前層 `P` を層 `aP` へ送り、自然変換 `η_P:P→i(aP)` を与える構成です。ここで `i` は層から
前層への包含です。普遍性は、任意の層 `Q` に対する自然な全単射

$$
\operatorname{Hom}_{\mathsf{Sh}(\mathcal C,J)}(aP,Q)
\simeq
\operatorname{Hom}_{\widehat{\mathcal C}}(P,iQ).
$$

で表されます。つまり `P` から層へ向かう射は `η_P` を通って一意に因子化します。層化を、局所要素を
場当たり的に追加する一つのアルゴリズムではなく、包含関手の左随伴として特徴づけます。
-/

example : (Cᵒᵖ ⥤ Type w) ⥤ Sheaf (⊥ : GrothendieckTopology C) (Type w) :=
  presheafToSheaf (⊥ : GrothendieckTopology C) (Type w)

example :
    presheafToSheaf (⊥ : GrothendieckTopology C) (Type w) ⊣
      sheafToPresheaf (⊥ : GrothendieckTopology C) (Type w) :=
  sheafificationAdjunction (⊥ : GrothendieckTopology C) (Type w)

example (Q : Sheaf (⊥ : GrothendieckTopology C) (Type w)) :
    (((presheafToSheaf (⊥ : GrothendieckTopology C) (Type w)).obj P ⟶ Q) ≃
      (P ⟶ Q.obj)) :=
  (sheafificationAdjunction (⊥ : GrothendieckTopology C) (Type w)).homEquiv P Q

/-!
上のLeanコードでは最粗位相を使っています。この場合は全前層が既に層なので層化の存在が自動的です。
一般のサイトと値圏について層化が存在するには仮定が必要であり、`HasWeakSheafify J A` は包含関手が
左随伴を持つことを記録します。集合値前層など標準的な場合にはplus構成を二回行う具体的な層化を構成できます。

## `Prop` に置かれた存在と計算内容

mathlibの `IsSheafFor` は `∃! t, ...` という命題です。この表現は貼り合わせの存在と一意性を厳密に述べますが、
貼り合わせを計算するプログラムをデータとして保持しません。`IsSheafFor.amalgamate` は命題的な存在証明から
選択によって元を取り出すため `noncomputable` です。

原理論で貼り合わせの証人全体を `Type` に置けば、証人の計算内容や高次の同一性を区別する余地があります。
ここでの `Prop` とLeanの証明無関連性はその構造を消去します。したがって層条件の証明から実行可能な
貼り合わせ手続きを得たと結論してはいけません。

## 要点

* 篩上の要素族は、各射 `f:Y→X` に局所要素 `x_f∈P(Y)` を割り当てる。
* 整合性は、同じ合成射になる二つの細分上で局所要素の制限が一致することをいう。
* 貼り合わせは全局所要素を制限として持つ大域要素である。
* 分離性は貼り合わせの一意性、層条件は整合族に対する存在一意性である。
* サイト上の層は全被覆篩について層条件を満たし、層の圏は前層圏の充満部分圏である。
* 層化は層の包含の左随伴であり、`Prop` の存在証明だけでは計算可能な貼り合わせ算法を与えない。

## 研究史と文献案内

Lerayが導入した層の着想は、Cartanのセミナーで局所データとコホモロジーを結ぶ理論へ整理されました。
Grothendieck [GRO57] は、アーベル群の層を含むアーベル圏のホモロジー代数を構築しました。サイトと
トポスによる一般化は [SGA4] で体系的に展開されました。篩上の整合族、米田による層条件、層化の説明は
[MM92] を参照してください。これらの段階を単一の「層の発明」へ縮約しません。
Leanの `IsSheafFor`, `Sheaf`, `sheafificationAdjunction` は [MATHLIB] の現行APIに従います。

## 問題

### 整合族と貼り合わせを定義から判定する

被覆篩 `S`、前層 `P`、大域要素 `t∈P(X)` を取り、`x_f=P(f)(t)` と定めてください。二つの合成
`g₁;f₁=g₂;f₂` に沿う制限が一致することを、前層の合成保存則から証明します。さらに `t` が `x` の
貼り合わせであることを示し、Leanの `is_compatible_of_exists_amalgamation` と各定義へ対応させてください。
どの推論が層条件を使わず全前層で成立するかを指摘できれば完了です。

### 分離的だが層でない前層を構成する

第58章の定値前層を、二つの互いに交わらない非空開集合を持つ空間上で考えます。大域定数は局所制限から
一意に決まるため分離性を満たす一方、二領域に異なる値を置く整合族は貼り合わさらないことを示してください。
一意性の証明と存在の反例を別々に書き、`IsSeparatedFor` と `IsSheafFor` の論理的な差へ翻訳します。
局所定値関数の層へ置き換えると何が追加されるか説明できれば完了です。

### 層化の普遍性から一意性を導く

層化射 `η_P:P→i(aP)` と層 `Q` への射 `f:P→iQ` を仮定します。随伴のhom全単射から射
`f̄:aP→Q` を構成し、`η_P;f̄=f` を示してください。同じ等式を満たす別の射が全単射の単射性により
`f̄` と等しいことを証明します。最後に、単に `aP` が層であるだけではこの一意性が得られない理由を述べ、
層化の構成と普遍的特徴づけを区別できれば完了です。
-/

end

end FormalLab.CategoryFoundations.Sheaves