import FormalLab.CategoryTheory.InitialAndTerminal

/-!
# 第43章：積の普遍性

直積型 `A × B` を「二成分を格納する組」と見るだけでは、その実装に依存しています。
圏論では、二つの射影を通して `A` と `B` を同時に観察でき、同じ観察を与える任意の対象から
一意な射が入ることによって積を特徴づけます。この定義は要素やメモリ表現を参照しません。

本章では `Type` の圏に限定して、射影、対化、二つの計算則、一意性を順に証明します。さらに
媒介射の存在一意性をhom型の全単射として組み直し、一般の圏で積を定義するときに残る構造と、
関数外延性や対の場合分けに依存する実装上の証明を分離します。

## 二本の観察を一本の媒介射に束ねる

圏 `𝒞` における積は、対象 `P` と射影 `π₁ : P → A`, `π₂ : P → B` であって、各 `X` に
ついて写像

$$
\mathcal C(X,P)\longrightarrow\mathcal C(X,A)\times\mathcal C(X,B),
\qquad
h\longmapsto(\pi_1\circ h,\pi_2\circ h)
$$

が全単射になるものです。型と関数の圏では `P = A × B`、射影は `Prod.fst`, `Prod.snd`
で実現されます。

`A × B` には射影 `Prod.fst : A × B → A` と `Prod.snd : A × B → B` があります。
任意の `f : X → A` と `g : X → B` に対して、両方を同時に実現する
`pair f g : X → A × B` が存在し、射影との合成条件を満たす関数はこれだけです。

ここで `X` は積を外から調べる任意の**試験対象**です。`f` と `g` は共通の始域を持つ
二本の観察で、まとめて**錐**の脚と呼ばれます。普遍性は、この二本のデータが積への一本の
媒介射とちょうど対応すると述べます。

```text
          pair f g
       X ----------> A × B
        \             /  \
       f \           /    \ g
          v         v      v
          A       fst      snd       B
```

図は補助であり、厳密な内容は下の二方程式と一意性です。

$$
\pi_1\circ\langle f,g\rangle=f,
\qquad
\pi_2\circ\langle f,g\rangle=g,
$$

$$
(\pi_1\circ h=f\land\pi_2\circ h=g)
\quad\Longrightarrow\quad
h=\langle f,g\rangle.
$$

普遍性を読む順序を固定します。

1. 任意の試験対象 `X` と射 `f : X → A`, `g : X → B` を受け取る。
2. 標準的な媒介射 `pair f g : X → A × B` を構成する。
3. 二射影との合成が元の `f`, `g` へ戻ると示す。
4. 同じ二方程式を満たす任意の `h` が標準射と等しいと示す。
-/

namespace FormalLab.CategoryTheory.Products

universe u v w z

open FormalLab.Logic.Equality

/-! ## 媒介関数を構成し、二つの計算則を証明する -/

/-- 二つの型の間の全単射を、順写像・逆写像・二つの逆法則として表します。 -/
structure FunctionEquiv (S : Type u) (T : Type v) where
  toFun : S → T
  invFun : T → S
  leftInverse : ∀ s, invFun (toFun s) = s
  rightInverse : ∀ t, toFun (invFun t) = t

/-- 二関数を点ごとの対へまとめる標準写像です。 -/
def pair {X : Type u} {A : Type v} {B : Type w}
    (f : X → A) (g : X → B) : X → A × B :=
  fun x => (f x, g x)

theorem firstProjection {X : Type u} {A : Type v} {B : Type w}
    (f : X → A) (g : X → B) :
    Prod.fst ∘ pair f g = f := by
  funext x
  rfl

theorem secondProjection {X : Type u} {A : Type v} {B : Type w}
    (f : X → A) (g : X → B) :
    Prod.snd ∘ pair f g = g := by
  funext x
  rfl

/-- 積の二成分を交換する写像も、二つの射影を対化して得られます。 -/
def swap {A : Type v} {B : Type w} : A × B → B × A :=
  pair Prod.snd Prod.fst

example {A : Type v} {B : Type w} (a : A) (b : B) : swap (a, b) = (b, a) :=
  rfl

/-! ## 一意性と、普遍性を一つの命題にまとめる -/

theorem pairUnique {X : Type u} {A : Type v} {B : Type w}
    (f : X → A) (g : X → B) (h : X → A × B)
    (hfst : Prod.fst ∘ h = f) (hsnd : Prod.snd ∘ h = g) :
    h = pair f g := by
  funext x
  apply Prod.ext
  · exact congrFun hfst x
  · exact congrFun hsnd x

/-- 積の普遍性を、二つの関数空間の間の同値としてまとめます。 -/
def productHomEquiv {X : Type u} {A : Type v} {B : Type w} :
    FunctionEquiv (X → A × B) ((X → A) × (X → B)) where
  toFun h := (Prod.fst ∘ h, Prod.snd ∘ h)
  invFun maps := pair maps.1 maps.2
  leftInverse h :=
    (pairUnique (Prod.fst ∘ h) (Prod.snd ∘ h) h rfl rfl).symm
  rightInverse maps := by
    apply Prod.ext
    · exact firstProjection maps.1 maps.2
    · exact secondProjection maps.1 maps.2

