>
Let $\sim$ be an [[equivalence relation]] on a set $A$.
> [!theorem]+ Theorem. ([[universal property of quotient sets]])
> The [[quotient set]] $A / \sim$ is [[universal property|universal]] with respect to the property of mapping $A$ to a set in such a way that equivalent elements have the same image.
>
> *Explicitly*, if we take the [[coslice category|coslice]] [[subcategory]] $\mathsf{C}$ whose general object is a set-function $A \xrightarrow{\varphi}Z$ satisfying $a' \sim a'' \implies \varphi(a')=\varphi(a'')$ and whose morphisms are commutative diagrams [^1]
>
> ```tikz
> \usepackage{tikz-cd}
> \begin{document}
> % https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZARgBpiBdUkANwEMAbAVxiRAEEQBfU9TXfIRQAGUsKq1GLNgC0A+sW68QGbHgJEATGIn1mrRCHmbuEmFADm8IqABmAJwgBbJKJA4ISMpP1sAOn709mgAFlgKSnaOLohuHkjaIAx0AEYwDAAK-OpCIPZYFiE4INR60oYBQaHhJjxRzl7U8YiJZQYgAdgWTnSmXEA
> \begin{tikzcd}
> Z_1 \arrow[rr, "\sigma"] & & Z_2 \\
> & A \arrow[lu, "\varphi_1"] \arrow[ru, "\varphi_2"'] &
> \end{tikzcd}
> \end{document}
> ```
> then the [[quotient set|canonical projection]] $A \xrightarrow{\pi} A / \sim$ is an [[terminal object|initial object]] in $\mathsf{C}$.
> i.e., there is a unique commutative diagram
>```tikz
\usepackage{tikz-cd}
\begin{document}
% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAEEB6AHW+wFsQAX1LpMufIRQAmclVqMWbAFrDRIDNjwEiARlK759Zq0Qdh8mFADm8IqABmAJwiDEskDghIyIBnQAjGAYABXFtKT8YBxwQamMl140LDVHFzcPLyR9BRM2XnonNAALVOp-INDwyTYnLGsS2JF01x9qbMRchNMQXggaGCcGLDAYYEK6YrKhCyEgA
\begin{tikzcd}
A/\sim \arrow[rr, "\overline{\varphi}"] & & Z \\
& A \arrow[lu, "\pi"] \arrow[ru, "\varphi"'] &
\end{tikzcd}
\end{document}
>```
> that is, a unique function $\overline{\varphi}$ making this diagram commute. $\overline{\varphi}$ is (well-)defined $\overline{\varphi}([a])=\varphi(a)$.
^theorem
> [!note]+ Remark.
> Observe the various implicitries in the original assertion. It did not say what the [[category]] is, nor that we should pay attention specifically to [[terminal object|initial objects]] rather than [[terminal object|final objects]]. Moreover, we also now know that the solution to the universal problem is not *really* $A / \sim$, but actually $A \xrightarrow{\pi} A / \sim$.
>
> But these are all clear from context. The canonical projection is really the only sensible set-morphism to define from $A$ to $A / \sim$. And the final object in $\mathsf{C}$ is the empty function (?), so surely that is not what is being referred to.
^note
> [!proof]+ Proof. ([[universal property of quotient sets]])
> Let $[a] \in A / \sim$ be arbitrary. If the diagram is indeed going to commute, then necessarily $\overline{\varphi}([a])=\varphi(a);$
> this tells us that $\overline{\varphi}$ is unique so long as it is [[well-defined]] in the sense that $[y]=[x]$ $\implies$ $\overline{\varphi}([y])=\overline{\varphi}([x])$.
>
> This it certainly is, for $[y]=[x] \implies y \sim x \implies \varphi(y)=\varphi(x)$
> by definition of objects $\varphi$ in $\mathsf{C}$.
^proof
#### References
> [!backlink]
> ```dataview
TABLE rows.file.link as "Further Reading"
FROM [[]]
FLATTEN file.tags
GROUP BY file.tags as Tag
> [!frontlink]
> ```dataview
> TABLE rows.file.link as "Further Reading"
> FROM outgoing([[]])
> FLATTEN file.tags as Tag
> WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom"
> GROUP BY Tag
> ```
#reformatrevisebatch02