description/proof of that for set with equivalence relation and subset with subset equivalence relation, there is canonical injection from quotient set of subset into quotient set of set
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of subset equivalence relation.
- The reader knows a definition of quotient set.
- The reader knows a definition of injection.
Target Context
- The reader will have a description and a proof of the proposition that for any set with any equivalence relation and any subset with the subset equivalence relation, there is the canonical injection from the quotient set of the subset into the quotient set of the set.
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'\): \(\in \{\text{ the sets }\}\), with any equivalence relation, \(\sim'\)
\(S\): \(\subseteq S'\), with the subset equivalence relation, \(\sim\)
\(f'\): \(: S' \to S' / \sim', s' \mapsto [s']'\)
\(f\): \(: S \to S / \sim, s \mapsto [s]\)
\(g\): \(: S / \sim \to S' / \sim', [s] \mapsto [s]'\)
//
Statements:
\(g \in \{\text{ the injections }\}\)
\(\land\)
\(f' \vert_S = g \circ f\)
//
2: Proof
Whole Strategy: Step 1: see that \(g\) is indeed well-defined; Step 2: see that for each \([s_1], [s_2] \in S / \sim\) such that \([s_1] \neq [s_2]\), \(g ([s_1]) \neq g ([s_2])\); Step 3: see that \(f' \vert_S = g \circ f\).
Step 1:
Let us see that \(g\) is indeed well-defined.
For each \([s] \in S / \sim\), let \(s_1 \in S\) be any other that \([s_1] = [s]\), then, \(s_1 \sim s\), which implies that \(s_1 \sim' s\), so, \([s_1]' = [s]'\), so, \(g ([s]) = [s]'\) does not depend on the choice of the representative of \([s]\).
So, \(g\) is well-defined.
Step 2:
Let \([s_1], [s_2] \in S / \sim\) be any such that \([s_1] \neq [s_2]\).
\(g ([s_1]) \neq g ([s_2])\), because if \(g ([s_1]) = [s_1]' = [s_2]' = g ([s_2])\), which would imply that \(s_1 \sim' s_2\), so, \(s_1 \sim s_2\), so, \([s_1] = [s_2]\), a contradiction.
So, \(g\) is an injection.
Step 3:
For each \(s \in S\), \(f' \vert_S (s) = [s]'\), while \(g \circ f (s) = g ([s]) = [s]'\).
So, \(f' \vert_S = g \circ f\).
