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 #
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 Filter.CompleteLattice
in
Mathlib/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.
Tags #
setoid, equivalence, iseqv, relation, equivalence relation
Defining ≤
for equivalence relations.
Equations
The kernel of a function is an equivalence relation.
Equations
Instances For
The kernel of the quotient map induced by an equivalence relation r equals r.
Given types α
, β
, the product of two equivalence relations r
on α
and s
on β
:
(x₁, x₂), (y₁, y₂) ∈ α × β
are related by r.prod s
iff x₁
is related to y₁
by r
and x₂
is related to y₂
by s
.
Equations
Instances For
The infimum of two equivalence relations.
Equations
The infimum of 2 equivalence relations r and s is the same relation as the infimum of the underlying binary operations.
The infimum of a set of equivalence relations.
Equations
The complete lattice of equivalence relations on a type, with bottom element =
and top element the trivial equivalence relation.
Equations
The supremum of two equivalence relations r and s is the equivalence closure of the binary
relation x is related to y by r or s
.
The supremum of 2 equivalence relations r and s is the equivalence closure of the supremum of the underlying binary operations.
The supremum of a set S of equivalence relations is the equivalence closure of the binary
relation there exists r ∈ S relating x and y
.
The equivalence closure of an equivalence relation r is r.
Equivalence closure is idempotent.
The equivalence closure of a binary relation r is contained in any equivalence relation containing r.
Equivalence closure of binary relations is monotone.
There is a Galois insertion of equivalence relations on α into binary relations on α, with equivalence closure the lower adjoint.
Equations
Instances For
A function from α to β is injective iff its kernel is the bottom element of the complete lattice of equivalence relations on α.
The uniqueness part of the universal property for quotients of an arbitrary type.
Given a map f from α to β, the natural map from the quotient of α by the kernel of f is injective.
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.
If f
has a computable right-inverse, then the quotient by its kernel is equivalent to its
domain.
Equations
Instances For
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.
Equations
Instances For
Given a function f : α → β
and equivalence relation r
on α
, the equivalence
closure of the relation on f
's image defined by 'x ≈ y
iff the elements of f⁻¹(x)
are
related to the elements of f⁻¹(y)
by r
.'
Equations
Instances For
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.
Equations
Instances For
A special case of the equivalence closure of an equivalence relation r equalling r.
Given a function f : α → β
, an equivalence relation r
on β
induces an equivalence
relation on α
defined by 'x ≈ y
iff f(x)
is related to f(y)
by r
'.
See note [reducible non-instances].
Equations
Instances For
Given a map f : N → M
and an equivalence relation r
on β
, the equivalence relation
induced on α
by f
equals the kernel of r
's quotient map composed with f
.
The third isomorphism theorem for sets.
Equations
Instances For
Given an equivalence relation r
on α
, the order-preserving bijection between the set of
equivalence relations containing r
and the equivalence relations on the quotient of α
by r
.
Equations
Instances For
Given two equivalence relations with r ≤ s
, a bijection between the sum of the quotients by
r
on each equivalence class by s
and the quotient by r
.