import FormalLab.CategoryTheory.Products

/-!
# 第44章：余積と双対性

積の定義に現れる全ての射を反転すると、射影は入射に、対化は余対化に、共通始域は共通終域に
変わります。その結果得られるのが余積です。双対性は積と余積が何となく似ているという観察では
なく、射の向きと合成順を一貫して反転して定義と定理を移す操作です。

本章では直和型を `Type` における余積として構成し、計算則と一意性を積の証明と対照します。
反対圏をまだ形式化していない段階でも、各式の始域・終域を検査すれば双対化を実行できることを
確かめます。後の圏・反対圏・関手では、この操作を一般の構造として定義し直します。

## 二つの生成源から出る射を一本に束ねる

圏 `𝒞` における余積は、対象 `Q` と入射 `ι₁ : A → Q`, `ι₂ : B → Q` であって、各 `X` に
ついて

$$
\mathcal C(Q,X)\longrightarrow\mathcal C(A,X)\times\mathcal C(B,X),
\qquad
h\longmapsto(h\circ\iota_1,h\circ\iota_2)
$$

が全単射になるものです。型と関数の圏では直和型 `A ⊕ B` がこの役割を果たします。

`A ⊕ B` には入射 `Sum.inl : A → A ⊕ B` と `Sum.inr : B → A ⊕ B` があります。
`f : A → X` と `g : B → X` から場合分けで `copair f g : A ⊕ B → X` を作れます。
入射との合成が `f`、`g` になる関数はこれだけです。

積では共通の始域から二射が**出て**、一意な射が積へ入ります。余積では二射が共通の
終域へ**入り**、一意な射が余積から出ます。この全面的な矢印反転が双対化です。

$$
\begin{array}{c|c}
\text{積} & \text{余積}\\ \hline
X\to A,\;X\to B & A\to X,\;B\to X\\
X\to A\times B & A\mathbin{\oplus}B\to X\\
\pi_i\circ\langle f,g\rangle=f_i & [f,g]\circ\iota_i=f_i
\end{array}
$$

単語を置換する前に、各射の始域・終域と合成順を反転します。その結果として射影は入射、
対化は余対化、終対象は始対象へ移ります。


-/

namespace FormalLab.CategoryTheory.Coproducts

universe u v w z

open FormalLab.Logic.Equality

/-! ## 余対化を構成し、二つの計算則を証明する -/

/-- 二関数を直和上の一関数へまとめる標準写像です。 -/
def copair {A : Type u} {B : Type v} {X : Type w}
    (f : A → X) (g : B → X) : A ⊕ B → X :=
  Sum.elim f g

theorem leftInjection {A : Type u} {B : Type v} {X : Type w}
    (f : A → X) (g : B → X) :
    copair f g ∘ Sum.inl = f := by
  funext a
  rfl

theorem rightInjection {A : Type u} {B : Type v} {X : Type w}
    (f : A → X) (g : B → X) :
    copair f g ∘ Sum.inr = g := by
  funext b
  rfl

/-- 直和の左右を交換する写像は、二つの入射を余対化して得られます。 -/
def swap {A : Type u} {B : Type v} : A ⊕ B → B ⊕ A :=
  copair Sum.inr Sum.inl

example {A : Type u} {B : Type v} (a : A) :
    swap (A := A) (B := B) (Sum.inl a) = (Sum.inr a : B ⊕ A) :=
  rfl

/-- 左右交換を二度行うと、どの直和要素も元へ戻ります。 -/
theorem swap_involutive {A : Type u} {B : Type v} (value : A ⊕ B) :
    swap (A := B) (B := A) (swap value) = value := by
  cases value <;> rfl

/-! ## 一意性と普遍性 -/

theorem copairUnique {A : Type u} {B : Type v} {X : Type w}
    (f : A → X) (g : B → X) (h : A ⊕ B → X)
    (hleft : h ∘ Sum.inl = f) (hright : h ∘ Sum.inr = g) :
    h = copair f g := by
  funext value
  cases value with
  | inl a => exact congrFun hleft a
  | inr b => exact congrFun hright b

