description/proof of that for map, if inverse exists, inverse is unique
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of inverse of map.
Target Context
- The reader will have a description and a proof of the proposition that for any map, if an inverse exists, the inverse is the unique inverse.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(S_1\): \(\in \{\text{ the sets }\}\)
\(S_2\): \(\in \{\text{ the sets }\}\)
\(f\): \(: S_1 \to S_2\)
//
Statements:
\(\exists f', f'': S_2 \to S_1 ((f' \circ f = id_{S_1} \land f \circ f' = id_{S_2}) \land (f'' \circ f = id_{S_1} \land f \circ f'' = id_{S_2}))\)
\(\implies\)
\(f' = f''\)
//
2: Proof
Whole Strategy: Step 1: evaluate \(f' \circ f \circ f''\).
Step 1:
As \(f' \circ f = id_{S_1}\), \((f' \circ f) \circ f'' = id_{S_1} \circ f''\), which is valid, because \(f''\) is into \(S_1\) and \(f' \circ f\) is from \(S_1\).
\((f' \circ f) \circ f'' = f' \circ (f \circ f'')\), because compositions of maps is associative, as is mentioned in Note for the definition of composition of maps, \(= f' \circ id_{S_2} = f'\).
On the other hand, \(id_{S_1} \circ f'' = f''\).
So, \(f' = f''\).
