definition of quotient collection
Topics
About: collection
The table of contents of this article
Starting Context
- The reader knows a definition of equivalence relation on collection.
Target Context
- The reader will have a definition of quotient collection.
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:
\( C\): \(\in \{\text{ the collections }\}\)
\( \sim\): \(\in \{\text{ the equivalence relations on } C\}\)
\(*C / \sim\): \(= \{p \in Pow (C) \setminus \emptyset \vert \forall p', p'' \in p (p' \sim p'') \land \forall p' \in p, \forall p'' \in C \setminus p (\lnot p' \sim p'')\}\)
//
Conditions:
//
\(C / \sim\) is well-defined, because for each \(p \in Pow (C) \setminus \emptyset\), whether \(p \in C / \sim\) or not is unambiguous. Whether \(C / \sim\) partitions \(C\) is another issue, but \(C / \sim\) indeed partitions \(C\) as is shown in Note.
In other words, the quotient collection is the collection of the equivalence classes of \(C\) by \(\sim\).
2: Note
\(C / \sim\) is a partition of \(C\), which means that each element of \(C\) is contained in a single element of \(C / \sim\): for each \(p \in C\), there is the element of \(C / \sim\), \([p]\), defined by \(\{p' \in C \vert p' \sim p\}\), because for each \(p', p'' \in [p]\), \(p' \sim p\) and \(p'' \sim p\), which implies that \(p' \sim p''\), and for each \(p' \in [p], p'' \in C \setminus [p]\), \(p \sim p'\) and \(\lnot p \sim p''\), which implies that \(\lnot p' \sim p''\), because if \(p' \sim p''\), \(p \sim p''\), a contradiction; \(p\) does not belong to any other element of \(C / \sim\), because if \(p\) belonged to another element, \([p'] \in C / \sim\), for each element, \(p'' \in [p']\), \(p'' \sim p\), which would mean that \(p'' \in [p]\), and for each element, \(p'' \in [p]\), \(p'' \sim p\), which would mean that \(p'' \in [p']\), so, \([p'] = [p]\) after all.
\(f: C \to C / \sim, s \mapsto [s]\) is called "classification map of \(C\) with respect to \(\sim\)".
\(f\) is well-defined, because \([s] \in C / \sim\) is uniquely determined, because \(C / \sim\) is a partition of \(C\).
\(f\) is a surjection, because for each \([s] \in C / \sim\), \(f (s) = [s]\).
