import FormalLab.Mathematics.Sets

/-!
# 第21章：数学的関数とその性質

関数 `f : A → B` があることと、その関数が入力の情報を失わないこと、終域の全てへ届くことは
別の主張です。前者はデータであり、後二者は量化と等式で述べる性質です。図だけを眺めると
似て見える単射・全射も、証明で与える情報の向きは反対です。

本章ではまず単射・全射・全単射を定義します。次に左逆と右逆を導入し、含意関係を合成式から導きます。
さらに像が存在証人を保持し、逆像が述語への代入で得られることを比較します。この区別は
同値、商、圏論における同型と普遍写像を学ぶ際に再利用します。

## 関数が情報を失うか、値を覆うかを問う

関数 `f : A → B` に対して、標準的な定義は次です。

$$
\begin{aligned}
\mathsf{Injective}(f)
  &\;\Longleftrightarrow\; \forall x,y:A.\; f(x)=f(y)\to x=y,\\
\mathsf{Surjective}(f)
  &\;\Longleftrightarrow\; \forall b:B.\;\exists a:A.\;f(a)=b,\\
\mathsf{Bijective}(f)
  &\;\Longleftrightarrow\;\mathsf{Injective}(f)\land\mathsf{Surjective}(f).
\end{aligned}
$$

関数 `f` はデータです。単射性や全射性は `f` についての命題です。

* **単射**：`f x = f y` なら `x = y`。同じ出力へ潰れた入力を区別できる。
* **全射**：各 `y : β` に対し `f x = y` となる `x` が存在する。
* **全単射**：単射かつ全射。

単射・全射は式だけでなく、始域 `α` と終域 `β` を含めた関数全体の性質です。同じ計算規則
でも終域を広げれば全射でなくなることがあります。また単射は「異なる出力を返す」という
意味ではなく、等しい出力から入力の等しさを回収できるという意味です。


-/

namespace FormalLab.Mathematics.FunctionProperties

universe u v

open FormalLab.Mathematics.Sets

/-! ## 単射・全射・全単射を述語として定義する -/

/-- 同じ像を持つ二入力が等しい、という単射性の定義です。 -/
def IsInjective {α : Type u} {β : Type v} (f : α → β) : Prop :=
  ∀ ⦃x y⦄, f x = f y → x = y

/-- 終域の各値が何らかの入力の像である、という全射性の定義です。 -/
def IsSurjective {α : Type u} {β : Type v} (f : α → β) : Prop :=
  ∀ y, ∃ x, f x = y

/-- 一つの関数について単射性と全射性を束ねます。 -/
structure IsBijective {α : Type u} {β : Type v} (f : α → β) : Prop where
  injective : IsInjective f
  surjective : IsSurjective f

/-- 恒等関数は、入力を失わず全ての終域要素へ届きます。 -/
theorem identityBijective (α : Type u) : IsBijective (fun x : α => x) where
  injective := by
    intro x y h
    exact h
  surjective := fun y => ⟨y, rfl⟩

/-- 自然数の後者関数は単射です。 -/
theorem successorInjective : IsInjective Nat.succ :=
  by
    intro x y h
    exact Nat.succ.inj h

/-- 後者関数は `0` へ届かないので、自然数上では全射ではありません。 -/
theorem successorNotSurjective : ¬IsSurjective Nat.succ := by
  intro surjective
  obtain ⟨x, impossible⟩ := surjective 0
  exact Nat.noConfusion impossible

/-!
## 逆の左右は合成後の恒等式で決まる

「`g` は `f` の逆」と言う前に、どちらの合成が恒等になるかを明示します。`g ∘ f = id`
なら、まず `f` で送った入力を `g` が回収するので `g` は `f` の**左逆**です。
`f ∘ g = id` なら、任意の終域要素を `g` で原像候補へ戻して `f` で復元するため右逆です。
名前は式の中で `g` が `f` の左右どちらに現れるかにも対応します。

