import Mathlib.CategoryTheory.FiberedCategory.Grothendieck
import Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
import FormalLab.CategoryTheory.Equivalences
import FormalLab.CategoryTheory.Limits

/-!
# 第72章：スライス圏・添字圏・ファイブレーション——変化する文脈の上で対象を運ぶ

型族 `A : I → Type` では、添字 `i : I` が変わると利用できる型 `A i` も変わります。関数 `f : J → I` を
通じて添字を読み替えれば、新しい型族 `j ↦ A (f j)` が得られます。この操作は単なる関数合成ですが、一般の
圏では「対象 `I` の上にある対象」を射 `f : J ⟶ I` に沿って引き戻す操作になります。

本章は、この一つの操作を三段階で組み立てます。まずスライス圏 `C/I` で「`I` の上にある対象」を定義し、
引戻しによる再添字付けを普遍性から作ります。次に、基底の各対象ごとに圏が変わる添字圏を導入します。最後に、
変化する圏を一つの全圏と射影関手へ束ね、再添字付けをCartesian射の普遍性として回収するファイブレーションへ
進みます。

## `Type` における引戻しを要素から作る

関数 `f : J → I` と `p : E → I` の引戻しは、同じ `I` の要素へ写る対だけを集めた型

$$
J\times_I E=\{(j,e)\in J\times E\mid f(j)=p(e)\}.
$$

です。二つの射影は可換な正方形を作ります。
-/

namespace FormalLab.Bridges.SlicesIndexedCategoriesAndFibrations

universe u

