Lean4で全単射や逆関数の性質を証明

この記事について

ヨビノリ群論入門をLean4で形式化の流れで全単射の性質が必要になるので色々示しておきます。

おまじない

import Mathlib.Tactic

noncomputable section

変数定義もしておきます。

variable {α β γ : Type*}

全単射の定義

単射であるという命題と全射であるという命題を持つ構造体として定義しました。

structure MyBijective (f : α → β) where
  isinj : ∀ a1 a2 : α, f a1 = f a2 → a1 = a2
  issurj : ∀ b : β, ∃ a : α, f a = b

名前空間を開いておきます。

namespace MyBijective

全単射の性質を証明

• 全単射の合成が全単射であること

theorem bij_comp_is_bij (f : α → β) (g : β → γ) (hf : MyBijective f) (hg : MyBijective g) :
    MyBijective (g ∘ f) := by
  constructor
  · intro a1 a2 gfeq
    exact hf.isinj a1 a2 (hg.isinj (f a1) (f a2) gfeq)
  · intro c
    rcases (hg.issurj c) with ⟨b, geq⟩
    rcases (hf.issurj b) with ⟨a, feq⟩
    use a
    show g (f a) = c
    rw [feq, geq]

• 恒等関数が全単射であること

theorem idFun_is_bij : MyBijective (fun a : α ↦ a) :=
    ⟨fun _ _ ha ↦ ha, by intro b; use b⟩

逆関数の定義

全射性から、行き先βのあらゆる元にそこに行く定義域αの元があるのでそれをとってきます。

def inv_bij (f : α → β) (hf : MyBijective f) (b : β) : α := Classical.choose (hf.issurj b)

逆関数の性質を証明

• 逆関数がしっかり右逆写像になっていること

theorem inv_bij_is_right_inv (f : α → β) (hf : MyBijective f) (b : β) :
    f (inv_bij f hf b) = b := Classical.choose_spec (hf.issurj b)

• 逆関数がしっかり左逆写像になっていること

theorem inv_bij_is_left_inv (f : α → β) (hf : MyBijective f) (a : α) :
    (inv_bij f hf) (f a) = a := hf.isinj _ a (Classical.choose_spec (hf.issurj (f a)))

• 逆関数もまた全単射であること

theorem inv_bij_is_bij (f : α → β) (hf : MyBijective f) :
    MyBijective (inv_bij f hf) := by
  constructor
  · intro b1 b2 inveq
    have : f (inv_bij f hf b1) = f (inv_bij f hf b2) := by rw [inveq]
    rw [inv_bij_is_right_inv f hf b1, inv_bij_is_right_inv f hf b2] at this
    exact this
  · intro a
    use f a
    exact inv_bij_is_left_inv f hf a