import Mathlib.CategoryTheory.Yoneda
import FormalLab.CategoryTheory.Functors

/-!
# 第58章：前層――局所データを制限する反変関手

開集合 `U` ごとに、`U` 上で定義された関数の集合 `F(U)` を考えます。包含 `V⊆U` があれば、`U` 上の
関数を `V` へ制限できます。包含の向きは `V→U` ですが、制限写像は `F(U)→F(V)` と逆向きです。
さらに、同じ領域への制限は何も変えず、二段階の制限は合成した包含への一回の制限と一致します。

前層は、この「対象ごとのデータ」と「射に沿う逆向きの制限」を一般の圏へ移したものです。本章では
前層を反対圏上の関手として定義し、制限写像の二法則、前層間の射、定値前層、表現可能前層を順に調べます。
貼り合わせの存在や一意性は前層の定義には含まれず、後の層条件が課す追加条件です。

## 制限写像は射と逆向きに進む

圏 `C` と圏 `A` に対し、`A` 値前層とは関手

$$
P:C^{\mathrm{op}}\to A
$$

です。対象 `X` には `P(X)` を対応させます。射 `f:X→Y` は反対圏では `fᵒᵖ:Y→X` となるので、

$$
P(f):P(Y)\to P(X)
$$

が得られます。この射を制限写像と呼びます。向きの反転は比喩ではなく、反対圏を使うことで通常の
共変関手の定義へ組み込まれています。
-/

namespace FormalLab.CategoryFoundations.Presheaves

open _root_.CategoryTheory

universe t w v u

variable {C : Type u} [Category.{v} C]
variable {A : Type w} [Category.{t} A]

abbrev Presheaf (C : Type u) [Category.{v} C] (A : Type w) [Category.{t} A] := Cᵒᵖ ⥤ A

variable (P : Presheaf C A)
variable {X Y Z : C}

example (X : C) : A := P.obj (Opposite.op X)

example (f : X ⟶ Y) : P.obj (Opposite.op Y) ⟶ P.obj (Opposite.op X) := P.map f.op

/-!
同じ対象への制限と、二段階の制限は関手法則によって決まります。数学的には

$$
\rho_{X,X}=\mathrm{id}_{P(X)},
\qquad
\rho_{X,Z}=\rho_{Y,Z}\circ\rho_{X,Y}
\quad(Z\to Y\to X).
$$

と書けます。ここで `ρ_X,Y:P(X)→P(Y)` は包含または一般の射 `Y→X` に沿う制限です。Leanでは射の
合成を図式順に `≫` と書くため、反対圏での合成を展開した式は次の形になります。
-/

example (X : C) : P.map (𝟙 (Opposite.op X)) = 𝟙 (P.obj (Opposite.op X)) := P.map_id _

example (f : X ⟶ Y) (g : Y ⟶ Z) :
    P.map (f ≫ g).op = P.map g.op ≫ P.map f.op := by
  simp

/-!
右辺ではまず `P(g):P(Z)→P(Y)`、次に `P(f):P(Y)→P(X)` を適用します。反変性を「関手が合成を
反転する」とだけ覚えると、反対圏の合成と写像の向きを二重に反転しがちです。始域と終域を書き、
`P(Z)→P(Y)→P(X)` と追う方が確実です。

## 前層間の射は全ての制限と可換する

前層 `P,Q:Cᵒᵖ→A` の間の射は自然変換 `η:P⇒Q` です。各対象で射 `η_X:P(X)→Q(X)` を持ち、
任意の `f:X→Y` に対して次の正方形が可換になります。

$$
Q(f)\circ\eta_Y=\eta_X\circ P(f).
$$

したがって前層間の射は、対象ごとに勝手な写像を選ぶ族ではありません。変換してから制限する操作と、
制限してから変換する操作が一致します。
-/

variable {P Q : Presheaf C A}

example (η : P ⟶ Q) (f : X ⟶ Y) :
    P.map f.op ≫ η.app (Opposite.op X) = η.app (Opposite.op Y) ≫ Q.map f.op :=
  η.naturality f.op

/-!
前層を対象、自然変換を射とする関手圏 `[Cᵒᵖ,A]` では、恒等射と合成は対象ごとの恒等射と合成です。
自然性が合成で保存されるため、前層は単なるデータの集まりではなく一つの圏をなします。

## 定値前層は全ての制限を恒等射にする

対象 `a:A` を全ての `X` へ割り当て、全ての制限写像を `id_a` とする前層を定値前層と呼びます。
開集合上では「どの領域でも同じ値集合を使う」構成です。ただし位相空間上の定値層は一般に、この定値前層を
そのまま層とみなしたものではありません。貼り合わせ条件を満たすため、局所定値関数を使う構成が現れます。
-/