$$
\begin{array}{rcll}
g\circ f=\mathrm{id}_A
  &\Longleftrightarrow& \forall x:A.\;g(f(x))=x
  &\text{（$g$ は $f$ の左逆）},\\
f\circ g=\mathrm{id}_B
  &\Longleftrightarrow& \forall y:B.\;f(g(y))=y
  &\text{（$g$ は $f$ の右逆）}.
\end{array}
$$
-/

/-- `g (f x) = x`、すなわち `g ∘ f` が恒等になる条件です。 -/
def IsLeftInverse {α : Type u} {β : Type v} (g : β → α) (f : α → β) : Prop :=
  ∀ x, g (f x) = x

/-- `f (g y) = y`、すなわち `f ∘ g` が恒等になる条件です。 -/
def IsRightInverse {α : Type u} {β : Type v} (g : β → α) (f : α → β) : Prop :=
  ∀ y, f (g y) = y

/-- 左逆を持つ関数は単射です。 -/
theorem leftInverseGivesInjective {α : Type u} {β : Type v}
    {f : α → β} {g : β → α} (leftInverse : IsLeftInverse g f) : IsInjective f := by
  intro x y sameImage
  calc
    x = g (f x) := (leftInverse x).symm
    _ = g (f y) := congrArg g sameImage
    _ = y := leftInverse y

/-- 右逆を持つ関数は全射です。 -/
theorem rightInverseGivesSurjective {α : Type u} {β : Type v}
    {f : α → β} {g : β → α} (rightInverse : IsRightInverse g f) : IsSurjective f :=
  fun y => ⟨g y, rightInverse y⟩

/-- 両側逆を交換すると、逆関数自身も全単射になります。 -/
theorem inverseBijective {α : Type u} {β : Type v}
    {f : α → β} {g : β → α}
    (leftInverse : IsLeftInverse g f) (rightInverse : IsRightInverse g f) :
    IsBijective g where
  injective := leftInverseGivesInjective rightInverse
  surjective := rightInverseGivesSurjective leftInverse

/-!
左逆から単射を得る証明では、`f x = f y` の両辺へ `g` を適用し、その後に左逆則で
`g (f x)` と `g (f y)` を元の入力へ戻します。右逆から全射を得る証明では、要求された
`y` を見てから証人 `g y` を選びます。二つの証明は、単射と全射の量化子の違いをそのまま
反映しています。
-/

/-! ## 像は証人を探し、逆像は代入する -/

/-- `s` の要素を `f` で送って得られる値の集合です。 -/
def Image {α : Type u} {β : Type v} (f : α → β) (s : PredSet α) : PredSet β :=
  fun y => ∃ x, s x ∧ f x = y

/-- `f x` が `t` に属するような入力の集合です。 -/
def Preimage {α : Type u} {β : Type v} (f : α → β) (t : PredSet β) : PredSet α :=
  fun x => t (f x)

/-!
標準的な集合記法では、像と逆像は次のように書きます。

$$
\begin{aligned}
f[S]&=\{,y:B\mid \exists x:A.\;x\in S\land f(x)=y\,\},\\
f^{-1}[T]&=\{,x:A\mid f(x)\in T\,\}.
\end{aligned}
$$

像 `Image f s` の要素 `y` については、「`s` のどの要素から来たか」という原像の証人を
提供しなければなりません。逆像 `Preimage f t` の要素 `x` はすでに手元にあるので、
`f x` を計算して `t` の所属条件へ代入するだけです。この非対称性は名称ではなく量化子
`∃ x` の有無に現れます。
-/

example : Image Nat.succ (Singleton 0) 1 :=
  ⟨0, rfl, rfl⟩

example : Preimage Nat.succ (Singleton 1) 0 :=
  rfl

/-!
像を取ってから逆像を取ると、単射でない関数では元の集合より大きくなり得ます。単射性が
あれば、同じ像へ来た原像を元の点へ戻せるため、ちょうど元の集合を回収できます。双対的に、
逆像の像は一般には終域の集合の一部にしか届きませんが、全射性があれば全体を回収します。
-/