def TypePullback {I J E : Type u} (f : J → I) (p : E → I) : Type u :=
  { pair : J × E // f pair.1 = p pair.2 }

def typePullbackFst {I J E : Type u} {f : J → I} {p : E → I} :
    TypePullback f p → J :=
  fun x => x.1.1

def typePullbackSnd {I J E : Type u} {f : J → I} {p : E → I} :
    TypePullback f p → E :=
  fun x => x.1.2

theorem typePullback_square {I J E : Type u} {f : J → I} {p : E → I} :
    f ∘ typePullbackFst (f := f) (p := p) =
      p ∘ typePullbackSnd (f := f) (p := p) := by
  funext x
  exact x.2

def typePullbackLift {I J E Z : Type u} {f : J → I} {p : E → I}
    (q : Z → J) (r : Z → E) (commutes : f ∘ q = p ∘ r) : Z → TypePullback f p :=
  fun z => ⟨(q z, r z), congrFun commutes z⟩

theorem typePullbackLift_fst {I J E Z : Type u} {f : J → I} {p : E → I}
    (q : Z → J) (r : Z → E) (commutes : f ∘ q = p ∘ r) :
    typePullbackFst ∘ typePullbackLift q r commutes = q := rfl

theorem typePullbackLift_snd {I J E Z : Type u} {f : J → I} {p : E → I}
    (q : Z → J) (r : Z → E) (commutes : f ∘ q = p ∘ r) :
    typePullbackSnd ∘ typePullbackLift q r commutes = r := rfl

theorem typePullbackLift_unique {I J E Z : Type u} {f : J → I} {p : E → I}
    (q : Z → J) (r : Z → E) (commutes : f ∘ q = p ∘ r)
    (candidate : Z → TypePullback f p)
    (candidate_fst : typePullbackFst ∘ candidate = q)
    (candidate_snd : typePullbackSnd ∘ candidate = r) :
    candidate = typePullbackLift q r commutes := by
  funext z
  apply Subtype.ext
  apply Prod.ext
  · exact congrFun candidate_fst z
  · exact congrFun candidate_snd z

/-!
`typePullbackLift` は可換な任意の対 `q : Z→J`, `r : Z→E` を引戻しへ持ち上げます。二つの射影との合成が
元の関数へ戻ることは定義的に成り立ち、候補の一意性は二成分の一致から従います。したがって部分型の証明成分は
付加的な飾りではなく、媒介関数が引戻しへ入るための可換条件を保持しています。

型族 `A : I→Type` の全空間 `Σi,A(i)` を `I` へ射影し、`f : J→I` に沿って上の引戻しを取ると、各 `j` の
上にある要素は `A(f(j))` です。再添字付け `f⁎A=A∘f` は、全空間の引戻しをファイバーごとに読んだものです。

## スライス圏では対象が共通の終域を持つ

圏 `C` と対象 `I` を固定します。スライス圏 `C/I` の対象は射 `p:E⟶I` であり、二対象 `p:E⟶I` と
`q:F⟶I` の間の射は、`h:E⟶F` で `h≫q=p` を満たす可換三角形です。

$$
h:E\longrightarrow F,
\qquad
h;q=p:E\longrightarrow I.
$$

mathlibでは `Over I` が `C/I`、`Over.mk p` が対象、`Over.homMk h` が可換条件を伴う射です。
-/

open _root_.CategoryTheory

universe uC vC

variable {C : Type uC} [Category.{vC} C]
variable {I J E F : C}

def sliceObject (p : E ⟶ I) : Over I := Over.mk p

def sliceMorphism {p : E ⟶ I} {q : F ⟶ I} (h : E ⟶ F) (triangle : h ≫ q = p) :
    Over.mk p ⟶ Over.mk q :=
  Over.homMk h triangle

@[simp]
theorem sliceMorphism_left {p : E ⟶ I} {q : F ⟶ I} (h : E ⟶ F) (triangle : h ≫ q = p) :
    (sliceMorphism h triangle).left = h := rfl

theorem sliceMorphism_triangle {P Q : Over I} (h : P ⟶ Q) :
    h.left ≫ Q.hom = P.hom :=
  Over.w h

/-!
スライス圏の射は、全圏 `C` の射に方程式を一つ添えたものです。恒等射と合成が再び方程式を満たすため、
通常の圏を成します。対象の終域を固定しただけの集合ではなく、終域への構造写像を保存する射まで含む点が重要です。

射 `f:I⟶J` との後合成は、`C/I` の対象 `p:E⟶I` を `f∘p:E⟶J` へ送ります。本書の合成順では
`p≫f` です。これは関手 `Σ_f : C/I → C/J` を与えます。
-/

def dependentSumFunctor (f : I ⟶ J) : Over I ⥤ Over J := Over.map f

@[simp]
theorem dependentSumFunctor_obj_hom (f : I ⟶ J) (P : Over I) :
    ((dependentSumFunctor f).obj P).hom = P.hom ≫ f := rfl

example : dependentSumFunctor (𝟙 I) ≅ 𝟭 (Over I) :=
  Over.mapId I

/-!
記号 `Σ_f` は、`Type` ではファイバーを `f` に沿ってまとめる依存和に対応します。ただし一般圏の
`Over.map f` は後合成だけで定義でき、引戻しの存在を仮定しません。

## 引戻し関手は再添字付けを与える

反対向きの `f⁎ : C/J → C/I` を作るには引戻しが必要です。`q:F⟶J` を `f:I⟶J` に沿って引き戻し、
射影 `I×_J F⟶I` を新しいスライス対象とします。引戻しを整合的に選ぶと、この操作は対象だけでなく射にも作用する
関手になります。

mathlibの `ChosenPullbacksAlong f` は、この選択を `Over.map f` の右随伴として保持します。右随伴そのものが
再添字付け関手であり、随伴 `Σ_f ⊣ f⁎` が引戻しの普遍性をまとめます。
-/

variable {X Y : C} (f : X ⟶ Y)

def reindexingFunctor [ChosenPullbacksAlong f] : Over Y ⥤ Over X :=
  ChosenPullbacksAlong.pullback f

example [ChosenPullbacksAlong f] :
    Over.map f ⊣ reindexingFunctor f :=
  ChosenPullbacksAlong.mapPullbackAdj f

example [ChosenPullbacksAlong f] (Q : Over Y) :
    (reindexingFunctor f).obj Q ⟶ (reindexingFunctor f).obj Q :=
  𝟙 _

/-!
「引戻しが存在する」と「引戻し関手を一つ選んだ」は同じデータではありません。存在だけから古典的選択で関手を
得ることはできますが、定義的な計算則や合成との整合性は選択に依存します。`ChosenPullbacksAlong.pullbackId` と
`ChosenPullbacksAlong.pullbackComp` は、恒等射に沿う再添字付けが恒等関手と、合成に沿う再添字付けが関手合成と
それぞれ自然同型になることを表します。一般には等号ではなく自然同型であるため、添字圏は擬関手として現れます。

## 一つの射影関手からファイバーを切り出す

関手 `p:E⥤B` を考えます。基底対象 `b:B` 上のファイバー `E_b` は、`p(X)=b` である対象と、基底では恒等射
`𝟙 b` へ写る射からなる圏です。ここで「ファイバー」は集合論的な逆像ではなく、それ自身が射を持つ圏です。

mathlibの `p.Fiber b` は対象を等式つきの部分型として保持し、射を `IsHomLift p (𝟙 b)` を満たす全圏の射として
定義します。`fiberInclusion` は証明成分を忘れて全圏 `E` へ戻す忠実関手です。
-/

universe uB vB uE vE

variable {B : Type uB} {Total : Type uE}
variable [Category.{vB} B] [Category.{vE} Total]
variable (p : Total ⥤ B) (b : B)

abbrev fiberCategory := p.Fiber b

def includeFiber : fiberCategory p b ⥤ Total := Functor.Fiber.fiberInclusion

theorem fiber_object_lies_over (A : fiberCategory p b) : p.obj A.1 = b := A.2

example : (Functor.Fiber.fiberInclusion : p.Fiber b ⥤ Total).Faithful := inferInstance

/-!
全圏の射が別の基底射へ写るなら、それは同じファイバー内の射ではありません。基底方向の移動とファイバー内部の
変換を分けることが、この構成の役割です。

## Cartesian射は最も普遍的な持ち上げである

基底射 `f:R⟶S` と、`S` 上の対象 `a` を取ります。全圏の射 `φ:b⟶a` が `f` の上にあるとは
`p(φ)=f` であることです。そのような `φ` がCartesianであるとは、`f` の上にある任意の別の射
`φ′:b′⟶a` が、`R` 上の垂直射 `χ:b′⟶b` を通じて一意に `φ′=χ≫φ` と分解することです。

$$
\varphi'=\chi;\varphi,
\qquad
p(\chi)=\mathrm{id}_R,
\qquad
p(\varphi)=f.
$$

これは逆像の要素を選ぶ条件ではなく、可換図式に対する存在一意性です。
-/

open Functor
open IsHomLift

variable {R S : B} {a a' liftA : Total}
variable {baseMap : R ⟶ S} {cartesianMap : liftA ⟶ a} {otherMap : a' ⟶ a}

noncomputable def verticalComparison
    [p.IsCartesian baseMap cartesianMap] [IsHomLift p baseMap otherMap] :
    a' ⟶ liftA :=
  Functor.IsCartesian.map p baseMap cartesianMap otherMap

theorem verticalComparison_fac
    [p.IsCartesian baseMap cartesianMap] [IsHomLift p baseMap otherMap] :
    verticalComparison p (baseMap := baseMap) (cartesianMap := cartesianMap)
        (otherMap := otherMap) ≫ cartesianMap = otherMap :=
  Functor.IsCartesian.fac p baseMap cartesianMap otherMap

/-!
`verticalComparison` の基底像は `𝟙 R` です。したがって比較射は基底をさらに動かさず、二つの持ち上げの差だけを
ファイバー内で測ります。同じ `f` と終域に対するCartesian持ち上げの始域は、垂直な同型を除いて一意です。

## ファイブレーションは全ての再添字付けを持つ

`p:E⥤B` が前ファイバー圏であるとは、任意の `f:R⟶p(a)` にCartesian持ち上げが存在することです。mathlibの
`IsPreFibered` はこの存在を表し、`pullbackObj` と `pullbackMap` は古典的選択による一つの持ち上げです。
`IsFibered` はさらにCartesian射の合成がCartesianであることを要求します。強Cartesian射による標準的な定義とは
同値ですが、現行APIは二段階を区別して保持します。
-/

variable [p.IsPreFibered]

noncomputable def chosenReindexedObject {a : Total} {R S : B}
    (ha : p.obj a = S) (f : R ⟶ S) : Total :=
  Functor.IsPreFibered.pullbackObj ha f

noncomputable def chosenCartesianMap {a : Total} {R S : B}
    (ha : p.obj a = S) (f : R ⟶ S) : chosenReindexedObject p ha f ⟶ a :=
  Functor.IsPreFibered.pullbackMap ha f

theorem chosenReindexedObject_lies_over {a : Total} {R S : B}
    (ha : p.obj a = S) (f : R ⟶ S) :
    p.obj (chosenReindexedObject p ha f) = R :=
  Functor.IsPreFibered.pullbackObj_proj ha f

/-!
ここで得た対象を `f⁎a` と書きたくなりますが、選択した持ち上げを射に作用させ、恒等・合成に関する整合性を
与えて初めて添字圏になります。ファイブレーションが与えるのは本質的に擬関手 `Bᵒᵖ→Cat` です。恒等と合成は
Cartesian持ち上げの一意性から得る自然同型を介して保たれます。これらの選択を切断（cleavage）と呼びます。

## Grothendieck構成は変化する圏を一つへ束ねる

反変擬関手 `F:Bᵒᵖ→Cat` が各 `b` に圏 `F(b)`、各 `f:R⟶S` に再添字付け
`f⁎:F(S)→F(R)` を割り当てるとします。Grothendieck構成 `∫F` の対象は依存対 `(b,x)`、射は基底射と
ファイバー射を組にしたものです。射影 `∫F→B` は基底成分を取り出します。

mathlibは反変擬関手に `Pseudofunctor.CoGrothendieck` を用い、その射影 `forget F` がファイバー圏をなすことを
型クラスとして証明しています。
-/

open Opposite Bicategory

variable {Base : Type uB} [Category.{vB} Base]

example (Indexed : LocallyDiscrete Baseᵒᵖ ⥤ᵖ Cat) :
    (Pseudofunctor.CoGrothendieck.forget Indexed).IsFibered :=
  inferInstance

/-!
擬関手からファイブレーションへはGrothendieck構成で進みます。逆向きには、cleavageを持つファイブレーションから
再添字付け擬関手を作ります。この二操作は適切な2圏的意味で対応します。ただし「同じデータ」と呼ぶ前に、
対応の水準を指定する必要があります。
厳密な等号、圏同値、双圏同値は異なる主張です。本章のLeanコードは擬関手からファイブレーションを得る向きを
検査しており、その全2圏同値を証明したとは主張しません。

## 依存型の文脈へ向けた読み替え

依存型理論では、文脈を基底対象、文脈上の型をファイバーの対象、型の項をファイバー内の適切な切断として読みます。
代入 `σ:Δ→Γ` に沿う型の代入 `A[σ]` は再添字付け `σ⁎A` です。代入の恒等則と合成則は、再添字付けの
擬関手的な恒等・合成整合性に対応します。

この対応だけでは依存関数型、依存対型、同一性型をまだ解釈できません。各構成子には再添字付けと両立する随伴や
引戻し安定性が追加で必要です。次章の局所デカルト閉圏は、各スライス圏の指数対象を通して依存積を準備します。

## 双対概念と混同しやすい境界

Cartesian持ち上げは基底射に沿って対象を反変に引き戻すため、ファイブレーションは反変な添字付けに対応します。
射を共変に押し進める普遍的なcocartesian持ち上げを持つものはopfibrationです。一つの射影が両方の構造を持つ
場合もありますが、一方から他方が自動的に従うわけではありません。

また、スライス圏 `C/I` は一つの基底 `I` を固定した圏であり、ファイブレーション `p:E→B` のファイバー
`E_I` は射影から切り出した圏です。余域関手が作る標準的なファイブレーションでは両者が対応しますが、一般の
ファイブレーションのファイバーを常にスライス圏と同一視してはいけません。

## 要点

* スライス圏 `C/I` の対象は `I` への射、射はその構造射と可換な三角形である。
* `f:I→J` との後合成は `Σ_f:C/I→C/J`、引戻しは再添字付け `f⁎:C/J→C/I` を与える。
* 選ばれた引戻しでは `Σ_f⊣f⁎` が成り立ち、恒等・合成との両立は一般に自然同型で表される。
* 関手 `p:E→B` のファイバーは、基底の一対象へ写る対象と恒等射の上にある射からなる圏である。
* Cartesian射は基底射の上にある射を垂直射を通じて一意に分解する普遍的な持ち上げである。
* ファイブレーションと反変添字圏はGrothendieck構成を介して対応するが、対応の厳密な水準を指定する必要がある。

## 研究史と文献案内

ファイバー圏と降下の体系的な定式化は、GrothendieckによるSGA 1第VI exposé [SGA1] に遡ります。同文献の
幾何学的目的と現代の型理論的使用を同一視せず、Cartesian射とファイバー圏の原定式化を確認する一次資料として
読みます。Bénabou [BEN85] はファイバー圏を圏論の基礎づけと結び、擬関手的な視点を含む理論の展開を読むための
一次論文です。

型理論・圏論的論理との対応には Jacobs [JAC99] が、ファイブレーションを統一概念として体系を構成する標準研究書
です。本章の `IsCartesian`, `IsPreFibered`, `IsFibered` は [MATHLIB] の現行実装に従います。特に前ファイバー性と
合成閉性を別の型クラスにした設計は現行API上の区別であり、全ての文献が同じ定義配置を採用するわけではありません。

## 問題

### `Type` の引戻しの普遍性を同値としてまとめる

`TypePullback f p` からの関数と、`f∘q=p∘r` を満たす関数対 `(q,r)` の間の同値を構成してください。
`typePullbackLift` を一方向、二射影を逆方向とし、`typePullbackLift_unique` で一方の逆法則を証明します。
もう一方は関数外延性と部分型の外延性で示します。可換条件をデータとして持つ場合と命題として外に置く場合で、
同値の型がどう変わるかも記述できれば完了です。

### スライス圏の射を手で合成する

`p:E⟶I`, `q:F⟶I`, `r:G⟶I` と可換三角形 `h:E⟶F`, `k:F⟶G` を取り、
`sliceMorphism h` と `sliceMorphism k` の合成を作ってください。その `left` が `h≫k` であることと、終域 `I` への
三角形が可換であることをLeanで示します。次に三角形の仮定を一つ削り、`Over.homMk` を構成できない具体例を
`Type` で与えます。対象、射、保存すべき構造をそれぞれ特定できれば完了です。

### 二回の再添字付けを一回の再添字付けと比較する

`f:I⟶J`, `g:J⟶K` に沿う選ばれた引戻しについて、`(g≫f)⁎` ではなく合成順を正しく追い、
`ChosenPullbacksAlong.pullbackComp` が与える自然同型の両辺を書き下してください。`Type` の明示的な引戻しでは
対応する全単射を構成し、なぜ一般圏では定義的等号を要求しないのかを説明します。恒等射の場合も
`pullbackId` と比較し、擬関手の二つの単位・合成制約を復元できれば完了です。

### Cartesian持ち上げの一意性を図式で証明する

同じ基底射 `f:R⟶S` と同じ終域 `a` に対する二つのCartesian射 `φ:b⟶a`, `ψ:c⟶a` を仮定します。
各普遍性から垂直比較射 `b⟶c`, `c⟶b` を作り、その合成が恒等射になることを一意性で証明してください。
得られるのは全圏での任意の同型ではなく、基底の恒等射上にある垂直同型です。mathlibの
`Functor.IsCartesian.domainUniqueUpToIso` と照合し、どの仮定が各逆法則に使われたかを示せれば完了です。

### Grothendieck構成の射を依存対として読む

反変擬関手 `F:Bᵒᵖ→Cat` に対する `∫F` の対象と射を、基底成分とファイバー成分へ分解して書いてください。
恒等射と合成で擬関手の単位・合成同型が必要になる箇所を追跡します。その後、射影がCartesian持ち上げを持つことを
単位ファイバー射から説明し、`Pseudofunctor.CoGrothendieck.cartesianLift` と比較してください。厳密関手だけを
使った場合に消える輸送と、擬関手の場合に残る整合条件を区別できれば完了です。
-/

end FormalLab.Bridges.SlicesIndexedCategoriesAndFibrations