/-- 余積の普遍性を、二つの関数空間の間の同値としてまとめます。 -/
def coproductHomEquiv {A : Type u} {B : Type v} {X : Type w} :
    Products.FunctionEquiv (A ⊕ B → X) ((A → X) × (B → X)) where
  toFun h := (h ∘ Sum.inl, h ∘ Sum.inr)
  invFun maps := copair maps.1 maps.2
  leftInverse h :=
    (copairUnique (h ∘ Sum.inl) (h ∘ Sum.inr) h rfl rfl).symm
  rightInverse maps := by
    apply Prod.ext
    · exact leftInjection maps.1 maps.2
    · exact rightInjection maps.1 maps.2

/-!
積の一意性では出力対の二成分を射影しました。余積の一意性では入力が `inl a` か `inr b`
かを場合分けします。各分岐で対応する合成条件を具体的な要素へ適用すれば、関数値が一致
します。証明操作まで、射影による観察と入射による生成が双対的に対応しています。
-/

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

/-- 通常の直和と二入射は、各試験対象 `X` に対して余積の普遍性を満たします。 -/
theorem sumIsCoproductAt (A : Type u) (B : Type v) (X : Type w) :
    IsCoproductAt (C := A ⊕ B) Sum.inl Sum.inr X := by
  intro f g
  exact ⟨copair f g, ⟨leftInjection f g, rightInjection f g⟩,
    fun h laws => copairUnique f g h laws.left laws.right⟩

/-!
## `Sum.elim`が表す場合分け

`Sum.elim f g` はLeanの直和型に対する除去原理で、数学的記法の余対化 `[f,g]` を実現します。
`cases value` は余積の普遍性そのものではなく、`Sum` の二構成子について証明項を作るための
tactic記法です。一般の圏では要素の場合分けを使えないため、ここでの証明手順と余積の抽象的な
定義を区別します。

## 双対化と逆関数を混同しない

双対は `A × B` の記号を `A ⊕ B` に置き換えるだけではありません。射の向き、合成の
順序、普遍射の始域と終域を全て反転します。また `Type` では積と余積の内部表現が異なり、
双対だから同じ計算規則を持つわけではありません。

また双対性は、`Type` という一つの圏の中に対象同士の具体的な等式を与える主張ではありません。
圏 `C` の射を反転した反対圏 `Cᵒᵖ` で、定義や定理の形が移り合うという原理です。

## 要点

* 余積は二入射と組になり、共通終域への二射を一意な媒介射へまとめる。
* 計算則は媒介射を入射の後に合成すると元の射へ戻ることを述べる。
* 一意性は直和の二構成子について場合分けして証明する。
* 双対化では射の向き、合成順、普遍射の始域・終域を一貫して反転する。
* 双対な構成は同じ内部表現や同じ計算規則を持つとは限らない。

## 研究史と文献案内

双対性は個別の類似ではなく、圏 `𝒞` から射を反転した反対圏 `𝒞ᵒᵖ` へ定義と定理を移す
原理です。圏・関手・自然同値の原典は [EM45]、反対圏と普遍構成の標準的扱いは [MAC98;
LEI14] を参照してください。双対な定義が同じ内部表現や同じ計算規則を持つとは限りません。

## 問題

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

`IsCoproductAt` を展開し、二つの入射と任意の共通終域への二射から媒介射を作る過程を示せ。
`copairUnique` が直和の二構成子で場合分けする理由を、関数が全入力で一意に決まるという外延性へ
結びつけて説明する。

成分を交換する `swap` を定義し、二回適用すると元へ戻ることを証明せよ。積の場合の証明と並べ、
積では射影、余積では構成子による場合分けが中心になる差を指摘すること。

### 普遍性を写像集合の同値として表す

余積の普遍性を `(A ⊕ B → X)` と `(A → X) × (B → X)` の同値として構成せよ。順写像は入射との
合成、逆写像は場合分けであり、二つの逆法則がどの計算規則と外延性に依存するかを追う。

積のhom集合の同値と比較し、変数 `X` が式のどちら側に現れるかを書け。この変位が射の反転と
どのように対応するかを説明できれば完了である。

### 双対化を定義から実行する

`IsProductAt` の全ての矢印を反転して `IsCoproductAt` を導き、同じ手順を始対象と終対象にも適用せよ。
[MAC98] または [LEI14] の反対圏の定義と照合し、合成順序も反転することを確認する。

「射を反転する」は各関数の逆関数を選ぶことではない。逆関数を持たない写像を含む圏でも反対圏を
作れる理由を述べ、双対性が具体的な型同士の等式を与えるという誤読を反例で退けること。
-/

end FormalLab.CategoryTheory.Coproducts