description/proof of that for set with equivalence relation, subset, canonical injection from quotient set into quotient set, and subset of quotient set of subset, preimage under classification map of image of subset under canonical injection is saturation of preimage under classification map of subset
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of quotient set.
- The reader knows a definition of saturation of subset of set with equivalence relation.
- The reader knows a definition of map preimage of subset of codomain.
- The reader admits 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.
Target Context
- The reader will have a description and a proof of the proposition that for any set with any equivalence relation, any subset, the canonical injection from the quotient set of the subset into the quotient set of the set, and any subset of the quotient set of the subset, the preimage under the classification map of the set of the image of the subset under the canonical injection is the saturation of the preimage under the classification map of the subset of the subset.
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]'\)
\(\widetilde{S}\): \(\subseteq S / \sim\)
//
Statements:
\(f'^{-1} (g (\widetilde{S})) = Sat (f^{-1} (\widetilde{S}), \sim')\)
//
2: Proof
Whole Strategy: Step 1: see that for each \(p \in f'^{-1} (g (\widetilde{S}))\), \(p \in Sat (f^{-1} (\widetilde{S}), \sim')\); Step 2: see that for each \(p \in Sat (f^{-1} (\widetilde{S}), \sim')\), \(p \in f'^{-1} (g (\widetilde{S}))\).
Step 1:
Let \(p \in f'^{-1} (g (\widetilde{S}))\) be any.
\(f' (p) \in g (\widetilde{S})\).
There is a \([s] \in \widetilde{S}\) such that \(f' (p) = g ([s])\).
But \(g ([s]) = g (f (s)) = f' \vert_{S} (s)\), by 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, \(= f' (s)\).
So, \(f' (p) = f' (s)\), which means that \(p \sim' s\).
\(g (f (s)) = g ([s]) = f' (p) \in g (\widetilde{S})\).
As \(g\) is an injection, by 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, \(f (s) \in \widetilde{S}\), because there is an \(\widetilde{s} \in \widetilde{S}\) such that \(g (f (s)) = g (\widetilde{s})\), which implies that \(f (s) = \widetilde{s} \in \widetilde{S}\), so, \(s \in f^{-1} (\widetilde{S})\).
So, \(p \in Sat (f^{-1} (\widetilde{S}), \sim')\).
So, \(f'^{-1} (g (\widetilde{S})) \subseteq Sat (f^{-1} (\widetilde{S}), \sim')\).
Step 2:
Let \(p \in Sat (f^{-1} (\widetilde{S}), \sim')\) be any,
There is an \(s \in f^{-1} (\widetilde{S})\) such that \(p \sim' s\), which implies that \(f' (p) = f' (s)\).
\(f (s) \in \widetilde{S}\).
\(g (f (s)) \in g (\widetilde{S})\).
But \(f' (p) = f' (s) = f' \vert_S (s) = g (f (s))\), by 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, \(\in g (\widetilde{S})\).
So, \(p \in f'^{-1} (g (\widetilde{S}))\).
So, \(Sat (f^{-1} (\widetilde{S}), \sim') \subseteq f'^{-1} (g (\widetilde{S}))\).
Step 3:
So, \(f'^{-1} (g (\widetilde{S})) = Sat (f^{-1} (\widetilde{S}), \sim')\).