/-!
`pairUnique` ではまず関数外延性で入力 `x` を固定し、次に積の外延性で二成分を比較します。
第一成分の等式は `hfst`、第二成分の等式は `hsnd` を `x` へ適用して得ます。どちらか一方
だけでは、もう一方の成分が異なる関数を排除できないため一意性は証明できません。
-/

/-- 固定した試験対象 `X` に対し、二射影が積の普遍性を満たすという定義です。 -/
def IsProductAt {P : Type z} {A : Type v} {B : Type w}
    (fst : P → A) (snd : P → B) (X : Type u) : Prop :=
  ∀ (f : X → A) (g : X → B),
    ExistsExactlyOne (fun h : X → P => fst ∘ h = f ∧ snd ∘ h = g)

/-- 通常の直積と二射影は、各試験対象 `X` に対して積の普遍性を満たします。 -/
theorem productIsProductAt (A : Type v) (B : Type w) (X : Type u) :
    IsProductAt (P := A × B) Prod.fst Prod.snd X := by
  intro f g
  exact ⟨pair f g, ⟨firstProjection f g, secondProjection f g⟩,
    fun h laws => pairUnique f g h laws.left laws.right⟩

/-!
## `FunctionEquiv`と外延性が担う役割

`FunctionEquiv S T` は本章で定義した、順写像・逆写像・左右の逆法則を束ねる構造です。
mathlibの同値 `Equiv` と同じ四成分を露出しますが、ここではimport依存を増やさず全単射の
証拠を一行ずつ追うために局所定義を使います。また、これは圏同値を表す構造ではありません。
`funext` は関数値の点ごとの等式から関数等式を作り、`Prod.ext` は二成分の等式から対の
等式を作ります。これらは通常の数学的証明に現れる外延性をLeanの証明項へ移す手段です。

## 普遍性と内部表現

`A × B` の組という内部表現は一つの実現です。普遍性は射影と一意な対化だけを述べるため、
同じ性質を満たす別の実現も一意な同型を通じて同じ役割を果たします。「一意」は対象が
定義的に同一という意味ではなく、与えた射影を保つ媒介射が一意という意味です。

`IsProductAt` は一つの `X` に相対化した定義です。圏論の積はすべての対象 `X` に
同時にこの性質を要求し、射影も圏の射として扱います。また積の普遍性と、型 `A × B` の
具体的なメモリ表現を同一視しません。

## 要点

* 積は対象 `A × B` だけでなく、二射影と組にして普遍性を持つ。
* 共通始域からの二射 `f`, `g` は、一意な媒介射 `pair f g` へまとめられる。
* 計算則は媒介射を射影すると元の射へ戻ること、一意性はその条件が媒介射を決めることを述べる。
* 普遍性を満たす実現は内部表現ではなく、一意な同型を除いて決まる。

## 研究史と文献案内

積を座標対として構成すること自体は圏論以前からあります。圏論的な転換は、内部要素でなく
全ての試験対象からの射と一意な媒介射で積を特徴づける点にあります。本章が用いる普遍性の語彙は、
Eilenberg–Mac Laneによる1945年の圏・関手・自然同値の枠組み [EM45] より後に標準化されました。
したがって、現在の積の定義を同論文へ直接帰属させません。

[LEI14] は普遍性をhom集合の同型、表現可能性、極限へ段階的に一般化します。[MAC98] は
積を一般の極限の一例として位置づけます。[LS86] は、積と関数型がCartesian closed categoryで
論理・型理論へ結びつく過程を扱います。

## 問題

### 錐から媒介射を構成する

`productIsProductAt` を展開し、任意の共通始域 `X` と二射から作る媒介射、二つの可換条件、
一意性を指せ。`pairUnique` で片方の射影条件だけでは不足する例を作り、積の値が両成分により
決定されることを関数外延性で証明する。

さらに成分を交換する `swap` を二回適用すると元に戻ることを示せ。値に対する計算と、関数全体の
等式へ上げる外延性の段階を分けること。

### 普遍性をhom集合の同値として読む

積の普遍性を `(X → A × B)` と `(X → A) × (X → B)` の対応として書き、順写像・逆写像・二つの
逆法則を構成せよ。[LEI14] の存在一意性による定義とhom集合の全単射による定式化を比較し、
`productHomEquiv` の四フィールドへ対応づける。

この全単射が全ての `X` に一様に存在することが重要である。特定の `X` について要素数が一致する
だけでは普遍性にならない理由を説明せよ。

### 零項の積と一意性の意味を調べる

終対象を零成分の積とみなし、任意の共通始域から選ぶべき射影が一つもないため、媒介射が一意に
なるという議論を与えよ。二項積の定義を単に `A × B` の構文へ依存させず、零項・多項の場合へ
一般化できる形で述べること。

最後に、媒介射の一意性、積対象の定義的等しさ、積対象同士の一意な同型を区別せよ。普遍性が与える
一意性の水準を正確に説明できれば完了である。
-/

end FormalLab.CategoryTheory.Products