全射・単射と左逆・右逆写像

関数 f : A → B が全射であるとは、任意の b : B に対して f a = b となる a : A が存在することをいいます。また、f が単射であるとは、任意の a₁, a₂ : A に対して f a₁ = f a₂ ならば a₁ = a₂ となることをいいます。

これを Lean で表現すると次のようになります。

variable {A B : Type}

/-- 関数の全射性 -/
def Function.Surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b

/-- 関数の単射性 -/
def Function.Injective (f : A → B) : Prop := ∀ {a₁ a₂ : A}, f a₁ = f a₂ → a₁ = a₂

一見すると、全射と単射はペアになる概念とは思えないかもしれません。束縛変数の数も違いますし、意味上もまったく独立した概念のように見えます。

しかし、A が空でないと仮定すれば、選択原理 Classical.choice を使うことによって、全射 f : A → B があれば逆方向の単射 g : B → A が構成でき、逆に単射 f : A → B があれば逆方向の全射 g : B → A を構成することができます。

ある意味で、全射と単射はペアをなす概念であると言えるかもしれないですね。今回の演習問題のテーマはこの定理です。

問1: 全射から逆方向の単射

まずは、全射 f : A → B が存在すれば逆方向の単射 g : B → A も存在することを示しましょう。

実際にはより強く、f ∘ g = id を満たすような g が構成できます。一般に、f ∘ g = id が成り立つとき、g を f の右逆写像であるとか、切断(section)であるとかいいます。

-- 選択原理を使用する
open Function Classical

/-- 全射 `f : A → B` があれば、選択原理を使用することにより
単射 `g : B → A` を作ることができる。-/
theorem surj_to_inj (f : A → B) (hsurj : Surjective f)
    : ∃ g : B → A, Injective g := by
  -- まず `g` を構成する。
  -- 任意の `b : B` に対して `f` の全射性より
  -- `f a = b` となる `a : A` が存在するのでそれを返す。
  let g : B → A := fun b => sorry

  -- `g` の定義と `f` の全射性から、`f (g b) = b` が成り立つ。
  have gdef : ∀ b, f (g b) = b := by
    sorry

  -- `f ∘ g = id` を使って、
  -- `g` が単射であることを示す。
  sorry

問2: 単射から逆方向の全射

次に f : A → B が単射であれば、逆方向の全射 g : B → A も存在することを示しましょう。

これも実際にはより強く、g ∘ f = id を満たすような g が構成できます。一般に、g ∘ f = id が成り立つとき、g を f の左逆写像であるとか、引き込み(retraction)であるとかいいます。

/-- 単射 `f : A → B` があれば、選択原理を使用することにより
全射 `g : B → A` を作ることができる。 -/
theorem inj_to_surj [Inhabited A] (f : A → B) (hinj : Injective f)
    : ∃ g : B → A, Surjective g := by
  -- まず `g` を構成する。
  -- `g b` の値を構成するために、`b : B` が `f` の像に入っているかで場合分けをし、
  -- 入っていなければ適当な値、入っていれば `b = f a` となる `a` を返すようにする。
  let g : B → A := fun b => sorry

  -- `g` の定義と `f` の単射性から、`g (f a) = a` が成り立つ。
  have gdef : ∀ a, g (f a) = a := by
    sorry

  -- `g ∘ f = id` を使って、
  -- `g` が全射であることを示す。
  sorry