選択公理と逆写像

#「単射（左逆写像）」との構造的な違い

項目	単射 ↔ 左逆写像 (g(f(x)) = x)	全射 ↔ 右逆写像 (f(g(y)) = y)
主役	元の要素 x が主役。	目標の値 y が主役。
証明の核	f が情報を潰さない（単射）から戻れる。	f が全域をカバーする（全射）から、どこからでも戻れる。
逆関数の役割	f x を受け取って、唯一の x を特定する。	y を受け取って、適当な（少なくとも1つの）x を選ぶ。
選択公理	inverse の定義自体には使われるが、戻す力は f の単射性に依存。	y から x を選ぶ際に、選択公理が本質的な役割を果たす。

---

1. 「構成」と「性質」を分離する標準的な流れ

数学の定理の多くは、「まず対象を定義（構成）し、次にその性質を証明する」というステップを踏みます。 今回の例もその典型です。

1. 構成: inverse f を「あるならそれ、ないならデフォルト」と定義。
2. 性質1 (inverse_spec): 原像があるなら、送って戻すと一致する。
3. 性質2 (Injective 等): 単射性や全射性との関係を証明。

この「インターフェース（定義）」と「実装の正しさ（証明）」を分けるスタイルは、Leanに限らず現代数学の標準的な記述方法です。

2. 「選択公理」の具体的な使い方

数学の教科書では「全射であれば右逆写像が存在する」と一行で書かれることが多いですが、それをコンピュータが理解できる形で具体化したのが今回のコードです。

• 「選ぶ」という行為: Classical.choose を使うことで、数学者が頭の中で行っている「無数にある候補から1つ取り出す」という操作を明示的に記述しています。
• 非構成的証明: 「具体的な計算手順（アルゴリズム）は分からないが、存在することだけは確かだ」という論理を扱う際に、このパターンは必須となります。

3. 関数の「全単射（Bijective）」を扱う基礎

今回証明した「単射 ↔ 左逆写像」「全射 ↔ 右逆写像」の2つを組み合わせると、以下の有名な定理が完成します。

定理: $f$ が全単射（Bijective）であることと、$f$ に（両側）逆関数 $f^{-1}$ が存在することは同値である。

この定理は、群論、位相空間論、線形代数など、あらゆる分野の入り口で使われます。そのため、今回のような証明は「数学という建物の土台作り」として非常によく現れるのです。