description/proof of that saturation of subset of set with equivalence relation is set iff canonical injection from quotient set of subset into quotient set of set is bijection
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of saturation of subset of set with equivalence relation.
- The reader knows a definition of quotient set.
- The reader knows a definition of bijection.
- 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 the saturation of any subset of any set with any equivalence relation is the set if and only if the canonical injection from the quotient set of the subset into the quotient set of the set is a bijection.
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 / \sim \to S' / \sim', [s] \mapsto [s]'\)
//
Statements:
\(Sat (S, \sim') = S'\)
\(\iff\)
\(f \in \{\text{ the bijections }\}\)
//
2: Proof
Whole Strategy: Step 1: see that \(f\) is an injection; Step 2: suppose that \(Sat (S, \sim') = S'\); Step 3: see that \(f\) is a bijection; Step 4: suppose that \(f\) is a bijection; Step 5: see that \(Sat (S, \sim') = S'\).
Step 1:
\(f\) is valid and 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.
Step 2:
Let us suppose that \(Sat (S, \sim') = S'\).
Step 3:
Let \([s']' \in S' / \sim'\) be any.
\(s' \in S'\), so, \(s' \in Sat (S, \sim')\).
So, there is an \(s \in S\) such that \(s \sim' s'\), which implies that \([s]' = [s']'\).
\(f ([s]) = [s]' = [s']'\).
So, \(f\) is a surjection.
So, \(f\) is a bijection.
Step 4:
Let us suppose that \(f\) is a bijection.
Step 5:
Let \(s' \in S'\) be any.
There is an \(s \in S\) such that \(f ([s]) = [s']'\), because \(f\) is a surjection.
\(f ([s]) = [s]'\), so, \([s]' = [s']'\).
That means that \(s \sim' s'\), and so, \(s' \in Sat (S, \sim')\).
So, \(S' \subseteq Sat (S, \sim')\).
As \(Sat (S, \sim') \subseteq S'\), \(Sat (S, \sim') = S'\).