/-- 単射なら、集合を像へ送り逆像で戻す操作は元の集合を回収します。 -/
theorem preimageImage_eq_of_injective {α : Type u} {β : Type v}
    {f : α → β} (injective : IsInjective f) (s : PredSet α) :
    Preimage f (Image f s) = s := by
  funext x
  apply propext
  constructor
  · rintro ⟨x', hx', sameImage⟩
    have sameInput : x' = x := injective sameImage
    simpa [sameInput] using hx'
  · intro hx
    exact ⟨x, hx, rfl⟩

/-- 全射なら、集合を逆像へ戻し像へ送る操作は元の集合を回収します。 -/
theorem imagePreimage_eq_of_surjective {α : Type u} {β : Type v}
    {f : α → β} (surjective : IsSurjective f) (t : PredSet β) :
    Image f (Preimage f t) = t := by
  funext y
  apply propext
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact hx
  · intro hy
    obtain ⟨x, sameImage⟩ := surjective y
    have hx : Preimage f t x := by
      change t (f x)
      simpa [sameImage] using hy
    exact ⟨x, hx, sameImage⟩

/-!
## 逆写像と選択に関する注意

左逆から単射、右逆から全射という向きは構成的です。逆向きは同じ形ではありません。
全射から各 `y` の原像を一斉に選んで右逆を作るには選択の問題があり、単射から全終域上の
左逆を作るには像の外で返す値も必要です。「逆も明らか」とはしません。

全単射の証明と、実際の逆関数をデータとして持つ同値も区別します。本章の
`IsBijective f` は `f` の性質を記録しますが、逆関数そのものをフィールドとしては
保持していません。

## 要点

* 関数はデータで、単射・全射・全単射は始域と終域を含む関数の性質である。
* 左逆は入力を回収するため単射性を、右逆は終域の原像を与えるため全射性を導く。
* 像の所属は原像の証人を要求し、逆像の所属は関数適用による代入で定まる。
* 性質としての全単射と、逆関数を備えた構造は区別する。

## 研究史と文献案内

関数概念は解析式から任意の対応へ一度に置き換わったのではなく、Fourier級数などをめぐる
19世紀の議論、集合論、写像による構造研究を通じて一般化されました。Dedekindの自然数論
[DED88] は写像を構造の中心に置く原典の一つです。現代の集合論的定義と型理論的関数を
同一視せず、始域・終域・等式の基礎理論を確認します。

## 問題

### 左逆から単射を復元する

関数 `f : α → β` と `g : β → α` について、左逆と右逆の式を合成の順序まで含めて
数式で書け。次に `leftInverseGivesInjective` の等式列を一行ずつ展開し、各行が合同性、
左逆の仮定、与えられた等式のどれを使うか注記せよ。

最後に、全単射な `f` と、`f` の左逆かつ右逆である `g` から `IsBijective g` をLeanで
証明する。単射と全射の証明で左右どちらの逆の式を使ったかを説明できれば完了である。

### 像と逆像の量化を比較する

`Image f s y` と `Preimage f t x` を論理結合子と量化記号だけで展開せよ。前者では始域の
要素を存在量化するのに、後者では `f x` を直接検査できる理由を、型の情報の流れとして
説明する。具体例として `f n = n % 2` を用い、単集合の像と逆像を一つずつ計算せよ。

同じ式で定めた関数でも終域を変えると全射性が変わる例を作り、全射性が値の計算だけでなく
始域・終域を含む関数の型の性質であることを確認せよ。

### 逆関数を選ぶために必要な仮定を調べる

単射 `f : α → β` から左逆 `g : β → α` を構成しようとすると、像の外の `y : β` に
どの値を返すかが未決定になる。`α` が空の場合と空でない場合を分け、どの箇所で既定値または
選択原理が必要になるかを分析せよ。

「単射なら無条件に計算可能な左逆が得られる」という主張の誤りを、型が空である例を含めて
示すこと。定理として証明できる部分と、追加仮定に依存する構成を区別できれば完了である。
-/

end FormalLab.Mathematics.FunctionProperties