def constantPresheaf (a : A) : Presheaf C A := (Functor.const Cᵒᵖ).obj a

example (a : A) (X : C) : (constantPresheaf (C := C) a).obj (Opposite.op X) = a := rfl

example (a : A) (f : X ⟶ Y) :
    (constantPresheaf (C := C) a).map f.op = 𝟙 a := rfl

/-!
これは前層の正例です。一方、対象ごとに `D(X)` を割り当てただけで制限写像を与えない族は前層では
ありません。制限写像を与えても、二段階の制限が一回の制限と一致しなければ関手の合成保存則が失敗します。

## 表現可能前層は射を制限する

対象 `T:C` を固定すると、`X` を `Hom_C(X,T)` へ送る米田前層 `h_T` が得られます。射 `f:X→Y` に
沿う制限は前合成です。

$$
\mathcal C(Y,T)\longrightarrow\mathcal C(X,T),
\qquad g\longmapsto f;g.
$$

第51章の米田の補題は、任意の集合値前層 `P` に対して `Nat(h_T,P)≃P(T)` を与えます。この定理は
前層の定義には不要です。前層を反変関手として構成した後で、表現可能前層から来る射によって一般の前層を
調べる追加原理として接続します。
-/

example (T : C) : Presheaf C (Type v) := yoneda.obj T

theorem yoneda_restriction (T : C) (f : X ⟶ Y) (g : Y ⟶ T) :
    (yoneda.obj T).map f.op g = f ≫ g := rfl

/-!
## 前層と層を分ける反例

前層法則が保証するのは、データを小さい領域へ一貫して制限できることだけです。互いに重なる領域上の
データが一致するとき、それらを大きい領域上の一つのデータへ貼り合わせられるとは限りません。また、
貼り合わせが存在しても一意とは限りません。この二条件を追加したものが層です。

この区別は定値前層で既に現れます。離れた二領域に異なる定数を置けば、交わり上では自動的に一致しても、
全体上の一つの定数には貼り合わさりません。したがって「全ての制限が恒等射である」という簡単な前層法則から
層条件を推論してはいけません。

## 要点

* `A` 値前層は反対圏からの関手 `Cᵒᵖ→A` である。
* 射 `f:X→Y` は逆向きの制限射 `P(Y)→P(X)` を誘導する。
* 恒等射保存と合成保存は、同じ領域への制限と段階的な制限の法則である。
* 前層間の射は自然変換であり、全ての制限写像と可換する。
* 表現可能前層は `Hom(-,T)` であり、米田の補題が一般の前層の要素と結びつける。
* 貼り合わせの存在と一意性は前層の定義には含まれない。

## 研究史と文献案内

層は位相空間上の局所データを組織する概念としてLerayの仕事に由来し、Cartanのセミナーを通じて
層とコホモロジーの理論が整備されました。Grothendieck [GRO57] はアーベル圏と導来関手の枠組みで
アーベル群の層を扱います。同論文の全内容を、本章の集合値前層という入口だけに縮約しません。
サイト上の前層と層の圏論的な体系は [SGA4]、現代的な標準解説は [MM92] を参照してください。
Leanの反対圏、関手圏、`yoneda` は [MATHLIB] の現行APIに従います。

## 問題

### 制限の合成則を二つの記法で導く

射 `X→Y→Z` と前層 `P` を取り、`P(Z)→P(Y)→P(X)` の各写像の始域と終域を書いてください。
反対圏で `(f≫g)ᵒᵖ=gᵒᵖ≫fᵒᵖ` となることから、関手法則を制限写像の合成則へ翻訳します。
Leanで `P.map_comp g.op f.op` を使って同じ式を証明し、式の順序を逆にした候補が型検査を通らない
理由まで説明できれば完了です。

### 対象ごとの写像を自然変換へ昇格する

二つの集合値前層 `P,Q` と関数族 `η_X:P(X)→Q(X)` を考えます。自然変換にするための可換式を全ての
`f:X→Y` について書き、定値前層間では一つの関数 `a→b` がその条件を満たすことを証明してください。
次に対象ごとに異なる関数を選び、自然性が破れる小さな圏の例を構成します。データと法則の両方を
`NatTrans` のフィールドへ対応させられれば完了です。

### 定値前層が層にならない状況を分析する

二つの互いに交わらない非空開集合からなる空間を考え、二点以上を持つ集合 `A` の定値前層を置きます。
二領域に異なる値を選んだ局所データが交わり上で一致することと、全体上の定数へ貼り合わさらないことを
示してください。どの段階までは前層法則だけで成立し、どの段階で貼り合わせの存在が失敗したかを区別します。
同じ例を局所定値関数の層と比較し、定値前層と定値層を識別できれば完了です。
-/

end FormalLab.CategoryFoundations.Presheaves