.. _equiv_relns:

Equivalence Relations
=====================

Classical Set Theory
--------------------

1) A *binary relation* :math:`\star` on a set :math:`S` is the following information: for each :math:`(s,t)\in S^2` we have a proposition :math:`s \star t`. An example is the less-than relation :math:`<` on :math:`\mathbb{R}`; for each pair of real numbers :math:`a` and :math:`b` we have a true-false statement :math:`a<b`.

2) Two other equivalent ways of modelling the definition: a binary relation can be thought of as a subset of :math:`S^2`, the dictionary being that :math:`(s,t)` is in the subset iff :math:`s \star t`. Or it could be thought of as a map from :math:`S^2` to the set :math:`\{T,F\}`.

3) A binary relation :math:`\sim` on a set :math:`S` is *reflexive* if

.. math::
      
   \forall s\in S, s\sim s,

and it is *symmetric* if

.. math::

   \forall s,t\in S, s \sim t \to t \sim s

It is *transitive* if

.. math::

   \forall s, t, u\in S, s \sim t \land t \sim u \to s \sim u,

and it is an *equivalence relation* if it is reflexive, symmetric
and transitive. Examples show that none of the three axioms for an
equivalence relation can be dropped. For example the binary relation
:math:`\le` is reflexive and transitive, but not symmetric.

4) If :math:`\sim` is an equivalence relation on :math:`S`, we may partition :math:`S` into disjoint *equivalence classes*; these form a *partition* of :math:`S`. One can check that conversely, from a partition of :math:`S` one can construct an equivalence relation, defined by :math:`s \sim t` if :math:`s` and :math:`t` are in the same part of the partition, and these two dictionaries provide two distinct ways of thinking about the same idea.

Universal properties of the quotient
------------------------------------

Let `S` be a set and let :math:`\star` be an equivalence relation on `S`. We would like to characterise the set `Q` of equivalence classes of `S` under :math:`star` by writing down properties which will determine it uniquely. Here are some which spring to mind.

1) There is a natural map :math:`m:S\to Q`.

2) This map is surjective.

3) If :math:`s_1, s_2\in S` then :math:`m(s_1)=m(s_2)` if and only if :math:`s_1\star s_2`.
      
One can put all of these properties together to deduce the *universal property* of `Q` , which a mathematician would describe thus: "If `X` is any set, then to give a map :math:`f:Q\to X` is to give a map :math:`g:S\to X` such that for :math:`s,t\in S` , :math:`s\star t\implies f(s)=f(t)` . Given `f` , one defines :math:`g=m\circ f` , and one uses the properties above to show that this induces a bijection between the `f` s and the `g` s.

Lean's dependent type theory.
-----------------------------

The quotient construction is actually not a standard part of dependent type theory, but mathematicians could get nowhere without it so it has been explicitly added to Lean as a third kind of type -- a quotient type.

``quot(*)=Q``

``quot.mk(*)=m``

``quot.ind``