Equivalence relations #
This file defines the complete lattice of equivalence relations on a type, results about the inductively defined equivalence closure of a binary relation, and the analogues of some isomorphism theorems for quotients of arbitrary types.
Implementation notes #
Rel and lemmas ending in ' make it easier to talk about different
equivalence relations on the same type.
The complete lattice instance for equivalence relations could have been defined by lifting
the Galois insertion of equivalence relations on α into binary relations on α, and then using
CompleteLattice.copy to define a complete lattice instance with more appropriate
definitional equalities (a similar example is
Order/Filter/Basic.lean). This does not save space, however, and is less clear.
Partitions are not defined as a separate structure here; users are encouraged to
reason about them using the existing
Setoid and its infrastructure.
setoid, equivalence, iseqv, relation, equivalence relation
Given a map f from α to β, the kernel of f is the unique equivalence relation on α whose induced map from the quotient of α to β is injective.
The quotient of α by the kernel of a surjective function f bijects with f's codomain.
If a specific right-inverse of
f is known,
Setoid.quotientKerEquivOfRightInverse can be
definitionally more useful.
Given a surjective function f whose kernel is contained in an equivalence relation r, the equivalence relation on f's codomain defined by x ≈ y ↔ the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by r.