セット（集合）エンドモーフィズム（自己準同形写像）に対して、もしも、ドメイン（定義域）の上へのサージェクション（全射）があってサージェクション（全射）がサージェクション（全射）の後にエンドモーフィズム（自己準同形写像）を作用させるのと等しい場合、エンドモーフィズム（自己準同形写像）はアイデンティティ（恒等写像）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、%ストラクチャー（構造）種類名%エンドモーフィズム（自己準同形写像）の定義を知っている。
- 読者は、サージェクション（全射）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のセット（集合）エンドモーフィズム（自己準同形写像）に対して、もしも、当該エンドモーフィズム（自己準同形写像）の当該ドメイン（定義域）の上への任意のサージェクション（全射）があって当該サージェクション（全射）が当該サージェクション（全射）の後に当該エンドモーフィズム（自己準同形写像）を作用させるのと等しい場合、当該エンドモーフィズム（自己準同形写像）はアイデンティティ（恒等写像）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S\): \(\in \{\text{ 全てのセット（集合）たち }\}\)
\(f\): \(: S \to S\)
//
ステートメント（言明）たち:
\(\exists S' \in \{\text{ 全てのセット（集合）たち }\}, \exists f': S' \to S \in \{\text{ 全てのサージェクション（全射）たち }\} (f' = f \circ f')\)
\(\implies\)
\(f = id: S \to S\)
//
3: 証明
全体戦略: ステップ1: 任意の\(s \in S\)を取り、ある\(s' \in S'\)に対して、\(s = f' (s')\)であることを見る; ステップ2: \(f (s) = s\)であることを見る。
ステップ1:
\(s \in S\)は任意のものであるとしよう。
\(f'\)はサージェクティブ（全射）であるから、以下を満たすある\(s' \in S'\)、つまり、\(s = f' (s')\)、がある。
ステップ2:
\(f' = f \circ f'\)であるから、\(s = f' (s') = f \circ f' (s') = f (s)\)。
\(s\)は恣意的であるから、それが意味するのは、\(f\)はアイデンティティマップ（恒等写像）であるということ。
3: 注
\(f\)がベクトルたちスペース（空間）エンドモーフィズム（自己準同形写像）であるケースに対しては、\(f'\)に対してより少なく要求するある命題がある。
