全射/単射の分裂

[Seasawher]

全射はレトラクションであり、単射はセクションである。これは選択公理のいい練習になりそうだなと思う。

/- # 全射と単射の split 性

単射 A → B があれば、全射 B → A が作れるし、
全射 -/
import Mathlib.Logic.Function.Defs

open Function

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

variable {A B : Type}

/-- 全射 `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 : B) → {a : A // f a = b} := fun b =>
    have h : ∃ a, f a = b := hsurj b
    ⟨Classical.choose h, Classical.choose_spec h⟩
  let g : B → A := fun b => (g' b).val

  -- `g` の定義と `f` の全射性から、`f (g b) = b` が成り立つ。
  have gdef : ∀ b, f (g b) = b := by
    intro b
    rw [show g b = (g' b).val from rfl]
    simp_all [(g' b).property]

  -- `g` が単射であることを示したい。
  -- それには、`f ∘ g = id` を示せば十分。
  suffices ∀ b, f (g b) = b from by
    exists g
    intro b₁ b₂ h
    replace h : b₁ = b₂ := calc
      _ = f (g b₁) := by rw [this]
      _ = f (g b₂) := by rw [h]
      _ = _ := by rw [this]
    exact h

  -- しかし `f ∘ g = id` は既に示していたので、証明が完了する。
  exact gdef

/-- 単射 `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 := fun b =>
    if h : ∃ a, f a = b then Classical.choose h
    else default

  -- `g` の定義と `f` の単射性から、`g (f a) = a` が成り立つ。
  have gdef : ∀ a, g (f a) = a := by
    -- `a : A` が与えられたとする。
    intro a

    -- `g` の定義を展開する
    dsimp only [g]

    -- `f a` は明らかに `f` の像に入っているということを利用して、
    -- `g` の定義の中の `if` 式を簡約する。
    split
    case isFalse h =>
      have : ∃ a₁, f a₁ = f a := ⟨a, rfl⟩
      simp_all [this]

    -- 後は `f` の単射性から従う。
    case isTrue h =>
      have := Classical.choose_spec h
      apply hinj
      assumption

  -- `g` が全射であることを示したい。
  -- それには、`g ∘ f = id` を示せば十分。
  suffices ∀ a, g (f a) = a from by
    exists g
    intro a
    exists f a
    apply this

  -- `g ∘ f = id` を示す。
  exact show ∀ a, g (f a) = a from by
    -- `a : A` が与えられたとする。
    intro a

    -- `f` の単射性により、`f (g (f a)) = f a` を示せばよい。
    apply hinj

    -- それは先に示した `g (f a) = a` から従う。
    simp [gdef]